Step | Hyp | Ref
| Expression |
1 | | 4sqlem11.1 |
. . . . . . 7
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} |
2 | | 4sq.2 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
3 | | 4sq.3 |
. . . . . . 7
⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1)) |
4 | | 4sq.4 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℙ) |
5 | | 4sq.5 |
. . . . . . 7
⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆) |
6 | | 4sq.6 |
. . . . . . 7
⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} |
7 | | 4sq.7 |
. . . . . . 7
⊢ 𝑀 = inf(𝑇, ℝ, < ) |
8 | | 4sq.m |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘2)) |
9 | | 4sq.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℤ) |
10 | | 4sq.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℤ) |
11 | | 4sq.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℤ) |
12 | | 4sq.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℤ) |
13 | | 4sq.e |
. . . . . . 7
⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
14 | | 4sq.f |
. . . . . . 7
⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
15 | | 4sq.g |
. . . . . . 7
⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
16 | | 4sq.h |
. . . . . . 7
⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
17 | | 4sq.r |
. . . . . . 7
⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) |
18 | | 4sq.p |
. . . . . . 7
⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2)))) |
19 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18 | 4sqlem16 12441 |
. . . . . 6
⊢ (𝜑 → (𝑅 ≤ 𝑀 ∧ ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃)))) |
20 | 19 | simpld 112 |
. . . . 5
⊢ (𝜑 → 𝑅 ≤ 𝑀) |
21 | 1, 2, 3, 4, 5, 6, 7 | 4sqlem13m 12438 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑗 𝑗 ∈ 𝑇 ∧ 𝑀 < 𝑃)) |
22 | 21 | simpld 112 |
. . . . . . 7
⊢ (𝜑 → ∃𝑗 𝑗 ∈ 𝑇) |
23 | | 1zzd 9311 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 1 ∈ ℤ) |
24 | | nnuz 9595 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
25 | 24 | rabeqi 2745 |
. . . . . . . . 9
⊢ {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} = {𝑖 ∈ (ℤ≥‘1)
∣ (𝑖 · 𝑃) ∈ 𝑆} |
26 | 6, 25 | eqtri 2210 |
. . . . . . . 8
⊢ 𝑇 = {𝑖 ∈ (ℤ≥‘1)
∣ (𝑖 · 𝑃) ∈ 𝑆} |
27 | 6 | ssrab3 3256 |
. . . . . . . . . . . . . . . 16
⊢ 𝑇 ⊆
ℕ |
28 | | simpr 110 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 𝑗 ∈ 𝑇) |
29 | | elfznn 10086 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ (1...𝑗) → 𝑖 ∈ ℕ) |
30 | 29 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑖 ∈ ℕ) |
31 | | prmnn 12145 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
32 | 4, 31 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑃 ∈ ℕ) |
33 | 32 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → 𝑃 ∈ ℕ) |
34 | 30, 33 | nnmulcld 8999 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈ ℕ) |
35 | 34 | nnnn0d 9260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → (𝑖 · 𝑃) ∈
ℕ0) |
36 | 1 | 4sqlemsdc 12435 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 · 𝑃) ∈ ℕ0 →
DECID (𝑖
· 𝑃) ∈ 𝑆) |
37 | 35, 36 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑗)) → DECID (𝑖 · 𝑃) ∈ 𝑆) |
38 | 23, 26, 28, 37 | infssuzcldc 11987 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → inf(𝑇, ℝ, < ) ∈ 𝑇) |
39 | 22, 38 | exlimddv 1910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇) |
40 | 7, 39 | eqeltrid 2276 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ 𝑇) |
41 | 27, 40 | sselid 3168 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℕ) |
42 | 41 | nnred 8963 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℝ) |
43 | 21 | simprd 114 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 < 𝑃) |
44 | 42, 43 | ltned 8102 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ≠ 𝑃) |
45 | 41 | nncnd 8964 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑀 ∈ ℂ) |
46 | 45 | sqvald 10685 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀)) |
47 | 46 | breq1d 4028 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ (𝑀 · 𝑀) ∥ (𝑀 · 𝑃))) |
48 | 41 | nnzd 9405 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℤ) |
49 | | prmz 12146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
50 | 4, 49 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℤ) |
51 | 41 | nnne0d 8995 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ≠ 0) |
52 | | dvdscmulr 11862 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃)) |
53 | 48, 50, 48, 51, 52 | syl112anc 1253 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃)) |
54 | | dvdsprm 12172 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃)) |
55 | 8, 4, 54 | syl2anc 411 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃)) |
56 | 47, 53, 55 | 3bitrd 214 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 = 𝑃)) |
57 | 56 | necon3bbid 2400 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (¬ (𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 ≠ 𝑃)) |
58 | 44, 57 | mpbird 167 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ (𝑀↑2) ∥ (𝑀 · 𝑃)) |
59 | | orc 713 |
. . . . . . . . . . . . 13
⊢ (𝑅 = 0 → (𝑅 = 0 ∨ 𝑅 = 𝑀)) |
60 | 19 | simprd 114 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃))) |
61 | 59, 60 | syl5 32 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑅 = 0 → (𝑀↑2) ∥ (𝑀 · 𝑃))) |
62 | 58, 61 | mtod 664 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑅 = 0) |
63 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18 | 4sqlem14 12439 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈
ℕ0) |
64 | | elnn0 9209 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℕ0
↔ (𝑅 ∈ ℕ
∨ 𝑅 =
0)) |
65 | 63, 64 | sylib 122 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅 ∈ ℕ ∨ 𝑅 = 0)) |
66 | 62, 65 | ecased 1360 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ ℕ) |
67 | | gzreim 12414 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i]) |
68 | 9, 10, 67 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i]) |
69 | | gzcn 12407 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ) |
70 | 68, 69 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ) |
71 | 70 | absvalsq2d 11227 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2))) |
72 | 9 | zred 9406 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐴 ∈ ℝ) |
73 | 10 | zred 9406 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐵 ∈ ℝ) |
74 | 72, 73 | crred 11020 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴) |
75 | 74 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2)) |
76 | 72, 73 | crimd 11021 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵) |
77 | 76 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2)) |
78 | 75, 77 | oveq12d 5915 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2))) |
79 | 71, 78 | eqtrd 2222 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2))) |
80 | | gzreim 12414 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i]) |
81 | 11, 12, 80 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i]) |
82 | | gzcn 12407 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ) |
83 | 81, 82 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ) |
84 | 83 | absvalsq2d 11227 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2))) |
85 | 11 | zred 9406 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐶 ∈ ℝ) |
86 | 12 | zred 9406 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐷 ∈ ℝ) |
87 | 85, 86 | crred 11020 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶) |
88 | 87 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2)) |
89 | 85, 86 | crimd 11021 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷) |
90 | 89 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2)) |
91 | 88, 90 | oveq12d 5915 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2))) |
92 | 84, 91 | eqtrd 2222 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = ((𝐶↑2) + (𝐷↑2))) |
93 | 79, 92 | oveq12d 5915 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2)))) |
94 | 18, 93 | eqtr4d 2225 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 · 𝑃) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2))) |
95 | 94 | oveq1d 5912 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀)) |
96 | 32 | nncnd 8964 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ ℂ) |
97 | 41 | nnap0d 8996 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 # 0) |
98 | 96, 45, 97 | divcanap3d 8783 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = 𝑃) |
99 | 95, 98 | eqtr3d 2224 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) = 𝑃) |
100 | 9, 41, 13 | 4sqlem5 12417 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ)) |
101 | 100 | simpld 112 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐸 ∈ ℤ) |
102 | 10, 41, 14 | 4sqlem5 12417 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ)) |
103 | 102 | simpld 112 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹 ∈ ℤ) |
104 | | gzreim 12414 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (𝐸 + (i · 𝐹)) ∈ ℤ[i]) |
105 | 101, 103,
104 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℤ[i]) |
106 | | gzcn 12407 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 + (i · 𝐹)) ∈ ℤ[i] → (𝐸 + (i · 𝐹)) ∈ ℂ) |
107 | 105, 106 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℂ) |
108 | 107 | absvalsq2d 11227 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2))) |
109 | 101 | zred 9406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐸 ∈ ℝ) |
110 | 103 | zred 9406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹 ∈ ℝ) |
111 | 109, 110 | crred 11020 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℜ‘(𝐸 + (i · 𝐹))) = 𝐸) |
112 | 111 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((ℜ‘(𝐸 + (i · 𝐹)))↑2) = (𝐸↑2)) |
113 | 109, 110 | crimd 11021 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℑ‘(𝐸 + (i · 𝐹))) = 𝐹) |
114 | 113 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((ℑ‘(𝐸 + (i · 𝐹)))↑2) = (𝐹↑2)) |
115 | 112, 114 | oveq12d 5915 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)) = ((𝐸↑2) + (𝐹↑2))) |
116 | 108, 115 | eqtrd 2222 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = ((𝐸↑2) + (𝐹↑2))) |
117 | 11, 41, 15 | 4sqlem5 12417 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ)) |
118 | 117 | simpld 112 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐺 ∈ ℤ) |
119 | 12, 41, 16 | 4sqlem5 12417 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ)) |
120 | 119 | simpld 112 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐻 ∈ ℤ) |
121 | | gzreim 12414 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ ℤ ∧ 𝐻 ∈ ℤ) → (𝐺 + (i · 𝐻)) ∈ ℤ[i]) |
122 | 118, 120,
121 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℤ[i]) |
123 | | gzcn 12407 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 + (i · 𝐻)) ∈ ℤ[i] → (𝐺 + (i · 𝐻)) ∈ ℂ) |
124 | 122, 123 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℂ) |
125 | 124 | absvalsq2d 11227 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2))) |
126 | 118 | zred 9406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐺 ∈ ℝ) |
127 | 120 | zred 9406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐻 ∈ ℝ) |
128 | 126, 127 | crred 11020 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℜ‘(𝐺 + (i · 𝐻))) = 𝐺) |
129 | 128 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((ℜ‘(𝐺 + (i · 𝐻)))↑2) = (𝐺↑2)) |
130 | 126, 127 | crimd 11021 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℑ‘(𝐺 + (i · 𝐻))) = 𝐻) |
131 | 130 | oveq1d 5912 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((ℑ‘(𝐺 + (i · 𝐻)))↑2) = (𝐻↑2)) |
132 | 129, 131 | oveq12d 5915 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)) = ((𝐺↑2) + (𝐻↑2))) |
133 | 125, 132 | eqtrd 2222 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = ((𝐺↑2) + (𝐻↑2))) |
134 | 116, 133 | oveq12d 5915 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
135 | 134 | oveq1d 5912 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)) |
136 | 135, 17 | eqtr4di 2240 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = 𝑅) |
137 | 99, 136 | oveq12d 5915 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑃 · 𝑅)) |
138 | 66 | nncnd 8964 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ ℂ) |
139 | 96, 138 | mulcomd 8010 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑃 · 𝑅) = (𝑅 · 𝑃)) |
140 | 137, 139 | eqtrd 2222 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑅 · 𝑃)) |
141 | | eqid 2189 |
. . . . . . . . . . . 12
⊢
(((abs‘(𝐴 + (i
· 𝐵)))↑2) +
((abs‘(𝐶 + (i
· 𝐷)))↑2)) =
(((abs‘(𝐴 + (i
· 𝐵)))↑2) +
((abs‘(𝐶 + (i
· 𝐷)))↑2)) |
142 | | eqid 2189 |
. . . . . . . . . . . 12
⊢
(((abs‘(𝐸 + (i
· 𝐹)))↑2) +
((abs‘(𝐺 + (i
· 𝐻)))↑2)) =
(((abs‘(𝐸 + (i
· 𝐹)))↑2) +
((abs‘(𝐺 + (i
· 𝐻)))↑2)) |
143 | 9 | zcnd 9407 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ ℂ) |
144 | | ax-icn 7937 |
. . . . . . . . . . . . . . . . . 18
⊢ i ∈
ℂ |
145 | 10 | zcnd 9407 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈ ℂ) |
146 | | mulcl 7969 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i
∈ ℂ ∧ 𝐵
∈ ℂ) → (i · 𝐵) ∈ ℂ) |
147 | 144, 145,
146 | sylancr 414 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (i · 𝐵) ∈
ℂ) |
148 | 101 | zcnd 9407 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐸 ∈ ℂ) |
149 | 103 | zcnd 9407 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ∈ ℂ) |
150 | | mulcl 7969 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i
∈ ℂ ∧ 𝐹
∈ ℂ) → (i · 𝐹) ∈ ℂ) |
151 | 144, 149,
150 | sylancr 414 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (i · 𝐹) ∈
ℂ) |
152 | 143, 147,
148, 151 | addsub4d 8346 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹)))) |
153 | 144 | a1i 9 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → i ∈
ℂ) |
154 | 153, 145,
149 | subdid 8402 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (i · (𝐵 − 𝐹)) = ((i · 𝐵) − (i · 𝐹))) |
155 | 154 | oveq2d 5913 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹)))) |
156 | 152, 155 | eqtr4d 2225 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹)))) |
157 | 156 | oveq1d 5912 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀)) |
158 | 143, 148 | subcld 8299 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 − 𝐸) ∈ ℂ) |
159 | 145, 149 | subcld 8299 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 − 𝐹) ∈ ℂ) |
160 | | mulcl 7969 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ (𝐵
− 𝐹) ∈ ℂ)
→ (i · (𝐵
− 𝐹)) ∈
ℂ) |
161 | 144, 159,
160 | sylancr 414 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (i · (𝐵 − 𝐹)) ∈ ℂ) |
162 | 158, 161,
45, 97 | divdirapd 8817 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀) = (((𝐴 − 𝐸) / 𝑀) + ((i · (𝐵 − 𝐹)) / 𝑀))) |
163 | 153, 159,
45, 97 | divassapd 8814 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((i · (𝐵 − 𝐹)) / 𝑀) = (i · ((𝐵 − 𝐹) / 𝑀))) |
164 | 163 | oveq2d 5913 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐴 − 𝐸) / 𝑀) + ((i · (𝐵 − 𝐹)) / 𝑀)) = (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀)))) |
165 | 157, 162,
164 | 3eqtrd 2226 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀)))) |
166 | 100 | simprd 114 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 − 𝐸) / 𝑀) ∈ ℤ) |
167 | 102 | simprd 114 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐵 − 𝐹) / 𝑀) ∈ ℤ) |
168 | | gzreim 12414 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 − 𝐸) / 𝑀) ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ) → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i]) |
169 | 166, 167,
168 | syl2anc 411 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i]) |
170 | 165, 169 | eqeltrd 2266 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) ∈ ℤ[i]) |
171 | 11 | zcnd 9407 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐶 ∈ ℂ) |
172 | 12 | zcnd 9407 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐷 ∈ ℂ) |
173 | | mulcl 7969 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i
∈ ℂ ∧ 𝐷
∈ ℂ) → (i · 𝐷) ∈ ℂ) |
174 | 144, 172,
173 | sylancr 414 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (i · 𝐷) ∈
ℂ) |
175 | 118 | zcnd 9407 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 ∈ ℂ) |
176 | 120 | zcnd 9407 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐻 ∈ ℂ) |
177 | | mulcl 7969 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i
∈ ℂ ∧ 𝐻
∈ ℂ) → (i · 𝐻) ∈ ℂ) |
178 | 144, 176,
177 | sylancr 414 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (i · 𝐻) ∈
ℂ) |
179 | 171, 174,
175, 178 | addsub4d 8346 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻)))) |
180 | 153, 172,
176 | subdid 8402 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (i · (𝐷 − 𝐻)) = ((i · 𝐷) − (i · 𝐻))) |
181 | 180 | oveq2d 5913 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻)))) |
182 | 179, 181 | eqtr4d 2225 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻)))) |
183 | 182 | oveq1d 5912 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀)) |
184 | 171, 175 | subcld 8299 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶 − 𝐺) ∈ ℂ) |
185 | 172, 176 | subcld 8299 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐷 − 𝐻) ∈ ℂ) |
186 | | mulcl 7969 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ (𝐷
− 𝐻) ∈ ℂ)
→ (i · (𝐷
− 𝐻)) ∈
ℂ) |
187 | 144, 185,
186 | sylancr 414 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (i · (𝐷 − 𝐻)) ∈ ℂ) |
188 | 184, 187,
45, 97 | divdirapd 8817 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀) = (((𝐶 − 𝐺) / 𝑀) + ((i · (𝐷 − 𝐻)) / 𝑀))) |
189 | 153, 185,
45, 97 | divassapd 8814 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((i · (𝐷 − 𝐻)) / 𝑀) = (i · ((𝐷 − 𝐻) / 𝑀))) |
190 | 189 | oveq2d 5913 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐶 − 𝐺) / 𝑀) + ((i · (𝐷 − 𝐻)) / 𝑀)) = (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀)))) |
191 | 183, 188,
190 | 3eqtrd 2226 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀)))) |
192 | 117 | simprd 114 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐶 − 𝐺) / 𝑀) ∈ ℤ) |
193 | 119 | simprd 114 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐷 − 𝐻) / 𝑀) ∈ ℤ) |
194 | | gzreim 12414 |
. . . . . . . . . . . . . 14
⊢ ((((𝐶 − 𝐺) / 𝑀) ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ) → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i]) |
195 | 192, 193,
194 | syl2anc 411 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i]) |
196 | 191, 195 | eqeltrd 2266 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) ∈ ℤ[i]) |
197 | 32 | nnnn0d 9260 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
198 | 99, 197 | eqeltrd 2266 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) ∈
ℕ0) |
199 | 1, 68, 81, 105, 122, 141, 142, 41, 170, 196, 198 | mul4sqlem 12428 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) ∈ 𝑆) |
200 | 140, 199 | eqeltrrd 2267 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 · 𝑃) ∈ 𝑆) |
201 | | oveq1 5904 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑅 → (𝑖 · 𝑃) = (𝑅 · 𝑃)) |
202 | 201 | eleq1d 2258 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑅 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑅 · 𝑃) ∈ 𝑆)) |
203 | 202, 6 | elrab2 2911 |
. . . . . . . . . 10
⊢ (𝑅 ∈ 𝑇 ↔ (𝑅 ∈ ℕ ∧ (𝑅 · 𝑃) ∈ 𝑆)) |
204 | 66, 200, 203 | sylanbrc 417 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ 𝑇) |
205 | 204 | adantr 276 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → 𝑅 ∈ 𝑇) |
206 | | elfznn 10086 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (1...𝑅) → 𝑖 ∈ ℕ) |
207 | 206 | adantl 277 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑖 ∈ ℕ) |
208 | 32 | ad2antrr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → 𝑃 ∈ ℕ) |
209 | 207, 208 | nnmulcld 8999 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈ ℕ) |
210 | 209 | nnnn0d 9260 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → (𝑖 · 𝑃) ∈
ℕ0) |
211 | 210, 36 | syl 14 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑅)) → DECID (𝑖 · 𝑃) ∈ 𝑆) |
212 | 23, 26, 205, 211 | infssuzledc 11986 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑅) |
213 | 22, 212 | exlimddv 1910 |
. . . . . 6
⊢ (𝜑 → inf(𝑇, ℝ, < ) ≤ 𝑅) |
214 | 7, 213 | eqbrtrid 4053 |
. . . . 5
⊢ (𝜑 → 𝑀 ≤ 𝑅) |
215 | 66 | nnred 8963 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ ℝ) |
216 | 215, 42 | letri3d 8104 |
. . . . 5
⊢ (𝜑 → (𝑅 = 𝑀 ↔ (𝑅 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅))) |
217 | 20, 214, 216 | mpbir2and 946 |
. . . 4
⊢ (𝜑 → 𝑅 = 𝑀) |
218 | 217 | olcd 735 |
. . 3
⊢ (𝜑 → (𝑅 = 0 ∨ 𝑅 = 𝑀)) |
219 | 218, 60 | mpd 13 |
. 2
⊢ (𝜑 → (𝑀↑2) ∥ (𝑀 · 𝑃)) |
220 | 219, 58 | pm2.65i 640 |
1
⊢ ¬
𝜑 |