Proof of Theorem 4sqlem17
Step | Hyp | Ref
| Expression |
1 | | 4sq.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 15664 |
. . . . . 6
⊢ (𝜑 → (𝑅 ≤ 𝑀 ∧ ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃)))) |
20 | 19 | simpld 475 |
. . . . 5
⊢ (𝜑 → 𝑅 ≤ 𝑀) |
21 | | ssrab2 3687 |
. . . . . . . . 9
⊢ {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} ⊆ ℕ |
22 | 6, 21 | eqsstri 3635 |
. . . . . . . 8
⊢ 𝑇 ⊆
ℕ |
23 | | nnuz 11723 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
24 | 22, 23 | sseqtri 3637 |
. . . . . . 7
⊢ 𝑇 ⊆
(ℤ≥‘1) |
25 | 1, 2, 3, 4, 5, 6, 7 | 4sqlem13 15661 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃)) |
26 | 25 | simpld 475 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 ≠ ∅) |
27 | | infssuzcl 11772 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ⊆
(ℤ≥‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇) |
28 | 24, 26, 27 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇) |
29 | 7, 28 | syl5eqel 2705 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ 𝑇) |
30 | 22, 29 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℕ) |
31 | 30 | nnred 11035 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
32 | 25 | simprd 479 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 < 𝑃) |
33 | 31, 32 | ltned 10173 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≠ 𝑃) |
34 | 30 | nncnd 11036 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℂ) |
35 | 34 | sqvald 13005 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀↑2) = (𝑀 · 𝑀)) |
36 | 35 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ (𝑀 · 𝑀) ∥ (𝑀 · 𝑃))) |
37 | 30 | nnzd 11481 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℤ) |
38 | | prmz 15389 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
39 | 4, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℤ) |
40 | 30 | nnne0d 11065 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ≠ 0) |
41 | | dvdscmulr 15010 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃)) |
42 | 37, 39, 37, 40, 41 | syl112anc 1330 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀 ∥ 𝑃)) |
43 | | dvdsprm 15415 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈
(ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃)) |
44 | 8, 4, 43 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃)) |
45 | 36, 42, 44 | 3bitrd 294 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 = 𝑃)) |
46 | 45 | necon3bbid 2831 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ (𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 ≠ 𝑃)) |
47 | 33, 46 | mpbird 247 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (𝑀↑2) ∥ (𝑀 · 𝑃)) |
48 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18 | 4sqlem14 15662 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈
ℕ0) |
49 | | elnn0 11294 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℕ0
↔ (𝑅 ∈ ℕ
∨ 𝑅 =
0)) |
50 | 48, 49 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅 ∈ ℕ ∨ 𝑅 = 0)) |
51 | 50 | ord 392 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ 𝑅 ∈ ℕ → 𝑅 = 0)) |
52 | | orc 400 |
. . . . . . . . . . 11
⊢ (𝑅 = 0 → (𝑅 = 0 ∨ 𝑅 = 𝑀)) |
53 | 19 | simprd 479 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃))) |
54 | 52, 53 | syl5 34 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 = 0 → (𝑀↑2) ∥ (𝑀 · 𝑃))) |
55 | 51, 54 | syld 47 |
. . . . . . . . 9
⊢ (𝜑 → (¬ 𝑅 ∈ ℕ → (𝑀↑2) ∥ (𝑀 · 𝑃))) |
56 | 47, 55 | mt3d 140 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ ℕ) |
57 | | gzreim 15643 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i]) |
58 | 9, 10, 57 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i]) |
59 | | gzcn 15636 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ) |
61 | 60 | absvalsq2d 14182 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2))) |
62 | 9 | zred 11482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ∈ ℝ) |
63 | 10 | zred 11482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ∈ ℝ) |
64 | 62, 63 | crred 13971 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴) |
65 | 64 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2)) |
66 | 62, 63 | crimd 13972 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵) |
67 | 66 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2)) |
68 | 65, 67 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2))) |
69 | 61, 68 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2))) |
70 | | gzreim 15643 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i]) |
71 | 11, 12, 70 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i]) |
72 | | gzcn 15636 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ) |
74 | 73 | absvalsq2d 14182 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2))) |
75 | 11 | zred 11482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐶 ∈ ℝ) |
76 | 12 | zred 11482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐷 ∈ ℝ) |
77 | 75, 76 | crred 13971 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶) |
78 | 77 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2)) |
79 | 75, 76 | crimd 13972 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷) |
80 | 79 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2)) |
81 | 78, 80 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2))) |
82 | 74, 81 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = ((𝐶↑2) + (𝐷↑2))) |
83 | 69, 82 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2)))) |
84 | 18, 83 | eqtr4d 2659 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 · 𝑃) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2))) |
85 | 84 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀)) |
86 | | prmnn 15388 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
87 | 4, 86 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ ℕ) |
88 | 87 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℂ) |
89 | 88, 34, 40 | divcan3d 10806 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑀 · 𝑃) / 𝑀) = 𝑃) |
90 | 85, 89 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) = 𝑃) |
91 | 9, 30, 13 | 4sqlem5 15646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴 − 𝐸) / 𝑀) ∈ ℤ)) |
92 | 91 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐸 ∈ ℤ) |
93 | 10, 30, 14 | 4sqlem5 15646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ)) |
94 | 93 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ∈ ℤ) |
95 | | gzreim 15643 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (𝐸 + (i · 𝐹)) ∈ ℤ[i]) |
96 | 92, 94, 95 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℤ[i]) |
97 | | gzcn 15636 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸 + (i · 𝐹)) ∈ ℤ[i] → (𝐸 + (i · 𝐹)) ∈ ℂ) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℂ) |
99 | 98 | absvalsq2d 14182 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2))) |
100 | 92 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐸 ∈ ℝ) |
101 | 94 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ∈ ℝ) |
102 | 100, 101 | crred 13971 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℜ‘(𝐸 + (i · 𝐹))) = 𝐸) |
103 | 102 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℜ‘(𝐸 + (i · 𝐹)))↑2) = (𝐸↑2)) |
104 | 100, 101 | crimd 13972 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℑ‘(𝐸 + (i · 𝐹))) = 𝐹) |
105 | 104 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℑ‘(𝐸 + (i · 𝐹)))↑2) = (𝐹↑2)) |
106 | 103, 105 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)) = ((𝐸↑2) + (𝐹↑2))) |
107 | 99, 106 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = ((𝐸↑2) + (𝐹↑2))) |
108 | 11, 30, 15 | 4sqlem5 15646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶 − 𝐺) / 𝑀) ∈ ℤ)) |
109 | 108 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺 ∈ ℤ) |
110 | 12, 30, 16 | 4sqlem5 15646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ)) |
111 | 110 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐻 ∈ ℤ) |
112 | | gzreim 15643 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ ℤ ∧ 𝐻 ∈ ℤ) → (𝐺 + (i · 𝐻)) ∈ ℤ[i]) |
113 | 109, 111,
112 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℤ[i]) |
114 | | gzcn 15636 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 + (i · 𝐻)) ∈ ℤ[i] → (𝐺 + (i · 𝐻)) ∈ ℂ) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℂ) |
116 | 115 | absvalsq2d 14182 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2))) |
117 | 109 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺 ∈ ℝ) |
118 | 111 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐻 ∈ ℝ) |
119 | 117, 118 | crred 13971 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℜ‘(𝐺 + (i · 𝐻))) = 𝐺) |
120 | 119 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℜ‘(𝐺 + (i · 𝐻)))↑2) = (𝐺↑2)) |
121 | 117, 118 | crimd 13972 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℑ‘(𝐺 + (i · 𝐻))) = 𝐻) |
122 | 121 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((ℑ‘(𝐺 + (i · 𝐻)))↑2) = (𝐻↑2)) |
123 | 120, 122 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)) = ((𝐺↑2) + (𝐻↑2))) |
124 | 116, 123 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = ((𝐺↑2) + (𝐻↑2))) |
125 | 107, 124 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2)))) |
126 | 125 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)) |
127 | 126, 17 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = 𝑅) |
128 | 90, 127 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑃 · 𝑅)) |
129 | 56 | nncnd 11036 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ ℂ) |
130 | 88, 129 | mulcomd 10061 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 · 𝑅) = (𝑅 · 𝑃)) |
131 | 128, 130 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑅 · 𝑃)) |
132 | | eqid 2622 |
. . . . . . . . . 10
⊢
(((abs‘(𝐴 + (i
· 𝐵)))↑2) +
((abs‘(𝐶 + (i
· 𝐷)))↑2)) =
(((abs‘(𝐴 + (i
· 𝐵)))↑2) +
((abs‘(𝐶 + (i
· 𝐷)))↑2)) |
133 | | eqid 2622 |
. . . . . . . . . 10
⊢
(((abs‘(𝐸 + (i
· 𝐹)))↑2) +
((abs‘(𝐺 + (i
· 𝐻)))↑2)) =
(((abs‘(𝐸 + (i
· 𝐹)))↑2) +
((abs‘(𝐺 + (i
· 𝐻)))↑2)) |
134 | 9 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℂ) |
135 | | ax-icn 9995 |
. . . . . . . . . . . . . . . 16
⊢ i ∈
ℂ |
136 | 10 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ ℂ) |
137 | | mulcl 10020 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ 𝐵
∈ ℂ) → (i · 𝐵) ∈ ℂ) |
138 | 135, 136,
137 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (i · 𝐵) ∈
ℂ) |
139 | 92 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐸 ∈ ℂ) |
140 | 94 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹 ∈ ℂ) |
141 | | mulcl 10020 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ 𝐹
∈ ℂ) → (i · 𝐹) ∈ ℂ) |
142 | 135, 140,
141 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (i · 𝐹) ∈
ℂ) |
143 | 134, 138,
139, 142 | addsub4d 10439 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹)))) |
144 | 135 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → i ∈
ℂ) |
145 | 144, 136,
140 | subdid 10486 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (i · (𝐵 − 𝐹)) = ((i · 𝐵) − (i · 𝐹))) |
146 | 145 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) = ((𝐴 − 𝐸) + ((i · 𝐵) − (i · 𝐹)))) |
147 | 143, 146 | eqtr4d 2659 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴 − 𝐸) + (i · (𝐵 − 𝐹)))) |
148 | 147 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀)) |
149 | 134, 139 | subcld 10392 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 − 𝐸) ∈ ℂ) |
150 | 136, 140 | subcld 10392 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 − 𝐹) ∈ ℂ) |
151 | | mulcl 10020 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ (𝐵
− 𝐹) ∈ ℂ)
→ (i · (𝐵
− 𝐹)) ∈
ℂ) |
152 | 135, 150,
151 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (i · (𝐵 − 𝐹)) ∈ ℂ) |
153 | 149, 152,
34, 40 | divdird 10839 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴 − 𝐸) + (i · (𝐵 − 𝐹))) / 𝑀) = (((𝐴 − 𝐸) / 𝑀) + ((i · (𝐵 − 𝐹)) / 𝑀))) |
154 | 144, 150,
34, 40 | divassd 10836 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((i · (𝐵 − 𝐹)) / 𝑀) = (i · ((𝐵 − 𝐹) / 𝑀))) |
155 | 154 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴 − 𝐸) / 𝑀) + ((i · (𝐵 − 𝐹)) / 𝑀)) = (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀)))) |
156 | 148, 153,
155 | 3eqtrd 2660 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀)))) |
157 | 91 | simprd 479 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 − 𝐸) / 𝑀) ∈ ℤ) |
158 | 93 | simprd 479 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 − 𝐹) / 𝑀) ∈ ℤ) |
159 | | gzreim 15643 |
. . . . . . . . . . . 12
⊢ ((((𝐴 − 𝐸) / 𝑀) ∈ ℤ ∧ ((𝐵 − 𝐹) / 𝑀) ∈ ℤ) → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i]) |
160 | 157, 158,
159 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐴 − 𝐸) / 𝑀) + (i · ((𝐵 − 𝐹) / 𝑀))) ∈ ℤ[i]) |
161 | 156, 160 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) ∈ ℤ[i]) |
162 | 11 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ ℂ) |
163 | 12 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 ∈ ℂ) |
164 | | mulcl 10020 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ 𝐷
∈ ℂ) → (i · 𝐷) ∈ ℂ) |
165 | 135, 163,
164 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (i · 𝐷) ∈
ℂ) |
166 | 109 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ∈ ℂ) |
167 | 111 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐻 ∈ ℂ) |
168 | | mulcl 10020 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ 𝐻
∈ ℂ) → (i · 𝐻) ∈ ℂ) |
169 | 135, 167,
168 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (i · 𝐻) ∈
ℂ) |
170 | 162, 165,
166, 169 | addsub4d 10439 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻)))) |
171 | 144, 163,
167 | subdid 10486 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (i · (𝐷 − 𝐻)) = ((i · 𝐷) − (i · 𝐻))) |
172 | 171 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) = ((𝐶 − 𝐺) + ((i · 𝐷) − (i · 𝐻)))) |
173 | 170, 172 | eqtr4d 2659 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶 − 𝐺) + (i · (𝐷 − 𝐻)))) |
174 | 173 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀)) |
175 | 162, 166 | subcld 10392 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶 − 𝐺) ∈ ℂ) |
176 | 163, 167 | subcld 10392 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐷 − 𝐻) ∈ ℂ) |
177 | | mulcl 10020 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ (𝐷
− 𝐻) ∈ ℂ)
→ (i · (𝐷
− 𝐻)) ∈
ℂ) |
178 | 135, 176,
177 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (i · (𝐷 − 𝐻)) ∈ ℂ) |
179 | 175, 178,
34, 40 | divdird 10839 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐶 − 𝐺) + (i · (𝐷 − 𝐻))) / 𝑀) = (((𝐶 − 𝐺) / 𝑀) + ((i · (𝐷 − 𝐻)) / 𝑀))) |
180 | 144, 176,
34, 40 | divassd 10836 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((i · (𝐷 − 𝐻)) / 𝑀) = (i · ((𝐷 − 𝐻) / 𝑀))) |
181 | 180 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐶 − 𝐺) / 𝑀) + ((i · (𝐷 − 𝐻)) / 𝑀)) = (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀)))) |
182 | 174, 179,
181 | 3eqtrd 2660 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀)))) |
183 | 108 | simprd 479 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶 − 𝐺) / 𝑀) ∈ ℤ) |
184 | 110 | simprd 479 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐷 − 𝐻) / 𝑀) ∈ ℤ) |
185 | | gzreim 15643 |
. . . . . . . . . . . 12
⊢ ((((𝐶 − 𝐺) / 𝑀) ∈ ℤ ∧ ((𝐷 − 𝐻) / 𝑀) ∈ ℤ) → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i]) |
186 | 183, 184,
185 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐶 − 𝐺) / 𝑀) + (i · ((𝐷 − 𝐻) / 𝑀))) ∈ ℤ[i]) |
187 | 182, 186 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) ∈ ℤ[i]) |
188 | 87 | nnnn0d 11351 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
189 | 90, 188 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) ∈
ℕ0) |
190 | 1, 58, 71, 96, 113, 132, 133, 30, 161, 187, 189 | mul4sqlem 15657 |
. . . . . . . . 9
⊢ (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) ∈ 𝑆) |
191 | 131, 190 | eqeltrrd 2702 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 · 𝑃) ∈ 𝑆) |
192 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑅 → (𝑖 · 𝑃) = (𝑅 · 𝑃)) |
193 | 192 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑖 = 𝑅 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑅 · 𝑃) ∈ 𝑆)) |
194 | 193, 6 | elrab2 3366 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑇 ↔ (𝑅 ∈ ℕ ∧ (𝑅 · 𝑃) ∈ 𝑆)) |
195 | 56, 191, 194 | sylanbrc 698 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ 𝑇) |
196 | | infssuzle 11771 |
. . . . . . 7
⊢ ((𝑇 ⊆
(ℤ≥‘1) ∧ 𝑅 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑅) |
197 | 24, 195, 196 | sylancr 695 |
. . . . . 6
⊢ (𝜑 → inf(𝑇, ℝ, < ) ≤ 𝑅) |
198 | 7, 197 | syl5eqbr 4688 |
. . . . 5
⊢ (𝜑 → 𝑀 ≤ 𝑅) |
199 | 56 | nnred 11035 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ ℝ) |
200 | 199, 31 | letri3d 10179 |
. . . . 5
⊢ (𝜑 → (𝑅 = 𝑀 ↔ (𝑅 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅))) |
201 | 20, 198, 200 | mpbir2and 957 |
. . . 4
⊢ (𝜑 → 𝑅 = 𝑀) |
202 | 201 | olcd 408 |
. . 3
⊢ (𝜑 → (𝑅 = 0 ∨ 𝑅 = 𝑀)) |
203 | 202, 53 | mpd 15 |
. 2
⊢ (𝜑 → (𝑀↑2) ∥ (𝑀 · 𝑃)) |
204 | 203, 47 | pm2.65i 185 |
1
⊢ ¬
𝜑 |