| Step | Hyp | Ref
| Expression |
| 1 | | 01sqrexlem1.1 |
. . 3
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} |
| 2 | | 01sqrexlem1.2 |
. . 3
⊢ 𝐵 = sup(𝑆, ℝ, < ) |
| 3 | | 01sqrexlem5.3 |
. . 3
⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)} |
| 4 | 1, 2, 3 | 01sqrexlem6 15286 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵↑2) ≤ 𝐴) |
| 5 | 1, 2 | 01sqrexlem3 15283 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝑆 ⊆ ℝ ∧
𝑆 ≠ ∅ ∧
∃𝑦 ∈ ℝ
∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑦)) |
| 6 | 5 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑦)) |
| 7 | 1, 2 | 01sqrexlem4 15284 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵 ∈
ℝ+ ∧ 𝐵
≤ 1)) |
| 8 | 7 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵 ∈ ℝ+ ∧ 𝐵 ≤ 1)) |
| 9 | 8 | simpld 494 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 𝐵 ∈
ℝ+) |
| 10 | | rpre 13043 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
| 11 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
𝐴 ∈
ℝ) |
| 12 | | rpre 13043 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ∈
ℝ) |
| 13 | 12 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ+
∧ 𝐵 ≤ 1) →
𝐵 ∈
ℝ) |
| 14 | 7, 13 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
𝐵 ∈
ℝ) |
| 15 | 14 | resqcld 14165 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵↑2) ∈
ℝ) |
| 16 | 11, 15 | resubcld 11691 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐴 − (𝐵↑2)) ∈
ℝ) |
| 17 | 16 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ∈ ℝ) |
| 18 | 15, 11 | posdifd 11850 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
((𝐵↑2) < 𝐴 ↔ 0 < (𝐴 − (𝐵↑2)))) |
| 19 | 18 | biimpa 476 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 0 < (𝐴 − (𝐵↑2))) |
| 20 | 17, 19 | elrpd 13074 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ∈
ℝ+) |
| 21 | | 3rp 13040 |
. . . . . . 7
⊢ 3 ∈
ℝ+ |
| 22 | | rpdivcl 13060 |
. . . . . . 7
⊢ (((𝐴 − (𝐵↑2)) ∈ ℝ+ ∧ 3
∈ ℝ+) → ((𝐴 − (𝐵↑2)) / 3) ∈
ℝ+) |
| 23 | 20, 21, 22 | sylancl 586 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐴 − (𝐵↑2)) / 3) ∈
ℝ+) |
| 24 | 9, 23 | rpaddcld 13092 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈
ℝ+) |
| 25 | 14 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 𝐵 ∈ ℝ) |
| 26 | 25 | recnd 11289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 𝐵 ∈ ℂ) |
| 27 | | 3nn 12345 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
| 28 | | nndivre 12307 |
. . . . . . . . . . 11
⊢ (((𝐴 − (𝐵↑2)) ∈ ℝ ∧ 3 ∈
ℕ) → ((𝐴 −
(𝐵↑2)) / 3) ∈
ℝ) |
| 29 | 16, 27, 28 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
((𝐴 − (𝐵↑2)) / 3) ∈
ℝ) |
| 30 | 29 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐴 − (𝐵↑2)) / 3) ∈
ℝ) |
| 31 | 30 | recnd 11289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐴 − (𝐵↑2)) / 3) ∈
ℂ) |
| 32 | | binom2 14256 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ ((𝐴 − (𝐵↑2)) / 3) ∈ ℂ) →
((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2) = (((𝐵↑2) + (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3)))) + (((𝐴 − (𝐵↑2)) / 3)↑2))) |
| 33 | 26, 31, 32 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2) = (((𝐵↑2) + (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3)))) + (((𝐴 − (𝐵↑2)) / 3)↑2))) |
| 34 | 15 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵↑2) ∈ ℝ) |
| 35 | 34 | recnd 11289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵↑2) ∈ ℂ) |
| 36 | | 2re 12340 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
| 37 | 25, 30 | remulcld 11291 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵 · ((𝐴 − (𝐵↑2)) / 3)) ∈
ℝ) |
| 38 | | remulcl 11240 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ (𝐵
· ((𝐴 − (𝐵↑2)) / 3)) ∈ ℝ)
→ (2 · (𝐵
· ((𝐴 − (𝐵↑2)) / 3))) ∈
ℝ) |
| 39 | 36, 37, 38 | sylancr 587 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) ∈
ℝ) |
| 40 | 39 | recnd 11289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) ∈
ℂ) |
| 41 | 30 | resqcld 14165 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐴 − (𝐵↑2)) / 3)↑2) ∈
ℝ) |
| 42 | 41 | recnd 11289 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐴 − (𝐵↑2)) / 3)↑2) ∈
ℂ) |
| 43 | 35, 40, 42 | addassd 11283 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐵↑2) + (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3)))) + (((𝐴 − (𝐵↑2)) / 3)↑2)) = ((𝐵↑2) + ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)))) |
| 44 | 33, 43 | eqtrd 2777 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2) = ((𝐵↑2) + ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)))) |
| 45 | | 2cn 12341 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
| 46 | | mulass 11243 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℂ ∧ 𝐵
∈ ℂ ∧ ((𝐴
− (𝐵↑2)) / 3)
∈ ℂ) → ((2 · 𝐵) · ((𝐴 − (𝐵↑2)) / 3)) = (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3)))) |
| 47 | 45, 26, 31, 46 | mp3an2i 1468 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · 𝐵) · ((𝐴 − (𝐵↑2)) / 3)) = (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3)))) |
| 48 | 47 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) = ((2 · 𝐵) · ((𝐴 − (𝐵↑2)) / 3))) |
| 49 | 31 | sqvald 14183 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐴 − (𝐵↑2)) / 3)↑2) = (((𝐴 − (𝐵↑2)) / 3) · ((𝐴 − (𝐵↑2)) / 3))) |
| 50 | 48, 49 | oveq12d 7449 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)) = (((2 ·
𝐵) · ((𝐴 − (𝐵↑2)) / 3)) + (((𝐴 − (𝐵↑2)) / 3) · ((𝐴 − (𝐵↑2)) / 3)))) |
| 51 | | remulcl 11240 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 𝐵
∈ ℝ) → (2 · 𝐵) ∈ ℝ) |
| 52 | 36, 25, 51 | sylancr 587 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · 𝐵) ∈
ℝ) |
| 53 | 52 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · 𝐵) ∈
ℂ) |
| 54 | 53, 31, 31 | adddird 11286 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) · ((𝐴 − (𝐵↑2)) / 3)) = (((2 · 𝐵) · ((𝐴 − (𝐵↑2)) / 3)) + (((𝐴 − (𝐵↑2)) / 3) · ((𝐴 − (𝐵↑2)) / 3)))) |
| 55 | 50, 54 | eqtr4d 2780 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)) = (((2 ·
𝐵) + ((𝐴 − (𝐵↑2)) / 3)) · ((𝐴 − (𝐵↑2)) / 3))) |
| 56 | 7 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
𝐵 ≤ 1) |
| 57 | | 1red 11262 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) → 1
∈ ℝ) |
| 58 | | 2rp 13039 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
| 59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) → 2
∈ ℝ+) |
| 60 | 14, 57, 59 | lemul2d 13121 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵 ≤ 1 ↔ (2
· 𝐵) ≤ (2
· 1))) |
| 61 | 56, 60 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) → (2
· 𝐵) ≤ (2
· 1)) |
| 62 | 61 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · 𝐵) ≤ (2 ·
1)) |
| 63 | | 2t1e2 12429 |
. . . . . . . . . . . . 13
⊢ (2
· 1) = 2 |
| 64 | 62, 63 | breqtrdi 5184 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · 𝐵) ≤ 2) |
| 65 | 11 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 𝐴 ∈ ℝ) |
| 66 | | 1red 11262 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 1 ∈
ℝ) |
| 67 | 25 | sqge0d 14177 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 0 ≤ (𝐵↑2)) |
| 68 | 65, 34 | addge01d 11851 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (0 ≤ (𝐵↑2) ↔ 𝐴 ≤ (𝐴 + (𝐵↑2)))) |
| 69 | 67, 68 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 𝐴 ≤ (𝐴 + (𝐵↑2))) |
| 70 | 65, 34, 65 | lesubaddd 11860 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐴 − (𝐵↑2)) ≤ 𝐴 ↔ 𝐴 ≤ (𝐴 + (𝐵↑2)))) |
| 71 | 69, 70 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ≤ 𝐴) |
| 72 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 𝐴 ≤ 1) |
| 73 | 17, 65, 66, 71, 72 | letrd 11418 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ≤ 1) |
| 74 | | 1le3 12478 |
. . . . . . . . . . . . . . . 16
⊢ 1 ≤
3 |
| 75 | | 1re 11261 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
| 76 | | 3re 12346 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 ∈
ℝ |
| 77 | | letr 11355 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 − (𝐵↑2)) ∈ ℝ ∧ 1 ∈
ℝ ∧ 3 ∈ ℝ) → (((𝐴 − (𝐵↑2)) ≤ 1 ∧ 1 ≤ 3) →
(𝐴 − (𝐵↑2)) ≤
3)) |
| 78 | 75, 76, 77 | mp3an23 1455 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 − (𝐵↑2)) ∈ ℝ → (((𝐴 − (𝐵↑2)) ≤ 1 ∧ 1 ≤ 3) →
(𝐴 − (𝐵↑2)) ≤
3)) |
| 79 | 17, 78 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐴 − (𝐵↑2)) ≤ 1 ∧ 1 ≤ 3) →
(𝐴 − (𝐵↑2)) ≤
3)) |
| 80 | 74, 79 | mpan2i 697 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐴 − (𝐵↑2)) ≤ 1 → (𝐴 − (𝐵↑2)) ≤ 3)) |
| 81 | 73, 80 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ≤ 3) |
| 82 | | 3t1e3 12431 |
. . . . . . . . . . . . . 14
⊢ (3
· 1) = 3 |
| 83 | 81, 82 | breqtrrdi 5185 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ≤ (3 ·
1)) |
| 84 | | 3pos 12371 |
. . . . . . . . . . . . . . 15
⊢ 0 <
3 |
| 85 | | ledivmul 12144 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 − (𝐵↑2)) ∈ ℝ ∧ 1 ∈
ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (((𝐴 − (𝐵↑2)) / 3) ≤ 1 ↔ (𝐴 − (𝐵↑2)) ≤ (3 ·
1))) |
| 86 | 75, 85 | mp3an2 1451 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 − (𝐵↑2)) ∈ ℝ ∧ (3 ∈
ℝ ∧ 0 < 3)) → (((𝐴 − (𝐵↑2)) / 3) ≤ 1 ↔ (𝐴 − (𝐵↑2)) ≤ (3 ·
1))) |
| 87 | 76, 84, 86 | mpanr12 705 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 − (𝐵↑2)) ∈ ℝ → (((𝐴 − (𝐵↑2)) / 3) ≤ 1 ↔ (𝐴 − (𝐵↑2)) ≤ (3 ·
1))) |
| 88 | 17, 87 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐴 − (𝐵↑2)) / 3) ≤ 1 ↔ (𝐴 − (𝐵↑2)) ≤ (3 ·
1))) |
| 89 | 83, 88 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐴 − (𝐵↑2)) / 3) ≤ 1) |
| 90 | | le2add 11745 |
. . . . . . . . . . . . . 14
⊢ ((((2
· 𝐵) ∈ ℝ
∧ ((𝐴 − (𝐵↑2)) / 3) ∈ ℝ)
∧ (2 ∈ ℝ ∧ 1 ∈ ℝ)) → (((2 · 𝐵) ≤ 2 ∧ ((𝐴 − (𝐵↑2)) / 3) ≤ 1) → ((2 ·
𝐵) + ((𝐴 − (𝐵↑2)) / 3)) ≤ (2 +
1))) |
| 91 | 36, 75, 90 | mpanr12 705 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝐵) ∈ ℝ
∧ ((𝐴 − (𝐵↑2)) / 3) ∈ ℝ)
→ (((2 · 𝐵)
≤ 2 ∧ ((𝐴 −
(𝐵↑2)) / 3) ≤ 1)
→ ((2 · 𝐵) +
((𝐴 − (𝐵↑2)) / 3)) ≤ (2 +
1))) |
| 92 | 52, 30, 91 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((2 · 𝐵) ≤ 2 ∧ ((𝐴 − (𝐵↑2)) / 3) ≤ 1) → ((2 ·
𝐵) + ((𝐴 − (𝐵↑2)) / 3)) ≤ (2 +
1))) |
| 93 | 64, 89, 92 | mp2and 699 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) ≤ (2 +
1)) |
| 94 | | df-3 12330 |
. . . . . . . . . . 11
⊢ 3 = (2 +
1) |
| 95 | 93, 94 | breqtrrdi 5185 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) ≤ 3) |
| 96 | 52, 30 | readdcld 11290 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) ∈
ℝ) |
| 97 | 76 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 3 ∈
ℝ) |
| 98 | 96, 97, 23 | lemul1d 13120 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) ≤ 3 ↔ (((2 ·
𝐵) + ((𝐴 − (𝐵↑2)) / 3)) · ((𝐴 − (𝐵↑2)) / 3)) ≤ (3 · ((𝐴 − (𝐵↑2)) / 3)))) |
| 99 | 95, 98 | mpbid 232 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) · ((𝐴 − (𝐵↑2)) / 3)) ≤ (3 · ((𝐴 − (𝐵↑2)) / 3))) |
| 100 | 17 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ∈ ℂ) |
| 101 | | 3cn 12347 |
. . . . . . . . . . 11
⊢ 3 ∈
ℂ |
| 102 | | 3ne0 12372 |
. . . . . . . . . . 11
⊢ 3 ≠
0 |
| 103 | | divcan2 11930 |
. . . . . . . . . . 11
⊢ (((𝐴 − (𝐵↑2)) ∈ ℂ ∧ 3 ∈
ℂ ∧ 3 ≠ 0) → (3 · ((𝐴 − (𝐵↑2)) / 3)) = (𝐴 − (𝐵↑2))) |
| 104 | 101, 102,
103 | mp3an23 1455 |
. . . . . . . . . 10
⊢ ((𝐴 − (𝐵↑2)) ∈ ℂ → (3 ·
((𝐴 − (𝐵↑2)) / 3)) = (𝐴 − (𝐵↑2))) |
| 105 | 100, 104 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (3 · ((𝐴 − (𝐵↑2)) / 3)) = (𝐴 − (𝐵↑2))) |
| 106 | 99, 105 | breqtrd 5169 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) · ((𝐴 − (𝐵↑2)) / 3)) ≤ (𝐴 − (𝐵↑2))) |
| 107 | 55, 106 | eqbrtrd 5165 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)) ≤ (𝐴 − (𝐵↑2))) |
| 108 | 39, 41 | readdcld 11290 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)) ∈
ℝ) |
| 109 | 34, 108, 65 | leaddsub2d 11865 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐵↑2) + ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2))) ≤ 𝐴 ↔ ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)) ≤ (𝐴 − (𝐵↑2)))) |
| 110 | 107, 109 | mpbird 257 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐵↑2) + ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2))) ≤ 𝐴) |
| 111 | 44, 110 | eqbrtrd 5165 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2) ≤ 𝐴) |
| 112 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑦 = (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) → (𝑦↑2) = ((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2)) |
| 113 | 112 | breq1d 5153 |
. . . . . 6
⊢ (𝑦 = (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) → ((𝑦↑2) ≤ 𝐴 ↔ ((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2) ≤ 𝐴)) |
| 114 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥↑2) = (𝑦↑2)) |
| 115 | 114 | breq1d 5153 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥↑2) ≤ 𝐴 ↔ (𝑦↑2) ≤ 𝐴)) |
| 116 | 115 | cbvrabv 3447 |
. . . . . . 7
⊢ {𝑥 ∈ ℝ+
∣ (𝑥↑2) ≤
𝐴} = {𝑦 ∈ ℝ+ ∣ (𝑦↑2) ≤ 𝐴} |
| 117 | 1, 116 | eqtri 2765 |
. . . . . 6
⊢ 𝑆 = {𝑦 ∈ ℝ+ ∣ (𝑦↑2) ≤ 𝐴} |
| 118 | 113, 117 | elrab2 3695 |
. . . . 5
⊢ ((𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈ 𝑆 ↔ ((𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈ ℝ+
∧ ((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2) ≤ 𝐴)) |
| 119 | 24, 111, 118 | sylanbrc 583 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈ 𝑆) |
| 120 | | suprub 12229 |
. . . . 5
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑦) ∧ (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈ 𝑆) → (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ sup(𝑆, ℝ, < )) |
| 121 | 120, 2 | breqtrrdi 5185 |
. . . 4
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑦) ∧ (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈ 𝑆) → (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ 𝐵) |
| 122 | 6, 119, 121 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ 𝐵) |
| 123 | 23 | rpgt0d 13080 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 0 < ((𝐴 − (𝐵↑2)) / 3)) |
| 124 | 29, 14 | ltaddposd 11847 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) → (0
< ((𝐴 − (𝐵↑2)) / 3) ↔ 𝐵 < (𝐵 + ((𝐴 − (𝐵↑2)) / 3)))) |
| 125 | 14, 29 | readdcld 11290 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈
ℝ) |
| 126 | 14, 125 | ltnled 11408 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵 < (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ↔ ¬ (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ 𝐵)) |
| 127 | 124, 126 | bitrd 279 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) → (0
< ((𝐴 − (𝐵↑2)) / 3) ↔ ¬
(𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ 𝐵)) |
| 128 | 127 | biimpa 476 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧ 0
< ((𝐴 − (𝐵↑2)) / 3)) → ¬
(𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ 𝐵) |
| 129 | 123, 128 | syldan 591 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ¬ (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ 𝐵) |
| 130 | 122, 129 | pm2.65da 817 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
¬ (𝐵↑2) < 𝐴) |
| 131 | 15, 11 | eqleltd 11405 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
((𝐵↑2) = 𝐴 ↔ ((𝐵↑2) ≤ 𝐴 ∧ ¬ (𝐵↑2) < 𝐴))) |
| 132 | 4, 130, 131 | mpbir2and 713 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵↑2) = 𝐴) |