Theorem efgt1p2

Description: The exponential of a positive real number is greater than the sum of the first three terms of the series expansion. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Assertion	efgt1p2	⊢ ( 𝐴 ∈ ℝ+ → ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) ) < ( exp ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
2		1nn0	⊢ 1 ∈ ℕ0
3		df-2	⊢ 2 = ( 1 + 1 )
4		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
5		0nn0	⊢ 0 ∈ ℕ0
6		1e0p1	⊢ 1 = ( 0 + 1 )
7		0z	⊢ 0 ∈ ℤ
8		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
9	8	eftval	⊢ ( 0 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 0 ) = ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) ) )
10	5 9	ax-mp	⊢ ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 0 ) = ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) )
11		eft0val	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) ) = 1 )
12	10 11	syl5eq	⊢ ( 𝐴 ∈ ℂ → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 0 ) = 1 )
13	7 12	seq1i	⊢ ( 𝐴 ∈ ℂ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 0 ) = 1 )
14	8	eftval	⊢ ( 1 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 1 ) = ( ( 𝐴 ↑ 1 ) / ( ! ‘ 1 ) ) )
15	2 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	1 5 6 13 23	seqp1i	⊢ ( 𝐴 ∈ ℂ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 1 ) = ( 1 + 𝐴 ) )
25	4 24	syl	⊢ ( 𝐴 ∈ ℝ+ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 1 ) = ( 1 + 𝐴 ) )
26		2nn0	⊢ 2 ∈ ℕ0
27	8	eftval	⊢ ( 2 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 2 ) = ( ( 𝐴 ↑ 2 ) / ( ! ‘ 2 ) ) )
28	26 27	ax-mp	⊢ ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 2 ) = ( ( 𝐴 ↑ 2 ) / ( ! ‘ 2 ) )
29		fac2	⊢ ( ! ‘ 2 ) = 2
30	29	oveq2i	⊢ ( ( 𝐴 ↑ 2 ) / ( ! ‘ 2 ) ) = ( ( 𝐴 ↑ 2 ) / 2 )
31	28 30	eqtri	⊢ ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 2 ) = ( ( 𝐴 ↑ 2 ) / 2 )
32	31	a1i	⊢ ( 𝐴 ∈ ℝ+ → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 2 ) = ( ( 𝐴 ↑ 2 ) / 2 ) )
33	1 2 3 25 32	seqp1i	⊢ ( 𝐴 ∈ ℝ+ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 2 ) = ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) ) )
34		id	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ+ )
35	26	a1i	⊢ ( 𝐴 ∈ ℝ+ → 2 ∈ ℕ0 )
36	8 34 35	effsumlt	⊢ ( 𝐴 ∈ ℝ+ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 2 ) < ( exp ‘ 𝐴 ) )
37	33 36	eqbrtrrd	⊢ ( 𝐴 ∈ ℝ+ → ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) ) < ( exp ‘ 𝐴 ) )