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