Proof of Theorem sqlecan
Step | Hyp | Ref
| Expression |
1 | | 0re 10835 |
. . . 4
⊢ 0 ∈
ℝ |
2 | | leloe 10919 |
. . . 4
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 ≤ 𝐴 ↔ (0 < 𝐴 ∨ 0 = 𝐴))) |
3 | 1, 2 | mpan 690 |
. . 3
⊢ (𝐴 ∈ ℝ → (0 ≤
𝐴 ↔ (0 < 𝐴 ∨ 0 = 𝐴))) |
4 | | recn 10819 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
5 | | sqval 13687 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴)) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → (𝐴↑2) = (𝐴 · 𝐴)) |
7 | 6 | breq1d 5063 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐴))) |
8 | 7 | 3ad2ant1 1135 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐴))) |
9 | | lemul1 11684 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐴))) |
10 | 8, 9 | bitr4d 285 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵)) |
11 | 10 | 3exp 1121 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵)))) |
12 | 11 | exp4a 435 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝐴 ∈ ℝ → (0 <
𝐴 → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵))))) |
13 | 12 | pm2.43a 54 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (0 <
𝐴 → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵)))) |
14 | 13 | adantrd 495 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → (0 < 𝐴 → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵)))) |
15 | 14 | com23 86 |
. . . 4
⊢ (𝐴 ∈ ℝ → (0 <
𝐴 → ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵)))) |
16 | | sq0 13761 |
. . . . . . . . . . . 12
⊢
(0↑2) = 0 |
17 | | 0le0 11931 |
. . . . . . . . . . . 12
⊢ 0 ≤
0 |
18 | 16, 17 | eqbrtri 5074 |
. . . . . . . . . . 11
⊢
(0↑2) ≤ 0 |
19 | | recn 10819 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
20 | 19 | mul01d 11031 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ → (𝐵 · 0) =
0) |
21 | 18, 20 | breqtrrid 5091 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ →
(0↑2) ≤ (𝐵 ·
0)) |
22 | 21 | adantl 485 |
. . . . . . . . 9
⊢ ((0 =
𝐴 ∧ 𝐵 ∈ ℝ) → (0↑2) ≤
(𝐵 ·
0)) |
23 | | oveq1 7220 |
. . . . . . . . . . 11
⊢ (0 =
𝐴 → (0↑2) =
(𝐴↑2)) |
24 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (0 =
𝐴 → (𝐵 · 0) = (𝐵 · 𝐴)) |
25 | 23, 24 | breq12d 5066 |
. . . . . . . . . 10
⊢ (0 =
𝐴 → ((0↑2) ≤
(𝐵 · 0) ↔
(𝐴↑2) ≤ (𝐵 · 𝐴))) |
26 | 25 | adantr 484 |
. . . . . . . . 9
⊢ ((0 =
𝐴 ∧ 𝐵 ∈ ℝ) → ((0↑2) ≤
(𝐵 · 0) ↔
(𝐴↑2) ≤ (𝐵 · 𝐴))) |
27 | 22, 26 | mpbid 235 |
. . . . . . . 8
⊢ ((0 =
𝐴 ∧ 𝐵 ∈ ℝ) → (𝐴↑2) ≤ (𝐵 · 𝐴)) |
28 | 27 | adantrr 717 |
. . . . . . 7
⊢ ((0 =
𝐴 ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴↑2) ≤ (𝐵 · 𝐴)) |
29 | | breq1 5056 |
. . . . . . . . 9
⊢ (0 =
𝐴 → (0 ≤ 𝐵 ↔ 𝐴 ≤ 𝐵)) |
30 | 29 | biimpa 480 |
. . . . . . . 8
⊢ ((0 =
𝐴 ∧ 0 ≤ 𝐵) → 𝐴 ≤ 𝐵) |
31 | 30 | adantrl 716 |
. . . . . . 7
⊢ ((0 =
𝐴 ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 𝐴 ≤ 𝐵) |
32 | 28, 31 | 2thd 268 |
. . . . . 6
⊢ ((0 =
𝐴 ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵)) |
33 | 32 | ex 416 |
. . . . 5
⊢ (0 =
𝐴 → ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵))) |
34 | 33 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ ℝ → (0 =
𝐴 → ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵)))) |
35 | 15, 34 | jaod 859 |
. . 3
⊢ (𝐴 ∈ ℝ → ((0 <
𝐴 ∨ 0 = 𝐴) → ((𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵)))) |
36 | 3, 35 | sylbid 243 |
. 2
⊢ (𝐴 ∈ ℝ → (0 ≤
𝐴 → ((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵)))) |
37 | 36 | imp31 421 |
1
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵)) |