Metamath Proof Explorer

Theorem 4sqlem15

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 4sqlem15 ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) = 0 ) ∧ ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) = 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 eluz2nn ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℕ )
20 8 19 syl ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
21 20 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
22 21 resqcld ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℝ )
23 22 rehalfcld ⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) / 2 ) ∈ ℝ )
24 23 rehalfcld ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ∈ ℝ )
25 24 recnd ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ∈ ℂ )
26 9 20 13 4sqlem5 ⊢ ( 𝜑 → ( 𝐸 ∈ ℤ ∧ ( ( 𝐴 − 𝐸 ) / 𝑀 ) ∈ ℤ ) )
27 26 simpld ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
28 zsqcl ⊢ ( 𝐸 ∈ ℤ → ( 𝐸 ↑ 2 ) ∈ ℤ )
29 27 28 syl ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℤ )
30 29 zred ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℝ )
31 30 recnd ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
32 10 20 14 4sqlem5 ⊢ ( 𝜑 → ( 𝐹 ∈ ℤ ∧ ( ( 𝐵 − 𝐹 ) / 𝑀 ) ∈ ℤ ) )
33 32 simpld ⊢ ( 𝜑 → 𝐹 ∈ ℤ )
34 zsqcl ⊢ ( 𝐹 ∈ ℤ → ( 𝐹 ↑ 2 ) ∈ ℤ )
35 33 34 syl ⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℤ )
36 35 zred ⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℝ )
37 36 recnd ⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ∈ ℂ )
38 25 25 31 37 addsub4d ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) = ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) ) )
39 23 recnd ⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) / 2 ) ∈ ℂ )
40 39 2halvesd ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) = ( ( 𝑀 ↑ 2 ) / 2 ) )
41 40 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) = ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) )
42 38 41 eqtr3d ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) ) = ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) ) = ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) )
44 22 recnd ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℂ )
45 44 2halvesd ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) / 2 ) + ( ( 𝑀 ↑ 2 ) / 2 ) ) = ( 𝑀 ↑ 2 ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝑀 ↑ 2 ) / 2 ) + ( ( 𝑀 ↑ 2 ) / 2 ) ) = ( 𝑀 ↑ 2 ) )
47 21 recnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
48 47 sqvald ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) = ( 𝑀 · 𝑀 ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( 𝑀 ↑ 2 ) = ( 𝑀 · 𝑀 ) )
50 simpr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → 𝑅 = 𝑀 )
51 17 50 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) = 𝑀 )
52 51 oveq1d ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) · 𝑀 ) = ( 𝑀 · 𝑀 ) )
53 30 36 readdcld ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℝ )
54 11 20 15 4sqlem5 ⊢ ( 𝜑 → ( 𝐺 ∈ ℤ ∧ ( ( 𝐶 − 𝐺 ) / 𝑀 ) ∈ ℤ ) )
55 54 simpld ⊢ ( 𝜑 → 𝐺 ∈ ℤ )
56 zsqcl ⊢ ( 𝐺 ∈ ℤ → ( 𝐺 ↑ 2 ) ∈ ℤ )
57 55 56 syl ⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) ∈ ℤ )
58 57 zred ⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) ∈ ℝ )
59 12 20 16 4sqlem5 ⊢ ( 𝜑 → ( 𝐻 ∈ ℤ ∧ ( ( 𝐷 − 𝐻 ) / 𝑀 ) ∈ ℤ ) )
60 59 simpld ⊢ ( 𝜑 → 𝐻 ∈ ℤ )
61 zsqcl ⊢ ( 𝐻 ∈ ℤ → ( 𝐻 ↑ 2 ) ∈ ℤ )
62 60 61 syl ⊢ ( 𝜑 → ( 𝐻 ↑ 2 ) ∈ ℤ )
63 62 zred ⊢ ( 𝜑 → ( 𝐻 ↑ 2 ) ∈ ℝ )
64 58 63 readdcld ⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ∈ ℝ )
65 53 64 readdcld ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℝ )
66 65 recnd ⊢ ( 𝜑 → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℂ )
67 20 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
68 66 47 67 divcan1d ⊢ ( 𝜑 → ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) · 𝑀 ) = ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) / 𝑀 ) · 𝑀 ) = ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) )
70 49 52 69 3eqtr2rd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = ( 𝑀 ↑ 2 ) )
71 46 70 oveq12d ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) + ( ( 𝑀 ↑ 2 ) / 2 ) ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) = ( ( 𝑀 ↑ 2 ) − ( 𝑀 ↑ 2 ) ) )
72 53 recnd ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ∈ ℂ )
73 64 recnd ⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ∈ ℂ )
74 39 39 72 73 addsub4d ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) + ( ( 𝑀 ↑ 2 ) / 2 ) ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) = ( ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) + ( ( 𝑀 ↑ 2 ) / 2 ) ) − ( ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) + ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) = ( ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) )
76 44 subidd ⊢ ( 𝜑 → ( ( 𝑀 ↑ 2 ) − ( 𝑀 ↑ 2 ) ) = 0 )
77 76 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( 𝑀 ↑ 2 ) − ( 𝑀 ↑ 2 ) ) = 0 )
78 71 75 77 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) = 0 )
79 23 53 resubcld ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) ∈ ℝ )
80 9 20 13 4sqlem7 ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
81 10 20 14 4sqlem7 ⊢ ( 𝜑 → ( 𝐹 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
82 30 36 24 24 80 81 le2addd ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
83 82 40 breqtrd ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ≤ ( ( 𝑀 ↑ 2 ) / 2 ) )
84 23 53 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) ↔ ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ≤ ( ( 𝑀 ↑ 2 ) / 2 ) ) )
85 83 84 mpbird ⊢ ( 𝜑 → 0 ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) )
86 23 64 resubcld ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℝ )
87 11 20 15 4sqlem7 ⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
88 12 20 16 4sqlem7 ⊢ ( 𝜑 → ( 𝐻 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
89 58 63 24 24 87 88 le2addd ⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
90 89 40 breqtrd ⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ≤ ( ( 𝑀 ↑ 2 ) / 2 ) )
91 23 64 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ↔ ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ≤ ( ( 𝑀 ↑ 2 ) / 2 ) ) )
92 90 91 mpbird ⊢ ( 𝜑 → 0 ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) )
93 add20 ⊢ ( ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) ∈ ℝ ∧ 0 ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) ) ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ∈ ℝ ∧ 0 ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) = 0 ↔ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) = 0 ∧ ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = 0 ) ) )
94 79 85 86 92 93 syl22anc ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) = 0 ↔ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) = 0 ∧ ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = 0 ) ) )
95 94 biimpa ⊢ ( ( 𝜑 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) ) = 0 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) = 0 ∧ ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = 0 ) )
96 78 95 syldan ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) = 0 ∧ ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = 0 ) )
97 96 simpld ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐸 ↑ 2 ) + ( 𝐹 ↑ 2 ) ) ) = 0 )
98 43 97 eqtrd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) ) = 0 )
99 24 30 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) ∈ ℝ )
100 24 30 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) ↔ ( 𝐸 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
101 80 100 mpbird ⊢ ( 𝜑 → 0 ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) )
102 24 36 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) ∈ ℝ )
103 24 36 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) ↔ ( 𝐹 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
104 81 103 mpbird ⊢ ( 𝜑 → 0 ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) )
105 add20 ⊢ ( ( ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) ) ∧ ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) ) ) → ( ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) ) = 0 ↔ ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) = 0 ) ) )
106 99 101 102 104 105 syl22anc ⊢ ( 𝜑 → ( ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) ) = 0 ↔ ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) = 0 ) ) )
107 106 biimpa ⊢ ( ( 𝜑 ∧ ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) ) = 0 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) = 0 ) )
108 98 107 syldan ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) = 0 ) )
109 58 recnd ⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) ∈ ℂ )
110 63 recnd ⊢ ( 𝜑 → ( 𝐻 ↑ 2 ) ∈ ℂ )
111 25 25 109 110 addsub4d ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) ) )
112 40 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) + ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) )
113 111 112 eqtr3d ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) ) = ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) )
114 113 adantr ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) ) = ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) )
115 96 simprd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( 𝑀 ↑ 2 ) / 2 ) − ( ( 𝐺 ↑ 2 ) + ( 𝐻 ↑ 2 ) ) ) = 0 )
116 114 115 eqtrd ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) ) = 0 )
117 24 58 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) ∈ ℝ )
118 24 58 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) ↔ ( 𝐺 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
119 87 118 mpbird ⊢ ( 𝜑 → 0 ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) )
120 24 63 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) ∈ ℝ )
121 24 63 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) ↔ ( 𝐻 ↑ 2 ) ≤ ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
122 88 121 mpbird ⊢ ( 𝜑 → 0 ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) )
123 add20 ⊢ ( ( ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) ) ∧ ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) ) ) → ( ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) ) = 0 ↔ ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) = 0 ) ) )
124 117 119 120 122 123 syl22anc ⊢ ( 𝜑 → ( ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) ) = 0 ↔ ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) = 0 ) ) )
125 124 biimpa ⊢ ( ( 𝜑 ∧ ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) + ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) ) = 0 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) = 0 ) )
126 116 125 syldan ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) = 0 ) )
127 108 126 jca ⊢ ( ( 𝜑 ∧ 𝑅 = 𝑀 ) → ( ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐸 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐹 ↑ 2 ) ) = 0 ) ∧ ( ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐺 ↑ 2 ) ) = 0 ∧ ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐻 ↑ 2 ) ) = 0 ) ) )