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 ) ) )