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