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

Theorem 4sqlem17 15712
Description: Lemma for 4sq 15715. (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 15711 . . . . . 6 (𝜑 → (𝑅𝑀 ∧ ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃))))
2019simpld 474 . . . . 5 (𝜑𝑅𝑀)
21 ssrab2 3720 . . . . . . . . 9 {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} ⊆ ℕ
226, 21eqsstri 3668 . . . . . . . 8 𝑇 ⊆ ℕ
23 nnuz 11761 . . . . . . . 8 ℕ = (ℤ‘1)
2422, 23sseqtri 3670 . . . . . . 7 𝑇 ⊆ (ℤ‘1)
251, 2, 3, 4, 5, 6, 74sqlem13 15708 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))
2625simpld 474 . . . . . . . . . . . . . . 15 (𝜑𝑇 ≠ ∅)
27 infssuzcl 11810 . . . . . . . . . . . . . . 15 ((𝑇 ⊆ (ℤ‘1) ∧ 𝑇 ≠ ∅) → inf(𝑇, ℝ, < ) ∈ 𝑇)
2824, 26, 27sylancr 696 . . . . . . . . . . . . . 14 (𝜑 → inf(𝑇, ℝ, < ) ∈ 𝑇)
297, 28syl5eqel 2734 . . . . . . . . . . . . 13 (𝜑𝑀𝑇)
3022, 29sseldi 3634 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℕ)
3130nnred 11073 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
3225simprd 478 . . . . . . . . . . 11 (𝜑𝑀 < 𝑃)
3331, 32ltned 10211 . . . . . . . . . 10 (𝜑𝑀𝑃)
3430nncnd 11074 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℂ)
3534sqvald 13045 . . . . . . . . . . . . 13 (𝜑 → (𝑀↑2) = (𝑀 · 𝑀))
3635breq1d 4695 . . . . . . . . . . . 12 (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ (𝑀 · 𝑀) ∥ (𝑀 · 𝑃)))
3730nnzd 11519 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℤ)
38 prmz 15436 . . . . . . . . . . . . . 14 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
394, 38syl 17 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℤ)
4030nnne0d 11103 . . . . . . . . . . . . 13 (𝜑𝑀 ≠ 0)
41 dvdscmulr 15057 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀𝑃))
4237, 39, 37, 40, 41syl112anc 1370 . . . . . . . . . . . 12 (𝜑 → ((𝑀 · 𝑀) ∥ (𝑀 · 𝑃) ↔ 𝑀𝑃))
43 dvdsprm 15462 . . . . . . . . . . . . 13 ((𝑀 ∈ (ℤ‘2) ∧ 𝑃 ∈ ℙ) → (𝑀𝑃𝑀 = 𝑃))
448, 4, 43syl2anc 694 . . . . . . . . . . . 12 (𝜑 → (𝑀𝑃𝑀 = 𝑃))
4536, 42, 443bitrd 294 . . . . . . . . . . 11 (𝜑 → ((𝑀↑2) ∥ (𝑀 · 𝑃) ↔ 𝑀 = 𝑃))
4645necon3bbid 2860 . . . . . . . . . 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 15709 . . . . . . . . . . . 12 (𝜑𝑅 ∈ ℕ0)
49 elnn0 11332 . . . . . . . . . . . 12 (𝑅 ∈ ℕ0 ↔ (𝑅 ∈ ℕ ∨ 𝑅 = 0))
5048, 49sylib 208 . . . . . . . . . . 11 (𝜑 → (𝑅 ∈ ℕ ∨ 𝑅 = 0))
5150ord 391 . . . . . . . . . 10 (𝜑 → (¬ 𝑅 ∈ ℕ → 𝑅 = 0))
52 orc 399 . . . . . . . . . . 11 (𝑅 = 0 → (𝑅 = 0 ∨ 𝑅 = 𝑀))
5319simprd 478 . . . . . . . . . . 11 (𝜑 → ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃)))
5452, 53syl5 34 . . . . . . . . . 10 (𝜑 → (𝑅 = 0 → (𝑀↑2) ∥ (𝑀 · 𝑃)))
5551, 54syld 47 . . . . . . . . 9 (𝜑 → (¬ 𝑅 ∈ ℕ → (𝑀↑2) ∥ (𝑀 · 𝑃)))
5647, 55mt3d 140 . . . . . . . 8 (𝜑𝑅 ∈ ℕ)
57 gzreim 15690 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
589, 10, 57syl2anc 694 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
59 gzcn 15683 . . . . . . . . . . . . . . . . . 18 ((𝐴 + (i · 𝐵)) ∈ ℤ[i] → (𝐴 + (i · 𝐵)) ∈ ℂ)
6058, 59syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 + (i · 𝐵)) ∈ ℂ)
6160absvalsq2d 14226 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)))
629zred 11520 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ)
6310zred 11520 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℝ)
6462, 63crred 14015 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℜ‘(𝐴 + (i · 𝐵))) = 𝐴)
6564oveq1d 6705 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℜ‘(𝐴 + (i · 𝐵)))↑2) = (𝐴↑2))
6662, 63crimd 14016 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℑ‘(𝐴 + (i · 𝐵))) = 𝐵)
6766oveq1d 6705 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℑ‘(𝐴 + (i · 𝐵)))↑2) = (𝐵↑2))
6865, 67oveq12d 6708 . . . . . . . . . . . . . . . 16 (𝜑 → (((ℜ‘(𝐴 + (i · 𝐵)))↑2) + ((ℑ‘(𝐴 + (i · 𝐵)))↑2)) = ((𝐴↑2) + (𝐵↑2)))
6961, 68eqtrd 2685 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘(𝐴 + (i · 𝐵)))↑2) = ((𝐴↑2) + (𝐵↑2)))
70 gzreim 15690 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
7111, 12, 70syl2anc 694 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℤ[i])
72 gzcn 15683 . . . . . . . . . . . . . . . . . 18 ((𝐶 + (i · 𝐷)) ∈ ℤ[i] → (𝐶 + (i · 𝐷)) ∈ ℂ)
7371, 72syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐶 + (i · 𝐷)) ∈ ℂ)
7473absvalsq2d 14226 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)))
7511zred 11520 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐶 ∈ ℝ)
7612zred 11520 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 ∈ ℝ)
7775, 76crred 14015 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℜ‘(𝐶 + (i · 𝐷))) = 𝐶)
7877oveq1d 6705 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℜ‘(𝐶 + (i · 𝐷)))↑2) = (𝐶↑2))
7975, 76crimd 14016 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℑ‘(𝐶 + (i · 𝐷))) = 𝐷)
8079oveq1d 6705 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℑ‘(𝐶 + (i · 𝐷)))↑2) = (𝐷↑2))
8178, 80oveq12d 6708 . . . . . . . . . . . . . . . 16 (𝜑 → (((ℜ‘(𝐶 + (i · 𝐷)))↑2) + ((ℑ‘(𝐶 + (i · 𝐷)))↑2)) = ((𝐶↑2) + (𝐷↑2)))
8274, 81eqtrd 2685 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘(𝐶 + (i · 𝐷)))↑2) = ((𝐶↑2) + (𝐷↑2)))
8369, 82oveq12d 6708 . . . . . . . . . . . . . 14 (𝜑 → (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))
8418, 83eqtr4d 2688 . . . . . . . . . . . . 13 (𝜑 → (𝑀 · 𝑃) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)))
8584oveq1d 6705 . . . . . . . . . . . 12 (𝜑 → ((𝑀 · 𝑃) / 𝑀) = ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀))
86 prmnn 15435 . . . . . . . . . . . . . . 15 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
874, 86syl 17 . . . . . . . . . . . . . 14 (𝜑𝑃 ∈ ℕ)
8887nncnd 11074 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℂ)
8988, 34, 40divcan3d 10844 . . . . . . . . . . . 12 (𝜑 → ((𝑀 · 𝑃) / 𝑀) = 𝑃)
9085, 89eqtr3d 2687 . . . . . . . . . . 11 (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) = 𝑃)
919, 30, 134sqlem5 15693 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐸 ∈ ℤ ∧ ((𝐴𝐸) / 𝑀) ∈ ℤ))
9291simpld 474 . . . . . . . . . . . . . . . . . 18 (𝜑𝐸 ∈ ℤ)
9310, 30, 144sqlem5 15693 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹 ∈ ℤ ∧ ((𝐵𝐹) / 𝑀) ∈ ℤ))
9493simpld 474 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 ∈ ℤ)
95 gzreim 15690 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ) → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
9692, 94, 95syl2anc 694 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℤ[i])
97 gzcn 15683 . . . . . . . . . . . . . . . . 17 ((𝐸 + (i · 𝐹)) ∈ ℤ[i] → (𝐸 + (i · 𝐹)) ∈ ℂ)
9896, 97syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 + (i · 𝐹)) ∈ ℂ)
9998absvalsq2d 14226 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)))
10092zred 11520 . . . . . . . . . . . . . . . . . 18 (𝜑𝐸 ∈ ℝ)
10194zred 11520 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 ∈ ℝ)
102100, 101crred 14015 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℜ‘(𝐸 + (i · 𝐹))) = 𝐸)
103102oveq1d 6705 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℜ‘(𝐸 + (i · 𝐹)))↑2) = (𝐸↑2))
104100, 101crimd 14016 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℑ‘(𝐸 + (i · 𝐹))) = 𝐹)
105104oveq1d 6705 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℑ‘(𝐸 + (i · 𝐹)))↑2) = (𝐹↑2))
106103, 105oveq12d 6708 . . . . . . . . . . . . . . 15 (𝜑 → (((ℜ‘(𝐸 + (i · 𝐹)))↑2) + ((ℑ‘(𝐸 + (i · 𝐹)))↑2)) = ((𝐸↑2) + (𝐹↑2)))
10799, 106eqtrd 2685 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(𝐸 + (i · 𝐹)))↑2) = ((𝐸↑2) + (𝐹↑2)))
10811, 30, 154sqlem5 15693 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐺 ∈ ℤ ∧ ((𝐶𝐺) / 𝑀) ∈ ℤ))
109108simpld 474 . . . . . . . . . . . . . . . . . 18 (𝜑𝐺 ∈ ℤ)
11012, 30, 164sqlem5 15693 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐻 ∈ ℤ ∧ ((𝐷𝐻) / 𝑀) ∈ ℤ))
111110simpld 474 . . . . . . . . . . . . . . . . . 18 (𝜑𝐻 ∈ ℤ)
112 gzreim 15690 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ ℤ ∧ 𝐻 ∈ ℤ) → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
113109, 111, 112syl2anc 694 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℤ[i])
114 gzcn 15683 . . . . . . . . . . . . . . . . 17 ((𝐺 + (i · 𝐻)) ∈ ℤ[i] → (𝐺 + (i · 𝐻)) ∈ ℂ)
115113, 114syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐺 + (i · 𝐻)) ∈ ℂ)
116115absvalsq2d 14226 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)))
117109zred 11520 . . . . . . . . . . . . . . . . . 18 (𝜑𝐺 ∈ ℝ)
118111zred 11520 . . . . . . . . . . . . . . . . . 18 (𝜑𝐻 ∈ ℝ)
119117, 118crred 14015 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℜ‘(𝐺 + (i · 𝐻))) = 𝐺)
120119oveq1d 6705 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℜ‘(𝐺 + (i · 𝐻)))↑2) = (𝐺↑2))
121117, 118crimd 14016 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℑ‘(𝐺 + (i · 𝐻))) = 𝐻)
122121oveq1d 6705 . . . . . . . . . . . . . . . 16 (𝜑 → ((ℑ‘(𝐺 + (i · 𝐻)))↑2) = (𝐻↑2))
123120, 122oveq12d 6708 . . . . . . . . . . . . . . 15 (𝜑 → (((ℜ‘(𝐺 + (i · 𝐻)))↑2) + ((ℑ‘(𝐺 + (i · 𝐻)))↑2)) = ((𝐺↑2) + (𝐻↑2)))
124116, 123eqtrd 2685 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(𝐺 + (i · 𝐻)))↑2) = ((𝐺↑2) + (𝐻↑2)))
125107, 124oveq12d 6708 . . . . . . . . . . . . 13 (𝜑 → (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))))
126125oveq1d 6705 . . . . . . . . . . . 12 (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀))
127126, 17syl6eqr 2703 . . . . . . . . . . 11 (𝜑 → ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀) = 𝑅)
12890, 127oveq12d 6708 . . . . . . . . . 10 (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑃 · 𝑅))
12956nncnd 11074 . . . . . . . . . . 11 (𝜑𝑅 ∈ ℂ)
13088, 129mulcomd 10099 . . . . . . . . . 10 (𝜑 → (𝑃 · 𝑅) = (𝑅 · 𝑃))
131128, 130eqtrd 2685 . . . . . . . . 9 (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) = (𝑅 · 𝑃))
132 eqid 2651 . . . . . . . . . 10 (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) = (((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2))
133 eqid 2651 . . . . . . . . . 10 (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) = (((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2))
1349zcnd 11521 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℂ)
135 ax-icn 10033 . . . . . . . . . . . . . . . 16 i ∈ ℂ
13610zcnd 11521 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ ℂ)
137 mulcl 10058 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝐵 ∈ ℂ) → (i · 𝐵) ∈ ℂ)
138135, 136, 137sylancr 696 . . . . . . . . . . . . . . 15 (𝜑 → (i · 𝐵) ∈ ℂ)
13992zcnd 11521 . . . . . . . . . . . . . . 15 (𝜑𝐸 ∈ ℂ)
14094zcnd 11521 . . . . . . . . . . . . . . . 16 (𝜑𝐹 ∈ ℂ)
141 mulcl 10058 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝐹 ∈ ℂ) → (i · 𝐹) ∈ ℂ)
142135, 140, 141sylancr 696 . . . . . . . . . . . . . . 15 (𝜑 → (i · 𝐹) ∈ ℂ)
143134, 138, 139, 142addsub4d 10477 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴𝐸) + ((i · 𝐵) − (i · 𝐹))))
144135a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → i ∈ ℂ)
145144, 136, 140subdid 10524 . . . . . . . . . . . . . . 15 (𝜑 → (i · (𝐵𝐹)) = ((i · 𝐵) − (i · 𝐹)))
146145oveq2d 6706 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴𝐸) + (i · (𝐵𝐹))) = ((𝐴𝐸) + ((i · 𝐵) − (i · 𝐹))))
147143, 146eqtr4d 2688 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) = ((𝐴𝐸) + (i · (𝐵𝐹))))
148147oveq1d 6705 . . . . . . . . . . . 12 (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴𝐸) + (i · (𝐵𝐹))) / 𝑀))
149134, 139subcld 10430 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝐸) ∈ ℂ)
150136, 140subcld 10430 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐹) ∈ ℂ)
151 mulcl 10058 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (𝐵𝐹) ∈ ℂ) → (i · (𝐵𝐹)) ∈ ℂ)
152135, 150, 151sylancr 696 . . . . . . . . . . . . 13 (𝜑 → (i · (𝐵𝐹)) ∈ ℂ)
153149, 152, 34, 40divdird 10877 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐸) + (i · (𝐵𝐹))) / 𝑀) = (((𝐴𝐸) / 𝑀) + ((i · (𝐵𝐹)) / 𝑀)))
154144, 150, 34, 40divassd 10874 . . . . . . . . . . . . 13 (𝜑 → ((i · (𝐵𝐹)) / 𝑀) = (i · ((𝐵𝐹) / 𝑀)))
155154oveq2d 6706 . . . . . . . . . . . 12 (𝜑 → (((𝐴𝐸) / 𝑀) + ((i · (𝐵𝐹)) / 𝑀)) = (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))))
156148, 153, 1553eqtrd 2689 . . . . . . . . . . 11 (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) = (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))))
15791simprd 478 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐸) / 𝑀) ∈ ℤ)
15893simprd 478 . . . . . . . . . . . 12 (𝜑 → ((𝐵𝐹) / 𝑀) ∈ ℤ)
159 gzreim 15690 . . . . . . . . . . . 12 ((((𝐴𝐸) / 𝑀) ∈ ℤ ∧ ((𝐵𝐹) / 𝑀) ∈ ℤ) → (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))) ∈ ℤ[i])
160157, 158, 159syl2anc 694 . . . . . . . . . . 11 (𝜑 → (((𝐴𝐸) / 𝑀) + (i · ((𝐵𝐹) / 𝑀))) ∈ ℤ[i])
161156, 160eqeltrd 2730 . . . . . . . . . 10 (𝜑 → (((𝐴 + (i · 𝐵)) − (𝐸 + (i · 𝐹))) / 𝑀) ∈ ℤ[i])
16211zcnd 11521 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℂ)
16312zcnd 11521 . . . . . . . . . . . . . . . 16 (𝜑𝐷 ∈ ℂ)
164 mulcl 10058 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝐷 ∈ ℂ) → (i · 𝐷) ∈ ℂ)
165135, 163, 164sylancr 696 . . . . . . . . . . . . . . 15 (𝜑 → (i · 𝐷) ∈ ℂ)
166109zcnd 11521 . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ ℂ)
167111zcnd 11521 . . . . . . . . . . . . . . . 16 (𝜑𝐻 ∈ ℂ)
168 mulcl 10058 . . . . . . . . . . . . . . . 16 ((i ∈ ℂ ∧ 𝐻 ∈ ℂ) → (i · 𝐻) ∈ ℂ)
169135, 167, 168sylancr 696 . . . . . . . . . . . . . . 15 (𝜑 → (i · 𝐻) ∈ ℂ)
170162, 165, 166, 169addsub4d 10477 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶𝐺) + ((i · 𝐷) − (i · 𝐻))))
171144, 163, 167subdid 10524 . . . . . . . . . . . . . . 15 (𝜑 → (i · (𝐷𝐻)) = ((i · 𝐷) − (i · 𝐻)))
172171oveq2d 6706 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶𝐺) + (i · (𝐷𝐻))) = ((𝐶𝐺) + ((i · 𝐷) − (i · 𝐻))))
173170, 172eqtr4d 2688 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) = ((𝐶𝐺) + (i · (𝐷𝐻))))
174173oveq1d 6705 . . . . . . . . . . . 12 (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶𝐺) + (i · (𝐷𝐻))) / 𝑀))
175162, 166subcld 10430 . . . . . . . . . . . . 13 (𝜑 → (𝐶𝐺) ∈ ℂ)
176163, 167subcld 10430 . . . . . . . . . . . . . 14 (𝜑 → (𝐷𝐻) ∈ ℂ)
177 mulcl 10058 . . . . . . . . . . . . . 14 ((i ∈ ℂ ∧ (𝐷𝐻) ∈ ℂ) → (i · (𝐷𝐻)) ∈ ℂ)
178135, 176, 177sylancr 696 . . . . . . . . . . . . 13 (𝜑 → (i · (𝐷𝐻)) ∈ ℂ)
179175, 178, 34, 40divdird 10877 . . . . . . . . . . . 12 (𝜑 → (((𝐶𝐺) + (i · (𝐷𝐻))) / 𝑀) = (((𝐶𝐺) / 𝑀) + ((i · (𝐷𝐻)) / 𝑀)))
180144, 176, 34, 40divassd 10874 . . . . . . . . . . . . 13 (𝜑 → ((i · (𝐷𝐻)) / 𝑀) = (i · ((𝐷𝐻) / 𝑀)))
181180oveq2d 6706 . . . . . . . . . . . 12 (𝜑 → (((𝐶𝐺) / 𝑀) + ((i · (𝐷𝐻)) / 𝑀)) = (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))))
182174, 179, 1813eqtrd 2689 . . . . . . . . . . 11 (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) = (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))))
183108simprd 478 . . . . . . . . . . . 12 (𝜑 → ((𝐶𝐺) / 𝑀) ∈ ℤ)
184110simprd 478 . . . . . . . . . . . 12 (𝜑 → ((𝐷𝐻) / 𝑀) ∈ ℤ)
185 gzreim 15690 . . . . . . . . . . . 12 ((((𝐶𝐺) / 𝑀) ∈ ℤ ∧ ((𝐷𝐻) / 𝑀) ∈ ℤ) → (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))) ∈ ℤ[i])
186183, 184, 185syl2anc 694 . . . . . . . . . . 11 (𝜑 → (((𝐶𝐺) / 𝑀) + (i · ((𝐷𝐻) / 𝑀))) ∈ ℤ[i])
187182, 186eqeltrd 2730 . . . . . . . . . 10 (𝜑 → (((𝐶 + (i · 𝐷)) − (𝐺 + (i · 𝐻))) / 𝑀) ∈ ℤ[i])
18887nnnn0d 11389 . . . . . . . . . . 11 (𝜑𝑃 ∈ ℕ0)
18990, 188eqeltrd 2730 . . . . . . . . . 10 (𝜑 → ((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) ∈ ℕ0)
1901, 58, 71, 96, 113, 132, 133, 30, 161, 187, 189mul4sqlem 15704 . . . . . . . . 9 (𝜑 → (((((abs‘(𝐴 + (i · 𝐵)))↑2) + ((abs‘(𝐶 + (i · 𝐷)))↑2)) / 𝑀) · ((((abs‘(𝐸 + (i · 𝐹)))↑2) + ((abs‘(𝐺 + (i · 𝐻)))↑2)) / 𝑀)) ∈ 𝑆)
191131, 190eqeltrrd 2731 . . . . . . . 8 (𝜑 → (𝑅 · 𝑃) ∈ 𝑆)
192 oveq1 6697 . . . . . . . . . 10 (𝑖 = 𝑅 → (𝑖 · 𝑃) = (𝑅 · 𝑃))
193192eleq1d 2715 . . . . . . . . 9 (𝑖 = 𝑅 → ((𝑖 · 𝑃) ∈ 𝑆 ↔ (𝑅 · 𝑃) ∈ 𝑆))
194193, 6elrab2 3399 . . . . . . . 8 (𝑅𝑇 ↔ (𝑅 ∈ ℕ ∧ (𝑅 · 𝑃) ∈ 𝑆))
19556, 191, 194sylanbrc 699 . . . . . . 7 (𝜑𝑅𝑇)
196 infssuzle 11809 . . . . . . 7 ((𝑇 ⊆ (ℤ‘1) ∧ 𝑅𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑅)
19724, 195, 196sylancr 696 . . . . . 6 (𝜑 → inf(𝑇, ℝ, < ) ≤ 𝑅)
1987, 197syl5eqbr 4720 . . . . 5 (𝜑𝑀𝑅)
19956nnred 11073 . . . . . 6 (𝜑𝑅 ∈ ℝ)
200199, 31letri3d 10217 . . . . 5 (𝜑 → (𝑅 = 𝑀 ↔ (𝑅𝑀𝑀𝑅)))
20120, 198, 200mpbir2and 977 . . . 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 1523  wcel 2030  {cab 2637  wne 2823  wrex 2942  {crab 2945  wss 3607  c0 3948   class class class wbr 4685  cfv 5926  (class class class)co 6690  infcinf 8388  cc 9972  cr 9973  0cc0 9974  1c1 9975  ici 9976   + caddc 9977   · cmul 9979   < clt 10112  cle 10113  cmin 10304   / cdiv 10722  cn 11058  2c2 11108  0cn0 11330  cz 11415  cuz 11725  ...cfz 12364   mod cmo 12708  cexp 12900  cre 13881  cim 13882  abscabs 14018  cdvds 15027  cprime 15432  ℤ[i]cgz 15680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-dvds 15028  df-gcd 15264  df-prm 15433  df-gz 15681
This theorem is referenced by:  4sqlem18  15713
  Copyright terms: Public domain W3C validator