This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 sselid ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
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 )