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	syl5eq	⊢ ( 𝐴 ∈ ℂ → ( ( 𝑛 ∈ ℕ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	syl5eq	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 1 ) / ( ! ‘ 1 ) ) = 𝐴 )
23	15 22	syl5eq	⊢ ( 𝐴 ∈ ℂ → ( ( 𝑛 ∈ ℕ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 ‘ 𝐴 ) )