Proof of Theorem efltlemlt
Step | Hyp | Ref
| Expression |
1 | | efltlemlt.lt |
. . . . 5
⊢ (𝜑 → (exp‘𝐴) < (exp‘𝐵)) |
2 | 1 | ad2antrr 480 |
. . . 4
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐵 < 𝐴) → (exp‘𝐴) < (exp‘𝐵)) |
3 | | efltlemlt.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | 3 | ad2antrr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐵 < 𝐴) → 𝐵 ∈ ℝ) |
5 | 4 | reefcld 11543 |
. . . . 5
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐵 < 𝐴) → (exp‘𝐵) ∈ ℝ) |
6 | | efltlemlt.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
7 | 6 | ad2antrr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐵 < 𝐴) → 𝐴 ∈ ℝ) |
8 | 7 | reefcld 11543 |
. . . . 5
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐵 < 𝐴) → (exp‘𝐴) ∈ ℝ) |
9 | 6 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) → 𝐴 ∈ ℝ) |
10 | | efltim 11572 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 < 𝐴 → (exp‘𝐵) < (exp‘𝐴))) |
11 | 3, 9, 10 | syl2an2r 585 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) → (𝐵 < 𝐴 → (exp‘𝐵) < (exp‘𝐴))) |
12 | 11 | imp 123 |
. . . . 5
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐵 < 𝐴) → (exp‘𝐵) < (exp‘𝐴)) |
13 | 5, 8, 12 | ltnsymd 7974 |
. . . 4
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐵 < 𝐴) → ¬ (exp‘𝐴) < (exp‘𝐵)) |
14 | 2, 13 | pm2.21dd 610 |
. . 3
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐵 < 𝐴) → 𝐴 < 𝐵) |
15 | 6 | reefcld 11543 |
. . . . . . 7
⊢ (𝜑 → (exp‘𝐴) ∈
ℝ) |
16 | 3 | reefcld 11543 |
. . . . . . 7
⊢ (𝜑 → (exp‘𝐵) ∈
ℝ) |
17 | 15, 16, 1 | ltled 7973 |
. . . . . . 7
⊢ (𝜑 → (exp‘𝐴) ≤ (exp‘𝐵)) |
18 | 15, 16, 17 | abssuble0d 11054 |
. . . . . 6
⊢ (𝜑 →
(abs‘((exp‘𝐴)
− (exp‘𝐵))) =
((exp‘𝐵) −
(exp‘𝐴))) |
19 | 18 | ad2antrr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐴 < (𝐵 + 𝐷)) → (abs‘((exp‘𝐴) − (exp‘𝐵))) = ((exp‘𝐵) − (exp‘𝐴))) |
20 | | efltlemlt.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈
ℝ+) |
21 | 20 | rpred 9581 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℝ) |
22 | 6, 3, 21 | absdifltd 11055 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) < 𝐷 ↔ ((𝐵 − 𝐷) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐷)))) |
23 | 22 | biimprd 157 |
. . . . . . 7
⊢ (𝜑 → (((𝐵 − 𝐷) < 𝐴 ∧ 𝐴 < (𝐵 + 𝐷)) → (abs‘(𝐴 − 𝐵)) < 𝐷)) |
24 | 23 | impl 378 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐴 < (𝐵 + 𝐷)) → (abs‘(𝐴 − 𝐵)) < 𝐷) |
25 | | efltlemlt.ed |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐴 − 𝐵)) < 𝐷 → (abs‘((exp‘𝐴) − (exp‘𝐵))) < ((exp‘𝐵) − (exp‘𝐴)))) |
26 | 25 | ad2antrr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐴 < (𝐵 + 𝐷)) → ((abs‘(𝐴 − 𝐵)) < 𝐷 → (abs‘((exp‘𝐴) − (exp‘𝐵))) < ((exp‘𝐵) − (exp‘𝐴)))) |
27 | 24, 26 | mpd 13 |
. . . . 5
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐴 < (𝐵 + 𝐷)) → (abs‘((exp‘𝐴) − (exp‘𝐵))) < ((exp‘𝐵) − (exp‘𝐴))) |
28 | 19, 27 | eqbrtrrd 3984 |
. . . 4
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐴 < (𝐵 + 𝐷)) → ((exp‘𝐵) − (exp‘𝐴)) < ((exp‘𝐵) − (exp‘𝐴))) |
29 | 16, 15 | resubcld 8235 |
. . . . . 6
⊢ (𝜑 → ((exp‘𝐵) − (exp‘𝐴)) ∈
ℝ) |
30 | 29 | ad2antrr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐴 < (𝐵 + 𝐷)) → ((exp‘𝐵) − (exp‘𝐴)) ∈ ℝ) |
31 | 30 | ltnrd 7967 |
. . . 4
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐴 < (𝐵 + 𝐷)) → ¬ ((exp‘𝐵) − (exp‘𝐴)) < ((exp‘𝐵) − (exp‘𝐴))) |
32 | 28, 31 | pm2.21dd 610 |
. . 3
⊢ (((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) ∧ 𝐴 < (𝐵 + 𝐷)) → 𝐴 < 𝐵) |
33 | 3, 20 | ltaddrpd 9615 |
. . . . 5
⊢ (𝜑 → 𝐵 < (𝐵 + 𝐷)) |
34 | 3, 21 | readdcld 7886 |
. . . . . 6
⊢ (𝜑 → (𝐵 + 𝐷) ∈ ℝ) |
35 | | axltwlin 7924 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ (𝐵 + 𝐷) ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 < (𝐵 + 𝐷) → (𝐵 < 𝐴 ∨ 𝐴 < (𝐵 + 𝐷)))) |
36 | 3, 34, 6, 35 | syl3anc 1217 |
. . . . 5
⊢ (𝜑 → (𝐵 < (𝐵 + 𝐷) → (𝐵 < 𝐴 ∨ 𝐴 < (𝐵 + 𝐷)))) |
37 | 33, 36 | mpd 13 |
. . . 4
⊢ (𝜑 → (𝐵 < 𝐴 ∨ 𝐴 < (𝐵 + 𝐷))) |
38 | 37 | adantr 274 |
. . 3
⊢ ((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) → (𝐵 < 𝐴 ∨ 𝐴 < (𝐵 + 𝐷))) |
39 | 14, 32, 38 | mpjaodan 788 |
. 2
⊢ ((𝜑 ∧ (𝐵 − 𝐷) < 𝐴) → 𝐴 < 𝐵) |
40 | | simpr 109 |
. 2
⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) |
41 | 3, 20 | ltsubrpd 9614 |
. . 3
⊢ (𝜑 → (𝐵 − 𝐷) < 𝐵) |
42 | 3, 21 | resubcld 8235 |
. . . 4
⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℝ) |
43 | | axltwlin 7924 |
. . . 4
⊢ (((𝐵 − 𝐷) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝐵 − 𝐷) < 𝐵 → ((𝐵 − 𝐷) < 𝐴 ∨ 𝐴 < 𝐵))) |
44 | 42, 3, 6, 43 | syl3anc 1217 |
. . 3
⊢ (𝜑 → ((𝐵 − 𝐷) < 𝐵 → ((𝐵 − 𝐷) < 𝐴 ∨ 𝐴 < 𝐵))) |
45 | 41, 44 | mpd 13 |
. 2
⊢ (𝜑 → ((𝐵 − 𝐷) < 𝐴 ∨ 𝐴 < 𝐵)) |
46 | 39, 40, 45 | mpjaodan 788 |
1
⊢ (𝜑 → 𝐴 < 𝐵) |