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

Metamath Proof Explorer

Theorem eflegeo

Description: The exponential function on the reals between 0 and 1 lies below the comparable geometric series sum. (Contributed by Paul Chapman, 11-Sep-2007)

Ref Expression
Hypotheses eflegeo.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
eflegeo.2 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
eflegeo.3 ⊢ ( 𝜑 → 𝐴 < 1 )
Assertion eflegeo ( 𝜑 → ( exp ‘ 𝐴 ) ≤ ( 1 / ( 1 − 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 eflegeo.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 eflegeo.2 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
3 eflegeo.3 ⊢ ( 𝜑 → 𝐴 < 1 )
4 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
5 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
6 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
7 6 eftval ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
9 reeftcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
10 1 9 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
11 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑘 ) )
12 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) )
13 ovex ⊢ ( 𝐴 ↑ 𝑘 ) ∈ V
14 11 12 13 fvmpt ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
16 reexpcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ )
17 1 16 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ )
18 faccl ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℕ )
20 19 nnred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℝ )
21 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
23 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ 𝐴 )
24 21 22 23 expge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ ( 𝐴 ↑ 𝑘 ) )
25 19 nnge1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 1 ≤ ( ! ‘ 𝑘 ) )
26 17 20 24 25 lemulge12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ≤ ( ( ! ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
27 19 nngt0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 0 < ( ! ‘ 𝑘 ) )
28 ledivmul ⊢ ( ( ( 𝐴 ↑ 𝑘 ) ∈ ℝ ∧ ( 𝐴 ↑ 𝑘 ) ∈ ℝ ∧ ( ( ! ‘ 𝑘 ) ∈ ℝ ∧ 0 < ( ! ‘ 𝑘 ) ) ) → ( ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ≤ ( 𝐴 ↑ 𝑘 ) ↔ ( 𝐴 ↑ 𝑘 ) ≤ ( ( ! ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
29 17 17 20 27 28 syl112anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ≤ ( 𝐴 ↑ 𝑘 ) ↔ ( 𝐴 ↑ 𝑘 ) ≤ ( ( ! ‘ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
30 26 29 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ≤ ( 𝐴 ↑ 𝑘 ) )
31 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
32 6 efcllem ⊢ ( 𝐴 ∈ ℂ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ∈ dom ⇝ )
33 31 32 syl ⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ∈ dom ⇝ )
34 1 2 absidd ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) = 𝐴 )
35 34 3 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) < 1 )
36 31 35 15 geolim ⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ⇝ ( 1 / ( 1 − 𝐴 ) ) )
37 seqex ⊢ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ∈ V
38 ovex ⊢ ( 1 / ( 1 − 𝐴 ) ) ∈ V
39 37 38 breldm ⊢ ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ⇝ ( 1 / ( 1 − 𝐴 ) ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ∈ dom ⇝ )
40 36 39 syl ⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ∈ dom ⇝ )
41 4 5 8 10 15 17 30 33 40 isumle ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ≤ Σ 𝑘 ∈ ℕ0 ( 𝐴 ↑ 𝑘 ) )
42 efval ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
43 31 42 syl ⊢ ( 𝜑 → ( exp ‘ 𝐴 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
44 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
45 31 44 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
46 4 5 15 45 36 isumclim ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 ( 𝐴 ↑ 𝑘 ) = ( 1 / ( 1 − 𝐴 ) ) )
47 46 eqcomd ⊢ ( 𝜑 → ( 1 / ( 1 − 𝐴 ) ) = Σ 𝑘 ∈ ℕ0 ( 𝐴 ↑ 𝑘 ) )
48 41 43 47 3brtr4d ⊢ ( 𝜑 → ( exp ‘ 𝐴 ) ≤ ( 1 / ( 1 − 𝐴 ) ) )