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