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	2	a1i	⊢ ( 𝐴 ∈ ℝ+ → 1 ∈ ℕ0 )
4		df-2	⊢ 2 = ( 1 + 1 )
5		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
6		0nn0	⊢ 0 ∈ ℕ0
7	6	a1i	⊢ ( 𝐴 ∈ ℂ → 0 ∈ ℕ0 )
8		1e0p1	⊢ 1 = ( 0 + 1 )
9		0z	⊢ 0 ∈ ℤ
10		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
11	10	eftval	⊢ ( 0 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 0 ) = ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) ) )
12	6 11	ax-mp	⊢ ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 0 ) = ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) )
13		eft0val	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) ) = 1 )
14	12 13	eqtrid	⊢ ( 𝐴 ∈ ℂ → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 0 ) = 1 )
15	9 14	seq1i	⊢ ( 𝐴 ∈ ℂ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 0 ) = 1 )
16	10	eftval	⊢ ( 1 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 1 ) = ( ( 𝐴 ↑ 1 ) / ( ! ‘ 1 ) ) )
17	2 16	ax-mp	⊢ ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 1 ) = ( ( 𝐴 ↑ 1 ) / ( ! ‘ 1 ) )
18		fac1	⊢ ( ! ‘ 1 ) = 1
19	18	oveq2i	⊢ ( ( 𝐴 ↑ 1 ) / ( ! ‘ 1 ) ) = ( ( 𝐴 ↑ 1 ) / 1 )
20		exp1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = 𝐴 )
21	20	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 1 ) / 1 ) = ( 𝐴 / 1 ) )
22		div1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 / 1 ) = 𝐴 )
23	21 22	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 1 ) / 1 ) = 𝐴 )
24	19 23	eqtrid	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 1 ) / ( ! ‘ 1 ) ) = 𝐴 )
25	17 24	eqtrid	⊢ ( 𝐴 ∈ ℂ → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 1 ) = 𝐴 )
26	1 7 8 15 25	seqp1d	⊢ ( 𝐴 ∈ ℂ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 1 ) = ( 1 + 𝐴 ) )
27	5 26	syl	⊢ ( 𝐴 ∈ ℝ+ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 1 ) = ( 1 + 𝐴 ) )
28		2nn0	⊢ 2 ∈ ℕ0
29	10	eftval	⊢ ( 2 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 2 ) = ( ( 𝐴 ↑ 2 ) / ( ! ‘ 2 ) ) )
30	28 29	ax-mp	⊢ ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 2 ) = ( ( 𝐴 ↑ 2 ) / ( ! ‘ 2 ) )
31		fac2	⊢ ( ! ‘ 2 ) = 2
32	31	oveq2i	⊢ ( ( 𝐴 ↑ 2 ) / ( ! ‘ 2 ) ) = ( ( 𝐴 ↑ 2 ) / 2 )
33	30 32	eqtri	⊢ ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 2 ) = ( ( 𝐴 ↑ 2 ) / 2 )
34	33	a1i	⊢ ( 𝐴 ∈ ℝ+ → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 2 ) = ( ( 𝐴 ↑ 2 ) / 2 ) )
35	1 3 4 27 34	seqp1d	⊢ ( 𝐴 ∈ ℝ+ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 2 ) = ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) ) )
36		id	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ+ )
37	28	a1i	⊢ ( 𝐴 ∈ ℝ+ → 2 ∈ ℕ0 )
38	10 36 37	effsumlt	⊢ ( 𝐴 ∈ ℝ+ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 2 ) < ( exp ‘ 𝐴 ) )
39	35 38	eqbrtrrd	⊢ ( 𝐴 ∈ ℝ+ → ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) ) < ( exp ‘ 𝐴 ) )