# 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 ${⊢}{S}=\left\{{n}|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {z}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}{n}={{x}}^{2}+{{y}}^{2}+{{z}}^{2}+{{w}}^{2}\right\}$
4sq.2 ${⊢}{\phi }\to {N}\in ℕ$
4sq.3 ${⊢}{\phi }\to {P}=2\cdot {N}+1$
4sq.4 ${⊢}{\phi }\to {P}\in ℙ$
4sq.5 ${⊢}{\phi }\to \left(0\dots 2\cdot {N}\right)\subseteq {S}$
4sq.6 ${⊢}{T}=\left\{{i}\in ℕ|{i}{P}\in {S}\right\}$
4sq.7 ${⊢}{M}=sup\left({T},ℝ,<\right)$
4sq.m ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 2}$
4sq.a ${⊢}{\phi }\to {A}\in ℤ$
4sq.b ${⊢}{\phi }\to {B}\in ℤ$
4sq.c ${⊢}{\phi }\to {C}\in ℤ$
4sq.d ${⊢}{\phi }\to {D}\in ℤ$
4sq.e ${⊢}{E}=\left(\left({A}+\left(\frac{{M}}{2}\right)\right)\mathrm{mod}{M}\right)-\left(\frac{{M}}{2}\right)$
4sq.f ${⊢}{F}=\left(\left({B}+\left(\frac{{M}}{2}\right)\right)\mathrm{mod}{M}\right)-\left(\frac{{M}}{2}\right)$
4sq.g ${⊢}{G}=\left(\left({C}+\left(\frac{{M}}{2}\right)\right)\mathrm{mod}{M}\right)-\left(\frac{{M}}{2}\right)$
4sq.h ${⊢}{H}=\left(\left({D}+\left(\frac{{M}}{2}\right)\right)\mathrm{mod}{M}\right)-\left(\frac{{M}}{2}\right)$
4sq.r ${⊢}{R}=\frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}$
4sq.p ${⊢}{\phi }\to {M}{P}={{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}$
Assertion 4sqlem16 ${⊢}{\phi }\to \left({R}\le {M}\wedge \left(\left({R}=0\vee {R}={M}\right)\to {{M}}^{2}\parallel {M}{P}\right)\right)$

### Proof

Step Hyp Ref Expression
1 4sq.1 ${⊢}{S}=\left\{{n}|\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {z}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℤ\phantom{\rule{.4em}{0ex}}{n}={{x}}^{2}+{{y}}^{2}+{{z}}^{2}+{{w}}^{2}\right\}$
2 4sq.2 ${⊢}{\phi }\to {N}\in ℕ$
3 4sq.3 ${⊢}{\phi }\to {P}=2\cdot {N}+1$
4 4sq.4 ${⊢}{\phi }\to {P}\in ℙ$
5 4sq.5 ${⊢}{\phi }\to \left(0\dots 2\cdot {N}\right)\subseteq {S}$
6 4sq.6 ${⊢}{T}=\left\{{i}\in ℕ|{i}{P}\in {S}\right\}$
7 4sq.7 ${⊢}{M}=sup\left({T},ℝ,<\right)$
8 4sq.m ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 2}$
9 4sq.a ${⊢}{\phi }\to {A}\in ℤ$
10 4sq.b ${⊢}{\phi }\to {B}\in ℤ$
11 4sq.c ${⊢}{\phi }\to {C}\in ℤ$
12 4sq.d ${⊢}{\phi }\to {D}\in ℤ$
13 4sq.e ${⊢}{E}=\left(\left({A}+\left(\frac{{M}}{2}\right)\right)\mathrm{mod}{M}\right)-\left(\frac{{M}}{2}\right)$
14 4sq.f ${⊢}{F}=\left(\left({B}+\left(\frac{{M}}{2}\right)\right)\mathrm{mod}{M}\right)-\left(\frac{{M}}{2}\right)$
15 4sq.g ${⊢}{G}=\left(\left({C}+\left(\frac{{M}}{2}\right)\right)\mathrm{mod}{M}\right)-\left(\frac{{M}}{2}\right)$
16 4sq.h ${⊢}{H}=\left(\left({D}+\left(\frac{{M}}{2}\right)\right)\mathrm{mod}{M}\right)-\left(\frac{{M}}{2}\right)$
17 4sq.r ${⊢}{R}=\frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}$
18 4sq.p ${⊢}{\phi }\to {M}{P}={{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}$
19 eluz2nn ${⊢}{M}\in {ℤ}_{\ge 2}\to {M}\in ℕ$
20 8 19 syl ${⊢}{\phi }\to {M}\in ℕ$
21 9 20 13 4sqlem5 ${⊢}{\phi }\to \left({E}\in ℤ\wedge \frac{{A}-{E}}{{M}}\in ℤ\right)$
22 21 simpld ${⊢}{\phi }\to {E}\in ℤ$
23 zsqcl ${⊢}{E}\in ℤ\to {{E}}^{2}\in ℤ$
24 22 23 syl ${⊢}{\phi }\to {{E}}^{2}\in ℤ$
25 24 zred ${⊢}{\phi }\to {{E}}^{2}\in ℝ$
26 10 20 14 4sqlem5 ${⊢}{\phi }\to \left({F}\in ℤ\wedge \frac{{B}-{F}}{{M}}\in ℤ\right)$
27 26 simpld ${⊢}{\phi }\to {F}\in ℤ$
28 zsqcl ${⊢}{F}\in ℤ\to {{F}}^{2}\in ℤ$
29 27 28 syl ${⊢}{\phi }\to {{F}}^{2}\in ℤ$
30 29 zred ${⊢}{\phi }\to {{F}}^{2}\in ℝ$
31 25 30 readdcld ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}\in ℝ$
32 11 20 15 4sqlem5 ${⊢}{\phi }\to \left({G}\in ℤ\wedge \frac{{C}-{G}}{{M}}\in ℤ\right)$
33 32 simpld ${⊢}{\phi }\to {G}\in ℤ$
34 zsqcl ${⊢}{G}\in ℤ\to {{G}}^{2}\in ℤ$
35 33 34 syl ${⊢}{\phi }\to {{G}}^{2}\in ℤ$
36 35 zred ${⊢}{\phi }\to {{G}}^{2}\in ℝ$
37 12 20 16 4sqlem5 ${⊢}{\phi }\to \left({H}\in ℤ\wedge \frac{{D}-{H}}{{M}}\in ℤ\right)$
38 37 simpld ${⊢}{\phi }\to {H}\in ℤ$
39 zsqcl ${⊢}{H}\in ℤ\to {{H}}^{2}\in ℤ$
40 38 39 syl ${⊢}{\phi }\to {{H}}^{2}\in ℤ$
41 40 zred ${⊢}{\phi }\to {{H}}^{2}\in ℝ$
42 36 41 readdcld ${⊢}{\phi }\to {{G}}^{2}+{{H}}^{2}\in ℝ$
43 20 nnred ${⊢}{\phi }\to {M}\in ℝ$
44 43 resqcld ${⊢}{\phi }\to {{M}}^{2}\in ℝ$
45 44 rehalfcld ${⊢}{\phi }\to \frac{{{M}}^{2}}{2}\in ℝ$
46 45 rehalfcld ${⊢}{\phi }\to \frac{\frac{{{M}}^{2}}{2}}{2}\in ℝ$
47 9 20 13 4sqlem7 ${⊢}{\phi }\to {{E}}^{2}\le \frac{\frac{{{M}}^{2}}{2}}{2}$
48 10 20 14 4sqlem7 ${⊢}{\phi }\to {{F}}^{2}\le \frac{\frac{{{M}}^{2}}{2}}{2}$
49 25 30 46 46 47 48 le2addd ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}\le \left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)+\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)$
50 45 recnd ${⊢}{\phi }\to \frac{{{M}}^{2}}{2}\in ℂ$
51 50 2halvesd ${⊢}{\phi }\to \left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)+\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)=\frac{{{M}}^{2}}{2}$
52 49 51 breqtrd ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}\le \frac{{{M}}^{2}}{2}$
53 11 20 15 4sqlem7 ${⊢}{\phi }\to {{G}}^{2}\le \frac{\frac{{{M}}^{2}}{2}}{2}$
54 12 20 16 4sqlem7 ${⊢}{\phi }\to {{H}}^{2}\le \frac{\frac{{{M}}^{2}}{2}}{2}$
55 36 41 46 46 53 54 le2addd ${⊢}{\phi }\to {{G}}^{2}+{{H}}^{2}\le \left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)+\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)$
56 55 51 breqtrd ${⊢}{\phi }\to {{G}}^{2}+{{H}}^{2}\le \frac{{{M}}^{2}}{2}$
57 31 42 45 45 52 56 le2addd ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\le \left(\frac{{{M}}^{2}}{2}\right)+\left(\frac{{{M}}^{2}}{2}\right)$
58 44 recnd ${⊢}{\phi }\to {{M}}^{2}\in ℂ$
59 58 2halvesd ${⊢}{\phi }\to \left(\frac{{{M}}^{2}}{2}\right)+\left(\frac{{{M}}^{2}}{2}\right)={{M}}^{2}$
60 57 59 breqtrd ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\le {{M}}^{2}$
61 43 recnd ${⊢}{\phi }\to {M}\in ℂ$
62 61 sqvald ${⊢}{\phi }\to {{M}}^{2}={M}\cdot {M}$
63 60 62 breqtrd ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\le {M}\cdot {M}$
64 31 42 readdcld ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\in ℝ$
65 20 nngt0d ${⊢}{\phi }\to 0<{M}$
66 ledivmul ${⊢}\left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\in ℝ\wedge {M}\in ℝ\wedge \left({M}\in ℝ\wedge 0<{M}\right)\right)\to \left(\frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}\le {M}↔{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\le {M}\cdot {M}\right)$
67 64 43 43 65 66 syl112anc ${⊢}{\phi }\to \left(\frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}\le {M}↔{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\le {M}\cdot {M}\right)$
68 63 67 mpbird ${⊢}{\phi }\to \frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}\le {M}$
69 17 68 eqbrtrid ${⊢}{\phi }\to {R}\le {M}$
70 simpr ${⊢}\left({\phi }\wedge {R}=0\right)\to {R}=0$
71 17 70 syl5eqr ${⊢}\left({\phi }\wedge {R}=0\right)\to \frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}=0$
72 64 recnd ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\in ℂ$
73 20 nnne0d ${⊢}{\phi }\to {M}\ne 0$
74 72 61 73 diveq0ad ${⊢}{\phi }\to \left(\frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}=0↔{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}=0\right)$
75 zsqcl2 ${⊢}{E}\in ℤ\to {{E}}^{2}\in {ℕ}_{0}$
76 22 75 syl ${⊢}{\phi }\to {{E}}^{2}\in {ℕ}_{0}$
77 zsqcl2 ${⊢}{F}\in ℤ\to {{F}}^{2}\in {ℕ}_{0}$
78 27 77 syl ${⊢}{\phi }\to {{F}}^{2}\in {ℕ}_{0}$
79 76 78 nn0addcld ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}\in {ℕ}_{0}$
80 79 nn0ge0d ${⊢}{\phi }\to 0\le {{E}}^{2}+{{F}}^{2}$
81 zsqcl2 ${⊢}{G}\in ℤ\to {{G}}^{2}\in {ℕ}_{0}$
82 33 81 syl ${⊢}{\phi }\to {{G}}^{2}\in {ℕ}_{0}$
83 zsqcl2 ${⊢}{H}\in ℤ\to {{H}}^{2}\in {ℕ}_{0}$
84 38 83 syl ${⊢}{\phi }\to {{H}}^{2}\in {ℕ}_{0}$
85 82 84 nn0addcld ${⊢}{\phi }\to {{G}}^{2}+{{H}}^{2}\in {ℕ}_{0}$
86 85 nn0ge0d ${⊢}{\phi }\to 0\le {{G}}^{2}+{{H}}^{2}$
87 add20 ${⊢}\left(\left({{E}}^{2}+{{F}}^{2}\in ℝ\wedge 0\le {{E}}^{2}+{{F}}^{2}\right)\wedge \left({{G}}^{2}+{{H}}^{2}\in ℝ\wedge 0\le {{G}}^{2}+{{H}}^{2}\right)\right)\to \left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}=0↔\left({{E}}^{2}+{{F}}^{2}=0\wedge {{G}}^{2}+{{H}}^{2}=0\right)\right)$
88 31 80 42 86 87 syl22anc ${⊢}{\phi }\to \left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}=0↔\left({{E}}^{2}+{{F}}^{2}=0\wedge {{G}}^{2}+{{H}}^{2}=0\right)\right)$
89 74 88 bitrd ${⊢}{\phi }\to \left(\frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}=0↔\left({{E}}^{2}+{{F}}^{2}=0\wedge {{G}}^{2}+{{H}}^{2}=0\right)\right)$
90 89 biimpa ${⊢}\left({\phi }\wedge \frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}=0\right)\to \left({{E}}^{2}+{{F}}^{2}=0\wedge {{G}}^{2}+{{H}}^{2}=0\right)$
91 71 90 syldan ${⊢}\left({\phi }\wedge {R}=0\right)\to \left({{E}}^{2}+{{F}}^{2}=0\wedge {{G}}^{2}+{{H}}^{2}=0\right)$
92 91 simpld ${⊢}\left({\phi }\wedge {R}=0\right)\to {{E}}^{2}+{{F}}^{2}=0$
93 76 nn0ge0d ${⊢}{\phi }\to 0\le {{E}}^{2}$
94 78 nn0ge0d ${⊢}{\phi }\to 0\le {{F}}^{2}$
95 add20 ${⊢}\left(\left({{E}}^{2}\in ℝ\wedge 0\le {{E}}^{2}\right)\wedge \left({{F}}^{2}\in ℝ\wedge 0\le {{F}}^{2}\right)\right)\to \left({{E}}^{2}+{{F}}^{2}=0↔\left({{E}}^{2}=0\wedge {{F}}^{2}=0\right)\right)$
96 25 93 30 94 95 syl22anc ${⊢}{\phi }\to \left({{E}}^{2}+{{F}}^{2}=0↔\left({{E}}^{2}=0\wedge {{F}}^{2}=0\right)\right)$
97 96 biimpa ${⊢}\left({\phi }\wedge {{E}}^{2}+{{F}}^{2}=0\right)\to \left({{E}}^{2}=0\wedge {{F}}^{2}=0\right)$
98 92 97 syldan ${⊢}\left({\phi }\wedge {R}=0\right)\to \left({{E}}^{2}=0\wedge {{F}}^{2}=0\right)$
99 98 simpld ${⊢}\left({\phi }\wedge {R}=0\right)\to {{E}}^{2}=0$
100 9 20 13 99 4sqlem9 ${⊢}\left({\phi }\wedge {R}=0\right)\to {{M}}^{2}\parallel {{A}}^{2}$
101 98 simprd ${⊢}\left({\phi }\wedge {R}=0\right)\to {{F}}^{2}=0$
102 10 20 14 101 4sqlem9 ${⊢}\left({\phi }\wedge {R}=0\right)\to {{M}}^{2}\parallel {{B}}^{2}$
103 20 nnsqcld ${⊢}{\phi }\to {{M}}^{2}\in ℕ$
104 103 nnzd ${⊢}{\phi }\to {{M}}^{2}\in ℤ$
105 zsqcl ${⊢}{A}\in ℤ\to {{A}}^{2}\in ℤ$
106 9 105 syl ${⊢}{\phi }\to {{A}}^{2}\in ℤ$
107 zsqcl ${⊢}{B}\in ℤ\to {{B}}^{2}\in ℤ$
108 10 107 syl ${⊢}{\phi }\to {{B}}^{2}\in ℤ$
109 dvds2add ${⊢}\left({{M}}^{2}\in ℤ\wedge {{A}}^{2}\in ℤ\wedge {{B}}^{2}\in ℤ\right)\to \left(\left({{M}}^{2}\parallel {{A}}^{2}\wedge {{M}}^{2}\parallel {{B}}^{2}\right)\to {{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}\right)\right)$
110 104 106 108 109 syl3anc ${⊢}{\phi }\to \left(\left({{M}}^{2}\parallel {{A}}^{2}\wedge {{M}}^{2}\parallel {{B}}^{2}\right)\to {{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}\right)\right)$
111 110 adantr ${⊢}\left({\phi }\wedge {R}=0\right)\to \left(\left({{M}}^{2}\parallel {{A}}^{2}\wedge {{M}}^{2}\parallel {{B}}^{2}\right)\to {{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}\right)\right)$
112 100 102 111 mp2and ${⊢}\left({\phi }\wedge {R}=0\right)\to {{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}\right)$
113 91 simprd ${⊢}\left({\phi }\wedge {R}=0\right)\to {{G}}^{2}+{{H}}^{2}=0$
114 82 nn0ge0d ${⊢}{\phi }\to 0\le {{G}}^{2}$
115 84 nn0ge0d ${⊢}{\phi }\to 0\le {{H}}^{2}$
116 add20 ${⊢}\left(\left({{G}}^{2}\in ℝ\wedge 0\le {{G}}^{2}\right)\wedge \left({{H}}^{2}\in ℝ\wedge 0\le {{H}}^{2}\right)\right)\to \left({{G}}^{2}+{{H}}^{2}=0↔\left({{G}}^{2}=0\wedge {{H}}^{2}=0\right)\right)$
117 36 114 41 115 116 syl22anc ${⊢}{\phi }\to \left({{G}}^{2}+{{H}}^{2}=0↔\left({{G}}^{2}=0\wedge {{H}}^{2}=0\right)\right)$
118 117 biimpa ${⊢}\left({\phi }\wedge {{G}}^{2}+{{H}}^{2}=0\right)\to \left({{G}}^{2}=0\wedge {{H}}^{2}=0\right)$
119 113 118 syldan ${⊢}\left({\phi }\wedge {R}=0\right)\to \left({{G}}^{2}=0\wedge {{H}}^{2}=0\right)$
120 119 simpld ${⊢}\left({\phi }\wedge {R}=0\right)\to {{G}}^{2}=0$
121 11 20 15 120 4sqlem9 ${⊢}\left({\phi }\wedge {R}=0\right)\to {{M}}^{2}\parallel {{C}}^{2}$
122 119 simprd ${⊢}\left({\phi }\wedge {R}=0\right)\to {{H}}^{2}=0$
123 12 20 16 122 4sqlem9 ${⊢}\left({\phi }\wedge {R}=0\right)\to {{M}}^{2}\parallel {{D}}^{2}$
124 zsqcl ${⊢}{C}\in ℤ\to {{C}}^{2}\in ℤ$
125 11 124 syl ${⊢}{\phi }\to {{C}}^{2}\in ℤ$
126 zsqcl ${⊢}{D}\in ℤ\to {{D}}^{2}\in ℤ$
127 12 126 syl ${⊢}{\phi }\to {{D}}^{2}\in ℤ$
128 dvds2add ${⊢}\left({{M}}^{2}\in ℤ\wedge {{C}}^{2}\in ℤ\wedge {{D}}^{2}\in ℤ\right)\to \left(\left({{M}}^{2}\parallel {{C}}^{2}\wedge {{M}}^{2}\parallel {{D}}^{2}\right)\to {{M}}^{2}\parallel \left({{C}}^{2}+{{D}}^{2}\right)\right)$
129 104 125 127 128 syl3anc ${⊢}{\phi }\to \left(\left({{M}}^{2}\parallel {{C}}^{2}\wedge {{M}}^{2}\parallel {{D}}^{2}\right)\to {{M}}^{2}\parallel \left({{C}}^{2}+{{D}}^{2}\right)\right)$
130 129 adantr ${⊢}\left({\phi }\wedge {R}=0\right)\to \left(\left({{M}}^{2}\parallel {{C}}^{2}\wedge {{M}}^{2}\parallel {{D}}^{2}\right)\to {{M}}^{2}\parallel \left({{C}}^{2}+{{D}}^{2}\right)\right)$
131 121 123 130 mp2and ${⊢}\left({\phi }\wedge {R}=0\right)\to {{M}}^{2}\parallel \left({{C}}^{2}+{{D}}^{2}\right)$
132 106 108 zaddcld ${⊢}{\phi }\to {{A}}^{2}+{{B}}^{2}\in ℤ$
133 125 127 zaddcld ${⊢}{\phi }\to {{C}}^{2}+{{D}}^{2}\in ℤ$
134 dvds2add ${⊢}\left({{M}}^{2}\in ℤ\wedge {{A}}^{2}+{{B}}^{2}\in ℤ\wedge {{C}}^{2}+{{D}}^{2}\in ℤ\right)\to \left(\left({{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}\right)\wedge {{M}}^{2}\parallel \left({{C}}^{2}+{{D}}^{2}\right)\right)\to {{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}\right)\right)$
135 104 132 133 134 syl3anc ${⊢}{\phi }\to \left(\left({{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}\right)\wedge {{M}}^{2}\parallel \left({{C}}^{2}+{{D}}^{2}\right)\right)\to {{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}\right)\right)$
136 135 adantr ${⊢}\left({\phi }\wedge {R}=0\right)\to \left(\left({{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}\right)\wedge {{M}}^{2}\parallel \left({{C}}^{2}+{{D}}^{2}\right)\right)\to {{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}\right)\right)$
137 112 131 136 mp2and ${⊢}\left({\phi }\wedge {R}=0\right)\to {{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}\right)$
138 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 4sqlem15 ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left(\left(\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{E}}^{2}=0\wedge \left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{F}}^{2}=0\right)\wedge \left(\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{G}}^{2}=0\wedge \left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{H}}^{2}=0\right)\right)$
139 138 simpld ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left(\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{E}}^{2}=0\wedge \left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{F}}^{2}=0\right)$
140 139 simpld ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{E}}^{2}=0$
141 9 20 13 140 4sqlem10 ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{M}}^{2}\parallel \left({{A}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)$
142 139 simprd ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{F}}^{2}=0$
143 10 20 14 142 4sqlem10 ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{M}}^{2}\parallel \left({{B}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)$
144 104 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{M}}^{2}\in ℤ$
145 106 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{A}}^{2}\in ℤ$
146 46 recnd ${⊢}{\phi }\to \frac{\frac{{{M}}^{2}}{2}}{2}\in ℂ$
147 24 zcnd ${⊢}{\phi }\to {{E}}^{2}\in ℂ$
148 146 147 subeq0ad ${⊢}{\phi }\to \left(\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{E}}^{2}=0↔\frac{\frac{{{M}}^{2}}{2}}{2}={{E}}^{2}\right)$
149 148 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left(\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{E}}^{2}=0↔\frac{\frac{{{M}}^{2}}{2}}{2}={{E}}^{2}\right)$
150 140 149 mpbid ${⊢}\left({\phi }\wedge {R}={M}\right)\to \frac{\frac{{{M}}^{2}}{2}}{2}={{E}}^{2}$
151 24 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{E}}^{2}\in ℤ$
152 150 151 eqeltrd ${⊢}\left({\phi }\wedge {R}={M}\right)\to \frac{\frac{{{M}}^{2}}{2}}{2}\in ℤ$
153 145 152 zsubcld ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{A}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\in ℤ$
154 108 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{B}}^{2}\in ℤ$
155 154 152 zsubcld ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{B}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\in ℤ$
156 dvds2add ${⊢}\left({{M}}^{2}\in ℤ\wedge {{A}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\in ℤ\wedge {{B}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\in ℤ\right)\to \left(\left({{M}}^{2}\parallel \left({{A}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)\wedge {{M}}^{2}\parallel \left({{B}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)\right)\to {{M}}^{2}\parallel \left(\left({{A}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)+{{B}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)\right)$
157 144 153 155 156 syl3anc ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left(\left({{M}}^{2}\parallel \left({{A}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)\wedge {{M}}^{2}\parallel \left({{B}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)\right)\to {{M}}^{2}\parallel \left(\left({{A}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)+{{B}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)\right)$
158 141 143 157 mp2and ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{M}}^{2}\parallel \left(\left({{A}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)+{{B}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)$
159 106 zcnd ${⊢}{\phi }\to {{A}}^{2}\in ℂ$
160 108 zcnd ${⊢}{\phi }\to {{B}}^{2}\in ℂ$
161 159 160 146 146 addsub4d ${⊢}{\phi }\to {{A}}^{2}+{{B}}^{2}-\left(\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)+\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)=\left({{A}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)+{{B}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)$
162 51 oveq2d ${⊢}{\phi }\to {{A}}^{2}+{{B}}^{2}-\left(\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)+\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)={{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)$
163 161 162 eqtr3d ${⊢}{\phi }\to \left({{A}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)+{{B}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)={{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)$
164 163 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left({{A}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)+{{B}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)={{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)$
165 158 164 breqtrd ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\right)$
166 138 simprd ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left(\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{G}}^{2}=0\wedge \left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{H}}^{2}=0\right)$
167 166 simpld ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{G}}^{2}=0$
168 11 20 15 167 4sqlem10 ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{M}}^{2}\parallel \left({{C}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)$
169 166 simprd ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)-{{H}}^{2}=0$
170 12 20 16 169 4sqlem10 ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{M}}^{2}\parallel \left({{D}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)$
171 125 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{C}}^{2}\in ℤ$
172 171 152 zsubcld ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{C}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\in ℤ$
173 127 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{D}}^{2}\in ℤ$
174 173 152 zsubcld ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{D}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\in ℤ$
175 dvds2add ${⊢}\left({{M}}^{2}\in ℤ\wedge {{C}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\in ℤ\wedge {{D}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\in ℤ\right)\to \left(\left({{M}}^{2}\parallel \left({{C}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)\wedge {{M}}^{2}\parallel \left({{D}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)\right)\to {{M}}^{2}\parallel \left(\left({{C}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)+{{D}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)\right)$
176 144 172 174 175 syl3anc ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left(\left({{M}}^{2}\parallel \left({{C}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)\wedge {{M}}^{2}\parallel \left({{D}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)\right)\to {{M}}^{2}\parallel \left(\left({{C}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)+{{D}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)\right)$
177 168 170 176 mp2and ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{M}}^{2}\parallel \left(\left({{C}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)+{{D}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)$
178 125 zcnd ${⊢}{\phi }\to {{C}}^{2}\in ℂ$
179 127 zcnd ${⊢}{\phi }\to {{D}}^{2}\in ℂ$
180 178 179 146 146 addsub4d ${⊢}{\phi }\to {{C}}^{2}+{{D}}^{2}-\left(\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)+\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)=\left({{C}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)+{{D}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)$
181 51 oveq2d ${⊢}{\phi }\to {{C}}^{2}+{{D}}^{2}-\left(\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)+\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)={{C}}^{2}+{{D}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)$
182 180 181 eqtr3d ${⊢}{\phi }\to \left({{C}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)+{{D}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)={{C}}^{2}+{{D}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)$
183 182 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left({{C}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\right)+{{D}}^{2}-\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)={{C}}^{2}+{{D}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)$
184 177 183 breqtrd ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{M}}^{2}\parallel \left({{C}}^{2}+{{D}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\right)$
185 132 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{A}}^{2}+{{B}}^{2}\in ℤ$
186 51 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)+\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)=\frac{{{M}}^{2}}{2}$
187 152 152 zaddcld ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)+\left(\frac{\frac{{{M}}^{2}}{2}}{2}\right)\in ℤ$
188 186 187 eqeltrrd ${⊢}\left({\phi }\wedge {R}={M}\right)\to \frac{{{M}}^{2}}{2}\in ℤ$
189 185 188 zsubcld ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\in ℤ$
190 133 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{C}}^{2}+{{D}}^{2}\in ℤ$
191 190 188 zsubcld ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{C}}^{2}+{{D}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\in ℤ$
192 dvds2add ${⊢}\left({{M}}^{2}\in ℤ\wedge {{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\in ℤ\wedge {{C}}^{2}+{{D}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\in ℤ\right)\to \left(\left({{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\right)\wedge {{M}}^{2}\parallel \left({{C}}^{2}+{{D}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\right)\right)\to {{M}}^{2}\parallel \left(\left({{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left(\frac{{{M}}^{2}}{2}\right)\right)\right)$
193 144 189 191 192 syl3anc ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left(\left({{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\right)\wedge {{M}}^{2}\parallel \left({{C}}^{2}+{{D}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\right)\right)\to {{M}}^{2}\parallel \left(\left({{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left(\frac{{{M}}^{2}}{2}\right)\right)\right)$
194 165 184 193 mp2and ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{M}}^{2}\parallel \left(\left({{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left(\frac{{{M}}^{2}}{2}\right)\right)$
195 132 zcnd ${⊢}{\phi }\to {{A}}^{2}+{{B}}^{2}\in ℂ$
196 133 zcnd ${⊢}{\phi }\to {{C}}^{2}+{{D}}^{2}\in ℂ$
197 195 196 50 50 addsub4d ${⊢}{\phi }\to \left({{A}}^{2}+{{B}}^{2}\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left(\left(\frac{{{M}}^{2}}{2}\right)+\left(\frac{{{M}}^{2}}{2}\right)\right)=\left({{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left(\frac{{{M}}^{2}}{2}\right)$
198 59 oveq2d ${⊢}{\phi }\to \left({{A}}^{2}+{{B}}^{2}\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left(\left(\frac{{{M}}^{2}}{2}\right)+\left(\frac{{{M}}^{2}}{2}\right)\right)=\left({{A}}^{2}+{{B}}^{2}\right)+\left({{C}}^{2}+{{D}}^{2}\right)-{{M}}^{2}$
199 197 198 eqtr3d ${⊢}{\phi }\to \left({{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left(\frac{{{M}}^{2}}{2}\right)=\left({{A}}^{2}+{{B}}^{2}\right)+\left({{C}}^{2}+{{D}}^{2}\right)-{{M}}^{2}$
200 199 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left({{A}}^{2}+{{B}}^{2}-\left(\frac{{{M}}^{2}}{2}\right)\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left(\frac{{{M}}^{2}}{2}\right)=\left({{A}}^{2}+{{B}}^{2}\right)+\left({{C}}^{2}+{{D}}^{2}\right)-{{M}}^{2}$
201 194 200 breqtrd ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{M}}^{2}\parallel \left(\left({{A}}^{2}+{{B}}^{2}\right)+\left({{C}}^{2}+{{D}}^{2}\right)-{{M}}^{2}\right)$
202 132 133 zaddcld ${⊢}{\phi }\to {{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}\in ℤ$
203 202 adantr ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}\in ℤ$
204 dvdssubr ${⊢}\left({{M}}^{2}\in ℤ\wedge {{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}\in ℤ\right)\to \left({{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}\right)↔{{M}}^{2}\parallel \left(\left({{A}}^{2}+{{B}}^{2}\right)+\left({{C}}^{2}+{{D}}^{2}\right)-{{M}}^{2}\right)\right)$
205 144 203 204 syl2anc ${⊢}\left({\phi }\wedge {R}={M}\right)\to \left({{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}\right)↔{{M}}^{2}\parallel \left(\left({{A}}^{2}+{{B}}^{2}\right)+\left({{C}}^{2}+{{D}}^{2}\right)-{{M}}^{2}\right)\right)$
206 201 205 mpbird ${⊢}\left({\phi }\wedge {R}={M}\right)\to {{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}\right)$
207 137 206 jaodan ${⊢}\left({\phi }\wedge \left({R}=0\vee {R}={M}\right)\right)\to {{M}}^{2}\parallel \left({{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}\right)$
208 18 adantr ${⊢}\left({\phi }\wedge \left({R}=0\vee {R}={M}\right)\right)\to {M}{P}={{A}}^{2}+{{B}}^{2}+{{C}}^{2}+{{D}}^{2}$
209 207 208 breqtrrd ${⊢}\left({\phi }\wedge \left({R}=0\vee {R}={M}\right)\right)\to {{M}}^{2}\parallel {M}{P}$
210 209 ex ${⊢}{\phi }\to \left(\left({R}=0\vee {R}={M}\right)\to {{M}}^{2}\parallel {M}{P}\right)$
211 69 210 jca ${⊢}{\phi }\to \left({R}\le {M}\wedge \left(\left({R}=0\vee {R}={M}\right)\to {{M}}^{2}\parallel {M}{P}\right)\right)$