This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efgt1p

Description: The exponential of a positive real number is greater than 1 plus that number. (Contributed by Mario Carneiro, 14-Mar-2014) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Assertion efgt1p ( 𝐴 ∈ ℝ+ → ( 1 + 𝐴 ) < ( exp ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 rpcn ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
2 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
3 0nn0 ⊢ 0 ∈ ℕ0
4 3 a1i ⊢ ( 𝐴 ∈ ℂ → 0 ∈ ℕ0 )
5 1e0p1 ⊢ 1 = ( 0 + 1 )
6 0z ⊢ 0 ∈ ℤ
7 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
8 7 eftval ⊢ ( 0 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 0 ) = ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) ) )
9 3 8 ax-mp ⊢ ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 0 ) = ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) )
10 eft0val ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) ) = 1 )
11 9 10 eqtrid ⊢ ( 𝐴 ∈ ℂ → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 0 ) = 1 )
12 6 11 seq1i ⊢ ( 𝐴 ∈ ℂ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 0 ) = 1 )
13 1nn0 ⊢ 1 ∈ ℕ0
14 7 eftval ⊢ ( 1 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 1 ) = ( ( 𝐴 ↑ 1 ) / ( ! ‘ 1 ) ) )
15 13 14 ax-mp ⊢ ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 1 ) = ( ( 𝐴 ↑ 1 ) / ( ! ‘ 1 ) )
16 fac1 ⊢ ( ! ‘ 1 ) = 1
17 16 oveq2i ⊢ ( ( 𝐴 ↑ 1 ) / ( ! ‘ 1 ) ) = ( ( 𝐴 ↑ 1 ) / 1 )
18 exp1 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = 𝐴 )
19 18 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 1 ) / 1 ) = ( 𝐴 / 1 ) )
20 div1 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 / 1 ) = 𝐴 )
21 19 20 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 1 ) / 1 ) = 𝐴 )
22 17 21 eqtrid ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 1 ) / ( ! ‘ 1 ) ) = 𝐴 )
23 15 22 eqtrid ⊢ ( 𝐴 ∈ ℂ → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 1 ) = 𝐴 )
24 2 4 5 12 23 seqp1d ⊢ ( 𝐴 ∈ ℂ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 1 ) = ( 1 + 𝐴 ) )
25 1 24 syl ⊢ ( 𝐴 ∈ ℝ+ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 1 ) = ( 1 + 𝐴 ) )
26 id ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ+ )
27 13 a1i ⊢ ( 𝐴 ∈ ℝ+ → 1 ∈ ℕ0 )
28 7 26 27 effsumlt ⊢ ( 𝐴 ∈ ℝ+ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 1 ) < ( exp ‘ 𝐴 ) )
29 25 28 eqbrtrrd ⊢ ( 𝐴 ∈ ℝ+ → ( 1 + 𝐴 ) < ( exp ‘ 𝐴 ) )