# Metamath Proof Explorer

## Theorem 4sqlem14

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 4sqlem14 ( 𝜑𝑅 ∈ ℕ0 )

### 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 6 ssrab3 𝑇 ⊆ ℕ
20 nnuz ℕ = ( ℤ ‘ 1 )
21 19 20 sseqtri 𝑇 ⊆ ( ℤ ‘ 1 )
22 1 2 3 4 5 6 7 4sqlem13 ( 𝜑 → ( 𝑇 ≠ ∅ ∧ 𝑀 < 𝑃 ) )
23 22 simpld ( 𝜑𝑇 ≠ ∅ )
24 infssuzcl ( ( 𝑇 ⊆ ( ℤ ‘ 1 ) ∧ 𝑇 ≠ ∅ ) → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
25 21 23 24 sylancr ( 𝜑 → inf ( 𝑇 , ℝ , < ) ∈ 𝑇 )
26 7 25 eqeltrid ( 𝜑𝑀𝑇 )
27 19 26 sseldi ( 𝜑𝑀 ∈ ℕ )
28 27 nnzd ( 𝜑𝑀 ∈ ℤ )
29 prmz ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
30 4 29 syl ( 𝜑𝑃 ∈ ℤ )
31 28 30 zmulcld ( 𝜑 → ( 𝑀 · 𝑃 ) ∈ ℤ )
32 9 27 13 4sqlem5 ( 𝜑 → ( 𝐸 ∈ ℤ ∧ ( ( 𝐴𝐸 ) / 𝑀 ) ∈ ℤ ) )
33 32 simpld ( 𝜑𝐸 ∈ ℤ )
34 zsqcl2 ( 𝐸 ∈ ℤ → ( 𝐸 ↑ 2 ) ∈ ℕ0 )
35 33 34 syl ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℕ0 )
36 10 27 14 4sqlem5 ( 𝜑 → ( 𝐹 ∈ ℤ ∧ ( ( 𝐵𝐹 ) / 𝑀 ) ∈ ℤ ) )
37 36 simpld ( 𝜑𝐹 ∈ ℤ )
38 zsqcl2 ( 𝐹 ∈ ℤ → ( 𝐹 ↑ 2 ) ∈ ℕ0 )
39 37 38 syl ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℕ0 )
40 35 39 nn0addcld ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℕ0 )
41 40 nn0zd ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℤ )
42 11 27 15 4sqlem5 ( 𝜑 → ( 𝐺 ∈ ℤ ∧ ( ( 𝐶𝐺 ) / 𝑀 ) ∈ ℤ ) )
43 42 simpld ( 𝜑𝐺 ∈ ℤ )
44 zsqcl2 ( 𝐺 ∈ ℤ → ( 𝐺 ↑ 2 ) ∈ ℕ0 )
45 43 44 syl ( 𝜑 → ( 𝐺 ↑ 2 ) ∈ ℕ0 )
46 12 27 16 4sqlem5 ( 𝜑 → ( 𝐻 ∈ ℤ ∧ ( ( 𝐷𝐻 ) / 𝑀 ) ∈ ℤ ) )
47 46 simpld ( 𝜑𝐻 ∈ ℤ )
48 zsqcl2 ( 𝐻 ∈ ℤ → ( 𝐻 ↑ 2 ) ∈ ℕ0 )
49 47 48 syl ( 𝜑 → ( 𝐻 ↑ 2 ) ∈ ℕ0 )
50 45 49 nn0addcld ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ∈ ℕ0 )
51 50 nn0zd ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ∈ ℤ )
52 41 51 zaddcld ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℤ )
53 31 52 zsubcld ( 𝜑 → ( ( 𝑀 · 𝑃 ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) ∈ ℤ )
54 dvdsmul1 ( ( 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → 𝑀 ∥ ( 𝑀 · 𝑃 ) )
55 28 30 54 syl2anc ( 𝜑𝑀 ∥ ( 𝑀 · 𝑃 ) )
56 zsqcl ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
57 9 56 syl ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℤ )
58 zsqcl ( 𝐵 ∈ ℤ → ( 𝐵 ↑ 2 ) ∈ ℤ )
59 10 58 syl ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℤ )
60 57 59 zaddcld ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℤ )
61 60 41 zsubcld ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) ∈ ℤ )
62 zsqcl ( 𝐶 ∈ ℤ → ( 𝐶 ↑ 2 ) ∈ ℤ )
63 11 62 syl ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℤ )
64 zsqcl ( 𝐷 ∈ ℤ → ( 𝐷 ↑ 2 ) ∈ ℤ )
65 12 64 syl ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℤ )
66 63 65 zaddcld ( 𝜑 → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℤ )
67 66 51 zsubcld ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℤ )
68 35 nn0zd ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℤ )
69 57 68 zsubcld ( 𝜑 → ( ( 𝐴 ↑ 2 ) − ( 𝐸 ↑ 2 ) ) ∈ ℤ )
70 39 nn0zd ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℤ )
71 59 70 zsubcld ( 𝜑 → ( ( 𝐵 ↑ 2 ) − ( 𝐹 ↑ 2 ) ) ∈ ℤ )
72 9 27 13 4sqlem8 ( 𝜑𝑀 ∥ ( ( 𝐴 ↑ 2 ) − ( 𝐸 ↑ 2 ) ) )
73 10 27 14 4sqlem8 ( 𝜑𝑀 ∥ ( ( 𝐵 ↑ 2 ) − ( 𝐹 ↑ 2 ) ) )
74 28 69 71 72 73 dvds2addd ( 𝜑𝑀 ∥ ( ( ( 𝐴 ↑ 2 ) − ( 𝐸 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) − ( 𝐹 ↑ 2 ) ) ) )
75 9 zcnd ( 𝜑𝐴 ∈ ℂ )
76 75 sqcld ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
77 10 zcnd ( 𝜑𝐵 ∈ ℂ )
78 77 sqcld ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
79 33 zcnd ( 𝜑𝐸 ∈ ℂ )
80 79 sqcld ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
81 37 zcnd ( 𝜑𝐹 ∈ ℂ )
82 81 sqcld ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℂ )
83 76 78 80 82 addsub4d ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( 𝐸 ↑ 2 ) ) + ( ( 𝐵 ↑ 2 ) − ( 𝐹 ↑ 2 ) ) ) )
84 74 83 breqtrrd ( 𝜑𝑀 ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) )
85 45 nn0zd ( 𝜑 → ( 𝐺 ↑ 2 ) ∈ ℤ )
86 63 85 zsubcld ( 𝜑 → ( ( 𝐶 ↑ 2 ) − ( 𝐺 ↑ 2 ) ) ∈ ℤ )
87 49 nn0zd ( 𝜑 → ( 𝐻 ↑ 2 ) ∈ ℤ )
88 65 87 zsubcld ( 𝜑 → ( ( 𝐷 ↑ 2 ) − ( 𝐻 ↑ 2 ) ) ∈ ℤ )
89 11 27 15 4sqlem8 ( 𝜑𝑀 ∥ ( ( 𝐶 ↑ 2 ) − ( 𝐺 ↑ 2 ) ) )
90 12 27 16 4sqlem8 ( 𝜑𝑀 ∥ ( ( 𝐷 ↑ 2 ) − ( 𝐻 ↑ 2 ) ) )
91 28 86 88 89 90 dvds2addd ( 𝜑𝑀 ∥ ( ( ( 𝐶 ↑ 2 ) − ( 𝐺 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) − ( 𝐻 ↑ 2 ) ) ) )
92 11 zcnd ( 𝜑𝐶 ∈ ℂ )
93 92 sqcld ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℂ )
94 12 zcnd ( 𝜑𝐷 ∈ ℂ )
95 94 sqcld ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℂ )
96 43 zcnd ( 𝜑𝐺 ∈ ℂ )
97 96 sqcld ( 𝜑 → ( 𝐺 ↑ 2 ) ∈ ℂ )
98 47 zcnd ( 𝜑𝐻 ∈ ℂ )
99 98 sqcld ( 𝜑 → ( 𝐻 ↑ 2 ) ∈ ℂ )
100 93 95 97 99 addsub4d ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) − ( 𝐺 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) − ( 𝐻 ↑ 2 ) ) ) )
101 91 100 breqtrrd ( 𝜑𝑀 ∥ ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) )
102 28 61 67 84 101 dvds2addd ( 𝜑𝑀 ∥ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) + ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) )
103 18 oveq1d ( 𝜑 → ( ( 𝑀 · 𝑃 ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) )
104 76 78 addcld ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℂ )
105 93 95 addcld ( 𝜑 → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℂ )
106 80 82 addcld ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℂ )
107 97 99 addcld ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ∈ ℂ )
108 104 105 106 107 addsub4d ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) + ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) )
109 103 108 eqtrd ( 𝜑 → ( ( 𝑀 · 𝑃 ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) + ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) )
110 102 109 breqtrrd ( 𝜑𝑀 ∥ ( ( 𝑀 · 𝑃 ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) )
111 28 31 53 55 110 dvds2subd ( 𝜑𝑀 ∥ ( ( 𝑀 · 𝑃 ) − ( ( 𝑀 · 𝑃 ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) ) )
112 27 nncnd ( 𝜑𝑀 ∈ ℂ )
113 prmnn ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
114 4 113 syl ( 𝜑𝑃 ∈ ℕ )
115 114 nncnd ( 𝜑𝑃 ∈ ℂ )
116 112 115 mulcld ( 𝜑 → ( 𝑀 · 𝑃 ) ∈ ℂ )
117 106 107 addcld ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℂ )
118 116 117 nncand ( 𝜑 → ( ( 𝑀 · 𝑃 ) − ( ( 𝑀 · 𝑃 ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) ) = ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) )
119 111 118 breqtrd ( 𝜑𝑀 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) )
120 27 nnne0d ( 𝜑𝑀 ≠ 0 )
121 40 50 nn0addcld ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℕ0 )
122 121 nn0zd ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℤ )
123 dvdsval2 ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℤ ) → ( 𝑀 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ↔ ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) ∈ ℤ ) )
124 28 120 122 123 syl3anc ( 𝜑 → ( 𝑀 ∥ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ↔ ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) ∈ ℤ ) )
125 119 124 mpbid ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) ∈ ℤ )
126 121 nn0red ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℝ )
127 121 nn0ge0d ( 𝜑 → 0 ≤ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) )
128 27 nnred ( 𝜑𝑀 ∈ ℝ )
129 27 nngt0d ( 𝜑 → 0 < 𝑀 )
130 divge0 ( ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℝ ∧ 0 ≤ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ) → 0 ≤ ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) )
131 126 127 128 129 130 syl22anc ( 𝜑 → 0 ≤ ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) )
132 elnn0z ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) ∈ ℕ0 ↔ ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) ∈ ℤ ∧ 0 ≤ ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) ) )
133 125 131 132 sylanbrc ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) ∈ ℕ0 )
134 17 133 eqeltrid ( 𝜑𝑅 ∈ ℕ0 )