Step | Hyp | Ref
| Expression |
1 | | sqrlem1.1 |
. . 3
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} |
2 | | sqrlem1.2 |
. . 3
⊢ 𝐵 = sup(𝑆, ℝ, < ) |
3 | | sqrlem5.3 |
. . 3
⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)} |
4 | 1, 2, 3 | sqrlem6 13836 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵↑2) ≤ 𝐴) |
5 | 1, 2 | sqrlem3 13833 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝑆 ⊆ ℝ ∧
𝑆 ≠ ∅ ∧
∃𝑦 ∈ ℝ
∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑦)) |
6 | 5 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑦)) |
7 | 1, 2 | sqrlem4 13834 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵 ∈
ℝ+ ∧ 𝐵
≤ 1)) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵 ∈ ℝ+ ∧ 𝐵 ≤ 1)) |
9 | 8 | simpld 474 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 𝐵 ∈
ℝ+) |
10 | | rpre 11715 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
11 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
𝐴 ∈
ℝ) |
12 | | rpre 11715 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ∈
ℝ) |
13 | 12 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ+
∧ 𝐵 ≤ 1) →
𝐵 ∈
ℝ) |
14 | 7, 13 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
𝐵 ∈
ℝ) |
15 | 14 | resqcld 12897 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵↑2) ∈
ℝ) |
16 | 11, 15 | resubcld 10337 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐴 − (𝐵↑2)) ∈
ℝ) |
17 | 16 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ∈ ℝ) |
18 | 15, 11 | posdifd 10493 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
((𝐵↑2) < 𝐴 ↔ 0 < (𝐴 − (𝐵↑2)))) |
19 | 18 | biimpa 500 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 0 < (𝐴 − (𝐵↑2))) |
20 | 17, 19 | elrpd 11745 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ∈
ℝ+) |
21 | | 3re 10971 |
. . . . . . . 8
⊢ 3 ∈
ℝ |
22 | | 3pos 10991 |
. . . . . . . 8
⊢ 0 <
3 |
23 | 21, 22 | elrpii 11711 |
. . . . . . 7
⊢ 3 ∈
ℝ+ |
24 | | rpdivcl 11732 |
. . . . . . 7
⊢ (((𝐴 − (𝐵↑2)) ∈ ℝ+ ∧ 3
∈ ℝ+) → ((𝐴 − (𝐵↑2)) / 3) ∈
ℝ+) |
25 | 20, 23, 24 | sylancl 693 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐴 − (𝐵↑2)) / 3) ∈
ℝ+) |
26 | 9, 25 | rpaddcld 11763 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈
ℝ+) |
27 | 14 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 𝐵 ∈ ℝ) |
28 | 27 | recnd 9947 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 𝐵 ∈ ℂ) |
29 | | 3nn 11063 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
30 | | nndivre 10933 |
. . . . . . . . . . 11
⊢ (((𝐴 − (𝐵↑2)) ∈ ℝ ∧ 3 ∈
ℕ) → ((𝐴 −
(𝐵↑2)) / 3) ∈
ℝ) |
31 | 16, 29, 30 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
((𝐴 − (𝐵↑2)) / 3) ∈
ℝ) |
32 | 31 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐴 − (𝐵↑2)) / 3) ∈
ℝ) |
33 | 32 | recnd 9947 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐴 − (𝐵↑2)) / 3) ∈
ℂ) |
34 | | binom2 12841 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ ((𝐴 − (𝐵↑2)) / 3) ∈ ℂ) →
((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2) = (((𝐵↑2) + (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3)))) + (((𝐴 − (𝐵↑2)) / 3)↑2))) |
35 | 28, 33, 34 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2) = (((𝐵↑2) + (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3)))) + (((𝐴 − (𝐵↑2)) / 3)↑2))) |
36 | 15 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵↑2) ∈ ℝ) |
37 | 36 | recnd 9947 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵↑2) ∈ ℂ) |
38 | | 2re 10967 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
39 | 27, 32 | remulcld 9949 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵 · ((𝐴 − (𝐵↑2)) / 3)) ∈
ℝ) |
40 | | remulcl 9900 |
. . . . . . . . . 10
⊢ ((2
∈ ℝ ∧ (𝐵
· ((𝐴 − (𝐵↑2)) / 3)) ∈ ℝ)
→ (2 · (𝐵
· ((𝐴 − (𝐵↑2)) / 3))) ∈
ℝ) |
41 | 38, 39, 40 | sylancr 694 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) ∈
ℝ) |
42 | 41 | recnd 9947 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) ∈
ℂ) |
43 | 32 | resqcld 12897 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐴 − (𝐵↑2)) / 3)↑2) ∈
ℝ) |
44 | 43 | recnd 9947 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐴 − (𝐵↑2)) / 3)↑2) ∈
ℂ) |
45 | 37, 42, 44 | addassd 9941 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐵↑2) + (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3)))) + (((𝐴 − (𝐵↑2)) / 3)↑2)) = ((𝐵↑2) + ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)))) |
46 | 35, 45 | eqtrd 2644 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2) = ((𝐵↑2) + ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)))) |
47 | | 2cn 10968 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
48 | | mulass 9903 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 𝐵
∈ ℂ ∧ ((𝐴
− (𝐵↑2)) / 3)
∈ ℂ) → ((2 · 𝐵) · ((𝐴 − (𝐵↑2)) / 3)) = (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3)))) |
49 | 47, 48 | mp3an1 1403 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℂ ∧ ((𝐴 − (𝐵↑2)) / 3) ∈ ℂ) → ((2
· 𝐵) ·
((𝐴 − (𝐵↑2)) / 3)) = (2 ·
(𝐵 · ((𝐴 − (𝐵↑2)) / 3)))) |
50 | 28, 33, 49 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · 𝐵) · ((𝐴 − (𝐵↑2)) / 3)) = (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3)))) |
51 | 50 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) = ((2 · 𝐵) · ((𝐴 − (𝐵↑2)) / 3))) |
52 | 33 | sqvald 12867 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐴 − (𝐵↑2)) / 3)↑2) = (((𝐴 − (𝐵↑2)) / 3) · ((𝐴 − (𝐵↑2)) / 3))) |
53 | 51, 52 | oveq12d 6567 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)) = (((2 ·
𝐵) · ((𝐴 − (𝐵↑2)) / 3)) + (((𝐴 − (𝐵↑2)) / 3) · ((𝐴 − (𝐵↑2)) / 3)))) |
54 | | remulcl 9900 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 𝐵
∈ ℝ) → (2 · 𝐵) ∈ ℝ) |
55 | 38, 27, 54 | sylancr 694 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · 𝐵) ∈
ℝ) |
56 | 55 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · 𝐵) ∈
ℂ) |
57 | 56, 33, 33 | adddird 9944 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) · ((𝐴 − (𝐵↑2)) / 3)) = (((2 · 𝐵) · ((𝐴 − (𝐵↑2)) / 3)) + (((𝐴 − (𝐵↑2)) / 3) · ((𝐴 − (𝐵↑2)) / 3)))) |
58 | 53, 57 | eqtr4d 2647 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)) = (((2 ·
𝐵) + ((𝐴 − (𝐵↑2)) / 3)) · ((𝐴 − (𝐵↑2)) / 3))) |
59 | 7 | simprd 478 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
𝐵 ≤ 1) |
60 | | 2pos 10989 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
2 |
61 | | 1re 9918 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
62 | | lemul2 10755 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ ℝ ∧ 1 ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐵 ≤ 1 ↔ (2 · 𝐵) ≤ (2 · 1))) |
63 | 61, 62 | mp3an2 1404 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → (𝐵 ≤ 1 ↔ (2 · 𝐵) ≤ (2 · 1))) |
64 | 38, 60, 63 | mpanr12 717 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℝ → (𝐵 ≤ 1 ↔ (2 · 𝐵) ≤ (2 ·
1))) |
65 | 14, 64 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵 ≤ 1 ↔ (2
· 𝐵) ≤ (2
· 1))) |
66 | 59, 65 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) → (2
· 𝐵) ≤ (2
· 1)) |
67 | 66 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · 𝐵) ≤ (2 ·
1)) |
68 | | 2t1e2 11053 |
. . . . . . . . . . . . 13
⊢ (2
· 1) = 2 |
69 | 67, 68 | syl6breq 4624 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (2 · 𝐵) ≤ 2) |
70 | 11 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 𝐴 ∈ ℝ) |
71 | 61 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 1 ∈
ℝ) |
72 | 27 | sqge0d 12898 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 0 ≤ (𝐵↑2)) |
73 | 70, 36 | addge01d 10494 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (0 ≤ (𝐵↑2) ↔ 𝐴 ≤ (𝐴 + (𝐵↑2)))) |
74 | 72, 73 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 𝐴 ≤ (𝐴 + (𝐵↑2))) |
75 | 70, 36, 70 | lesubaddd 10503 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐴 − (𝐵↑2)) ≤ 𝐴 ↔ 𝐴 ≤ (𝐴 + (𝐵↑2)))) |
76 | 74, 75 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ≤ 𝐴) |
77 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 𝐴 ≤ 1) |
78 | 17, 70, 71, 76, 77 | letrd 10073 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ≤ 1) |
79 | | 1le3 11121 |
. . . . . . . . . . . . . . . 16
⊢ 1 ≤
3 |
80 | | letr 10010 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 − (𝐵↑2)) ∈ ℝ ∧ 1 ∈
ℝ ∧ 3 ∈ ℝ) → (((𝐴 − (𝐵↑2)) ≤ 1 ∧ 1 ≤ 3) →
(𝐴 − (𝐵↑2)) ≤
3)) |
81 | 61, 21, 80 | mp3an23 1408 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 − (𝐵↑2)) ∈ ℝ → (((𝐴 − (𝐵↑2)) ≤ 1 ∧ 1 ≤ 3) →
(𝐴 − (𝐵↑2)) ≤
3)) |
82 | 17, 81 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐴 − (𝐵↑2)) ≤ 1 ∧ 1 ≤ 3) →
(𝐴 − (𝐵↑2)) ≤
3)) |
83 | 79, 82 | mpan2i 709 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐴 − (𝐵↑2)) ≤ 1 → (𝐴 − (𝐵↑2)) ≤ 3)) |
84 | 78, 83 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ≤ 3) |
85 | | 3t1e3 11055 |
. . . . . . . . . . . . . 14
⊢ (3
· 1) = 3 |
86 | 84, 85 | syl6breqr 4625 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ≤ (3 ·
1)) |
87 | | ledivmul 10778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 − (𝐵↑2)) ∈ ℝ ∧ 1 ∈
ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (((𝐴 − (𝐵↑2)) / 3) ≤ 1 ↔ (𝐴 − (𝐵↑2)) ≤ (3 ·
1))) |
88 | 61, 87 | mp3an2 1404 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 − (𝐵↑2)) ∈ ℝ ∧ (3 ∈
ℝ ∧ 0 < 3)) → (((𝐴 − (𝐵↑2)) / 3) ≤ 1 ↔ (𝐴 − (𝐵↑2)) ≤ (3 ·
1))) |
89 | 21, 22, 88 | mpanr12 717 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 − (𝐵↑2)) ∈ ℝ → (((𝐴 − (𝐵↑2)) / 3) ≤ 1 ↔ (𝐴 − (𝐵↑2)) ≤ (3 ·
1))) |
90 | 17, 89 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐴 − (𝐵↑2)) / 3) ≤ 1 ↔ (𝐴 − (𝐵↑2)) ≤ (3 ·
1))) |
91 | 86, 90 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐴 − (𝐵↑2)) / 3) ≤ 1) |
92 | | le2add 10389 |
. . . . . . . . . . . . . 14
⊢ ((((2
· 𝐵) ∈ ℝ
∧ ((𝐴 − (𝐵↑2)) / 3) ∈ ℝ)
∧ (2 ∈ ℝ ∧ 1 ∈ ℝ)) → (((2 · 𝐵) ≤ 2 ∧ ((𝐴 − (𝐵↑2)) / 3) ≤ 1) → ((2 ·
𝐵) + ((𝐴 − (𝐵↑2)) / 3)) ≤ (2 +
1))) |
93 | 38, 61, 92 | mpanr12 717 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝐵) ∈ ℝ
∧ ((𝐴 − (𝐵↑2)) / 3) ∈ ℝ)
→ (((2 · 𝐵)
≤ 2 ∧ ((𝐴 −
(𝐵↑2)) / 3) ≤ 1)
→ ((2 · 𝐵) +
((𝐴 − (𝐵↑2)) / 3)) ≤ (2 +
1))) |
94 | 55, 32, 93 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((2 · 𝐵) ≤ 2 ∧ ((𝐴 − (𝐵↑2)) / 3) ≤ 1) → ((2 ·
𝐵) + ((𝐴 − (𝐵↑2)) / 3)) ≤ (2 +
1))) |
95 | 69, 91, 94 | mp2and 711 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) ≤ (2 +
1)) |
96 | | df-3 10957 |
. . . . . . . . . . 11
⊢ 3 = (2 +
1) |
97 | 95, 96 | syl6breqr 4625 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) ≤ 3) |
98 | 55, 32 | readdcld 9948 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) ∈
ℝ) |
99 | 21 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 3 ∈
ℝ) |
100 | 98, 99, 25 | lemul1d 11791 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) ≤ 3 ↔ (((2 ·
𝐵) + ((𝐴 − (𝐵↑2)) / 3)) · ((𝐴 − (𝐵↑2)) / 3)) ≤ (3 · ((𝐴 − (𝐵↑2)) / 3)))) |
101 | 97, 100 | mpbid 221 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) · ((𝐴 − (𝐵↑2)) / 3)) ≤ (3 · ((𝐴 − (𝐵↑2)) / 3))) |
102 | 17 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐴 − (𝐵↑2)) ∈ ℂ) |
103 | | 3cn 10972 |
. . . . . . . . . . 11
⊢ 3 ∈
ℂ |
104 | | 3ne0 10992 |
. . . . . . . . . . 11
⊢ 3 ≠
0 |
105 | | divcan2 10572 |
. . . . . . . . . . 11
⊢ (((𝐴 − (𝐵↑2)) ∈ ℂ ∧ 3 ∈
ℂ ∧ 3 ≠ 0) → (3 · ((𝐴 − (𝐵↑2)) / 3)) = (𝐴 − (𝐵↑2))) |
106 | 103, 104,
105 | mp3an23 1408 |
. . . . . . . . . 10
⊢ ((𝐴 − (𝐵↑2)) ∈ ℂ → (3 ·
((𝐴 − (𝐵↑2)) / 3)) = (𝐴 − (𝐵↑2))) |
107 | 102, 106 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (3 · ((𝐴 − (𝐵↑2)) / 3)) = (𝐴 − (𝐵↑2))) |
108 | 101, 107 | breqtrd 4609 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((2 · 𝐵) + ((𝐴 − (𝐵↑2)) / 3)) · ((𝐴 − (𝐵↑2)) / 3)) ≤ (𝐴 − (𝐵↑2))) |
109 | 58, 108 | eqbrtrd 4605 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)) ≤ (𝐴 − (𝐵↑2))) |
110 | 41, 43 | readdcld 9948 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)) ∈
ℝ) |
111 | 36, 110, 70 | leaddsub2d 10508 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (((𝐵↑2) + ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2))) ≤ 𝐴 ↔ ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2)) ≤ (𝐴 − (𝐵↑2)))) |
112 | 109, 111 | mpbird 246 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐵↑2) + ((2 · (𝐵 · ((𝐴 − (𝐵↑2)) / 3))) + (((𝐴 − (𝐵↑2)) / 3)↑2))) ≤ 𝐴) |
113 | 46, 112 | eqbrtrd 4605 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2) ≤ 𝐴) |
114 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑦 = (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) → (𝑦↑2) = ((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2)) |
115 | 114 | breq1d 4593 |
. . . . . 6
⊢ (𝑦 = (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) → ((𝑦↑2) ≤ 𝐴 ↔ ((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2) ≤ 𝐴)) |
116 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥↑2) = (𝑦↑2)) |
117 | 116 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥↑2) ≤ 𝐴 ↔ (𝑦↑2) ≤ 𝐴)) |
118 | 117 | cbvrabv 3172 |
. . . . . . 7
⊢ {𝑥 ∈ ℝ+
∣ (𝑥↑2) ≤
𝐴} = {𝑦 ∈ ℝ+ ∣ (𝑦↑2) ≤ 𝐴} |
119 | 1, 118 | eqtri 2632 |
. . . . . 6
⊢ 𝑆 = {𝑦 ∈ ℝ+ ∣ (𝑦↑2) ≤ 𝐴} |
120 | 115, 119 | elrab2 3333 |
. . . . 5
⊢ ((𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈ 𝑆 ↔ ((𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈ ℝ+
∧ ((𝐵 + ((𝐴 − (𝐵↑2)) / 3))↑2) ≤ 𝐴)) |
121 | 26, 113, 120 | sylanbrc 695 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈ 𝑆) |
122 | | suprub 10863 |
. . . . 5
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑦) ∧ (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈ 𝑆) → (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ sup(𝑆, ℝ, < )) |
123 | 122, 2 | syl6breqr 4625 |
. . . 4
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑦) ∧ (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈ 𝑆) → (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ 𝐵) |
124 | 6, 121, 123 | syl2anc 691 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ 𝐵) |
125 | 25 | rpgt0d 11751 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → 0 < ((𝐴 − (𝐵↑2)) / 3)) |
126 | 31, 14 | ltaddposd 10490 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) → (0
< ((𝐴 − (𝐵↑2)) / 3) ↔ 𝐵 < (𝐵 + ((𝐴 − (𝐵↑2)) / 3)))) |
127 | 14, 31 | readdcld 9948 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ∈
ℝ) |
128 | 14, 127 | ltnled 10063 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵 < (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ↔ ¬ (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ 𝐵)) |
129 | 126, 128 | bitrd 267 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) → (0
< ((𝐴 − (𝐵↑2)) / 3) ↔ ¬
(𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ 𝐵)) |
130 | 129 | biimpa 500 |
. . . 4
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧ 0
< ((𝐴 − (𝐵↑2)) / 3)) → ¬
(𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ 𝐵) |
131 | 125, 130 | syldan 486 |
. . 3
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝐵↑2) < 𝐴) → ¬ (𝐵 + ((𝐴 − (𝐵↑2)) / 3)) ≤ 𝐵) |
132 | 124, 131 | pm2.65da 598 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
¬ (𝐵↑2) < 𝐴) |
133 | 15, 11 | eqleltd 10060 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
((𝐵↑2) = 𝐴 ↔ ((𝐵↑2) ≤ 𝐴 ∧ ¬ (𝐵↑2) < 𝐴))) |
134 | 4, 132, 133 | mpbir2and 959 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵↑2) = 𝐴) |