Metamath Proof Explorer

Theorem 4sqlem17

Description: Lemma for 4sq . (Contributed by Mario Carneiro, 16-Jul-2014) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses 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 4sqlem17 ¬ 𝜑

Proof

Step Hyp Ref Expression
1 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
2 4sq.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 4sq.3 ⊢ ( 𝜑 → 𝑃 = ( ( 2 · 𝑁 ) + 1 ) )
4 4sq.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 4sq.5 ⊢ ( 𝜑 → ( 0 ... ( 2 · 𝑁 ) ) ⊆ 𝑆 )
6 4sq.6 ⊢ 𝑇 = { 𝑖 ∈ ℕ ∣ ( 𝑖 · 𝑃 ) ∈ 𝑆 }
7 4sq.7 ⊢ 𝑀 = inf ( 𝑇 , ℝ , < )
8 4sq.m ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 2 ) )
9 4sq.a ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
10 4sq.b ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
11 4sq.c ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
12 4sq.d ⊢ ( 𝜑 → 𝐷 ∈ ℤ )
13 4sq.e ⊢ 𝐸 = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
14 4sq.f ⊢ 𝐹 = ( ( ( 𝐵 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
15 4sq.g ⊢ 𝐺 = ( ( ( 𝐶 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
16 4sq.h ⊢ 𝐻 = ( ( ( 𝐷 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
17 4sq.r ⊢ 𝑅 = ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 )
18 4sq.p ⊢ ( 𝜑 → ( 𝑀 · 𝑃 ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
19 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 4sqlem16 ⊢ ( 𝜑 → ( 𝑅 ≤ 𝑀 ∧ ( ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) ) )
20 19 simpld ⊢ ( 𝜑 → 𝑅 ≤ 𝑀 )
21 6 ssrab3 ⊢ 𝑇 ⊆ ℕ
22 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
23 21 22 sseqtri ⊢ 𝑇 ⊆ ( ℤ≥ ‘ 1 )
24 1 2 3 4 5 6 7 4sqlem13 ⊢ ( 𝜑 → ( 𝑇 ≠ ∅ ∧ 𝑀 < 𝑃 ) )
25 24 simpld ⊢ ( 𝜑 → 𝑇 ≠ ∅ )
26 infssuzcl ⊢ ( ( 𝑇 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
27 23 25 26 sylancr ⊢ ( 𝜑 → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
28 7 27 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ 𝑇 )
29 21 28 sseldi ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
30 29 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
31 24 simprd ⊢ ( 𝜑 → 𝑀 < 𝑃 )
32 30 31 ltned ⊢ ( 𝜑 → 𝑀 ≠ 𝑃 )
33 29 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
34 33 sqvald ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) = ( 𝑀 · 𝑀 ) )
35 34 breq1d ⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ↔ ( 𝑀 · 𝑀 ) ∥ ( 𝑀 · 𝑃 ) ) )
36 29 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
37 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
38 4 37 syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
39 29 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
40 dvdscmulr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → ( ( 𝑀 · 𝑀 ) ∥ ( 𝑀 · 𝑃 ) ↔ 𝑀 ∥ 𝑃 ) )
41 36 38 36 39 40 syl112anc ⊢ ( 𝜑 → ( ( 𝑀 · 𝑀 ) ∥ ( 𝑀 · 𝑃 ) ↔ 𝑀 ∥ 𝑃 ) )
42 dvdsprm ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( 𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃 ) )
43 8 4 42 syl2anc ⊢ ( 𝜑 → ( 𝑀 ∥ 𝑃 ↔ 𝑀 = 𝑃 ) )
44 35 41 43 3bitrd ⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ↔ 𝑀 = 𝑃 ) )
45 44 necon3bbid ⊢ ( 𝜑 → ( ¬ ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ↔ 𝑀 ≠ 𝑃 ) )
46 32 45 mpbird ⊢ ( 𝜑 → ¬ ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) )
47 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 4sqlem14 ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
48 elnn0 ⊢ ( 𝑅 ∈ ℕ0 ↔ ( 𝑅 ∈ ℕ ∨ 𝑅 = 0 ) )
49 47 48 sylib ⊢ ( 𝜑 → ( 𝑅 ∈ ℕ ∨ 𝑅 = 0 ) )
50 49 ord ⊢ ( 𝜑 → ( ¬ 𝑅 ∈ ℕ → 𝑅 = 0 ) )
51 orc ⊢ ( 𝑅 = 0 → ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) )
52 19 simprd ⊢ ( 𝜑 → ( ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) )
53 51 52 syl5 ⊢ ( 𝜑 → ( 𝑅 = 0 → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) )
54 50 53 syld ⊢ ( 𝜑 → ( ¬ 𝑅 ∈ ℕ → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) )
55 46 54 mt3d ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
56 gzreim ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℤ[i] )
57 9 10 56 syl2anc ⊢ ( 𝜑 → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℤ[i] )
58 gzcn ⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℤ[i] → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
59 57 58 syl ⊢ ( 𝜑 → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
60 59 absvalsq2d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) )
61 9 zred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
62 10 zred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
63 61 62 crred ⊢ ( 𝜑 → ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐴 )
64 63 oveq1d ⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( 𝐴 ↑ 2 ) )
65 61 62 crimd ⊢ ( 𝜑 → ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = 𝐵 )
66 65 oveq1d ⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( 𝐵 ↑ 2 ) )
67 64 66 oveq12d ⊢ ( 𝜑 → ( ( ( ℜ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
68 60 67 eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
69 gzreim ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( 𝐶 + ( i · 𝐷 ) ) ∈ ℤ[i] )
70 11 12 69 syl2anc ⊢ ( 𝜑 → ( 𝐶 + ( i · 𝐷 ) ) ∈ ℤ[i] )
71 gzcn ⊢ ( ( 𝐶 + ( i · 𝐷 ) ) ∈ ℤ[i] → ( 𝐶 + ( i · 𝐷 ) ) ∈ ℂ )
72 70 71 syl ⊢ ( 𝜑 → ( 𝐶 + ( i · 𝐷 ) ) ∈ ℂ )
73 72 absvalsq2d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) )
74 11 zred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
75 12 zred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
76 74 75 crred ⊢ ( 𝜑 → ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) = 𝐶 )
77 76 oveq1d ⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) = ( 𝐶 ↑ 2 ) )
78 74 75 crimd ⊢ ( 𝜑 → ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) = 𝐷 )
79 78 oveq1d ⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) = ( 𝐷 ↑ 2 ) )
80 77 79 oveq12d ⊢ ( 𝜑 → ( ( ( ℜ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
81 73 80 eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
82 68 81 oveq12d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
83 18 82 eqtr4d ⊢ ( 𝜑 → ( 𝑀 · 𝑃 ) = ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) )
84 83 oveq1d ⊢ ( 𝜑 → ( ( 𝑀 · 𝑃 ) / 𝑀 ) = ( ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) / 𝑀 ) )
85 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
86 4 85 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
87 86 nncnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
88 87 33 39 divcan3d ⊢ ( 𝜑 → ( ( 𝑀 · 𝑃 ) / 𝑀 ) = 𝑃 )
89 84 88 eqtr3d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) / 𝑀 ) = 𝑃 )
90 9 29 13 4sqlem5 ⊢ ( 𝜑 → ( 𝐸 ∈ ℤ ∧ ( ( 𝐴 − 𝐸 ) / 𝑀 ) ∈ ℤ ) )
91 90 simpld ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
92 10 29 14 4sqlem5 ⊢ ( 𝜑 → ( 𝐹 ∈ ℤ ∧ ( ( 𝐵 − 𝐹 ) / 𝑀 ) ∈ ℤ ) )
93 92 simpld ⊢ ( 𝜑 → 𝐹 ∈ ℤ )
94 gzreim ⊢ ( ( 𝐸 ∈ ℤ ∧ 𝐹 ∈ ℤ ) → ( 𝐸 + ( i · 𝐹 ) ) ∈ ℤ[i] )
95 91 93 94 syl2anc ⊢ ( 𝜑 → ( 𝐸 + ( i · 𝐹 ) ) ∈ ℤ[i] )
96 gzcn ⊢ ( ( 𝐸 + ( i · 𝐹 ) ) ∈ ℤ[i] → ( 𝐸 + ( i · 𝐹 ) ) ∈ ℂ )
97 95 96 syl ⊢ ( 𝜑 → ( 𝐸 + ( i · 𝐹 ) ) ∈ ℂ )
98 97 absvalsq2d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) ) )
99 91 zred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
100 93 zred ⊢ ( 𝜑 → 𝐹 ∈ ℝ )
101 99 100 crred ⊢ ( 𝜑 → ( ℜ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) = 𝐸 )
102 101 oveq1d ⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) = ( 𝐸 ↑ 2 ) )
103 99 100 crimd ⊢ ( 𝜑 → ( ℑ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) = 𝐹 )
104 103 oveq1d ⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) = ( 𝐹 ↑ 2 ) )
105 102 104 oveq12d ⊢ ( 𝜑 → ( ( ( ℜ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
106 98 105 eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) = ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
107 11 29 15 4sqlem5 ⊢ ( 𝜑 → ( 𝐺 ∈ ℤ ∧ ( ( 𝐶 − 𝐺 ) / 𝑀 ) ∈ ℤ ) )
108 107 simpld ⊢ ( 𝜑 → 𝐺 ∈ ℤ )
109 12 29 16 4sqlem5 ⊢ ( 𝜑 → ( 𝐻 ∈ ℤ ∧ ( ( 𝐷 − 𝐻 ) / 𝑀 ) ∈ ℤ ) )
110 109 simpld ⊢ ( 𝜑 → 𝐻 ∈ ℤ )
111 gzreim ⊢ ( ( 𝐺 ∈ ℤ ∧ 𝐻 ∈ ℤ ) → ( 𝐺 + ( i · 𝐻 ) ) ∈ ℤ[i] )
112 108 110 111 syl2anc ⊢ ( 𝜑 → ( 𝐺 + ( i · 𝐻 ) ) ∈ ℤ[i] )
113 gzcn ⊢ ( ( 𝐺 + ( i · 𝐻 ) ) ∈ ℤ[i] → ( 𝐺 + ( i · 𝐻 ) ) ∈ ℂ )
114 112 113 syl ⊢ ( 𝜑 → ( 𝐺 + ( i · 𝐻 ) ) ∈ ℂ )
115 114 absvalsq2d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) )
116 108 zred ⊢ ( 𝜑 → 𝐺 ∈ ℝ )
117 110 zred ⊢ ( 𝜑 → 𝐻 ∈ ℝ )
118 116 117 crred ⊢ ( 𝜑 → ( ℜ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) = 𝐺 )
119 118 oveq1d ⊢ ( 𝜑 → ( ( ℜ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) = ( 𝐺 ↑ 2 ) )
120 116 117 crimd ⊢ ( 𝜑 → ( ℑ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) = 𝐻 )
121 120 oveq1d ⊢ ( 𝜑 → ( ( ℑ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) = ( 𝐻 ↑ 2 ) )
122 119 121 oveq12d ⊢ ( 𝜑 → ( ( ( ℜ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) = ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) )
123 115 122 eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) = ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) )
124 106 123 oveq12d ⊢ ( 𝜑 → ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) = ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) )
125 124 oveq1d ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) / 𝑀 ) = ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) )
126 125 17 syl6eqr ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) / 𝑀 ) = 𝑅 )
127 89 126 oveq12d ⊢ ( 𝜑 → ( ( ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) / 𝑀 ) · ( ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) / 𝑀 ) ) = ( 𝑃 · 𝑅 ) )
128 55 nncnd ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
129 87 128 mulcomd ⊢ ( 𝜑 → ( 𝑃 · 𝑅 ) = ( 𝑅 · 𝑃 ) )
130 127 129 eqtrd ⊢ ( 𝜑 → ( ( ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) / 𝑀 ) · ( ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) / 𝑀 ) ) = ( 𝑅 · 𝑃 ) )
131 eqid ⊢ ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) )
132 eqid ⊢ ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) )
133 9 zcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
134 ax-icn ⊢ i ∈ ℂ
135 10 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
136 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( i · 𝐵 ) ∈ ℂ )
137 134 135 136 sylancr ⊢ ( 𝜑 → ( i · 𝐵 ) ∈ ℂ )
138 91 zcnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
139 93 zcnd ⊢ ( 𝜑 → 𝐹 ∈ ℂ )
140 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐹 ∈ ℂ ) → ( i · 𝐹 ) ∈ ℂ )
141 134 139 140 sylancr ⊢ ( 𝜑 → ( i · 𝐹 ) ∈ ℂ )
142 133 137 138 141 addsub4d ⊢ ( 𝜑 → ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐸 + ( i · 𝐹 ) ) ) = ( ( 𝐴 − 𝐸 ) + ( ( i · 𝐵 ) − ( i · 𝐹 ) ) ) )
143 134 a1i ⊢ ( 𝜑 → i ∈ ℂ )
144 143 135 139 subdid ⊢ ( 𝜑 → ( i · ( 𝐵 − 𝐹 ) ) = ( ( i · 𝐵 ) − ( i · 𝐹 ) ) )
145 144 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 − 𝐸 ) + ( i · ( 𝐵 − 𝐹 ) ) ) = ( ( 𝐴 − 𝐸 ) + ( ( i · 𝐵 ) − ( i · 𝐹 ) ) ) )
146 142 145 eqtr4d ⊢ ( 𝜑 → ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐸 + ( i · 𝐹 ) ) ) = ( ( 𝐴 − 𝐸 ) + ( i · ( 𝐵 − 𝐹 ) ) ) )
147 146 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐸 + ( i · 𝐹 ) ) ) / 𝑀 ) = ( ( ( 𝐴 − 𝐸 ) + ( i · ( 𝐵 − 𝐹 ) ) ) / 𝑀 ) )
148 133 138 subcld ⊢ ( 𝜑 → ( 𝐴 − 𝐸 ) ∈ ℂ )
149 135 139 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝐹 ) ∈ ℂ )
150 mulcl ⊢ ( ( i ∈ ℂ ∧ ( 𝐵 − 𝐹 ) ∈ ℂ ) → ( i · ( 𝐵 − 𝐹 ) ) ∈ ℂ )
151 134 149 150 sylancr ⊢ ( 𝜑 → ( i · ( 𝐵 − 𝐹 ) ) ∈ ℂ )
152 148 151 33 39 divdird ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐸 ) + ( i · ( 𝐵 − 𝐹 ) ) ) / 𝑀 ) = ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) + ( ( i · ( 𝐵 − 𝐹 ) ) / 𝑀 ) ) )
153 143 149 33 39 divassd ⊢ ( 𝜑 → ( ( i · ( 𝐵 − 𝐹 ) ) / 𝑀 ) = ( i · ( ( 𝐵 − 𝐹 ) / 𝑀 ) ) )
154 153 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) + ( ( i · ( 𝐵 − 𝐹 ) ) / 𝑀 ) ) = ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) + ( i · ( ( 𝐵 − 𝐹 ) / 𝑀 ) ) ) )
155 147 152 154 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐸 + ( i · 𝐹 ) ) ) / 𝑀 ) = ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) + ( i · ( ( 𝐵 − 𝐹 ) / 𝑀 ) ) ) )
156 90 simprd ⊢ ( 𝜑 → ( ( 𝐴 − 𝐸 ) / 𝑀 ) ∈ ℤ )
157 92 simprd ⊢ ( 𝜑 → ( ( 𝐵 − 𝐹 ) / 𝑀 ) ∈ ℤ )
158 gzreim ⊢ ( ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) ∈ ℤ ∧ ( ( 𝐵 − 𝐹 ) / 𝑀 ) ∈ ℤ ) → ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) + ( i · ( ( 𝐵 − 𝐹 ) / 𝑀 ) ) ) ∈ ℤ[i] )
159 156 157 158 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐸 ) / 𝑀 ) + ( i · ( ( 𝐵 − 𝐹 ) / 𝑀 ) ) ) ∈ ℤ[i] )
160 155 159 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝐴 + ( i · 𝐵 ) ) − ( 𝐸 + ( i · 𝐹 ) ) ) / 𝑀 ) ∈ ℤ[i] )
161 11 zcnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
162 12 zcnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
163 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( i · 𝐷 ) ∈ ℂ )
164 134 162 163 sylancr ⊢ ( 𝜑 → ( i · 𝐷 ) ∈ ℂ )
165 108 zcnd ⊢ ( 𝜑 → 𝐺 ∈ ℂ )
166 110 zcnd ⊢ ( 𝜑 → 𝐻 ∈ ℂ )
167 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐻 ∈ ℂ ) → ( i · 𝐻 ) ∈ ℂ )
168 134 166 167 sylancr ⊢ ( 𝜑 → ( i · 𝐻 ) ∈ ℂ )
169 161 164 165 168 addsub4d ⊢ ( 𝜑 → ( ( 𝐶 + ( i · 𝐷 ) ) − ( 𝐺 + ( i · 𝐻 ) ) ) = ( ( 𝐶 − 𝐺 ) + ( ( i · 𝐷 ) − ( i · 𝐻 ) ) ) )
170 143 162 166 subdid ⊢ ( 𝜑 → ( i · ( 𝐷 − 𝐻 ) ) = ( ( i · 𝐷 ) − ( i · 𝐻 ) ) )
171 170 oveq2d ⊢ ( 𝜑 → ( ( 𝐶 − 𝐺 ) + ( i · ( 𝐷 − 𝐻 ) ) ) = ( ( 𝐶 − 𝐺 ) + ( ( i · 𝐷 ) − ( i · 𝐻 ) ) ) )
172 169 171 eqtr4d ⊢ ( 𝜑 → ( ( 𝐶 + ( i · 𝐷 ) ) − ( 𝐺 + ( i · 𝐻 ) ) ) = ( ( 𝐶 − 𝐺 ) + ( i · ( 𝐷 − 𝐻 ) ) ) )
173 172 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐶 + ( i · 𝐷 ) ) − ( 𝐺 + ( i · 𝐻 ) ) ) / 𝑀 ) = ( ( ( 𝐶 − 𝐺 ) + ( i · ( 𝐷 − 𝐻 ) ) ) / 𝑀 ) )
174 161 165 subcld ⊢ ( 𝜑 → ( 𝐶 − 𝐺 ) ∈ ℂ )
175 162 166 subcld ⊢ ( 𝜑 → ( 𝐷 − 𝐻 ) ∈ ℂ )
176 mulcl ⊢ ( ( i ∈ ℂ ∧ ( 𝐷 − 𝐻 ) ∈ ℂ ) → ( i · ( 𝐷 − 𝐻 ) ) ∈ ℂ )
177 134 175 176 sylancr ⊢ ( 𝜑 → ( i · ( 𝐷 − 𝐻 ) ) ∈ ℂ )
178 174 177 33 39 divdird ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐺 ) + ( i · ( 𝐷 − 𝐻 ) ) ) / 𝑀 ) = ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) + ( ( i · ( 𝐷 − 𝐻 ) ) / 𝑀 ) ) )
179 143 175 33 39 divassd ⊢ ( 𝜑 → ( ( i · ( 𝐷 − 𝐻 ) ) / 𝑀 ) = ( i · ( ( 𝐷 − 𝐻 ) / 𝑀 ) ) )
180 179 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) + ( ( i · ( 𝐷 − 𝐻 ) ) / 𝑀 ) ) = ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) + ( i · ( ( 𝐷 − 𝐻 ) / 𝑀 ) ) ) )
181 173 178 180 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐶 + ( i · 𝐷 ) ) − ( 𝐺 + ( i · 𝐻 ) ) ) / 𝑀 ) = ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) + ( i · ( ( 𝐷 − 𝐻 ) / 𝑀 ) ) ) )
182 107 simprd ⊢ ( 𝜑 → ( ( 𝐶 − 𝐺 ) / 𝑀 ) ∈ ℤ )
183 109 simprd ⊢ ( 𝜑 → ( ( 𝐷 − 𝐻 ) / 𝑀 ) ∈ ℤ )
184 gzreim ⊢ ( ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) ∈ ℤ ∧ ( ( 𝐷 − 𝐻 ) / 𝑀 ) ∈ ℤ ) → ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) + ( i · ( ( 𝐷 − 𝐻 ) / 𝑀 ) ) ) ∈ ℤ[i] )
185 182 183 184 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐺 ) / 𝑀 ) + ( i · ( ( 𝐷 − 𝐻 ) / 𝑀 ) ) ) ∈ ℤ[i] )
186 181 185 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝐶 + ( i · 𝐷 ) ) − ( 𝐺 + ( i · 𝐻 ) ) ) / 𝑀 ) ∈ ℤ[i] )
187 86 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
188 89 187 eqeltrd ⊢ ( 𝜑 → ( ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) / 𝑀 ) ∈ ℕ0 )
189 1 57 70 95 112 131 132 29 160 186 188 mul4sqlem ⊢ ( 𝜑 → ( ( ( ( ( abs ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐶 + ( i · 𝐷 ) ) ) ↑ 2 ) ) / 𝑀 ) · ( ( ( ( abs ‘ ( 𝐸 + ( i · 𝐹 ) ) ) ↑ 2 ) + ( ( abs ‘ ( 𝐺 + ( i · 𝐻 ) ) ) ↑ 2 ) ) / 𝑀 ) ) ∈ 𝑆 )
190 130 189 eqeltrrd ⊢ ( 𝜑 → ( 𝑅 · 𝑃 ) ∈ 𝑆 )
191 oveq1 ⊢ ( 𝑖 = 𝑅 → ( 𝑖 · 𝑃 ) = ( 𝑅 · 𝑃 ) )
192 191 eleq1d ⊢ ( 𝑖 = 𝑅 → ( ( 𝑖 · 𝑃 ) ∈ 𝑆 ↔ ( 𝑅 · 𝑃 ) ∈ 𝑆 ) )
193 192 6 elrab2 ⊢ ( 𝑅 ∈ 𝑇 ↔ ( 𝑅 ∈ ℕ ∧ ( 𝑅 · 𝑃 ) ∈ 𝑆 ) )
194 55 190 193 sylanbrc ⊢ ( 𝜑 → 𝑅 ∈ 𝑇 )
195 infssuzle ⊢ ( ( 𝑇 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑅 ∈ 𝑇 ) → inf ( 𝑇 , ℝ , < ) ≤ 𝑅 )
196 23 194 195 sylancr ⊢ ( 𝜑 → inf ( 𝑇 , ℝ , < ) ≤ 𝑅 )
197 7 196 eqbrtrid ⊢ ( 𝜑 → 𝑀 ≤ 𝑅 )
198 55 nnred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
199 198 30 letri3d ⊢ ( 𝜑 → ( 𝑅 = 𝑀 ↔ ( 𝑅 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅 ) ) )
200 20 197 199 mpbir2and ⊢ ( 𝜑 → 𝑅 = 𝑀 )
201 200 olcd ⊢ ( 𝜑 → ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) )
202 201 52 mpd ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) )
203 202 46 pm2.65i ⊢ ¬ 𝜑