# 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 ${⊢}{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 4sqlem14 ${⊢}{\phi }\to {R}\in {ℕ}_{0}$

### 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 6 ssrab3 ${⊢}{T}\subseteq ℕ$
20 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
21 19 20 sseqtri ${⊢}{T}\subseteq {ℤ}_{\ge 1}$
22 1 2 3 4 5 6 7 4sqlem13 ${⊢}{\phi }\to \left({T}\ne \varnothing \wedge {M}<{P}\right)$
23 22 simpld ${⊢}{\phi }\to {T}\ne \varnothing$
24 infssuzcl ${⊢}\left({T}\subseteq {ℤ}_{\ge 1}\wedge {T}\ne \varnothing \right)\to sup\left({T},ℝ,<\right)\in {T}$
25 21 23 24 sylancr ${⊢}{\phi }\to sup\left({T},ℝ,<\right)\in {T}$
26 7 25 eqeltrid ${⊢}{\phi }\to {M}\in {T}$
27 19 26 sseldi ${⊢}{\phi }\to {M}\in ℕ$
28 27 nnzd ${⊢}{\phi }\to {M}\in ℤ$
29 prmz ${⊢}{P}\in ℙ\to {P}\in ℤ$
30 4 29 syl ${⊢}{\phi }\to {P}\in ℤ$
31 dvdsmul1 ${⊢}\left({M}\in ℤ\wedge {P}\in ℤ\right)\to {M}\parallel {M}{P}$
32 28 30 31 syl2anc ${⊢}{\phi }\to {M}\parallel {M}{P}$
33 9 27 13 4sqlem8 ${⊢}{\phi }\to {M}\parallel \left({{A}}^{2}-{{E}}^{2}\right)$
34 10 27 14 4sqlem8 ${⊢}{\phi }\to {M}\parallel \left({{B}}^{2}-{{F}}^{2}\right)$
35 zsqcl ${⊢}{A}\in ℤ\to {{A}}^{2}\in ℤ$
36 9 35 syl ${⊢}{\phi }\to {{A}}^{2}\in ℤ$
37 9 27 13 4sqlem5 ${⊢}{\phi }\to \left({E}\in ℤ\wedge \frac{{A}-{E}}{{M}}\in ℤ\right)$
38 37 simpld ${⊢}{\phi }\to {E}\in ℤ$
39 zsqcl2 ${⊢}{E}\in ℤ\to {{E}}^{2}\in {ℕ}_{0}$
40 38 39 syl ${⊢}{\phi }\to {{E}}^{2}\in {ℕ}_{0}$
41 40 nn0zd ${⊢}{\phi }\to {{E}}^{2}\in ℤ$
42 36 41 zsubcld ${⊢}{\phi }\to {{A}}^{2}-{{E}}^{2}\in ℤ$
43 zsqcl ${⊢}{B}\in ℤ\to {{B}}^{2}\in ℤ$
44 10 43 syl ${⊢}{\phi }\to {{B}}^{2}\in ℤ$
45 10 27 14 4sqlem5 ${⊢}{\phi }\to \left({F}\in ℤ\wedge \frac{{B}-{F}}{{M}}\in ℤ\right)$
46 45 simpld ${⊢}{\phi }\to {F}\in ℤ$
47 zsqcl2 ${⊢}{F}\in ℤ\to {{F}}^{2}\in {ℕ}_{0}$
48 46 47 syl ${⊢}{\phi }\to {{F}}^{2}\in {ℕ}_{0}$
49 48 nn0zd ${⊢}{\phi }\to {{F}}^{2}\in ℤ$
50 44 49 zsubcld ${⊢}{\phi }\to {{B}}^{2}-{{F}}^{2}\in ℤ$
51 dvds2add ${⊢}\left({M}\in ℤ\wedge {{A}}^{2}-{{E}}^{2}\in ℤ\wedge {{B}}^{2}-{{F}}^{2}\in ℤ\right)\to \left(\left({M}\parallel \left({{A}}^{2}-{{E}}^{2}\right)\wedge {M}\parallel \left({{B}}^{2}-{{F}}^{2}\right)\right)\to {M}\parallel \left(\left({{A}}^{2}-{{E}}^{2}\right)+{{B}}^{2}-{{F}}^{2}\right)\right)$
52 28 42 50 51 syl3anc ${⊢}{\phi }\to \left(\left({M}\parallel \left({{A}}^{2}-{{E}}^{2}\right)\wedge {M}\parallel \left({{B}}^{2}-{{F}}^{2}\right)\right)\to {M}\parallel \left(\left({{A}}^{2}-{{E}}^{2}\right)+{{B}}^{2}-{{F}}^{2}\right)\right)$
53 33 34 52 mp2and ${⊢}{\phi }\to {M}\parallel \left(\left({{A}}^{2}-{{E}}^{2}\right)+{{B}}^{2}-{{F}}^{2}\right)$
54 9 zcnd ${⊢}{\phi }\to {A}\in ℂ$
55 54 sqcld ${⊢}{\phi }\to {{A}}^{2}\in ℂ$
56 10 zcnd ${⊢}{\phi }\to {B}\in ℂ$
57 56 sqcld ${⊢}{\phi }\to {{B}}^{2}\in ℂ$
58 38 zcnd ${⊢}{\phi }\to {E}\in ℂ$
59 58 sqcld ${⊢}{\phi }\to {{E}}^{2}\in ℂ$
60 46 zcnd ${⊢}{\phi }\to {F}\in ℂ$
61 60 sqcld ${⊢}{\phi }\to {{F}}^{2}\in ℂ$
62 55 57 59 61 addsub4d ${⊢}{\phi }\to {{A}}^{2}+{{B}}^{2}-\left({{E}}^{2}+{{F}}^{2}\right)=\left({{A}}^{2}-{{E}}^{2}\right)+{{B}}^{2}-{{F}}^{2}$
63 53 62 breqtrrd ${⊢}{\phi }\to {M}\parallel \left({{A}}^{2}+{{B}}^{2}-\left({{E}}^{2}+{{F}}^{2}\right)\right)$
64 11 27 15 4sqlem8 ${⊢}{\phi }\to {M}\parallel \left({{C}}^{2}-{{G}}^{2}\right)$
65 12 27 16 4sqlem8 ${⊢}{\phi }\to {M}\parallel \left({{D}}^{2}-{{H}}^{2}\right)$
66 zsqcl ${⊢}{C}\in ℤ\to {{C}}^{2}\in ℤ$
67 11 66 syl ${⊢}{\phi }\to {{C}}^{2}\in ℤ$
68 11 27 15 4sqlem5 ${⊢}{\phi }\to \left({G}\in ℤ\wedge \frac{{C}-{G}}{{M}}\in ℤ\right)$
69 68 simpld ${⊢}{\phi }\to {G}\in ℤ$
70 zsqcl2 ${⊢}{G}\in ℤ\to {{G}}^{2}\in {ℕ}_{0}$
71 69 70 syl ${⊢}{\phi }\to {{G}}^{2}\in {ℕ}_{0}$
72 71 nn0zd ${⊢}{\phi }\to {{G}}^{2}\in ℤ$
73 67 72 zsubcld ${⊢}{\phi }\to {{C}}^{2}-{{G}}^{2}\in ℤ$
74 zsqcl ${⊢}{D}\in ℤ\to {{D}}^{2}\in ℤ$
75 12 74 syl ${⊢}{\phi }\to {{D}}^{2}\in ℤ$
76 12 27 16 4sqlem5 ${⊢}{\phi }\to \left({H}\in ℤ\wedge \frac{{D}-{H}}{{M}}\in ℤ\right)$
77 76 simpld ${⊢}{\phi }\to {H}\in ℤ$
78 zsqcl2 ${⊢}{H}\in ℤ\to {{H}}^{2}\in {ℕ}_{0}$
79 77 78 syl ${⊢}{\phi }\to {{H}}^{2}\in {ℕ}_{0}$
80 79 nn0zd ${⊢}{\phi }\to {{H}}^{2}\in ℤ$
81 75 80 zsubcld ${⊢}{\phi }\to {{D}}^{2}-{{H}}^{2}\in ℤ$
82 dvds2add ${⊢}\left({M}\in ℤ\wedge {{C}}^{2}-{{G}}^{2}\in ℤ\wedge {{D}}^{2}-{{H}}^{2}\in ℤ\right)\to \left(\left({M}\parallel \left({{C}}^{2}-{{G}}^{2}\right)\wedge {M}\parallel \left({{D}}^{2}-{{H}}^{2}\right)\right)\to {M}\parallel \left(\left({{C}}^{2}-{{G}}^{2}\right)+{{D}}^{2}-{{H}}^{2}\right)\right)$
83 28 73 81 82 syl3anc ${⊢}{\phi }\to \left(\left({M}\parallel \left({{C}}^{2}-{{G}}^{2}\right)\wedge {M}\parallel \left({{D}}^{2}-{{H}}^{2}\right)\right)\to {M}\parallel \left(\left({{C}}^{2}-{{G}}^{2}\right)+{{D}}^{2}-{{H}}^{2}\right)\right)$
84 64 65 83 mp2and ${⊢}{\phi }\to {M}\parallel \left(\left({{C}}^{2}-{{G}}^{2}\right)+{{D}}^{2}-{{H}}^{2}\right)$
85 11 zcnd ${⊢}{\phi }\to {C}\in ℂ$
86 85 sqcld ${⊢}{\phi }\to {{C}}^{2}\in ℂ$
87 12 zcnd ${⊢}{\phi }\to {D}\in ℂ$
88 87 sqcld ${⊢}{\phi }\to {{D}}^{2}\in ℂ$
89 69 zcnd ${⊢}{\phi }\to {G}\in ℂ$
90 89 sqcld ${⊢}{\phi }\to {{G}}^{2}\in ℂ$
91 77 zcnd ${⊢}{\phi }\to {H}\in ℂ$
92 91 sqcld ${⊢}{\phi }\to {{H}}^{2}\in ℂ$
93 86 88 90 92 addsub4d ${⊢}{\phi }\to {{C}}^{2}+{{D}}^{2}-\left({{G}}^{2}+{{H}}^{2}\right)=\left({{C}}^{2}-{{G}}^{2}\right)+{{D}}^{2}-{{H}}^{2}$
94 84 93 breqtrrd ${⊢}{\phi }\to {M}\parallel \left({{C}}^{2}+{{D}}^{2}-\left({{G}}^{2}+{{H}}^{2}\right)\right)$
95 36 44 zaddcld ${⊢}{\phi }\to {{A}}^{2}+{{B}}^{2}\in ℤ$
96 40 48 nn0addcld ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}\in {ℕ}_{0}$
97 96 nn0zd ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}\in ℤ$
98 95 97 zsubcld ${⊢}{\phi }\to {{A}}^{2}+{{B}}^{2}-\left({{E}}^{2}+{{F}}^{2}\right)\in ℤ$
99 67 75 zaddcld ${⊢}{\phi }\to {{C}}^{2}+{{D}}^{2}\in ℤ$
100 71 79 nn0addcld ${⊢}{\phi }\to {{G}}^{2}+{{H}}^{2}\in {ℕ}_{0}$
101 100 nn0zd ${⊢}{\phi }\to {{G}}^{2}+{{H}}^{2}\in ℤ$
102 99 101 zsubcld ${⊢}{\phi }\to {{C}}^{2}+{{D}}^{2}-\left({{G}}^{2}+{{H}}^{2}\right)\in ℤ$
103 dvds2add ${⊢}\left({M}\in ℤ\wedge {{A}}^{2}+{{B}}^{2}-\left({{E}}^{2}+{{F}}^{2}\right)\in ℤ\wedge {{C}}^{2}+{{D}}^{2}-\left({{G}}^{2}+{{H}}^{2}\right)\in ℤ\right)\to \left(\left({M}\parallel \left({{A}}^{2}+{{B}}^{2}-\left({{E}}^{2}+{{F}}^{2}\right)\right)\wedge {M}\parallel \left({{C}}^{2}+{{D}}^{2}-\left({{G}}^{2}+{{H}}^{2}\right)\right)\right)\to {M}\parallel \left(\left({{A}}^{2}+{{B}}^{2}-\left({{E}}^{2}+{{F}}^{2}\right)\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left({{G}}^{2}+{{H}}^{2}\right)\right)\right)$
104 28 98 102 103 syl3anc ${⊢}{\phi }\to \left(\left({M}\parallel \left({{A}}^{2}+{{B}}^{2}-\left({{E}}^{2}+{{F}}^{2}\right)\right)\wedge {M}\parallel \left({{C}}^{2}+{{D}}^{2}-\left({{G}}^{2}+{{H}}^{2}\right)\right)\right)\to {M}\parallel \left(\left({{A}}^{2}+{{B}}^{2}-\left({{E}}^{2}+{{F}}^{2}\right)\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left({{G}}^{2}+{{H}}^{2}\right)\right)\right)$
105 63 94 104 mp2and ${⊢}{\phi }\to {M}\parallel \left(\left({{A}}^{2}+{{B}}^{2}-\left({{E}}^{2}+{{F}}^{2}\right)\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left({{G}}^{2}+{{H}}^{2}\right)\right)$
106 18 oveq1d ${⊢}{\phi }\to {M}{P}-\left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\right)=\left({{A}}^{2}+{{B}}^{2}\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\right)$
107 55 57 addcld ${⊢}{\phi }\to {{A}}^{2}+{{B}}^{2}\in ℂ$
108 86 88 addcld ${⊢}{\phi }\to {{C}}^{2}+{{D}}^{2}\in ℂ$
109 59 61 addcld ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}\in ℂ$
110 90 92 addcld ${⊢}{\phi }\to {{G}}^{2}+{{H}}^{2}\in ℂ$
111 107 108 109 110 addsub4d ${⊢}{\phi }\to \left({{A}}^{2}+{{B}}^{2}\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\right)=\left({{A}}^{2}+{{B}}^{2}-\left({{E}}^{2}+{{F}}^{2}\right)\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left({{G}}^{2}+{{H}}^{2}\right)$
112 106 111 eqtrd ${⊢}{\phi }\to {M}{P}-\left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\right)=\left({{A}}^{2}+{{B}}^{2}-\left({{E}}^{2}+{{F}}^{2}\right)\right)+\left({{C}}^{2}+{{D}}^{2}\right)-\left({{G}}^{2}+{{H}}^{2}\right)$
113 105 112 breqtrrd ${⊢}{\phi }\to {M}\parallel \left({M}{P}-\left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\right)\right)$
114 28 30 zmulcld ${⊢}{\phi }\to {M}{P}\in ℤ$
115 97 101 zaddcld ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\in ℤ$
116 114 115 zsubcld ${⊢}{\phi }\to {M}{P}-\left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\right)\in ℤ$
117 28 32 113 114 116 dvds2subd ${⊢}{\phi }\to {M}\parallel \left({M}{P}-\left({M}{P}-\left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\right)\right)\right)$
118 27 nncnd ${⊢}{\phi }\to {M}\in ℂ$
119 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
120 4 119 syl ${⊢}{\phi }\to {P}\in ℕ$
121 120 nncnd ${⊢}{\phi }\to {P}\in ℂ$
122 118 121 mulcld ${⊢}{\phi }\to {M}{P}\in ℂ$
123 109 110 addcld ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\in ℂ$
124 122 123 nncand ${⊢}{\phi }\to {M}{P}-\left({M}{P}-\left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\right)\right)={{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}$
125 117 124 breqtrd ${⊢}{\phi }\to {M}\parallel \left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\right)$
126 27 nnne0d ${⊢}{\phi }\to {M}\ne 0$
127 96 100 nn0addcld ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\in {ℕ}_{0}$
128 127 nn0zd ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\in ℤ$
129 dvdsval2 ${⊢}\left({M}\in ℤ\wedge {M}\ne 0\wedge {{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\in ℤ\right)\to \left({M}\parallel \left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\right)↔\frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}\in ℤ\right)$
130 28 126 128 129 syl3anc ${⊢}{\phi }\to \left({M}\parallel \left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\right)↔\frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}\in ℤ\right)$
131 125 130 mpbid ${⊢}{\phi }\to \frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}\in ℤ$
132 127 nn0red ${⊢}{\phi }\to {{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\in ℝ$
133 127 nn0ge0d ${⊢}{\phi }\to 0\le {{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}$
134 27 nnred ${⊢}{\phi }\to {M}\in ℝ$
135 27 nngt0d ${⊢}{\phi }\to 0<{M}$
136 divge0 ${⊢}\left(\left({{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\in ℝ\wedge 0\le {{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}\right)\wedge \left({M}\in ℝ\wedge 0<{M}\right)\right)\to 0\le \frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}$
137 132 133 134 135 136 syl22anc ${⊢}{\phi }\to 0\le \frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}$
138 elnn0z ${⊢}\frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}\in {ℕ}_{0}↔\left(\frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}\in ℤ\wedge 0\le \frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}\right)$
139 131 137 138 sylanbrc ${⊢}{\phi }\to \frac{{{E}}^{2}+{{F}}^{2}+{{G}}^{2}+{{H}}^{2}}{{M}}\in {ℕ}_{0}$
140 17 139 eqeltrid ${⊢}{\phi }\to {R}\in {ℕ}_{0}$