Step | Hyp | Ref
| Expression |
1 | | 2sq.1 |
. 2
⊢ 𝑆 = ran (𝑤 ∈ ℤ[i] ↦ ((abs‘𝑤)↑2)) |
2 | | 2sqlem8.m |
. . . 4
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘2)) |
3 | | eluz2b3 12407 |
. . . 4
⊢ (𝑀 ∈
(ℤ≥‘2) ↔ (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1)) |
4 | 2, 3 | sylib 221 |
. . 3
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑀 ≠ 1)) |
5 | 4 | simpld 498 |
. 2
⊢ (𝜑 → 𝑀 ∈ ℕ) |
6 | | 2sqlem9.7 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∥ 𝑁) |
7 | | eluzelz 12337 |
. . . . . . . . 9
⊢ (𝑀 ∈
(ℤ≥‘2) → 𝑀 ∈ ℤ) |
8 | 2, 7 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
9 | | 2sqlem8.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
10 | 9 | nnzd 12170 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) |
11 | | 2sqlem8.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℤ) |
12 | | 2sqlem8.c |
. . . . . . . . . . . 12
⊢ 𝐶 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
13 | 11, 5, 12 | 4sqlem5 16381 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 ∈ ℤ ∧ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ)) |
14 | 13 | simpld 498 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℤ) |
15 | | zsqcl 13589 |
. . . . . . . . . 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 16381 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷 ∈ ℤ ∧ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ)) |
20 | 19 | simpld 498 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℤ) |
21 | | zsqcl 13589 |
. . . . . . . . . 10
⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈
ℤ) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷↑2) ∈ ℤ) |
23 | 16, 22 | zaddcld 12175 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) |
24 | | zsqcl 13589 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈
ℤ) |
25 | 11, 24 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴↑2) ∈ ℤ) |
26 | 25, 16 | zsubcld 12176 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴↑2) − (𝐶↑2)) ∈ ℤ) |
27 | | zsqcl 13589 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈
ℤ) |
28 | 17, 27 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵↑2) ∈ ℤ) |
29 | 28, 22 | zsubcld 12176 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵↑2) − (𝐷↑2)) ∈ ℤ) |
30 | 11, 5, 12 | 4sqlem8 16384 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐶↑2))) |
31 | 17, 5, 18 | 4sqlem8 16384 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∥ ((𝐵↑2) − (𝐷↑2))) |
32 | 8, 26, 29, 30, 31 | dvds2addd 15740 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∥ (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2)))) |
33 | | 2sqlem8.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 = ((𝐴↑2) + (𝐵↑2))) |
34 | 33 | oveq1d 7188 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2)))) |
35 | 25 | zcnd 12172 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) |
36 | 28 | zcnd 12172 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵↑2) ∈ ℂ) |
37 | 16 | zcnd 12172 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶↑2) ∈ ℂ) |
38 | 22 | zcnd 12172 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷↑2) ∈ ℂ) |
39 | 35, 36, 37, 38 | addsub4d 11125 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2)))) |
40 | 34, 39 | eqtrd 2774 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − ((𝐶↑2) + (𝐷↑2))) = (((𝐴↑2) − (𝐶↑2)) + ((𝐵↑2) − (𝐷↑2)))) |
41 | 32, 40 | breqtrrd 5059 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2)))) |
42 | | dvdssub2 15749 |
. . . . . . . 8
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐶↑2) + (𝐷↑2)) ∈ ℤ) ∧ 𝑀 ∥ (𝑁 − ((𝐶↑2) + (𝐷↑2)))) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ((𝐶↑2) + (𝐷↑2)))) |
43 | 8, 10, 23, 41, 42 | syl31anc 1374 |
. . . . . . 7
⊢ (𝜑 → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ ((𝐶↑2) + (𝐷↑2)))) |
44 | 6, 43 | mpbid 235 |
. . . . . 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 26164 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℕ) |
49 | 48 | nnzd 12170 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℤ) |
50 | | zsqcl2 13597 |
. . . . . . . . . 10
⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈
ℕ0) |
51 | 49, 50 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈
ℕ0) |
52 | 51 | nn0cnd 12041 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℂ) |
53 | | 2sqlem8.e |
. . . . . . . . . . 11
⊢ 𝐸 = (𝐶 / (𝐶 gcd 𝐷)) |
54 | | gcddvds 15949 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷)) |
55 | 14, 20, 54 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ∧ (𝐶 gcd 𝐷) ∥ 𝐷)) |
56 | 55 | simpld 498 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐶) |
57 | 48 | nnne0d 11769 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶 gcd 𝐷) ≠ 0) |
58 | | dvdsval2 15705 |
. . . . . . . . . . . . 13
⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐶 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ)) |
59 | 49, 57, 14, 58 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐶 ↔ (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ)) |
60 | 56, 59 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 / (𝐶 gcd 𝐷)) ∈ ℤ) |
61 | 53, 60 | eqeltrid 2838 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℤ) |
62 | | zsqcl2 13597 |
. . . . . . . . . 10
⊢ (𝐸 ∈ ℤ → (𝐸↑2) ∈
ℕ0) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸↑2) ∈
ℕ0) |
64 | 63 | nn0cnd 12041 |
. . . . . . . 8
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) |
65 | | 2sqlem8.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝐷 / (𝐶 gcd 𝐷)) |
66 | 55 | simprd 499 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 gcd 𝐷) ∥ 𝐷) |
67 | | dvdsval2 15705 |
. . . . . . . . . . . . 13
⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ (𝐶 gcd 𝐷) ≠ 0 ∧ 𝐷 ∈ ℤ) → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ)) |
68 | 49, 57, 20, 67 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 gcd 𝐷) ∥ 𝐷 ↔ (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ)) |
69 | 66, 68 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷 / (𝐶 gcd 𝐷)) ∈ ℤ) |
70 | 65, 69 | eqeltrid 2838 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ℤ) |
71 | | zsqcl2 13597 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ℤ → (𝐹↑2) ∈
ℕ0) |
72 | 70, 71 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹↑2) ∈
ℕ0) |
73 | 72 | nn0cnd 12041 |
. . . . . . . 8
⊢ (𝜑 → (𝐹↑2) ∈ ℂ) |
74 | 52, 64, 73 | adddid 10746 |
. . . . . . 7
⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)))) |
75 | 49 | zcnd 12172 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 gcd 𝐷) ∈ ℂ) |
76 | 61 | zcnd 12172 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℂ) |
77 | 75, 76 | sqmuld 13617 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐸↑2))) |
78 | 53 | oveq2i 7184 |
. . . . . . . . . . 11
⊢ ((𝐶 gcd 𝐷) · 𝐸) = ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷))) |
79 | 14 | zcnd 12172 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℂ) |
80 | 79, 75, 57 | divcan2d 11499 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐶 / (𝐶 gcd 𝐷))) = 𝐶) |
81 | 78, 80 | syl5eq 2786 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐸) = 𝐶) |
82 | 81 | oveq1d 7188 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸)↑2) = (𝐶↑2)) |
83 | 77, 82 | eqtr3d 2776 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) = (𝐶↑2)) |
84 | 70 | zcnd 12172 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ℂ) |
85 | 75, 84 | sqmuld 13617 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))) |
86 | 65 | oveq2i 7184 |
. . . . . . . . . . 11
⊢ ((𝐶 gcd 𝐷) · 𝐹) = ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷))) |
87 | 20 | zcnd 12172 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈ ℂ) |
88 | 87, 75, 57 | divcan2d 11499 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐷 / (𝐶 gcd 𝐷))) = 𝐷) |
89 | 86, 88 | syl5eq 2786 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 gcd 𝐷) · 𝐹) = 𝐷) |
90 | 89 | oveq1d 7188 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐹)↑2) = (𝐷↑2)) |
91 | 85, 90 | eqtr3d 2776 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · (𝐹↑2)) = (𝐷↑2)) |
92 | 83, 91 | oveq12d 7191 |
. . . . . . 7
⊢ (𝜑 → ((((𝐶 gcd 𝐷)↑2) · (𝐸↑2)) + (((𝐶 gcd 𝐷)↑2) · (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2))) |
93 | 74, 92 | eqtrd 2774 |
. . . . . 6
⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) = ((𝐶↑2) + (𝐷↑2))) |
94 | 44, 93 | breqtrrd 5059 |
. . . . 5
⊢ (𝜑 → 𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2)))) |
95 | | zsqcl 13589 |
. . . . . . . 8
⊢ ((𝐶 gcd 𝐷) ∈ ℤ → ((𝐶 gcd 𝐷)↑2) ∈ ℤ) |
96 | 49, 95 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℤ) |
97 | 8, 96 | gcdcomd 15960 |
. . . . . 6
⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = (((𝐶 gcd 𝐷)↑2) gcd 𝑀)) |
98 | 49, 8 | gcdcld 15954 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈
ℕ0) |
99 | 98 | nn0zd 12169 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ) |
100 | | gcddvds 15949 |
. . . . . . . . . . . . . 14
⊢ (((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀)) |
101 | 49, 8, 100 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀)) |
102 | 101 | simpld 498 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐶 gcd 𝐷)) |
103 | 99, 49, 14, 102, 56 | dvdstrd 15743 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶) |
104 | 11, 14 | zsubcld 12176 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℤ) |
105 | 101 | simprd 499 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝑀) |
106 | 13 | simprd 499 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ) |
107 | 5 | nnne0d 11769 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ≠ 0) |
108 | | dvdsval2 15705 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐴 − 𝐶) ∈ ℤ) → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ)) |
109 | 8, 107, 104, 108 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 ∥ (𝐴 − 𝐶) ↔ ((𝐴 − 𝐶) / 𝑀) ∈ ℤ)) |
110 | 106, 109 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∥ (𝐴 − 𝐶)) |
111 | 99, 8, 104, 105, 110 | dvdstrd 15743 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶)) |
112 | | dvdssub2 15749 |
. . . . . . . . . . . 12
⊢
(((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐴 − 𝐶)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶)) |
113 | 99, 11, 14, 111, 112 | syl31anc 1374 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐶)) |
114 | 103, 113 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴) |
115 | 99, 49, 20, 102, 66 | dvdstrd 15743 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷) |
116 | 17, 20 | zsubcld 12176 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 − 𝐷) ∈ ℤ) |
117 | 19 | simprd 499 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ) |
118 | | dvdsval2 15705 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ (𝐵 − 𝐷) ∈ ℤ) → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ)) |
119 | 8, 107, 116, 118 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 ∥ (𝐵 − 𝐷) ↔ ((𝐵 − 𝐷) / 𝑀) ∈ ℤ)) |
120 | 117, 119 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∥ (𝐵 − 𝐷)) |
121 | 99, 8, 116, 105, 120 | dvdstrd 15743 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷)) |
122 | | dvdssub2 15749 |
. . . . . . . . . . . 12
⊢
(((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ (𝐵 − 𝐷)) → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷)) |
123 | 99, 17, 20, 121, 122 | syl31anc 1374 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵 ↔ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐷)) |
124 | 115, 123 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) |
125 | | ax-1ne0 10687 |
. . . . . . . . . . . . . . 15
⊢ 1 ≠
0 |
126 | 125 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ≠ 0) |
127 | 47, 126 | eqnetrd 3002 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 gcd 𝐵) ≠ 0) |
128 | 127 | neneqd 2940 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ (𝐴 gcd 𝐵) = 0) |
129 | | gcdeq0 15963 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0))) |
130 | 11, 17, 129 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 gcd 𝐵) = 0 ↔ (𝐴 = 0 ∧ 𝐵 = 0))) |
131 | 128, 130 | mtbid 327 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
132 | | dvdslegcd 15950 |
. . . . . . . . . . 11
⊢
(((((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵))) |
133 | 99, 11, 17, 131, 132 | syl31anc 1374 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐴 ∧ ((𝐶 gcd 𝐷) gcd 𝑀) ∥ 𝐵) → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵))) |
134 | 114, 124,
133 | mp2and 699 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ (𝐴 gcd 𝐵)) |
135 | 134, 47 | breqtrd 5057 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ≤ 1) |
136 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0) → 𝑀 = 0) |
137 | 136 | necon3ai 2960 |
. . . . . . . . . . 11
⊢ (𝑀 ≠ 0 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) |
138 | 107, 137 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) |
139 | | gcdn0cl 15948 |
. . . . . . . . . 10
⊢ ((((𝐶 gcd 𝐷) ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ ¬ ((𝐶 gcd 𝐷) = 0 ∧ 𝑀 = 0)) → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ) |
140 | 49, 8, 138, 139 | syl21anc 837 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) ∈ ℕ) |
141 | | nnle1eq1 11749 |
. . . . . . . . 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 235 |
. . . . . . 7
⊢ (𝜑 → ((𝐶 gcd 𝐷) gcd 𝑀) = 1) |
144 | | 2nn 11792 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
145 | 144 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℕ) |
146 | | rplpwr 16006 |
. . . . . . . 8
⊢ (((𝐶 gcd 𝐷) ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 2 ∈ ℕ)
→ (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1)) |
147 | 48, 5, 145, 146 | syl3anc 1372 |
. . . . . . 7
⊢ (𝜑 → (((𝐶 gcd 𝐷) gcd 𝑀) = 1 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1)) |
148 | 143, 147 | mpd 15 |
. . . . . 6
⊢ (𝜑 → (((𝐶 gcd 𝐷)↑2) gcd 𝑀) = 1) |
149 | 97, 148 | eqtrd 2774 |
. . . . 5
⊢ (𝜑 → (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) |
150 | 63, 72 | nn0addcld 12043 |
. . . . . . 7
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈
ℕ0) |
151 | 150 | nn0zd 12169 |
. . . . . 6
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) |
152 | | coprmdvds 16097 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ ((𝐶 gcd 𝐷)↑2) ∈ ℤ ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2)))) |
153 | 8, 96, 151, 152 | syl3anc 1372 |
. . . . 5
⊢ (𝜑 → ((𝑀 ∥ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2))) ∧ (𝑀 gcd ((𝐶 gcd 𝐷)↑2)) = 1) → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2)))) |
154 | 94, 149, 153 | mp2and 699 |
. . . 4
⊢ (𝜑 → 𝑀 ∥ ((𝐸↑2) + (𝐹↑2))) |
155 | | dvdsval2 15705 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)) |
156 | 8, 107, 151, 155 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → (𝑀 ∥ ((𝐸↑2) + (𝐹↑2)) ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ)) |
157 | 154, 156 | mpbid 235 |
. . 3
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) |
158 | 63 | nn0red 12040 |
. . . . 5
⊢ (𝜑 → (𝐸↑2) ∈ ℝ) |
159 | 72 | nn0red 12040 |
. . . . 5
⊢ (𝜑 → (𝐹↑2) ∈ ℝ) |
160 | 158, 159 | readdcld 10751 |
. . . 4
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℝ) |
161 | 5 | nnred 11734 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℝ) |
162 | 1, 45 | 2sqlem7 26163 |
. . . . . . 7
⊢ 𝑌 ⊆ (𝑆 ∩ ℕ) |
163 | | inss2 4121 |
. . . . . . 7
⊢ (𝑆 ∩ ℕ) ⊆
ℕ |
164 | 162, 163 | sstri 3887 |
. . . . . 6
⊢ 𝑌 ⊆
ℕ |
165 | 61, 70 | gcdcld 15954 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 gcd 𝐹) ∈
ℕ0) |
166 | 165 | nn0cnd 12041 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 gcd 𝐹) ∈ ℂ) |
167 | | 1cnd 10717 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
168 | 75 | mulid1d 10739 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 gcd 𝐷) · 1) = (𝐶 gcd 𝐷)) |
169 | 81, 89 | oveq12d 7191 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = (𝐶 gcd 𝐷)) |
170 | 14, 20 | gcdcld 15954 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 gcd 𝐷) ∈
ℕ0) |
171 | | mulgcd 15995 |
. . . . . . . . . . 11
⊢ (((𝐶 gcd 𝐷) ∈ ℕ0 ∧ 𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹))) |
172 | 170, 61, 70, 171 | syl3anc 1372 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐶 gcd 𝐷) · 𝐸) gcd ((𝐶 gcd 𝐷) · 𝐹)) = ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹))) |
173 | 168, 169,
172 | 3eqtr2rd 2781 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 gcd 𝐷) · (𝐸 gcd 𝐹)) = ((𝐶 gcd 𝐷) · 1)) |
174 | 166, 167,
75, 57, 173 | mulcanad 11356 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 gcd 𝐹) = 1) |
175 | | eqidd 2740 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2))) |
176 | | oveq1 7180 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐸 → (𝑥 gcd 𝑦) = (𝐸 gcd 𝑦)) |
177 | 176 | eqeq1d 2741 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐸 → ((𝑥 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝑦) = 1)) |
178 | | oveq1 7180 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐸 → (𝑥↑2) = (𝐸↑2)) |
179 | 178 | oveq1d 7188 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐸 → ((𝑥↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝑦↑2))) |
180 | 179 | eqeq2d 2750 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐸 → (((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)))) |
181 | 177, 180 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑥 = 𝐸 → (((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))))) |
182 | | oveq2 7181 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐹 → (𝐸 gcd 𝑦) = (𝐸 gcd 𝐹)) |
183 | 182 | eqeq1d 2741 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐹 → ((𝐸 gcd 𝑦) = 1 ↔ (𝐸 gcd 𝐹) = 1)) |
184 | | oveq1 7180 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐹 → (𝑦↑2) = (𝐹↑2)) |
185 | 184 | oveq2d 7189 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐹 → ((𝐸↑2) + (𝑦↑2)) = ((𝐸↑2) + (𝐹↑2))) |
186 | 185 | eqeq2d 2750 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐹 → (((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))) |
187 | 183, 186 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑦 = 𝐹 → (((𝐸 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝑦↑2))) ↔ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2))))) |
188 | 181, 187 | rspc2ev 3539 |
. . . . . . . 8
⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ∧ ((𝐸 gcd 𝐹) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝐸↑2) + (𝐹↑2)))) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))) |
189 | 61, 70, 174, 175, 188 | syl112anc 1375 |
. . . . . . 7
⊢ (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))) |
190 | | ovex 7206 |
. . . . . . . 8
⊢ ((𝐸↑2) + (𝐹↑2)) ∈ V |
191 | | eqeq1 2743 |
. . . . . . . . . 10
⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (𝑧 = ((𝑥↑2) + (𝑦↑2)) ↔ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))) |
192 | 191 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))) |
193 | 192 | 2rexbidv 3211 |
. . . . . . . 8
⊢ (𝑧 = ((𝐸↑2) + (𝐹↑2)) → (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ 𝑧 = ((𝑥↑2) + (𝑦↑2))) ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2))))) |
194 | 190, 193,
45 | elab2 3578 |
. . . . . . 7
⊢ (((𝐸↑2) + (𝐹↑2)) ∈ 𝑌 ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ((𝑥 gcd 𝑦) = 1 ∧ ((𝐸↑2) + (𝐹↑2)) = ((𝑥↑2) + (𝑦↑2)))) |
195 | 189, 194 | sylibr 237 |
. . . . . 6
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌) |
196 | 164, 195 | sseldi 3876 |
. . . . 5
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℕ) |
197 | 196 | nngt0d 11768 |
. . . 4
⊢ (𝜑 → 0 < ((𝐸↑2) + (𝐹↑2))) |
198 | 5 | nngt0d 11768 |
. . . 4
⊢ (𝜑 → 0 < 𝑀) |
199 | 160, 161,
197, 198 | divgt0d 11656 |
. . 3
⊢ (𝜑 → 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀)) |
200 | | elnnz 12075 |
. . 3
⊢ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ ↔ ((((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ ∧ 0 < (((𝐸↑2) + (𝐹↑2)) / 𝑀))) |
201 | 157, 199,
200 | sylanbrc 586 |
. 2
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ) |
202 | | prmnn 16118 |
. . . . . . . 8
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
203 | 202 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℕ) |
204 | 203 | nnred 11734 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℝ) |
205 | 157 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) |
206 | 205 | zred 12171 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℝ) |
207 | | peano2zm 12109 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
208 | 8, 207 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
209 | 208 | zred 12171 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 − 1) ∈ ℝ) |
210 | 209 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℝ) |
211 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀)) |
212 | | prmz 16119 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
213 | 212 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ ℤ) |
214 | 201 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ) |
215 | | dvdsle 15758 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℕ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) |
216 | 213, 214,
215 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) |
217 | 211, 216 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (((𝐸↑2) + (𝐹↑2)) / 𝑀)) |
218 | | zsqcl 13589 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℤ → (𝑀↑2) ∈
ℤ) |
219 | 8, 218 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀↑2) ∈ ℤ) |
220 | 219 | zred 12171 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀↑2) ∈ ℝ) |
221 | 220 | rehalfcld 11966 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑀↑2) / 2) ∈
ℝ) |
222 | 16 | zred 12171 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶↑2) ∈ ℝ) |
223 | 22 | zred 12171 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐷↑2) ∈ ℝ) |
224 | 222, 223 | readdcld 10751 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ∈ ℝ) |
225 | | 1red 10723 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℝ) |
226 | 48 | nnsqcld 13700 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℕ) |
227 | 226 | nnred 11734 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐶 gcd 𝐷)↑2) ∈ ℝ) |
228 | 150 | nn0ge0d 12042 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ ((𝐸↑2) + (𝐹↑2))) |
229 | 226 | nnge1d 11767 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ≤ ((𝐶 gcd 𝐷)↑2)) |
230 | 225, 227,
160, 228, 229 | lemul1ad 11660 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) ≤ (((𝐶 gcd 𝐷)↑2) · ((𝐸↑2) + (𝐹↑2)))) |
231 | 150 | nn0cnd 12041 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ ℂ) |
232 | 231 | mulid2d 10740 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 · ((𝐸↑2) + (𝐹↑2))) = ((𝐸↑2) + (𝐹↑2))) |
233 | 230, 232,
93 | 3brtr3d 5062 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝐶↑2) + (𝐷↑2))) |
234 | 221 | rehalfcld 11966 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑀↑2) / 2) / 2) ∈
ℝ) |
235 | 11, 5, 12 | 4sqlem7 16383 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐶↑2) ≤ (((𝑀↑2) / 2) / 2)) |
236 | 17, 5, 18 | 4sqlem7 16383 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐷↑2) ≤ (((𝑀↑2) / 2) / 2)) |
237 | 222, 223,
234, 234, 235, 236 | le2addd 11340 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2))) |
238 | 221 | recnd 10750 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀↑2) / 2) ∈
ℂ) |
239 | 238 | 2halvesd 11965 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((𝑀↑2) / 2) / 2) + (((𝑀↑2) / 2) / 2)) = ((𝑀↑2) / 2)) |
240 | 237, 239 | breqtrd 5057 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) ≤ ((𝑀↑2) / 2)) |
241 | 160, 224,
221, 233, 240 | letrd 10878 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ≤ ((𝑀↑2) / 2)) |
242 | 5 | nnsqcld 13700 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀↑2) ∈ ℕ) |
243 | 242 | nnrpd 12515 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀↑2) ∈
ℝ+) |
244 | | rphalflt 12504 |
. . . . . . . . . . . . . 14
⊢ ((𝑀↑2) ∈
ℝ+ → ((𝑀↑2) / 2) < (𝑀↑2)) |
245 | 243, 244 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑀↑2) / 2) < (𝑀↑2)) |
246 | 160, 221,
220, 241, 245 | lelttrd 10879 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀↑2)) |
247 | 8 | zcnd 12172 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℂ) |
248 | 247 | sqvald 13602 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀)) |
249 | 246, 248 | breqtrd 5057 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀)) |
250 | | ltdivmul 11596 |
. . . . . . . . . . . 12
⊢ ((((𝐸↑2) + (𝐹↑2)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 <
𝑀)) → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀))) |
251 | 160, 161,
161, 198, 250 | syl112anc 1375 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ ((𝐸↑2) + (𝐹↑2)) < (𝑀 · 𝑀))) |
252 | 249, 251 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀) |
253 | | zltlem1 12119 |
. . . . . . . . . . 11
⊢
(((((𝐸↑2) +
(𝐹↑2)) / 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ) →
((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))) |
254 | 157, 8, 253 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐸↑2) + (𝐹↑2)) / 𝑀) < 𝑀 ↔ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1))) |
255 | 252, 254 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)) |
256 | 255 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ≤ (𝑀 − 1)) |
257 | 204, 206,
210, 217, 256 | letrd 10878 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ≤ (𝑀 − 1)) |
258 | 208 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑀 − 1) ∈ ℤ) |
259 | | fznn 13069 |
. . . . . . . 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 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌) |
263 | 261, 262 | jca 515 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌)) |
264 | 46 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆)) |
265 | 151 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → ((𝐸↑2) + (𝐹↑2)) ∈ ℤ) |
266 | | dvdsmul2 15727 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∈ ℤ) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀))) |
267 | 8, 157, 266 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀))) |
268 | 231, 247,
107 | divcan2d 11499 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) = ((𝐸↑2) + (𝐹↑2))) |
269 | 267, 268 | breqtrd 5057 |
. . . . . . 7
⊢ (𝜑 → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2))) |
270 | 269 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → (((𝐸↑2) + (𝐹↑2)) / 𝑀) ∥ ((𝐸↑2) + (𝐹↑2))) |
271 | 213, 205,
265, 211, 270 | dvdstrd 15743 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∥ ((𝐸↑2) + (𝐹↑2))) |
272 | | breq1 5034 |
. . . . . . 7
⊢ (𝑏 = 𝑝 → (𝑏 ∥ 𝑎 ↔ 𝑝 ∥ 𝑎)) |
273 | | eleq1w 2816 |
. . . . . . 7
⊢ (𝑏 = 𝑝 → (𝑏 ∈ 𝑆 ↔ 𝑝 ∈ 𝑆)) |
274 | 272, 273 | imbi12d 348 |
. . . . . 6
⊢ (𝑏 = 𝑝 → ((𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) ↔ (𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆))) |
275 | | breq2 5035 |
. . . . . . 7
⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → (𝑝 ∥ 𝑎 ↔ 𝑝 ∥ ((𝐸↑2) + (𝐹↑2)))) |
276 | 275 | imbi1d 345 |
. . . . . 6
⊢ (𝑎 = ((𝐸↑2) + (𝐹↑2)) → ((𝑝 ∥ 𝑎 → 𝑝 ∈ 𝑆) ↔ (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝 ∈ 𝑆))) |
277 | 274, 276 | rspc2v 3537 |
. . . . 5
⊢ ((𝑝 ∈ (1...(𝑀 − 1)) ∧ ((𝐸↑2) + (𝐹↑2)) ∈ 𝑌) → (∀𝑏 ∈ (1...(𝑀 − 1))∀𝑎 ∈ 𝑌 (𝑏 ∥ 𝑎 → 𝑏 ∈ 𝑆) → (𝑝 ∥ ((𝐸↑2) + (𝐹↑2)) → 𝑝 ∈ 𝑆))) |
278 | 263, 264,
271, 277 | syl3c 66 |
. . . 4
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀))) → 𝑝 ∈ 𝑆) |
279 | 278 | expr 460 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ∈ 𝑆)) |
280 | 279 | ralrimiva 3097 |
. 2
⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (((𝐸↑2) + (𝐹↑2)) / 𝑀) → 𝑝 ∈ 𝑆)) |
281 | | inss1 4120 |
. . . . 5
⊢ (𝑆 ∩ ℕ) ⊆ 𝑆 |
282 | 162, 281 | sstri 3887 |
. . . 4
⊢ 𝑌 ⊆ 𝑆 |
283 | 282, 195 | sseldi 3876 |
. . 3
⊢ (𝜑 → ((𝐸↑2) + (𝐹↑2)) ∈ 𝑆) |
284 | 268, 283 | eqeltrd 2834 |
. 2
⊢ (𝜑 → (𝑀 · (((𝐸↑2) + (𝐹↑2)) / 𝑀)) ∈ 𝑆) |
285 | 1, 5, 201, 280, 284 | 2sqlem6 26162 |
1
⊢ (𝜑 → 𝑀 ∈ 𝑆) |