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

Metamath Proof Explorer

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 ‘ 𝐴 ) )