| Step | Hyp | Ref
| Expression |
| 1 | | 01sqrexlem1.1 |
. . . 4
⊢ 𝑆 = {𝑥 ∈ ℝ+ ∣ (𝑥↑2) ≤ 𝐴} |
| 2 | | 01sqrexlem1.2 |
. . . 4
⊢ 𝐵 = sup(𝑆, ℝ, < ) |
| 3 | | 01sqrexlem5.3 |
. . . 4
⊢ 𝑇 = {𝑦 ∣ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏)} |
| 4 | 1, 2, 3 | 01sqrexlem5 15285 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
((𝑇 ⊆ ℝ ∧
𝑇 ≠ ∅ ∧
∃𝑣 ∈ ℝ
∀𝑢 ∈ 𝑇 𝑢 ≤ 𝑣) ∧ (𝐵↑2) = sup(𝑇, ℝ, < ))) |
| 5 | 4 | simprd 495 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵↑2) = sup(𝑇, ℝ, <
)) |
| 6 | | vex 3484 |
. . . . . 6
⊢ 𝑣 ∈ V |
| 7 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑦 = 𝑣 → (𝑦 = (𝑎 · 𝑏) ↔ 𝑣 = (𝑎 · 𝑏))) |
| 8 | 7 | 2rexbidv 3222 |
. . . . . 6
⊢ (𝑦 = 𝑣 → (∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑦 = (𝑎 · 𝑏) ↔ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑣 = (𝑎 · 𝑏))) |
| 9 | 6, 8, 3 | elab2 3682 |
. . . . 5
⊢ (𝑣 ∈ 𝑇 ↔ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑣 = (𝑎 · 𝑏)) |
| 10 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → (𝑥↑2) = (𝑎↑2)) |
| 11 | 10 | breq1d 5153 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → ((𝑥↑2) ≤ 𝐴 ↔ (𝑎↑2) ≤ 𝐴)) |
| 12 | 11, 1 | elrab2 3695 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝑆 ↔ (𝑎 ∈ ℝ+ ∧ (𝑎↑2) ≤ 𝐴)) |
| 13 | 12 | simplbi 497 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑆 → 𝑎 ∈ ℝ+) |
| 14 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑏 → (𝑥↑2) = (𝑏↑2)) |
| 15 | 14 | breq1d 5153 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑏 → ((𝑥↑2) ≤ 𝐴 ↔ (𝑏↑2) ≤ 𝐴)) |
| 16 | 15, 1 | elrab2 3695 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝑆 ↔ (𝑏 ∈ ℝ+ ∧ (𝑏↑2) ≤ 𝐴)) |
| 17 | 16 | simplbi 497 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ 𝑆 → 𝑏 ∈ ℝ+) |
| 18 | | rpre 13043 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℝ+
→ 𝑎 ∈
ℝ) |
| 19 | 18 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → 𝑎 ∈ ℝ) |
| 20 | | rpre 13043 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ ℝ+
→ 𝑏 ∈
ℝ) |
| 21 | 20 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → 𝑏 ∈ ℝ) |
| 22 | | rpgt0 13047 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ ℝ+
→ 0 < 𝑏) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → 0 < 𝑏) |
| 24 | | lemul1 12119 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ (𝑏 ∈ ℝ ∧ 0 <
𝑏)) → (𝑎 ≤ 𝑏 ↔ (𝑎 · 𝑏) ≤ (𝑏 · 𝑏))) |
| 25 | 19, 21, 21, 23, 24 | syl112anc 1376 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → (𝑎 ≤ 𝑏 ↔ (𝑎 · 𝑏) ≤ (𝑏 · 𝑏))) |
| 26 | 13, 17, 25 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑎 ≤ 𝑏 ↔ (𝑎 · 𝑏) ≤ (𝑏 · 𝑏))) |
| 27 | 17 | rpcnd 13079 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ 𝑆 → 𝑏 ∈ ℂ) |
| 28 | 27 | sqvald 14183 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝑆 → (𝑏↑2) = (𝑏 · 𝑏)) |
| 29 | 28 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ 𝑆 → ((𝑎 · 𝑏) ≤ (𝑏↑2) ↔ (𝑎 · 𝑏) ≤ (𝑏 · 𝑏))) |
| 30 | 29 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → ((𝑎 · 𝑏) ≤ (𝑏↑2) ↔ (𝑎 · 𝑏) ≤ (𝑏 · 𝑏))) |
| 31 | 26, 30 | bitr4d 282 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑎 ≤ 𝑏 ↔ (𝑎 · 𝑏) ≤ (𝑏↑2))) |
| 32 | 31 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 ≤ 𝑏 ↔ (𝑎 · 𝑏) ≤ (𝑏↑2))) |
| 33 | 16 | simprbi 496 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ 𝑆 → (𝑏↑2) ≤ 𝐴) |
| 34 | 33 | ad2antll 729 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑏↑2) ≤ 𝐴) |
| 35 | 13 | rpred 13077 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝑆 → 𝑎 ∈ ℝ) |
| 36 | 17 | rpred 13077 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝑆 → 𝑏 ∈ ℝ) |
| 37 | | remulcl 11240 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 · 𝑏) ∈ ℝ) |
| 38 | 35, 36, 37 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑎 · 𝑏) ∈ ℝ) |
| 39 | 38 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 · 𝑏) ∈ ℝ) |
| 40 | 36 | resqcld 14165 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ 𝑆 → (𝑏↑2) ∈ ℝ) |
| 41 | 40 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑏↑2) ∈ ℝ) |
| 42 | | rpre 13043 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
| 43 | 42 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → 𝐴 ∈ ℝ) |
| 44 | | letr 11355 |
. . . . . . . . . . . 12
⊢ (((𝑎 · 𝑏) ∈ ℝ ∧ (𝑏↑2) ∈ ℝ ∧ 𝐴 ∈ ℝ) → (((𝑎 · 𝑏) ≤ (𝑏↑2) ∧ (𝑏↑2) ≤ 𝐴) → (𝑎 · 𝑏) ≤ 𝐴)) |
| 45 | 39, 41, 43, 44 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (((𝑎 · 𝑏) ≤ (𝑏↑2) ∧ (𝑏↑2) ≤ 𝐴) → (𝑎 · 𝑏) ≤ 𝐴)) |
| 46 | 34, 45 | mpan2d 694 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → ((𝑎 · 𝑏) ≤ (𝑏↑2) → (𝑎 · 𝑏) ≤ 𝐴)) |
| 47 | 32, 46 | sylbid 240 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 ≤ 𝑏 → (𝑎 · 𝑏) ≤ 𝐴)) |
| 48 | | rpgt0 13047 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℝ+
→ 0 < 𝑎) |
| 49 | 48 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → 0 < 𝑎) |
| 50 | | lemul2 12120 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ ℝ ∧ 𝑎 ∈ ℝ ∧ (𝑎 ∈ ℝ ∧ 0 <
𝑎)) → (𝑏 ≤ 𝑎 ↔ (𝑎 · 𝑏) ≤ (𝑎 · 𝑎))) |
| 51 | 21, 19, 19, 49, 50 | syl112anc 1376 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈
ℝ+) → (𝑏 ≤ 𝑎 ↔ (𝑎 · 𝑏) ≤ (𝑎 · 𝑎))) |
| 52 | 13, 17, 51 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑏 ≤ 𝑎 ↔ (𝑎 · 𝑏) ≤ (𝑎 · 𝑎))) |
| 53 | 13 | rpcnd 13079 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ 𝑆 → 𝑎 ∈ ℂ) |
| 54 | 53 | sqvald 14183 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝑆 → (𝑎↑2) = (𝑎 · 𝑎)) |
| 55 | 54 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑆 → ((𝑎 · 𝑏) ≤ (𝑎↑2) ↔ (𝑎 · 𝑏) ≤ (𝑎 · 𝑎))) |
| 56 | 55 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → ((𝑎 · 𝑏) ≤ (𝑎↑2) ↔ (𝑎 · 𝑏) ≤ (𝑎 · 𝑎))) |
| 57 | 52, 56 | bitr4d 282 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑏 ≤ 𝑎 ↔ (𝑎 · 𝑏) ≤ (𝑎↑2))) |
| 58 | 57 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑏 ≤ 𝑎 ↔ (𝑎 · 𝑏) ≤ (𝑎↑2))) |
| 59 | 12 | simprbi 496 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝑆 → (𝑎↑2) ≤ 𝐴) |
| 60 | 59 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎↑2) ≤ 𝐴) |
| 61 | 35 | resqcld 14165 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑆 → (𝑎↑2) ∈ ℝ) |
| 62 | 61 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎↑2) ∈ ℝ) |
| 63 | | letr 11355 |
. . . . . . . . . . . 12
⊢ (((𝑎 · 𝑏) ∈ ℝ ∧ (𝑎↑2) ∈ ℝ ∧ 𝐴 ∈ ℝ) → (((𝑎 · 𝑏) ≤ (𝑎↑2) ∧ (𝑎↑2) ≤ 𝐴) → (𝑎 · 𝑏) ≤ 𝐴)) |
| 64 | 39, 62, 43, 63 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (((𝑎 · 𝑏) ≤ (𝑎↑2) ∧ (𝑎↑2) ≤ 𝐴) → (𝑎 · 𝑏) ≤ 𝐴)) |
| 65 | 60, 64 | mpan2d 694 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → ((𝑎 · 𝑏) ≤ (𝑎↑2) → (𝑎 · 𝑏) ≤ 𝐴)) |
| 66 | 58, 65 | sylbid 240 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑏 ≤ 𝑎 → (𝑎 · 𝑏) ≤ 𝐴)) |
| 67 | 1, 2 | 01sqrexlem3 15283 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝑆 ⊆ ℝ ∧
𝑆 ≠ ∅ ∧
∃𝑦 ∈ ℝ
∀𝑣 ∈ 𝑆 𝑣 ≤ 𝑦)) |
| 68 | 67 | simp1d 1143 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
𝑆 ⊆
ℝ) |
| 69 | 68 | sseld 3982 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝑎 ∈ 𝑆 → 𝑎 ∈ ℝ)) |
| 70 | 68 | sseld 3982 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝑏 ∈ 𝑆 → 𝑏 ∈ ℝ)) |
| 71 | 69, 70 | anim12d 609 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ))) |
| 72 | 71 | imp 406 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ)) |
| 73 | | letric 11361 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 ≤ 𝑏 ∨ 𝑏 ≤ 𝑎)) |
| 74 | 72, 73 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 ≤ 𝑏 ∨ 𝑏 ≤ 𝑎)) |
| 75 | 47, 66, 74 | mpjaod 861 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) ∧
(𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 · 𝑏) ≤ 𝐴) |
| 76 | 75 | ex 412 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑎 · 𝑏) ≤ 𝐴)) |
| 77 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑣 = (𝑎 · 𝑏) → (𝑣 ≤ 𝐴 ↔ (𝑎 · 𝑏) ≤ 𝐴)) |
| 78 | 77 | biimprcd 250 |
. . . . . . 7
⊢ ((𝑎 · 𝑏) ≤ 𝐴 → (𝑣 = (𝑎 · 𝑏) → 𝑣 ≤ 𝐴)) |
| 79 | 76, 78 | syl6 35 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
((𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆) → (𝑣 = (𝑎 · 𝑏) → 𝑣 ≤ 𝐴))) |
| 80 | 79 | rexlimdvv 3212 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 𝑣 = (𝑎 · 𝑏) → 𝑣 ≤ 𝐴)) |
| 81 | 9, 80 | biimtrid 242 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝑣 ∈ 𝑇 → 𝑣 ≤ 𝐴)) |
| 82 | 81 | ralrimiv 3145 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
∀𝑣 ∈ 𝑇 𝑣 ≤ 𝐴) |
| 83 | 4 | simpld 494 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝑇 ⊆ ℝ ∧
𝑇 ≠ ∅ ∧
∃𝑣 ∈ ℝ
∀𝑢 ∈ 𝑇 𝑢 ≤ 𝑣)) |
| 84 | 42 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
𝐴 ∈
ℝ) |
| 85 | | suprleub 12234 |
. . . 4
⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑢 ∈ 𝑇 𝑢 ≤ 𝑣) ∧ 𝐴 ∈ ℝ) → (sup(𝑇, ℝ, < ) ≤ 𝐴 ↔ ∀𝑣 ∈ 𝑇 𝑣 ≤ 𝐴)) |
| 86 | 83, 84, 85 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(sup(𝑇, ℝ, < )
≤ 𝐴 ↔ ∀𝑣 ∈ 𝑇 𝑣 ≤ 𝐴)) |
| 87 | 82, 86 | mpbird 257 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
sup(𝑇, ℝ, < ) ≤
𝐴) |
| 88 | 5, 87 | eqbrtrd 5165 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝐴 ≤ 1) →
(𝐵↑2) ≤ 𝐴) |