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

Theorem 4sqlem17 15584
Description: Lemma for 4sq 15587. (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 15583 . . . . . 6 (𝜑 → (𝑅𝑀 ∧ ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃))))
2019simpld 475 . . . . 5 (𝜑𝑅𝑀)
21 ssrab2 3671 . . . . . . . . 9 {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} ⊆ ℕ
226, 21eqsstri 3619 . . . . . . . 8 𝑇 ⊆ ℕ
23 nnuz 11667 . . . . . . . 8 ℕ = (ℤ‘1)
2422, 23sseqtri 3621 . . . . . . 7 𝑇 ⊆ (ℤ‘1)
251, 2, 3, 4, 5, 6, 74sqlem13 15580 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))
2625simpld 475 . . . . . . . . . . . . . . 15 (𝜑𝑇 ≠ ∅)
27 infssuzcl 11716 . . . . . . . . . . . . . . 15 ((𝑇 ⊆ (ℤ‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇)
2824, 26, 27sylancr 694 . . . . . . . . . . . . . 14 (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
297, 28syl5eqel 2708 . . . . . . . . . . . . 13 (𝜑𝑀𝑇)
3022, 29sseldi 3586 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
3130nnred 10980 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
3225simprd 479 . . . . . . . . . . 11 (𝜑𝑀 < 𝑃)
3331, 32ltned 10118 . . . . . . . . . 10 (𝜑𝑀𝑃)
3430nncnd 10981 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℂ)
3534sqvald 12942 . . . . . . . . . . . . 13 (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
3635breq1d 4628 . . . . . . . . . . . 12 (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ (𝑀 · 𝑀) ∥ (𝑀 · 𝑃)))
3730nnzd 11425 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℤ)
38 prmz 15308 . . . . . . . . . . . . . 14 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
394, 38syl 17 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℤ)
4030nnne0d 11010 . . . . . . . . . . . . 13 (𝜑𝑀 ≠ 0)
41 dvdscmulr 14929 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀𝑃))
4237, 39, 37, 40, 41syl112anc 1327 . . . . . . . . . . . 12 (𝜑 → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀𝑃))
43 dvdsprm 15334 . . . . . . . . . . . . 13 ((𝑀 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (𝑀𝑃𝑀 = 𝑃))
448, 4, 43syl2anc 692 . . . . . . . . . . . 12 (𝜑 → (𝑀𝑃𝑀 = 𝑃))
4536, 42, 443bitrd 294 . . . . . . . . . . 11 (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 = 𝑃))
4645necon3bbid 2833 . . . . . . . . . 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 15581 . . . . . . . . . . . 12 (𝜑𝑅 ∈ ℕ0)
49 elnn0 11239 . . . . . . . . . . . 12 (𝑅 ∈ ℕ0 ↔ (𝑅 ∈ ℕ ∨ 𝑅 = 0))
5048, 49sylib 208 . . . . . . . . . . 11 (𝜑 → (𝑅 ∈ ℕ ∨ 𝑅 = 0))
5150ord 392 . . . . . . . . . 10 (𝜑 → (¬ 𝑅 ∈ ℕ → 𝑅 = 0))
52 orc 400 . . . . . . . . . . 11 (𝑅 = 0 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
5319simprd 479 . . . . . . . . . . 11 (𝜑 → ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃)))
5452, 53syl5 34 . . . . . . . . . 10 (𝜑 → (𝑅 = 0 → (𝑀↑2) ∥ (𝑀 · 𝑃)))
5551, 54syld 47 . . . . . . . . 9 (𝜑 → (¬ 𝑅 ∈ ℕ → (𝑀↑2) ∥ (𝑀 · 𝑃)))
5647, 55mt3d 140 . . . . . . . 8 (𝜑𝑅 ∈ ℕ)
57 gzreim 15562 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
589, 10, 57syl2anc 692 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
59 gzcn 15555 . . . . . . . . . . . . . . . . . 18 ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ)
6058, 59syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ)
6160absvalsq2d 14111 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)))
629zred 11426 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ)
6310zred 11426 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℝ)
6462, 63crred 13900 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
6564oveq1d 6620 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2))
6662, 63crimd 13901 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
6766oveq1d 6620 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2))
6865, 67oveq12d 6623 . . . . . . . . . . . . . . . 16 (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2)))
6961, 68eqtrd 2660 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2)))
70 gzreim 15562 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
7111, 12, 70syl2anc 692 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
72 gzcn 15555 . . . . . . . . . . . . . . . . . 18 ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ)
7371, 72syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ)
7473absvalsq2d 14111 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)))
7511zred 11426 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐶 ∈ ℝ)
7612zred 11426 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 ∈ ℝ)
7775, 76crred 13900 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶)
7877oveq1d 6620 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2))
7975, 76crimd 13901 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷)
8079oveq1d 6620 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2))
8178, 80oveq12d 6623 . . . . . . . . . . . . . . . 16 (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2)))
8274, 81eqtrd 2660 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = ((𝐶↑2) + (𝐷↑2)))
8369, 82oveq12d 6623 . . . . . . . . . . . . . 14 (𝜑 → (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
8418, 83eqtr4d 2663 . . . . . . . . . . . . 13 (𝜑 → (𝑀 · 𝑃) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)))
8584oveq1d 6620 . . . . . . . . . . . 12 (𝜑 → ((𝑀 · 𝑃) / 𝑀) = ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀))
86 prmnn 15307 . . . . . . . . . . . . . . 15 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
874, 86syl 17 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ ℕ)
8887nncnd 10981 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℂ)
8988, 34, 40divcan3d 10751 . . . . . . . . . . . 12 (𝜑 → ((𝑀 · 𝑃) / 𝑀) = 𝑃)
9085, 89eqtr3d 2662 . . . . . . . . . . 11 (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) = 𝑃)
919, 30, 134sqlem5 15565 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴𝐸) / 𝑀) ∈ ℤ))
9291simpld 475 . . . . . . . . . . . . . . . . . 18 (𝜑𝐸 ∈ ℤ)
9310, 30, 144sqlem5 15565 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵𝐹) / 𝑀) ∈ ℤ))
9493simpld 475 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 ∈ ℤ)
95 gzreim 15562 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
9692, 94, 95syl2anc 692 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
97 gzcn 15555 . . . . . . . . . . . . . . . . 17 ((𝐸 + (i · 𝐹)) ∈ ℤ[i] → (𝐸 + (i · 𝐹)) ∈ ℂ)
9896, 97syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℂ)
9998absvalsq2d 14111 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)))
10092zred 11426 . . . . . . . . . . . . . . . . . 18 (𝜑𝐸 ∈ ℝ)
10194zred 11426 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 ∈ ℝ)
102100, 101crred 13900 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℜ‘(𝐸 + (i · 𝐹))) = 𝐸)
103102oveq1d 6620 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℜ‘(𝐸 + (i · 𝐹)))↑2) = (𝐸↑2))
104100, 101crimd 13901 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℑ‘(𝐸 + (i · 𝐹))) = 𝐹)
105104oveq1d 6620 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℑ‘(𝐸 + (i · 𝐹)))↑2) = (𝐹↑2))
106103, 105oveq12d 6623 . . . . . . . . . . . . . . 15 (𝜑 → (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)) = ((𝐸↑2) + (𝐹↑2)))
10799, 106eqtrd 2660 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = ((𝐸↑2) + (𝐹↑2)))
10811, 30, 154sqlem5 15565 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶𝐺) / 𝑀) ∈ ℤ))
109108simpld 475 . . . . . . . . . . . . . . . . . 18 (𝜑𝐺 ∈ ℤ)
11012, 30, 164sqlem5 15565 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷𝐻) / 𝑀) ∈ ℤ))
111110simpld 475 . . . . . . . . . . . . . . . . . 18 (𝜑𝐻 ∈ ℤ)
112 gzreim 15562 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ ℤ ∧ 𝐻 ∈ ℤ) → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
113109, 111, 112syl2anc 692 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
114 gzcn 15555 . . . . . . . . . . . . . . . . 17 ((𝐺 + (i · 𝐻)) ∈ ℤ[i] → (𝐺 + (i · 𝐻)) ∈ ℂ)
115113, 114syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℂ)
116115absvalsq2d 14111 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)))
117109zred 11426 . . . . . . . . . . . . . . . . . 18 (𝜑𝐺 ∈ ℝ)
118111zred 11426 . . . . . . . . . . . . . . . . . 18 (𝜑𝐻 ∈ ℝ)
119117, 118crred 13900 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℜ‘(𝐺 + (i · 𝐻))) = 𝐺)
120119oveq1d 6620 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℜ‘(𝐺 + (i · 𝐻)))↑2) = (𝐺↑2))
121117, 118crimd 13901 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℑ‘(𝐺 + (i · 𝐻))) = 𝐻)
122121oveq1d 6620 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℑ‘(𝐺 + (i · 𝐻)))↑2) = (𝐻↑2))
123120, 122oveq12d 6623 . . . . . . . . . . . . . . 15 (𝜑 → (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)) = ((𝐺↑2) + (𝐻↑2)))
124116, 123eqtrd 2660 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = ((𝐺↑2) + (𝐻↑2)))
125107, 124oveq12d 6623 . . . . . . . . . . . . 13 (𝜑 → (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
126125oveq1d 6620 . . . . . . . . . . . 12 (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
127126, 17syl6eqr 2678 . . . . . . . . . . 11 (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = 𝑅)
12890, 127oveq12d 6623 . . . . . . . . . 10 (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑃 · 𝑅))
12956nncnd 10981 . . . . . . . . . . 11 (𝜑𝑅 ∈ ℂ)
13088, 129mulcomd 10006 . . . . . . . . . 10 (𝜑 → (𝑃 · 𝑅) = (𝑅 · 𝑃))
131128, 130eqtrd 2660 . . . . . . . . 9 (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑅 · 𝑃))
132 eqid 2626 . . . . . . . . . 10 (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2))
133 eqid 2626 . . . . . . . . . 10 (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2))
1349zcnd 11427 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℂ)
135 ax-icn 9940 . . . . . . . . . . . . . . . 16 i ∈ ℂ
13610zcnd 11427 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ ℂ)
137 mulcl 9965 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i · 𝐵) ∈ ℂ)
138135, 136, 137sylancr 694 . . . . . . . . . . . . . . 15 (𝜑 → (i · 𝐵) ∈ ℂ)
13992zcnd 11427 . . . . . . . . . . . . . . 15 (𝜑𝐸 ∈ ℂ)
14094zcnd 11427 . . . . . . . . . . . . . . . 16 (𝜑𝐹 ∈ ℂ)
141 mulcl 9965 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝐹 ∈ ℂ) → (i · 𝐹) ∈ ℂ)
142135, 140, 141sylancr 694 . . . . . . . . . . . . . . 15 (𝜑 → (i · 𝐹) ∈ ℂ)
143134, 138, 139, 142addsub4d 10384 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴𝐸) + ((i · 𝐵) − (i · 𝐹))))
144135a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → i ∈ ℂ)
145144, 136, 140subdid 10431 . . . . . . . . . . . . . . 15 (𝜑 → (i · (𝐵𝐹)) = ((i · 𝐵) − (i · 𝐹)))
146145oveq2d 6621 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝐸) + (i · (𝐵𝐹))) = ((𝐴𝐸) + ((i · 𝐵) − (i · 𝐹))))
147143, 146eqtr4d 2663 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴𝐸) + (i · (𝐵𝐹))))
148147oveq1d 6620 . . . . . . . . . . . 12 (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴𝐸) + (i · (𝐵𝐹))) / 𝑀))
149134, 139subcld 10337 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐸) ∈ ℂ)
150136, 140subcld 10337 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐹) ∈ ℂ)
151 mulcl 9965 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (𝐵𝐹) ∈ ℂ) → (i · (𝐵𝐹)) ∈ ℂ)
152135, 150, 151sylancr 694 . . . . . . . . . . . . 13 (𝜑 → (i · (𝐵𝐹)) ∈ ℂ)
153149, 152, 34, 40divdird 10784 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐸) + (i · (𝐵𝐹))) / 𝑀) = (((𝐴𝐸) / 𝑀) + ((i · (𝐵𝐹)) / 𝑀)))
154144, 150, 34, 40divassd 10781 . . . . . . . . . . . . 13 (𝜑 → ((i · (𝐵𝐹)) / 𝑀) = (i · ((𝐵𝐹) / 𝑀)))
155154oveq2d 6621 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐸) / 𝑀) + ((i · (𝐵𝐹)) / 𝑀)) = (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))))
156148, 153, 1553eqtrd 2664 . . . . . . . . . . 11 (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))))
15791simprd 479 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐸) / 𝑀) ∈ ℤ)
15893simprd 479 . . . . . . . . . . . 12 (𝜑 → ((𝐵𝐹) / 𝑀) ∈ ℤ)
159 gzreim 15562 . . . . . . . . . . . 12 ((((𝐴𝐸) / 𝑀) ∈ ℤ ∧ ((𝐵𝐹) / 𝑀) ∈ ℤ) → (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))) ∈ ℤ[i])
160157, 158, 159syl2anc 692 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))) ∈ ℤ[i])
161156, 160eqeltrd 2704 . . . . . . . . . 10 (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) ∈ ℤ[i])
16211zcnd 11427 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℂ)
16312zcnd 11427 . . . . . . . . . . . . . . . 16 (𝜑𝐷 ∈ ℂ)
164 mulcl 9965 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝐷 ∈ ℂ) → (i · 𝐷) ∈ ℂ)
165135, 163, 164sylancr 694 . . . . . . . . . . . . . . 15 (𝜑 → (i · 𝐷) ∈ ℂ)
166109zcnd 11427 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ ℂ)
167111zcnd 11427 . . . . . . . . . . . . . . . 16 (𝜑𝐻 ∈ ℂ)
168 mulcl 9965 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝐻 ∈ ℂ) → (i · 𝐻) ∈ ℂ)
169135, 167, 168sylancr 694 . . . . . . . . . . . . . . 15 (𝜑 → (i · 𝐻) ∈ ℂ)
170162, 165, 166, 169addsub4d 10384 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶𝐺) + ((i · 𝐷) − (i · 𝐻))))
171144, 163, 167subdid 10431 . . . . . . . . . . . . . . 15 (𝜑 → (i · (𝐷𝐻)) = ((i · 𝐷) − (i · 𝐻)))
172171oveq2d 6621 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶𝐺) + (i · (𝐷𝐻))) = ((𝐶𝐺) + ((i · 𝐷) − (i · 𝐻))))
173170, 172eqtr4d 2663 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶𝐺) + (i · (𝐷𝐻))))
174173oveq1d 6620 . . . . . . . . . . . 12 (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶𝐺) + (i · (𝐷𝐻))) / 𝑀))
175162, 166subcld 10337 . . . . . . . . . . . . 13 (𝜑 → (𝐶𝐺) ∈ ℂ)
176163, 167subcld 10337 . . . . . . . . . . . . . 14 (𝜑 → (𝐷𝐻) ∈ ℂ)
177 mulcl 9965 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (𝐷𝐻) ∈ ℂ) → (i · (𝐷𝐻)) ∈ ℂ)
178135, 176, 177sylancr 694 . . . . . . . . . . . . 13 (𝜑 → (i · (𝐷𝐻)) ∈ ℂ)
179175, 178, 34, 40divdird 10784 . . . . . . . . . . . 12 (𝜑 → (((𝐶𝐺) + (i · (𝐷𝐻))) / 𝑀) = (((𝐶𝐺) / 𝑀) + ((i · (𝐷𝐻)) / 𝑀)))
180144, 176, 34, 40divassd 10781 . . . . . . . . . . . . 13 (𝜑 → ((i · (𝐷𝐻)) / 𝑀) = (i · ((𝐷𝐻) / 𝑀)))
181180oveq2d 6621 . . . . . . . . . . . 12 (𝜑 → (((𝐶𝐺) / 𝑀) + ((i · (𝐷𝐻)) / 𝑀)) = (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))))
182174, 179, 1813eqtrd 2664 . . . . . . . . . . 11 (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))))
183108simprd 479 . . . . . . . . . . . 12 (𝜑 → ((𝐶𝐺) / 𝑀) ∈ ℤ)
184110simprd 479 . . . . . . . . . . . 12 (𝜑 → ((𝐷𝐻) / 𝑀) ∈ ℤ)
185 gzreim 15562 . . . . . . . . . . . 12 ((((𝐶𝐺) / 𝑀) ∈ ℤ ∧ ((𝐷𝐻) / 𝑀) ∈ ℤ) → (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))) ∈ ℤ[i])
186183, 184, 185syl2anc 692 . . . . . . . . . . 11 (𝜑 → (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))) ∈ ℤ[i])
187182, 186eqeltrd 2704 . . . . . . . . . 10 (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) ∈ ℤ[i])
18887nnnn0d 11296 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℕ0)
18990, 188eqeltrd 2704 . . . . . . . . . 10 (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) ∈ ℕ0)
1901, 58, 71, 96, 113, 132, 133, 30, 161, 187, 189mul4sqlem 15576 . . . . . . . . 9 (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) ∈ 𝑆)
191131, 190eqeltrrd 2705 . . . . . . . 8 (𝜑 → (𝑅 · 𝑃) ∈ 𝑆)
192 oveq1 6612 . . . . . . . . . 10 (𝑖 = 𝑅 → (𝑖 · 𝑃) = (𝑅 · 𝑃))
193192eleq1d 2688 . . . . . . . . 9 (𝑖 = 𝑅 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑅 · 𝑃) ∈ 𝑆))
194193, 6elrab2 3353 . . . . . . . 8 (𝑅𝑇 ↔ (𝑅 ∈ ℕ ∧ (𝑅 · 𝑃) ∈ 𝑆))
19556, 191, 194sylanbrc 697 . . . . . . 7 (𝜑𝑅𝑇)
196 infssuzle 11715 . . . . . . 7 ((𝑇 ⊆ (ℤ‘1) ∧ 𝑅𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑅)
19724, 195, 196sylancr 694 . . . . . 6 (𝜑 → inf(𝑇, ℝ, < ) ≤ 𝑅)
1987, 197syl5eqbr 4653 . . . . 5 (𝜑𝑀𝑅)
19956nnred 10980 . . . . . 6 (𝜑𝑅 ∈ ℝ)
200199, 31letri3d 10124 . . . . 5 (𝜑 → (𝑅 = 𝑀 ↔ (𝑅𝑀𝑀𝑅)))
20120, 198, 200mpbir2and 956 . . . 4 (𝜑𝑅 = 𝑀)
202201olcd 408 . . 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 383   = wceq 1480  wcel 1992  {cab 2612  wne 2796  wrex 2913  {crab 2916  wss 3560  c0 3896   class class class wbr 4618  cfv 5850  (class class class)co 6605  infcinf 8292  cc 9879  cr 9880  0cc0 9881  1c1 9882  ici 9883   + caddc 9884   · cmul 9886   < clt 10019  cle 10020  cmin 10211   / cdiv 10629  cn 10965  2c2 11015  0cn0 11237  cz 11322  cuz 11631  ...cfz 12265   mod cmo 12605  cexp 12797  cre 13766  cim 13767  abscabs 13903  cdvds 14902  cprime 15304  ℤ[i]cgz 15552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958  ax-pre-sup 9959
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-2o 7507  df-oadd 7510  df-er 7688  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-sup 8293  df-inf 8294  df-card 8710  df-cda 8935  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-div 10630  df-nn 10966  df-2 11024  df-3 11025  df-4 11026  df-n0 11238  df-xnn0 11309  df-z 11323  df-uz 11632  df-rp 11777  df-fz 12266  df-fl 12530  df-mod 12606  df-seq 12739  df-exp 12798  df-hash 13055  df-cj 13768  df-re 13769  df-im 13770  df-sqrt 13904  df-abs 13905  df-dvds 14903  df-gcd 15136  df-prm 15305  df-gz 15553
This theorem is referenced by:  4sqlem18  15585
  Copyright terms: Public domain W3C validator