| Step | Hyp | Ref
| Expression |
| 1 | | 2sq.1 |
. 2
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) |
| 2 | | 2sqlem8.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘2)) |
| 3 | | eluz2b3 12964 |
. . . 4
⊢ (𝑀 ∈
(ℤ≥‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1)) |
| 4 | 2, 3 | sylib 218 |
. . 3
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1)) |
| 5 | 4 | simpld 494 |
. 2
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 6 | | 2sqlem9.7 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∥ 𝑁) |
| 7 | | eluzelz 12888 |
. . . . . . . . 9
⊢ (𝑀 ∈
(ℤ≥‘2) → 𝑀 ∈ ℤ) |
| 8 | 2, 7 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 9 | | 2sqlem8.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 10 | 9 | nnzd 12640 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 11 | | 2sqlem8.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℤ) |
| 12 | | 2sqlem8.c |
. . . . . . . . . . . 12
⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
| 13 | 11, 5, 12 | 4sqlem5 16980 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 ∈ ℤ ∧ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ)) |
| 14 | 13 | simpld 494 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℤ) |
| 15 | | zsqcl 14169 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ℤ → (𝐶↑2) ∈
ℤ) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶↑2) ∈ ℤ) |
| 17 | | 2sqlem8.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℤ) |
| 18 | | 2sqlem8.d |
. . . . . . . . . . . 12
⊢ 𝐷 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
| 19 | 17, 5, 18 | 4sqlem5 16980 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷 ∈ ℤ ∧ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ)) |
| 20 | 19 | simpld 494 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℤ) |
| 21 | | zsqcl 14169 |
. . . . . . . . . 10
⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈
ℤ) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷↑2) ∈ ℤ) |
| 23 | 16, 22 | zaddcld 12726 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) |
| 24 | | zsqcl 14169 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈
ℤ) |
| 25 | 11, 24 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴↑2) ∈ ℤ) |
| 26 | 25, 16 | zsubcld 12727 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴↑2) − (𝐶↑2)) ∈ ℤ) |
| 27 | | zsqcl 14169 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈
ℤ) |
| 28 | 17, 27 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵↑2) ∈ ℤ) |
| 29 | 28, 22 | zsubcld 12727 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵↑2) − (𝐷↑2)) ∈ ℤ) |
| 30 | 11, 5, 12 | 4sqlem8 16983 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐶↑2))) |
| 31 | 17, 5, 18 | 4sqlem8 16983 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐷↑2))) |
| 32 | 8, 26, 29, 30, 31 | dvds2addd 16329 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2)))) |
| 33 | | 2sqlem8.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2))) |
| 34 | 33 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2)))) |
| 35 | 25 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) |
| 36 | 28 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵↑2) ∈ ℂ) |
| 37 | 16 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶↑2) ∈ ℂ) |
| 38 | 22 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷↑2) ∈ ℂ) |
| 39 | 35, 36, 37, 38 | addsub4d 11667 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2)))) |
| 40 | 34, 39 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2)))) |
| 41 | 32, 40 | breqtrrd 5171 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2)))) |
| 42 | | dvdssub2 16338 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) ∧ 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2)))) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ((𝐶↑2) + (𝐷↑2)))) |
| 43 | 8, 10, 23, 41, 42 | syl31anc 1375 |
. . . . . . 7
⊢ (𝜑 → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ((𝐶↑2) + (𝐷↑2)))) |
| 44 | 6, 43 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∥ ((𝐶↑2) + (𝐷↑2))) |
| 45 | | 2sqlem7.2 |
. . . . . . . . . . . 12
⊢ 𝑌 = {𝑧 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2)))} |
| 46 | | 2sqlem9.5 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) |
| 47 | | 2sqlem8.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) |
| 48 | 1, 45, 46, 6, 9, 2,
11, 17, 47, 33, 12, 18 | 2sqlem8a 27469 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ) |
| 49 | 48 | nnzd 12640 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℤ) |
| 50 | | zsqcl2 14178 |
. . . . . . . . . 10
⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈
ℕ0) |
| 51 | 49, 50 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈
ℕ0) |
| 52 | 51 | nn0cnd 12589 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℂ) |
| 53 | | 2sqlem8.e |
. . . . . . . . . . 11
⊢ 𝐸 = (𝐶 / (𝐶 gcd 𝐷)) |
| 54 | | gcddvds 16540 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷)) |
| 55 | 14, 20, 54 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷)) |
| 56 | 55 | simpld 494 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐶) |
| 57 | 48 | nnne0d 12316 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶 gcd 𝐷) ≠ 0) |
| 58 | | dvdsval2 16293 |
. . . . . . . . . . . . 13
⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐶 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ)) |
| 59 | 49, 57, 14, 58 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ)) |
| 60 | 56, 59 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ) |
| 61 | 53, 60 | eqeltrid 2845 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℤ) |
| 62 | | zsqcl2 14178 |
. . . . . . . . . 10
⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈
ℕ0) |
| 63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸↑2) ∈
ℕ0) |
| 64 | 63 | nn0cnd 12589 |
. . . . . . . 8
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) |
| 65 | | 2sqlem8.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝐷 / (𝐶 gcd 𝐷)) |
| 66 | 55 | simprd 495 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐷) |
| 67 | | dvdsval2 16293 |
. . . . . . . . . . . . 13
⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ)) |
| 68 | 49, 57, 20, 67 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ)) |
| 69 | 66, 68 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ) |
| 70 | 65, 69 | eqeltrid 2845 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ℤ) |
| 71 | | zsqcl2 14178 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈
ℕ0) |
| 72 | 70, 71 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹↑2) ∈
ℕ0) |
| 73 | 72 | nn0cnd 12589 |
. . . . . . . 8
⊢ (𝜑 → (𝐹↑2) ∈ ℂ) |
| 74 | 52, 64, 73 | adddid 11285 |
. . . . . . 7
⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)))) |
| 75 | 49 | zcnd 12723 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℂ) |
| 76 | 61 | zcnd 12723 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℂ) |
| 77 | 75, 76 | sqmuld 14198 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐸↑2))) |
| 78 | 53 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ ((𝐶 gcd 𝐷) · 𝐸) = ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷))) |
| 79 | 14 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 80 | 79, 75, 57 | divcan2d 12045 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷))) = 𝐶) |
| 81 | 78, 80 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐸) = 𝐶) |
| 82 | 81 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (𝐶↑2)) |
| 83 | 77, 82 | eqtr3d 2779 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) = (𝐶↑2)) |
| 84 | 70 | zcnd 12723 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ℂ) |
| 85 | 75, 84 | sqmuld 14198 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))) |
| 86 | 65 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ ((𝐶 gcd 𝐷) · 𝐹) = ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷))) |
| 87 | 20 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈ ℂ) |
| 88 | 87, 75, 57 | divcan2d 12045 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷))) = 𝐷) |
| 89 | 86, 88 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐹) = 𝐷) |
| 90 | 89 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (𝐷↑2)) |
| 91 | 85, 90 | eqtr3d 2779 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)) = (𝐷↑2)) |
| 92 | 83, 91 | oveq12d 7449 |
. . . . . . 7
⊢ (𝜑 → ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2))) |
| 93 | 74, 92 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2))) |
| 94 | 44, 93 | breqtrrd 5171 |
. . . . 5
⊢ (𝜑 → 𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2)))) |
| 95 | | zsqcl 14169 |
. . . . . . . 8
⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℤ) |
| 96 | 49, 95 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℤ) |
| 97 | 8, 96 | gcdcomd 16551 |
. . . . . 6
⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = (((𝐶 gcd 𝐷)↑2) gcd 𝑀)) |
| 98 | 49, 8 | gcdcld 16545 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈
ℕ0) |
| 99 | 98 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ) |
| 100 | | gcddvds 16540 |
. . . . . . . . . . . . . 14
⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀)) |
| 101 | 49, 8, 100 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀)) |
| 102 | 101 | simpld 494 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷)) |
| 103 | 99, 49, 14, 102, 56 | dvdstrd 16332 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶) |
| 104 | 11, 14 | zsubcld 12727 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℤ) |
| 105 | 101 | simprd 495 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀) |
| 106 | 13 | simprd 495 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ) |
| 107 | 5 | nnne0d 12316 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ≠ 0) |
| 108 | | dvdsval2 16293 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐴 − 𝐶) ∈ ℤ) → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ)) |
| 109 | 8, 107, 104, 108 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ)) |
| 110 | 106, 109 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∥ (𝐴 − 𝐶)) |
| 111 | 99, 8, 104, 105, 110 | dvdstrd 16332 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶)) |
| 112 | | dvdssub2 16338 |
. . . . . . . . . . . 12
⊢
(((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶)) |
| 113 | 99, 11, 14, 111, 112 | syl31anc 1375 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶)) |
| 114 | 103, 113 | mpbird 257 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴) |
| 115 | 99, 49, 20, 102, 66 | dvdstrd 16332 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷) |
| 116 | 17, 20 | zsubcld 12727 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℤ) |
| 117 | 19 | simprd 495 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ) |
| 118 | | dvdsval2 16293 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐵 − 𝐷) ∈ ℤ) → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ)) |
| 119 | 8, 107, 116, 118 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ)) |
| 120 | 117, 119 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∥ (𝐵 − 𝐷)) |
| 121 | 99, 8, 116, 105, 120 | dvdstrd 16332 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷)) |
| 122 | | dvdssub2 16338 |
. . . . . . . . . . . 12
⊢
(((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷)) |
| 123 | 99, 17, 20, 121, 122 | syl31anc 1375 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷)) |
| 124 | 115, 123 | mpbird 257 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) |
| 125 | | ax-1ne0 11224 |
. . . . . . . . . . . . . . 15
⊢ 1 ≠
0 |
| 126 | 125 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ≠ 0) |
| 127 | 47, 126 | eqnetrd 3008 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 gcd 𝐵) ≠ 0) |
| 128 | 127 | neneqd 2945 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ (𝐴 gcd 𝐵) = 0) |
| 129 | | gcdeq0 16554 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0))) |
| 130 | 11, 17, 129 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0))) |
| 131 | 128, 130 | mtbid 324 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
| 132 | | dvdslegcd 16541 |
. . . . . . . . . . 11
⊢
(((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵))) |
| 133 | 99, 11, 17, 131, 132 | syl31anc 1375 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵))) |
| 134 | 114, 124,
133 | mp2and 699 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)) |
| 135 | 134, 47 | breqtrd 5169 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1) |
| 136 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0) → 𝑀 = 0) |
| 137 | 136 | necon3ai 2965 |
. . . . . . . . . . 11
⊢ (𝑀 ≠ 0 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) |
| 138 | 107, 137 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) |
| 139 | | gcdn0cl 16539 |
. . . . . . . . . 10
⊢ ((((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ) |
| 140 | 49, 8, 138, 139 | syl21anc 838 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ) |
| 141 | | nnle1eq1 12296 |
. . . . . . . . 9
⊢ (((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1)) |
| 142 | 140, 141 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) = 1)) |
| 143 | 135, 142 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) = 1) |
| 144 | | 2nn 12339 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
| 145 | 144 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℕ) |
| 146 | | rplpwr 16595 |
. . . . . . . 8
⊢ (((𝐶 gcd 𝐷) ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 2 ∈ ℕ)
→ (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1)) |
| 147 | 48, 5, 145, 146 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1)) |
| 148 | 143, 147 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1) |
| 149 | 97, 148 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) |
| 150 | 63, 72 | nn0addcld 12591 |
. . . . . . 7
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈
ℕ0) |
| 151 | 150 | nn0zd 12639 |
. . . . . 6
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) |
| 152 | | coprmdvds 16690 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ ((𝐶 gcd 𝐷)↑2) ∈ ℤ ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2)))) |
| 153 | 8, 96, 151, 152 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2)))) |
| 154 | 94, 149, 153 | mp2and 699 |
. . . 4
⊢ (𝜑 → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))) |
| 155 | | dvdsval2 16293 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)) |
| 156 | 8, 107, 151, 155 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)) |
| 157 | 154, 156 | mpbid 232 |
. . 3
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) |
| 158 | 63 | nn0red 12588 |
. . . . 5
⊢ (𝜑 → (𝐸↑2) ∈ ℝ) |
| 159 | 72 | nn0red 12588 |
. . . . 5
⊢ (𝜑 → (𝐹↑2) ∈ ℝ) |
| 160 | 158, 159 | readdcld 11290 |
. . . 4
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℝ) |
| 161 | 5 | nnred 12281 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 162 | 1, 45 | 2sqlem7 27468 |
. . . . . . 7
⊢ 𝑌 ⊆ (𝑆 ∩ ℕ) |
| 163 | | inss2 4238 |
. . . . . . 7
⊢ (𝑆 ∩ ℕ) ⊆
ℕ |
| 164 | 162, 163 | sstri 3993 |
. . . . . 6
⊢ 𝑌 ⊆
ℕ |
| 165 | 61, 70 | gcdcld 16545 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 gcd 𝐹) ∈
ℕ0) |
| 166 | 165 | nn0cnd 12589 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 gcd 𝐹) ∈ ℂ) |
| 167 | | 1cnd 11256 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
| 168 | 75 | mulridd 11278 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 gcd 𝐷) · 1) = (𝐶 gcd 𝐷)) |
| 169 | 81, 89 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = (𝐶 gcd 𝐷)) |
| 170 | 14, 20 | gcdcld 16545 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 gcd 𝐷) ∈
ℕ0) |
| 171 | | mulgcd 16585 |
. . . . . . . . . . 11
⊢ (((𝐶 gcd 𝐷) ∈ ℕ0 ∧ 𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹))) |
| 172 | 170, 61, 70, 171 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹))) |
| 173 | 168, 169,
172 | 3eqtr2rd 2784 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)) = ((𝐶 gcd 𝐷) · 1)) |
| 174 | 166, 167,
75, 57, 173 | mulcanad 11898 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 gcd 𝐹) = 1) |
| 175 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2))) |
| 176 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐸 → (𝑥 gcd 𝑦) = (𝐸 gcd 𝑦)) |
| 177 | 176 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐸 → ((𝑥 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝑦) = 1)) |
| 178 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐸 → (𝑥↑2) = (𝐸↑2)) |
| 179 | 178 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐸 → ((𝑥↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝑦↑2))) |
| 180 | 179 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐸 → (((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)))) |
| 181 | 177, 180 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑥 = 𝐸 → (((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))))) |
| 182 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐹 → (𝐸 gcd 𝑦) = (𝐸 gcd 𝐹)) |
| 183 | 182 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐹 → ((𝐸 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝐹) = 1)) |
| 184 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐹 → (𝑦↑2) = (𝐹↑2)) |
| 185 | 184 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐹 → ((𝐸↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝐹↑2))) |
| 186 | 185 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐹 → (((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))) |
| 187 | 183, 186 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑦 = 𝐹 → (((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2))))) |
| 188 | 181, 187 | rspc2ev 3635 |
. . . . . . . 8
⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ∧ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))) |
| 189 | 61, 70, 174, 175, 188 | syl112anc 1376 |
. . . . . . 7
⊢ (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))) |
| 190 | | ovex 7464 |
. . . . . . . 8
⊢ ((𝐸↑2) + (𝐹↑2)) ∈ V |
| 191 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (𝑧 = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))) |
| 192 | 191 | anbi2d 630 |
. . . . . . . . 9
⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))) |
| 193 | 192 | 2rexbidv 3222 |
. . . . . . . 8
⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))) |
| 194 | 190, 193,
45 | elab2 3682 |
. . . . . . 7
⊢ (((𝐸↑2) + (𝐹↑2)) ∈ 𝑌 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))) |
| 195 | 189, 194 | sylibr 234 |
. . . . . 6
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌) |
| 196 | 164, 195 | sselid 3981 |
. . . . 5
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ) |
| 197 | 196 | nngt0d 12315 |
. . . 4
⊢ (𝜑 → 0 < ((𝐸↑2) + (𝐹↑2))) |
| 198 | 5 | nngt0d 12315 |
. . . 4
⊢ (𝜑 → 0 < 𝑀) |
| 199 | 160, 161,
197, 198 | divgt0d 12203 |
. . 3
⊢ (𝜑 → 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀)) |
| 200 | | elnnz 12623 |
. . 3
⊢ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ ↔ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀))) |
| 201 | 157, 199,
200 | sylanbrc 583 |
. 2
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ) |
| 202 | | prmnn 16711 |
. . . . . . . 8
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
| 203 | 202 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℕ) |
| 204 | 203 | nnred 12281 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℝ) |
| 205 | 157 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) |
| 206 | 205 | zred 12722 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℝ) |
| 207 | | peano2zm 12660 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
| 208 | 8, 207 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
| 209 | 208 | zred 12722 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 − 1) ∈ ℝ) |
| 210 | 209 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℝ) |
| 211 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀)) |
| 212 | | prmz 16712 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
| 213 | 212 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℤ) |
| 214 | 201 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ) |
| 215 | | dvdsle 16347 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) |
| 216 | 213, 214,
215 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) |
| 217 | 211, 216 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)) |
| 218 | | zsqcl 14169 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℤ → (𝑀↑2) ∈
ℤ) |
| 219 | 8, 218 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀↑2) ∈ ℤ) |
| 220 | 219 | zred 12722 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀↑2) ∈ ℝ) |
| 221 | 220 | rehalfcld 12513 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑀↑2) / 2) ∈
ℝ) |
| 222 | 16 | zred 12722 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶↑2) ∈ ℝ) |
| 223 | 22 | zred 12722 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐷↑2) ∈ ℝ) |
| 224 | 222, 223 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℝ) |
| 225 | | 1red 11262 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℝ) |
| 226 | 48 | nnsqcld 14283 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ) |
| 227 | 226 | nnred 12281 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℝ) |
| 228 | 150 | nn0ge0d 12590 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ ((𝐸↑2) + (𝐹↑2))) |
| 229 | 226 | nnge1d 12314 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ≤ ((𝐶 gcd 𝐷)↑2)) |
| 230 | 225, 227,
160, 228, 229 | lemul1ad 12207 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) ≤ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2)))) |
| 231 | 150 | nn0cnd 12589 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ) |
| 232 | 231 | mullidd 11279 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) = ((𝐸↑2) + (𝐹↑2))) |
| 233 | 230, 232,
93 | 3brtr3d 5174 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝐶↑2) + (𝐷↑2))) |
| 234 | 221 | rehalfcld 12513 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑀↑2) / 2) / 2) ∈
ℝ) |
| 235 | 11, 5, 12 | 4sqlem7 16982 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐶↑2) ≤ (((𝑀↑2) / 2) / 2)) |
| 236 | 17, 5, 18 | 4sqlem7 16982 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐷↑2) ≤ (((𝑀↑2) / 2) / 2)) |
| 237 | 222, 223,
234, 234, 235, 236 | le2addd 11882 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2))) |
| 238 | 221 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀↑2) / 2) ∈
ℂ) |
| 239 | 238 | 2halvesd 12512 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) = ((𝑀↑2) / 2)) |
| 240 | 237, 239 | breqtrd 5169 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((𝑀↑2) / 2)) |
| 241 | 160, 224,
221, 233, 240 | letrd 11418 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝑀↑2) / 2)) |
| 242 | 5 | nnsqcld 14283 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀↑2) ∈ ℕ) |
| 243 | 242 | nnrpd 13075 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀↑2) ∈
ℝ+) |
| 244 | | rphalflt 13064 |
. . . . . . . . . . . . . 14
⊢ ((𝑀↑2) ∈
ℝ+ → ((𝑀↑2) / 2) < (𝑀↑2)) |
| 245 | 243, 244 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑀↑2) / 2) < (𝑀↑2)) |
| 246 | 160, 221,
220, 241, 245 | lelttrd 11419 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀↑2)) |
| 247 | 8 | zcnd 12723 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 248 | 247 | sqvald 14183 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀)) |
| 249 | 246, 248 | breqtrd 5169 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)) |
| 250 | | ltdivmul 12143 |
. . . . . . . . . . . 12
⊢ ((((𝐸↑2) + (𝐹↑2)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 <
𝑀)) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀))) |
| 251 | 160, 161,
161, 198, 250 | syl112anc 1376 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀))) |
| 252 | 249, 251 | mpbird 257 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀) |
| 253 | | zltlem1 12670 |
. . . . . . . . . . 11
⊢
(((((𝐸↑2) +
(𝐹↑2)) / 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ) →
((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))) |
| 254 | 157, 8, 253 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))) |
| 255 | 252, 254 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)) |
| 256 | 255 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)) |
| 257 | 204, 206,
210, 217, 256 | letrd 11418 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (𝑀 − 1)) |
| 258 | 208 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℤ) |
| 259 | | fznn 13632 |
. . . . . . . 8
⊢ ((𝑀 − 1) ∈ ℤ
→ (𝑝 ∈
(1...(𝑀 − 1)) ↔
(𝑝 ∈ ℕ ∧
𝑝 ≤ (𝑀 − 1)))) |
| 260 | 258, 259 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ↔ (𝑝 ∈ ℕ ∧ 𝑝 ≤ (𝑀 − 1)))) |
| 261 | 203, 257,
260 | mpbir2and 713 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ (1...(𝑀 − 1))) |
| 262 | 195 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌) |
| 263 | 261, 262 | jca 511 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)) |
| 264 | 46 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) |
| 265 | 151 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) |
| 266 | | dvdsmul2 16316 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀))) |
| 267 | 8, 157, 266 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀))) |
| 268 | 231, 247,
107 | divcan2d 12045 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) = ((𝐸↑2) + (𝐹↑2))) |
| 269 | 267, 268 | breqtrd 5169 |
. . . . . . 7
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2))) |
| 270 | 269 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2))) |
| 271 | 213, 205,
265, 211, 270 | dvdstrd 16332 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ ((𝐸↑2) + (𝐹↑2))) |
| 272 | | breq1 5146 |
. . . . . . 7
⊢ (𝑏 = 𝑝 → (𝑏 ∥ 𝑎 ↔ 𝑝 ∥ 𝑎)) |
| 273 | | eleq1w 2824 |
. . . . . . 7
⊢ (𝑏 = 𝑝 → (𝑏 ∈ 𝑆 ↔ 𝑝 ∈ 𝑆)) |
| 274 | 272, 273 | imbi12d 344 |
. . . . . 6
⊢ (𝑏 = 𝑝 → ((𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ (𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆))) |
| 275 | | breq2 5147 |
. . . . . . 7
⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → (𝑝 ∥ 𝑎 ↔ 𝑝 ∥ ((𝐸↑2) + (𝐹↑2)))) |
| 276 | 275 | imbi1d 341 |
. . . . . 6
⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → ((𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝 ∈ 𝑆))) |
| 277 | 274, 276 | rspc2v 3633 |
. . . . 5
⊢ ((𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌) → (∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) → (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝 ∈ 𝑆))) |
| 278 | 263, 264,
271, 277 | syl3c 66 |
. . . 4
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ 𝑆) |
| 279 | 278 | expr 456 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ∈ 𝑆)) |
| 280 | 279 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ∈ 𝑆)) |
| 281 | | inss1 4237 |
. . . . 5
⊢ (𝑆 ∩ ℕ) ⊆ 𝑆 |
| 282 | 162, 281 | sstri 3993 |
. . . 4
⊢ 𝑌 ⊆ 𝑆 |
| 283 | 282, 195 | sselid 3981 |
. . 3
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑆) |
| 284 | 268, 283 | eqeltrd 2841 |
. 2
⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) ∈ 𝑆) |
| 285 | 1, 5, 201, 280, 284 | 2sqlem6 27467 |
1
⊢ (𝜑 → 𝑀 ∈ 𝑆) |