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

Metamath Proof Explorer

Theorem 4sqlem16

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 4sqlem16 ( 𝜑 → ( 𝑅 ≤ 𝑀 ∧ ( ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) ) )

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 eluz2nn ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℕ )
20 8 19 syl ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
21 9 20 13 4sqlem5 ⊢ ( 𝜑 → ( 𝐸 ∈ ℤ ∧ ( ( 𝐴 − 𝐸 ) / 𝑀 ) ∈ ℤ ) )
22 21 simpld ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
23 zsqcl ⊢ ( 𝐸 ∈ ℤ → ( 𝐸 ↑ 2 ) ∈ ℤ )
24 22 23 syl ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℤ )
25 24 zred ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℝ )
26 10 20 14 4sqlem5 ⊢ ( 𝜑 → ( 𝐹 ∈ ℤ ∧ ( ( 𝐵 − 𝐹 ) / 𝑀 ) ∈ ℤ ) )
27 26 simpld ⊢ ( 𝜑 → 𝐹 ∈ ℤ )
28 zsqcl ⊢ ( 𝐹 ∈ ℤ → ( 𝐹 ↑ 2 ) ∈ ℤ )
29 27 28 syl ⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℤ )
30 29 zred ⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℝ )
31 25 30 readdcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℝ )
32 11 20 15 4sqlem5 ⊢ ( 𝜑 → ( 𝐺 ∈ ℤ ∧ ( ( 𝐶 − 𝐺 ) / 𝑀 ) ∈ ℤ ) )
33 32 simpld ⊢ ( 𝜑 → 𝐺 ∈ ℤ )
34 zsqcl ⊢ ( 𝐺 ∈ ℤ → ( 𝐺 ↑ 2 ) ∈ ℤ )
35 33 34 syl ⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) ∈ ℤ )
36 35 zred ⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) ∈ ℝ )
37 12 20 16 4sqlem5 ⊢ ( 𝜑 → ( 𝐻 ∈ ℤ ∧ ( ( 𝐷 − 𝐻 ) / 𝑀 ) ∈ ℤ ) )
38 37 simpld ⊢ ( 𝜑 → 𝐻 ∈ ℤ )
39 zsqcl ⊢ ( 𝐻 ∈ ℤ → ( 𝐻 ↑ 2 ) ∈ ℤ )
40 38 39 syl ⊢ ( 𝜑 → ( 𝐻 ↑ 2 ) ∈ ℤ )
41 40 zred ⊢ ( 𝜑 → ( 𝐻 ↑ 2 ) ∈ ℝ )
42 36 41 readdcld ⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ∈ ℝ )
43 20 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
44 43 resqcld ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℝ )
45 44 rehalfcld ⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) / 2 ) ∈ ℝ )
46 45 rehalfcld ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ∈ ℝ )
47 9 20 13 4sqlem7 ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
48 10 20 14 4sqlem7 ⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
49 25 30 46 46 47 48 le2addd ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
50 45 recnd ⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) / 2 ) ∈ ℂ )
51 50 2halvesd ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) = ( ( 𝑀 ↑ 2 ) / 2 ) )
52 49 51 breqtrd ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ≤ ( ( 𝑀 ↑ 2 ) / 2 ) )
53 11 20 15 4sqlem7 ⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
54 12 20 16 4sqlem7 ⊢ ( 𝜑 → ( 𝐻 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
55 36 41 46 46 53 54 le2addd ⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
56 55 51 breqtrd ⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ≤ ( ( 𝑀 ↑ 2 ) / 2 ) )
57 31 42 45 45 52 56 le2addd ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) + ( ( 𝑀 ↑ 2 ) / 2 ) ) )
58 44 recnd ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℂ )
59 58 2halvesd ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) / 2 ) + ( ( 𝑀 ↑ 2 ) / 2 ) ) = ( 𝑀 ↑ 2 ) )
60 57 59 breqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ≤ ( 𝑀 ↑ 2 ) )
61 43 recnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
62 61 sqvald ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) = ( 𝑀 · 𝑀 ) )
63 60 62 breqtrd ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ≤ ( 𝑀 · 𝑀 ) )
64 31 42 readdcld ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℝ )
65 20 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
66 ledivmul ⊢ ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ) → ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) ≤ 𝑀 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ≤ ( 𝑀 · 𝑀 ) ) )
67 64 43 43 65 66 syl112anc ⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) ≤ 𝑀 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ≤ ( 𝑀 · 𝑀 ) ) )
68 63 67 mpbird ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) ≤ 𝑀 )
69 17 68 eqbrtrid ⊢ ( 𝜑 → 𝑅 ≤ 𝑀 )
70 simpr ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → 𝑅 = 0 )
71 17 70 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) = 0 )
72 64 recnd ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℂ )
73 20 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
74 72 61 73 diveq0ad ⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) = 0 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = 0 ) )
75 zsqcl2 ⊢ ( 𝐸 ∈ ℤ → ( 𝐸 ↑ 2 ) ∈ ℕ0 )
76 22 75 syl ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℕ0 )
77 zsqcl2 ⊢ ( 𝐹 ∈ ℤ → ( 𝐹 ↑ 2 ) ∈ ℕ0 )
78 27 77 syl ⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℕ0 )
79 76 78 nn0addcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℕ0 )
80 79 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) )
81 zsqcl2 ⊢ ( 𝐺 ∈ ℤ → ( 𝐺 ↑ 2 ) ∈ ℕ0 )
82 33 81 syl ⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) ∈ ℕ0 )
83 zsqcl2 ⊢ ( 𝐻 ∈ ℤ → ( 𝐻 ↑ 2 ) ∈ ℕ0 )
84 38 83 syl ⊢ ( 𝜑 → ( 𝐻 ↑ 2 ) ∈ ℕ0 )
85 82 84 nn0addcld ⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ∈ ℕ0 )
86 85 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) )
87 add20 ⊢ ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) ∧ ( ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = 0 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ∧ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ) ) )
88 31 80 42 86 87 syl22anc ⊢ ( 𝜑 → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = 0 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ∧ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ) ) )
89 74 88 bitrd ⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) = 0 ↔ ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ∧ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ) ) )
90 89 biimpa ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) = 0 ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ∧ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ) )
91 71 90 syldan ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ∧ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ) )
92 91 simpld ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 )
93 76 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐸 ↑ 2 ) )
94 78 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐹 ↑ 2 ) )
95 add20 ⊢ ( ( ( ( 𝐸 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐸 ↑ 2 ) ) ∧ ( ( 𝐹 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ↑ 2 ) ) ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ↔ ( ( 𝐸 ↑ 2 ) = 0 ∧ ( 𝐹 ↑ 2 ) = 0 ) ) )
96 25 93 30 94 95 syl22anc ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ↔ ( ( 𝐸 ↑ 2 ) = 0 ∧ ( 𝐹 ↑ 2 ) = 0 ) ) )
97 96 biimpa ⊢ ( ( 𝜑 ∧ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) = 0 ) → ( ( 𝐸 ↑ 2 ) = 0 ∧ ( 𝐹 ↑ 2 ) = 0 ) )
98 92 97 syldan ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( 𝐸 ↑ 2 ) = 0 ∧ ( 𝐹 ↑ 2 ) = 0 ) )
99 98 simpld ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝐸 ↑ 2 ) = 0 )
100 9 20 13 99 4sqlem9 ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) )
101 98 simprd ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝐹 ↑ 2 ) = 0 )
102 10 20 14 101 4sqlem9 ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) )
103 20 nnsqcld ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℕ )
104 103 nnzd ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℤ )
105 zsqcl ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
106 9 105 syl ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℤ )
107 zsqcl ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 ↑ 2 ) ∈ ℤ )
108 10 107 syl ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℤ )
109 dvds2add ⊢ ( ( ( 𝑀 ↑ 2 ) ∈ ℤ ∧ ( 𝐴 ↑ 2 ) ∈ ℤ ∧ ( 𝐵 ↑ 2 ) ∈ ℤ ) → ( ( ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ∧ ( 𝑀 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
110 104 106 108 109 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ∧ ( 𝑀 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
111 110 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( ( 𝑀 ↑ 2 ) ∥ ( 𝐴 ↑ 2 ) ∧ ( 𝑀 ↑ 2 ) ∥ ( 𝐵 ↑ 2 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
112 100 102 111 mp2and ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
113 91 simprd ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 )
114 82 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐺 ↑ 2 ) )
115 84 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 𝐻 ↑ 2 ) )
116 add20 ⊢ ( ( ( ( 𝐺 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐺 ↑ 2 ) ) ∧ ( ( 𝐻 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐻 ↑ 2 ) ) ) → ( ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ↔ ( ( 𝐺 ↑ 2 ) = 0 ∧ ( 𝐻 ↑ 2 ) = 0 ) ) )
117 36 114 41 115 116 syl22anc ⊢ ( 𝜑 → ( ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ↔ ( ( 𝐺 ↑ 2 ) = 0 ∧ ( 𝐻 ↑ 2 ) = 0 ) ) )
118 117 biimpa ⊢ ( ( 𝜑 ∧ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) = 0 ) → ( ( 𝐺 ↑ 2 ) = 0 ∧ ( 𝐻 ↑ 2 ) = 0 ) )
119 113 118 syldan ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( 𝐺 ↑ 2 ) = 0 ∧ ( 𝐻 ↑ 2 ) = 0 ) )
120 119 simpld ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝐺 ↑ 2 ) = 0 )
121 11 20 15 120 4sqlem9 ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) )
122 119 simprd ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝐻 ↑ 2 ) = 0 )
123 12 20 16 122 4sqlem9 ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝐷 ↑ 2 ) )
124 zsqcl ⊢ ( 𝐶 ∈ ℤ → ( 𝐶 ↑ 2 ) ∈ ℤ )
125 11 124 syl ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℤ )
126 zsqcl ⊢ ( 𝐷 ∈ ℤ → ( 𝐷 ↑ 2 ) ∈ ℤ )
127 12 126 syl ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℤ )
128 dvds2add ⊢ ( ( ( 𝑀 ↑ 2 ) ∈ ℤ ∧ ( 𝐶 ↑ 2 ) ∈ ℤ ∧ ( 𝐷 ↑ 2 ) ∈ ℤ ) → ( ( ( 𝑀 ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) ∧ ( 𝑀 ↑ 2 ) ∥ ( 𝐷 ↑ 2 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
129 104 125 127 128 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) ∧ ( 𝑀 ↑ 2 ) ∥ ( 𝐷 ↑ 2 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
130 129 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( ( 𝑀 ↑ 2 ) ∥ ( 𝐶 ↑ 2 ) ∧ ( 𝑀 ↑ 2 ) ∥ ( 𝐷 ↑ 2 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
131 121 123 130 mp2and ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
132 106 108 zaddcld ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℤ )
133 125 127 zaddcld ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℤ )
134 dvds2add ⊢ ( ( ( 𝑀 ↑ 2 ) ∈ ℤ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℤ ∧ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℤ ) → ( ( ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∧ ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ) )
135 104 132 133 134 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∧ ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ) )
136 135 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( ( ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∧ ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ) )
137 112 131 136 mp2and ⊢ ( ( 𝜑 ∧ 𝑅 = 0 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
138 104 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∈ ℤ )
139 132 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℤ )
140 51 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) = ( ( 𝑀 ↑ 2 ) / 2 ) )
141 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 4sqlem15 ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) = 0 ) ∧ ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) = 0 ) ) )
142 141 simpld ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) = 0 ) )
143 142 simpld ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 )
144 46 recnd ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ∈ ℂ )
145 24 zcnd ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
146 144 145 subeq0ad ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ↔ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) = ( 𝐸 ↑ 2 ) ) )
147 146 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ↔ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) = ( 𝐸 ↑ 2 ) ) )
148 143 147 mpbid ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) = ( 𝐸 ↑ 2 ) )
149 24 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝐸 ↑ 2 ) ∈ ℤ )
150 148 149 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ∈ ℤ )
151 150 150 zaddcld ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ∈ ℤ )
152 140 151 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝑀 ↑ 2 ) / 2 ) ∈ ℤ )
153 139 152 zsubcld ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) ∈ ℤ )
154 133 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℤ )
155 154 152 zsubcld ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) ∈ ℤ )
156 106 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝐴 ↑ 2 ) ∈ ℤ )
157 156 150 zsubcld ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ∈ ℤ )
158 108 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝐵 ↑ 2 ) ∈ ℤ )
159 158 150 zsubcld ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝐵 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ∈ ℤ )
160 9 20 13 143 4sqlem10 ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
161 142 simprd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) = 0 )
162 10 20 14 161 4sqlem10 ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐵 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
163 138 157 159 160 162 dvds2addd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐵 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) )
164 106 zcnd ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
165 108 zcnd ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
166 164 165 144 144 addsub4d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐵 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) )
167 51 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
168 166 167 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐵 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
169 168 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐵 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
170 163 169 breqtrd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
171 125 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝐶 ↑ 2 ) ∈ ℤ )
172 171 150 zsubcld ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝐶 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ∈ ℤ )
173 127 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝐷 ↑ 2 ) ∈ ℤ )
174 173 150 zsubcld ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝐷 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ∈ ℤ )
175 141 simprd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) = 0 ) )
176 175 simpld ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) = 0 )
177 11 20 15 176 4sqlem10 ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐶 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
178 175 simprd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) = 0 )
179 12 20 16 178 4sqlem10 ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐷 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
180 138 172 174 177 179 dvds2addd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐶 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐷 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) )
181 125 zcnd ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℂ )
182 127 zcnd ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℂ )
183 181 182 144 144 addsub4d ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐷 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) )
184 51 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
185 183 184 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐷 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
186 185 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝐶 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) + ( ( 𝐷 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
187 180 186 breqtrd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) )
188 138 153 155 170 187 dvds2addd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) + ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) ) )
189 132 zcnd ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℂ )
190 133 zcnd ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ∈ ℂ )
191 189 190 50 50 addsub4d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) + ( ( 𝑀 ↑ 2 ) / 2 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) + ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) ) )
192 59 oveq2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) + ( ( 𝑀 ↑ 2 ) / 2 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝑀 ↑ 2 ) ) )
193 191 192 eqtr3d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) + ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝑀 ↑ 2 ) ) )
194 193 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) + ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( ( 𝑀 ↑ 2 ) / 2 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝑀 ↑ 2 ) ) )
195 188 194 breqtrd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝑀 ↑ 2 ) ) )
196 132 133 zaddcld ⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ∈ ℤ )
197 196 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ∈ ℤ )
198 dvdssubr ⊢ ( ( ( 𝑀 ↑ 2 ) ∈ ℤ ∧ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ∈ ℤ ) → ( ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ↔ ( 𝑀 ↑ 2 ) ∥ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝑀 ↑ 2 ) ) ) )
199 138 197 198 syl2anc ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) ↔ ( 𝑀 ↑ 2 ) ∥ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) − ( 𝑀 ↑ 2 ) ) ) )
200 195 199 mpbird ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
201 137 200 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
202 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) ) → ( 𝑀 · 𝑃 ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) )
203 201 202 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) ) → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) )
204 203 ex ⊢ ( 𝜑 → ( ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) )
205 69 204 jca ⊢ ( 𝜑 → ( 𝑅 ≤ 𝑀 ∧ ( ( 𝑅 = 0 ∨ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) ∥ ( 𝑀 · 𝑃 ) ) ) )