MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4sqlem17 Structured version   Visualization version   GIF version

Theorem 4sqlem17 15788
Description: Lemma for 4sq 15791. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
Hypotheses
Ref Expression
4sq.1 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}
4sq.2 (𝜑𝑁 ∈ ℕ)
4sq.3 (𝜑𝑃 = ((2 · 𝑁) + 1))
4sq.4 (𝜑𝑃 ∈ ℙ)
4sq.5 (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)
4sq.6 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}
4sq.7 𝑀 = inf(𝑇, ℝ, < )
4sq.m (𝜑𝑀 ∈ (ℤ‘2))
4sq.a (𝜑𝐴 ∈ ℤ)
4sq.b (𝜑𝐵 ∈ ℤ)
4sq.c (𝜑𝐶 ∈ ℤ)
4sq.d (𝜑𝐷 ∈ ℤ)
4sq.e 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
4sq.f 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
4sq.g 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
4sq.h 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))
4sq.r 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)
4sq.p (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
Assertion
Ref Expression
4sqlem17 ¬ 𝜑
Distinct variable groups:   𝑤,𝑛,𝑥,𝑦,𝑧   𝐵,𝑛   𝑛,𝐸   𝑛,𝐺   𝑛,𝐻   𝐴,𝑛   𝐶,𝑛   𝐷,𝑛   𝑛,𝐹   𝑖,𝑛,𝑀   𝑛,𝑁   𝑃,𝑖,𝑛   𝜑,𝑛   𝑆,𝑖,𝑛   𝑅,𝑖
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐴(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐶(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐷(𝑥,𝑦,𝑧,𝑤,𝑖)   𝑃(𝑥,𝑦,𝑧,𝑤)   𝑅(𝑥,𝑦,𝑧,𝑤,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤)   𝑇(𝑥,𝑦,𝑧,𝑤,𝑖,𝑛)   𝐸(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐹(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐺(𝑥,𝑦,𝑧,𝑤,𝑖)   𝐻(𝑥,𝑦,𝑧,𝑤,𝑖)   𝑀(𝑥,𝑦,𝑧,𝑤)   𝑁(𝑥,𝑦,𝑧,𝑤,𝑖)

Proof of Theorem 4sqlem17
StepHypRef 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))))
191, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 184sqlem16 15787 . . . . . 6 (𝜑 → (𝑅𝑀 ∧ ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃))))
2019simpld 477 . . . . 5 (𝜑𝑅𝑀)
21 ssrab2 3793 . . . . . . . . 9 {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} ⊆ ℕ
226, 21eqsstri 3741 . . . . . . . 8 𝑇 ⊆ ℕ
23 nnuz 11837 . . . . . . . 8 ℕ = (ℤ‘1)
2422, 23sseqtri 3743 . . . . . . 7 𝑇 ⊆ (ℤ‘1)
251, 2, 3, 4, 5, 6, 74sqlem13 15784 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))
2625simpld 477 . . . . . . . . . . . . . . 15 (𝜑𝑇 ≠ ∅)
27 infssuzcl 11886 . . . . . . . . . . . . . . 15 ((𝑇 ⊆ (ℤ‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇)
2824, 26, 27sylancr 698 . . . . . . . . . . . . . 14 (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
297, 28syl5eqel 2807 . . . . . . . . . . . . 13 (𝜑𝑀𝑇)
3022, 29sseldi 3707 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
3130nnred 11148 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
3225simprd 482 . . . . . . . . . . 11 (𝜑𝑀 < 𝑃)
3331, 32ltned 10286 . . . . . . . . . 10 (𝜑𝑀𝑃)
3430nncnd 11149 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℂ)
3534sqvald 13120 . . . . . . . . . . . . 13 (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
3635breq1d 4770 . . . . . . . . . . . 12 (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ (𝑀 · 𝑀) ∥ (𝑀 · 𝑃)))
3730nnzd 11594 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℤ)
38 prmz 15512 . . . . . . . . . . . . . 14 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
394, 38syl 17 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℤ)
4030nnne0d 11178 . . . . . . . . . . . . 13 (𝜑𝑀 ≠ 0)
41 dvdscmulr 15133 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀𝑃))
4237, 39, 37, 40, 41syl112anc 1443 . . . . . . . . . . . 12 (𝜑 → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀𝑃))
43 dvdsprm 15538 . . . . . . . . . . . . 13 ((𝑀 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (𝑀𝑃𝑀 = 𝑃))
448, 4, 43syl2anc 696 . . . . . . . . . . . 12 (𝜑 → (𝑀𝑃𝑀 = 𝑃))
4536, 42, 443bitrd 294 . . . . . . . . . . 11 (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 = 𝑃))
4645necon3bbid 2933 . . . . . . . . . 10 (𝜑 → (¬ (𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀𝑃))
4733, 46mpbird 247 . . . . . . . . 9 (𝜑 → ¬ (𝑀↑2) ∥ (𝑀 · 𝑃))
481, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 184sqlem14 15785 . . . . . . . . . . . 12 (𝜑𝑅 ∈ ℕ0)
49 elnn0 11407 . . . . . . . . . . . 12 (𝑅 ∈ ℕ0 ↔ (𝑅 ∈ ℕ ∨ 𝑅 = 0))
5048, 49sylib 208 . . . . . . . . . . 11 (𝜑 → (𝑅 ∈ ℕ ∨ 𝑅 = 0))
5150ord 391 . . . . . . . . . 10 (𝜑 → (¬ 𝑅 ∈ ℕ → 𝑅 = 0))
52 orc 399 . . . . . . . . . . 11 (𝑅 = 0 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
5319simprd 482 . . . . . . . . . . 11 (𝜑 → ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃)))
5452, 53syl5 34 . . . . . . . . . 10 (𝜑 → (𝑅 = 0 → (𝑀↑2) ∥ (𝑀 · 𝑃)))
5551, 54syld 47 . . . . . . . . 9 (𝜑 → (¬ 𝑅 ∈ ℕ → (𝑀↑2) ∥ (𝑀 · 𝑃)))
5647, 55mt3d 140 . . . . . . . 8 (𝜑𝑅 ∈ ℕ)
57 gzreim 15766 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
589, 10, 57syl2anc 696 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
59 gzcn 15759 . . . . . . . . . . . . . . . . . 18 ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ)
6058, 59syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ)
6160absvalsq2d 14302 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)))
629zred 11595 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ)
6310zred 11595 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℝ)
6462, 63crred 14091 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
6564oveq1d 6780 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2))
6662, 63crimd 14092 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
6766oveq1d 6780 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2))
6865, 67oveq12d 6783 . . . . . . . . . . . . . . . 16 (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2)))
6961, 68eqtrd 2758 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2)))
70 gzreim 15766 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
7111, 12, 70syl2anc 696 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
72 gzcn 15759 . . . . . . . . . . . . . . . . . 18 ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ)
7371, 72syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ)
7473absvalsq2d 14302 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)))
7511zred 11595 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐶 ∈ ℝ)
7612zred 11595 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 ∈ ℝ)
7775, 76crred 14091 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶)
7877oveq1d 6780 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2))
7975, 76crimd 14092 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷)
8079oveq1d 6780 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2))
8178, 80oveq12d 6783 . . . . . . . . . . . . . . . 16 (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2)))
8274, 81eqtrd 2758 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = ((𝐶↑2) + (𝐷↑2)))
8369, 82oveq12d 6783 . . . . . . . . . . . . . 14 (𝜑 → (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
8418, 83eqtr4d 2761 . . . . . . . . . . . . 13 (𝜑 → (𝑀 · 𝑃) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)))
8584oveq1d 6780 . . . . . . . . . . . 12 (𝜑 → ((𝑀 · 𝑃) / 𝑀) = ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀))
86 prmnn 15511 . . . . . . . . . . . . . . 15 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
874, 86syl 17 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ ℕ)
8887nncnd 11149 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℂ)
8988, 34, 40divcan3d 10919 . . . . . . . . . . . 12 (𝜑 → ((𝑀 · 𝑃) / 𝑀) = 𝑃)
9085, 89eqtr3d 2760 . . . . . . . . . . 11 (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) = 𝑃)
919, 30, 134sqlem5 15769 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴𝐸) / 𝑀) ∈ ℤ))
9291simpld 477 . . . . . . . . . . . . . . . . . 18 (𝜑𝐸 ∈ ℤ)
9310, 30, 144sqlem5 15769 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵𝐹) / 𝑀) ∈ ℤ))
9493simpld 477 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 ∈ ℤ)
95 gzreim 15766 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
9692, 94, 95syl2anc 696 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
97 gzcn 15759 . . . . . . . . . . . . . . . . 17 ((𝐸 + (i · 𝐹)) ∈ ℤ[i] → (𝐸 + (i · 𝐹)) ∈ ℂ)
9896, 97syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℂ)
9998absvalsq2d 14302 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)))
10092zred 11595 . . . . . . . . . . . . . . . . . 18 (𝜑𝐸 ∈ ℝ)
10194zred 11595 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 ∈ ℝ)
102100, 101crred 14091 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℜ‘(𝐸 + (i · 𝐹))) = 𝐸)
103102oveq1d 6780 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℜ‘(𝐸 + (i · 𝐹)))↑2) = (𝐸↑2))
104100, 101crimd 14092 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℑ‘(𝐸 + (i · 𝐹))) = 𝐹)
105104oveq1d 6780 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℑ‘(𝐸 + (i · 𝐹)))↑2) = (𝐹↑2))
106103, 105oveq12d 6783 . . . . . . . . . . . . . . 15 (𝜑 → (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)) = ((𝐸↑2) + (𝐹↑2)))
10799, 106eqtrd 2758 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = ((𝐸↑2) + (𝐹↑2)))
10811, 30, 154sqlem5 15769 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶𝐺) / 𝑀) ∈ ℤ))
109108simpld 477 . . . . . . . . . . . . . . . . . 18 (𝜑𝐺 ∈ ℤ)
11012, 30, 164sqlem5 15769 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷𝐻) / 𝑀) ∈ ℤ))
111110simpld 477 . . . . . . . . . . . . . . . . . 18 (𝜑𝐻 ∈ ℤ)
112 gzreim 15766 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ ℤ ∧ 𝐻 ∈ ℤ) → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
113109, 111, 112syl2anc 696 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
114 gzcn 15759 . . . . . . . . . . . . . . . . 17 ((𝐺 + (i · 𝐻)) ∈ ℤ[i] → (𝐺 + (i · 𝐻)) ∈ ℂ)
115113, 114syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℂ)
116115absvalsq2d 14302 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)))
117109zred 11595 . . . . . . . . . . . . . . . . . 18 (𝜑𝐺 ∈ ℝ)
118111zred 11595 . . . . . . . . . . . . . . . . . 18 (𝜑𝐻 ∈ ℝ)
119117, 118crred 14091 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℜ‘(𝐺 + (i · 𝐻))) = 𝐺)
120119oveq1d 6780 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℜ‘(𝐺 + (i · 𝐻)))↑2) = (𝐺↑2))
121117, 118crimd 14092 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℑ‘(𝐺 + (i · 𝐻))) = 𝐻)
122121oveq1d 6780 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℑ‘(𝐺 + (i · 𝐻)))↑2) = (𝐻↑2))
123120, 122oveq12d 6783 . . . . . . . . . . . . . . 15 (𝜑 → (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)) = ((𝐺↑2) + (𝐻↑2)))
124116, 123eqtrd 2758 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = ((𝐺↑2) + (𝐻↑2)))
125107, 124oveq12d 6783 . . . . . . . . . . . . 13 (𝜑 → (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
126125oveq1d 6780 . . . . . . . . . . . 12 (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
127126, 17syl6eqr 2776 . . . . . . . . . . 11 (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = 𝑅)
12890, 127oveq12d 6783 . . . . . . . . . 10 (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑃 · 𝑅))
12956nncnd 11149 . . . . . . . . . . 11 (𝜑𝑅 ∈ ℂ)
13088, 129mulcomd 10174 . . . . . . . . . 10 (𝜑 → (𝑃 · 𝑅) = (𝑅 · 𝑃))
131128, 130eqtrd 2758 . . . . . . . . 9 (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑅 · 𝑃))
132 eqid 2724 . . . . . . . . . 10 (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2))
133 eqid 2724 . . . . . . . . . 10 (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2))
1349zcnd 11596 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℂ)
135 ax-icn 10108 . . . . . . . . . . . . . . . 16 i ∈ ℂ
13610zcnd 11596 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ ℂ)
137 mulcl 10133 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i · 𝐵) ∈ ℂ)
138135, 136, 137sylancr 698 . . . . . . . . . . . . . . 15 (𝜑 → (i · 𝐵) ∈ ℂ)
13992zcnd 11596 . . . . . . . . . . . . . . 15 (𝜑𝐸 ∈ ℂ)
14094zcnd 11596 . . . . . . . . . . . . . . . 16 (𝜑𝐹 ∈ ℂ)
141 mulcl 10133 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝐹 ∈ ℂ) → (i · 𝐹) ∈ ℂ)
142135, 140, 141sylancr 698 . . . . . . . . . . . . . . 15 (𝜑 → (i · 𝐹) ∈ ℂ)
143134, 138, 139, 142addsub4d 10552 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴𝐸) + ((i · 𝐵) − (i · 𝐹))))
144135a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → i ∈ ℂ)
145144, 136, 140subdid 10599 . . . . . . . . . . . . . . 15 (𝜑 → (i · (𝐵𝐹)) = ((i · 𝐵) − (i · 𝐹)))
146145oveq2d 6781 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝐸) + (i · (𝐵𝐹))) = ((𝐴𝐸) + ((i · 𝐵) − (i · 𝐹))))
147143, 146eqtr4d 2761 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴𝐸) + (i · (𝐵𝐹))))
148147oveq1d 6780 . . . . . . . . . . . 12 (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴𝐸) + (i · (𝐵𝐹))) / 𝑀))
149134, 139subcld 10505 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐸) ∈ ℂ)
150136, 140subcld 10505 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐹) ∈ ℂ)
151 mulcl 10133 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (𝐵𝐹) ∈ ℂ) → (i · (𝐵𝐹)) ∈ ℂ)
152135, 150, 151sylancr 698 . . . . . . . . . . . . 13 (𝜑 → (i · (𝐵𝐹)) ∈ ℂ)
153149, 152, 34, 40divdird 10952 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐸) + (i · (𝐵𝐹))) / 𝑀) = (((𝐴𝐸) / 𝑀) + ((i · (𝐵𝐹)) / 𝑀)))
154144, 150, 34, 40divassd 10949 . . . . . . . . . . . . 13 (𝜑 → ((i · (𝐵𝐹)) / 𝑀) = (i · ((𝐵𝐹) / 𝑀)))
155154oveq2d 6781 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐸) / 𝑀) + ((i · (𝐵𝐹)) / 𝑀)) = (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))))
156148, 153, 1553eqtrd 2762 . . . . . . . . . . 11 (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))))
15791simprd 482 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐸) / 𝑀) ∈ ℤ)
15893simprd 482 . . . . . . . . . . . 12 (𝜑 → ((𝐵𝐹) / 𝑀) ∈ ℤ)
159 gzreim 15766 . . . . . . . . . . . 12 ((((𝐴𝐸) / 𝑀) ∈ ℤ ∧ ((𝐵𝐹) / 𝑀) ∈ ℤ) → (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))) ∈ ℤ[i])
160157, 158, 159syl2anc 696 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))) ∈ ℤ[i])
161156, 160eqeltrd 2803 . . . . . . . . . 10 (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) ∈ ℤ[i])
16211zcnd 11596 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℂ)
16312zcnd 11596 . . . . . . . . . . . . . . . 16 (𝜑𝐷 ∈ ℂ)
164 mulcl 10133 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝐷 ∈ ℂ) → (i · 𝐷) ∈ ℂ)
165135, 163, 164sylancr 698 . . . . . . . . . . . . . . 15 (𝜑 → (i · 𝐷) ∈ ℂ)
166109zcnd 11596 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ ℂ)
167111zcnd 11596 . . . . . . . . . . . . . . . 16 (𝜑𝐻 ∈ ℂ)
168 mulcl 10133 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝐻 ∈ ℂ) → (i · 𝐻) ∈ ℂ)
169135, 167, 168sylancr 698 . . . . . . . . . . . . . . 15 (𝜑 → (i · 𝐻) ∈ ℂ)
170162, 165, 166, 169addsub4d 10552 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶𝐺) + ((i · 𝐷) − (i · 𝐻))))
171144, 163, 167subdid 10599 . . . . . . . . . . . . . . 15 (𝜑 → (i · (𝐷𝐻)) = ((i · 𝐷) − (i · 𝐻)))
172171oveq2d 6781 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶𝐺) + (i · (𝐷𝐻))) = ((𝐶𝐺) + ((i · 𝐷) − (i · 𝐻))))
173170, 172eqtr4d 2761 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶𝐺) + (i · (𝐷𝐻))))
174173oveq1d 6780 . . . . . . . . . . . 12 (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶𝐺) + (i · (𝐷𝐻))) / 𝑀))
175162, 166subcld 10505 . . . . . . . . . . . . 13 (𝜑 → (𝐶𝐺) ∈ ℂ)
176163, 167subcld 10505 . . . . . . . . . . . . . 14 (𝜑 → (𝐷𝐻) ∈ ℂ)
177 mulcl 10133 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (𝐷𝐻) ∈ ℂ) → (i · (𝐷𝐻)) ∈ ℂ)
178135, 176, 177sylancr 698 . . . . . . . . . . . . 13 (𝜑 → (i · (𝐷𝐻)) ∈ ℂ)
179175, 178, 34, 40divdird 10952 . . . . . . . . . . . 12 (𝜑 → (((𝐶𝐺) + (i · (𝐷𝐻))) / 𝑀) = (((𝐶𝐺) / 𝑀) + ((i · (𝐷𝐻)) / 𝑀)))
180144, 176, 34, 40divassd 10949 . . . . . . . . . . . . 13 (𝜑 → ((i · (𝐷𝐻)) / 𝑀) = (i · ((𝐷𝐻) / 𝑀)))
181180oveq2d 6781 . . . . . . . . . . . 12 (𝜑 → (((𝐶𝐺) / 𝑀) + ((i · (𝐷𝐻)) / 𝑀)) = (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))))
182174, 179, 1813eqtrd 2762 . . . . . . . . . . 11 (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))))
183108simprd 482 . . . . . . . . . . . 12 (𝜑 → ((𝐶𝐺) / 𝑀) ∈ ℤ)
184110simprd 482 . . . . . . . . . . . 12 (𝜑 → ((𝐷𝐻) / 𝑀) ∈ ℤ)
185 gzreim 15766 . . . . . . . . . . . 12 ((((𝐶𝐺) / 𝑀) ∈ ℤ ∧ ((𝐷𝐻) / 𝑀) ∈ ℤ) → (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))) ∈ ℤ[i])
186183, 184, 185syl2anc 696 . . . . . . . . . . 11 (𝜑 → (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))) ∈ ℤ[i])
187182, 186eqeltrd 2803 . . . . . . . . . 10 (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) ∈ ℤ[i])
18887nnnn0d 11464 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℕ0)
18990, 188eqeltrd 2803 . . . . . . . . . 10 (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) ∈ ℕ0)
1901, 58, 71, 96, 113, 132, 133, 30, 161, 187, 189mul4sqlem 15780 . . . . . . . . 9 (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) ∈ 𝑆)
191131, 190eqeltrrd 2804 . . . . . . . 8 (𝜑 → (𝑅 · 𝑃) ∈ 𝑆)
192 oveq1 6772 . . . . . . . . . 10 (𝑖 = 𝑅 → (𝑖 · 𝑃) = (𝑅 · 𝑃))
193192eleq1d 2788 . . . . . . . . 9 (𝑖 = 𝑅 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑅 · 𝑃) ∈ 𝑆))
194193, 6elrab2 3472 . . . . . . . 8 (𝑅𝑇 ↔ (𝑅 ∈ ℕ ∧ (𝑅 · 𝑃) ∈ 𝑆))
19556, 191, 194sylanbrc 701 . . . . . . 7 (𝜑𝑅𝑇)
196 infssuzle 11885 . . . . . . 7 ((𝑇 ⊆ (ℤ‘1) ∧ 𝑅𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑅)
19724, 195, 196sylancr 698 . . . . . 6 (𝜑 → inf(𝑇, ℝ, < ) ≤ 𝑅)
1987, 197syl5eqbr 4795 . . . . 5 (𝜑𝑀𝑅)
19956nnred 11148 . . . . . 6 (𝜑𝑅 ∈ ℝ)
200199, 31letri3d 10292 . . . . 5 (𝜑 → (𝑅 = 𝑀 ↔ (𝑅𝑀𝑀𝑅)))
20120, 198, 200mpbir2and 995 . . . 4 (𝜑𝑅 = 𝑀)
202201olcd 407 . . 3 (𝜑 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
203202, 53mpd 15 . 2 (𝜑 → (𝑀↑2) ∥ (𝑀 · 𝑃))
204203, 47pm2.65i 185 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382   = wceq 1596  wcel 2103  {cab 2710  wne 2896  wrex 3015  {crab 3018  wss 3680  c0 4023   class class class wbr 4760  cfv 6001  (class class class)co 6765  infcinf 8463  cc 10047  cr 10048  0cc0 10049  1c1 10050  ici 10051   + caddc 10052   · cmul 10054   < clt 10187  cle 10188  cmin 10379   / cdiv 10797  cn 11133  2c2 11183  0cn0 11405  cz 11490  cuz 11800  ...cfz 12440   mod cmo 12783  cexp 12975  cre 13957  cim 13958  abscabs 14094  cdvds 15103  cprime 15508  ℤ[i]cgz 15756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126  ax-pre-sup 10127
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-2o 7681  df-oadd 7684  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-sup 8464  df-inf 8465  df-card 8878  df-cda 9103  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-div 10798  df-nn 11134  df-2 11192  df-3 11193  df-4 11194  df-n0 11406  df-xnn0 11477  df-z 11491  df-uz 11801  df-rp 11947  df-fz 12441  df-fl 12708  df-mod 12784  df-seq 12917  df-exp 12976  df-hash 13233  df-cj 13959  df-re 13960  df-im 13961  df-sqrt 14095  df-abs 14096  df-dvds 15104  df-gcd 15340  df-prm 15509  df-gz 15757
This theorem is referenced by:  4sqlem18  15789
  Copyright terms: Public domain W3C validator