Proof of Theorem absle
Step | Hyp | Ref
| Expression |
1 | | simpll 519 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(abs‘𝐴) ≤ 𝐵) → 𝐴 ∈ ℝ) |
2 | 1 | renegcld 8250 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(abs‘𝐴) ≤ 𝐵) → -𝐴 ∈ ℝ) |
3 | 1 | recnd 7901 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(abs‘𝐴) ≤ 𝐵) → 𝐴 ∈ ℂ) |
4 | | abscl 10946 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
5 | 3, 4 | syl 14 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(abs‘𝐴) ≤ 𝐵) → (abs‘𝐴) ∈
ℝ) |
6 | | simplr 520 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(abs‘𝐴) ≤ 𝐵) → 𝐵 ∈ ℝ) |
7 | | leabs 10969 |
. . . . . . 7
⊢ (-𝐴 ∈ ℝ → -𝐴 ≤ (abs‘-𝐴)) |
8 | 2, 7 | syl 14 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(abs‘𝐴) ≤ 𝐵) → -𝐴 ≤ (abs‘-𝐴)) |
9 | | absneg 10945 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(abs‘-𝐴) =
(abs‘𝐴)) |
10 | 3, 9 | syl 14 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(abs‘𝐴) ≤ 𝐵) → (abs‘-𝐴) = (abs‘𝐴)) |
11 | 8, 10 | breqtrd 3990 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(abs‘𝐴) ≤ 𝐵) → -𝐴 ≤ (abs‘𝐴)) |
12 | | simpr 109 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(abs‘𝐴) ≤ 𝐵) → (abs‘𝐴) ≤ 𝐵) |
13 | 2, 5, 6, 11, 12 | letrd 7994 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(abs‘𝐴) ≤ 𝐵) → -𝐴 ≤ 𝐵) |
14 | | leabs 10969 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (abs‘𝐴)) |
15 | 14 | ad2antrr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(abs‘𝐴) ≤ 𝐵) → 𝐴 ≤ (abs‘𝐴)) |
16 | 1, 5, 6, 15, 12 | letrd 7994 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(abs‘𝐴) ≤ 𝐵) → 𝐴 ≤ 𝐵) |
17 | 13, 16 | jca 304 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧
(abs‘𝐴) ≤ 𝐵) → (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) |
18 | | simpll 519 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℝ) |
19 | | simplr 520 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → 𝐵 ∈ ℝ) |
20 | 18 | recnd 7901 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ∈ ℂ) |
21 | 20, 4 | syl 14 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → (abs‘𝐴) ∈ ℝ) |
22 | | axltwlin 7940 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧
(abs‘𝐴) ∈
ℝ ∧ 𝐴 ∈
ℝ) → (𝐵 <
(abs‘𝐴) → (𝐵 < 𝐴 ∨ 𝐴 < (abs‘𝐴)))) |
23 | 19, 21, 18, 22 | syl3anc 1220 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → (𝐵 < (abs‘𝐴) → (𝐵 < 𝐴 ∨ 𝐴 < (abs‘𝐴)))) |
24 | | simprr 522 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → 𝐴 ≤ 𝐵) |
25 | 18, 19 | lenltd 7988 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴)) |
26 | 24, 25 | mpbid 146 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → ¬ 𝐵 < 𝐴) |
27 | | pm2.53 712 |
. . . . . . . . 9
⊢ ((𝐵 < 𝐴 ∨ 𝐴 < (abs‘𝐴)) → (¬ 𝐵 < 𝐴 → 𝐴 < (abs‘𝐴))) |
28 | 23, 26, 27 | syl6ci 1425 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → (𝐵 < (abs‘𝐴) → 𝐴 < (abs‘𝐴))) |
29 | | simpl 108 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → 𝐴 ∈ ℝ) |
30 | 29 | recnd 7901 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → 𝐴 ∈ ℂ) |
31 | 30, 9 | syl 14 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → (abs‘-𝐴) = (abs‘𝐴)) |
32 | 29 | renegcld 8250 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → -𝐴 ∈ ℝ) |
33 | | 0red 7874 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → 0 ∈
ℝ) |
34 | | ltabs 10982 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → 𝐴 < 0) |
35 | 29, 33, 34 | ltled 7989 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → 𝐴 ≤ 0) |
36 | 29 | le0neg1d 8387 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) |
37 | 35, 36 | mpbid 146 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → 0 ≤ -𝐴) |
38 | | absid 10966 |
. . . . . . . . . 10
⊢ ((-𝐴 ∈ ℝ ∧ 0 ≤
-𝐴) →
(abs‘-𝐴) = -𝐴) |
39 | 32, 37, 38 | syl2anc 409 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → (abs‘-𝐴) = -𝐴) |
40 | 31, 39 | eqtr3d 2192 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < (abs‘𝐴)) → (abs‘𝐴) = -𝐴) |
41 | 18, 28, 40 | syl6an 1414 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → (𝐵 < (abs‘𝐴) → (abs‘𝐴) = -𝐴)) |
42 | | simprl 521 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → -𝐴 ≤ 𝐵) |
43 | | breq1 3968 |
. . . . . . . 8
⊢
((abs‘𝐴) =
-𝐴 → ((abs‘𝐴) ≤ 𝐵 ↔ -𝐴 ≤ 𝐵)) |
44 | 42, 43 | syl5ibrcom 156 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → ((abs‘𝐴) = -𝐴 → (abs‘𝐴) ≤ 𝐵)) |
45 | 41, 44 | syld 45 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → (𝐵 < (abs‘𝐴) → (abs‘𝐴) ≤ 𝐵)) |
46 | 21, 19 | lenltd 7988 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → ((abs‘𝐴) ≤ 𝐵 ↔ ¬ 𝐵 < (abs‘𝐴))) |
47 | 45, 46 | sylibd 148 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → (𝐵 < (abs‘𝐴) → ¬ 𝐵 < (abs‘𝐴))) |
48 | 47 | pm2.01d 608 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → ¬ 𝐵 < (abs‘𝐴)) |
49 | 48, 46 | mpbird 166 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵)) → (abs‘𝐴) ≤ 𝐵) |
50 | 17, 49 | impbida 586 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((abs‘𝐴) ≤ 𝐵 ↔ (-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵))) |
51 | | lenegcon1 8336 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 ≤ 𝐵 ↔ -𝐵 ≤ 𝐴)) |
52 | 51 | anbi1d 461 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((-𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵) ↔ (-𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))) |
53 | 50, 52 | bitrd 187 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((abs‘𝐴) ≤ 𝐵 ↔ (-𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵))) |