Theorem eflt

Description: The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007) (Revised by Mario Carneiro, 17-Jul-2014)

	Ref	Expression
Assertion	eflt	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( exp ‘ 𝐴 ) < ( exp ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tru	⊢ ⊤
2		fveq2	⊢ ( 𝑥 = 𝑦 → ( exp ‘ 𝑥 ) = ( exp ‘ 𝑦 ) )
3		fveq2	⊢ ( 𝑥 = 𝐴 → ( exp ‘ 𝑥 ) = ( exp ‘ 𝐴 ) )
4		fveq2	⊢ ( 𝑥 = 𝐵 → ( exp ‘ 𝑥 ) = ( exp ‘ 𝐵 ) )
5		ssid	⊢ ℝ ⊆ ℝ
6		reefcl	⊢ ( 𝑥 ∈ ℝ → ( exp ‘ 𝑥 ) ∈ ℝ )
7	6	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ( exp ‘ 𝑥 ) ∈ ℝ )
8		simp2	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℝ )
9		simp1	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ℝ )
10	8 9	resubcld	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → ( 𝑦 − 𝑥 ) ∈ ℝ )
11		posdif	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 < 𝑦 ↔ 0 < ( 𝑦 − 𝑥 ) ) )
12	11	biimp3a	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → 0 < ( 𝑦 − 𝑥 ) )
13	10 12	elrpd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → ( 𝑦 − 𝑥 ) ∈ ℝ+ )
14		efgt1	⊢ ( ( 𝑦 − 𝑥 ) ∈ ℝ+ → 1 < ( exp ‘ ( 𝑦 − 𝑥 ) ) )
15	13 14	syl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → 1 < ( exp ‘ ( 𝑦 − 𝑥 ) ) )
16	9	reefcld	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → ( exp ‘ 𝑥 ) ∈ ℝ )
17	10	reefcld	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → ( exp ‘ ( 𝑦 − 𝑥 ) ) ∈ ℝ )
18		efgt0	⊢ ( 𝑥 ∈ ℝ → 0 < ( exp ‘ 𝑥 ) )
19	9 18	syl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → 0 < ( exp ‘ 𝑥 ) )
20		ltmulgt11	⊢ ( ( ( exp ‘ 𝑥 ) ∈ ℝ ∧ ( exp ‘ ( 𝑦 − 𝑥 ) ) ∈ ℝ ∧ 0 < ( exp ‘ 𝑥 ) ) → ( 1 < ( exp ‘ ( 𝑦 − 𝑥 ) ) ↔ ( exp ‘ 𝑥 ) < ( ( exp ‘ 𝑥 ) · ( exp ‘ ( 𝑦 − 𝑥 ) ) ) ) )
21	16 17 19 20	syl3anc	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → ( 1 < ( exp ‘ ( 𝑦 − 𝑥 ) ) ↔ ( exp ‘ 𝑥 ) < ( ( exp ‘ 𝑥 ) · ( exp ‘ ( 𝑦 − 𝑥 ) ) ) ) )
22	15 21	mpbid	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → ( exp ‘ 𝑥 ) < ( ( exp ‘ 𝑥 ) · ( exp ‘ ( 𝑦 − 𝑥 ) ) ) )
23	9	recnd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ℂ )
24	10	recnd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → ( 𝑦 − 𝑥 ) ∈ ℂ )
25		efadd	⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 − 𝑥 ) ∈ ℂ ) → ( exp ‘ ( 𝑥 + ( 𝑦 − 𝑥 ) ) ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ ( 𝑦 − 𝑥 ) ) ) )
26	23 24 25	syl2anc	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → ( exp ‘ ( 𝑥 + ( 𝑦 − 𝑥 ) ) ) = ( ( exp ‘ 𝑥 ) · ( exp ‘ ( 𝑦 − 𝑥 ) ) ) )
27	8	recnd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℂ )
28	23 27	pncan3d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → ( 𝑥 + ( 𝑦 − 𝑥 ) ) = 𝑦 )
29	28	fveq2d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → ( exp ‘ ( 𝑥 + ( 𝑦 − 𝑥 ) ) ) = ( exp ‘ 𝑦 ) )
30	26 29	eqtr3d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → ( ( exp ‘ 𝑥 ) · ( exp ‘ ( 𝑦 − 𝑥 ) ) ) = ( exp ‘ 𝑦 ) )
31	22 30	breqtrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) → ( exp ‘ 𝑥 ) < ( exp ‘ 𝑦 ) )
32	31	3expia	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 < 𝑦 → ( exp ‘ 𝑥 ) < ( exp ‘ 𝑦 ) ) )
33	32	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 < 𝑦 → ( exp ‘ 𝑥 ) < ( exp ‘ 𝑦 ) ) )
34	2 3 4 5 7 33	ltord1	⊢ ( ( ⊤ ∧ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → ( 𝐴 < 𝐵 ↔ ( exp ‘ 𝐴 ) < ( exp ‘ 𝐵 ) ) )
35	1 34	mpan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( exp ‘ 𝐴 ) < ( exp ‘ 𝐵 ) ) )