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

Metamath Proof Explorer

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 ‘ 𝐵 ) ) )