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=n|xyzwn=x2+y2+z2+w2
4sq.2 φN
4sq.3 φP=2 N+1
4sq.4 φP
4sq.5 φ02 NS
4sq.6 T=i|iPS
4sq.7 M=supT<
4sq.m φM2
4sq.a φA
4sq.b φB
4sq.c φC
4sq.d φD
4sq.e E=A+M2modMM2
4sq.f F=B+M2modMM2
4sq.g G=C+M2modMM2
4sq.h H=D+M2modMM2
4sq.r R=E2+F2+G2+H2M
4sq.p φMP=A2+B2+C2+D2
Assertion 4sqlem16 φRMR=0R=MM2MP

Proof

Step Hyp Ref Expression
1 4sq.1 S=n|xyzwn=x2+y2+z2+w2
2 4sq.2 φN
3 4sq.3 φP=2 N+1
4 4sq.4 φP
5 4sq.5 φ02 NS
6 4sq.6 T=i|iPS
7 4sq.7 M=supT<
8 4sq.m φM2
9 4sq.a φA
10 4sq.b φB
11 4sq.c φC
12 4sq.d φD
13 4sq.e E=A+M2modMM2
14 4sq.f F=B+M2modMM2
15 4sq.g G=C+M2modMM2
16 4sq.h H=D+M2modMM2
17 4sq.r R=E2+F2+G2+H2M
18 4sq.p φMP=A2+B2+C2+D2
19 eluz2nn M2M
20 8 19 syl φM
21 9 20 13 4sqlem5 φEAEM
22 21 simpld φE
23 zsqcl EE2
24 22 23 syl φE2
25 24 zred φE2
26 10 20 14 4sqlem5 φFBFM
27 26 simpld φF
28 zsqcl FF2
29 27 28 syl φF2
30 29 zred φF2
31 25 30 readdcld φE2+F2
32 11 20 15 4sqlem5 φGCGM
33 32 simpld φG
34 zsqcl GG2
35 33 34 syl φG2
36 35 zred φG2
37 12 20 16 4sqlem5 φHDHM
38 37 simpld φH
39 zsqcl HH2
40 38 39 syl φH2
41 40 zred φH2
42 36 41 readdcld φG2+H2
43 20 nnred φM
44 43 resqcld φM2
45 44 rehalfcld φM22
46 45 rehalfcld φM222
47 9 20 13 4sqlem7 φE2M222
48 10 20 14 4sqlem7 φF2M222
49 25 30 46 46 47 48 le2addd φE2+F2M222+M222
50 45 recnd φM22
51 50 2halvesd φM222+M222=M22
52 49 51 breqtrd φE2+F2M22
53 11 20 15 4sqlem7 φG2M222
54 12 20 16 4sqlem7 φH2M222
55 36 41 46 46 53 54 le2addd φG2+H2M222+M222
56 55 51 breqtrd φG2+H2M22
57 31 42 45 45 52 56 le2addd φE2+F2+G2+H2M22+M22
58 44 recnd φM2
59 58 2halvesd φM22+M22=M2
60 57 59 breqtrd φE2+F2+G2+H2M2
61 43 recnd φM
62 61 sqvald φM2= M M
63 60 62 breqtrd φE2+F2+G2+H2 M M
64 31 42 readdcld φE2+F2+G2+H2
65 20 nngt0d φ0<M
66 ledivmul E2+F2+G2+H2MM0<ME2+F2+G2+H2MME2+F2+G2+H2 M M
67 64 43 43 65 66 syl112anc φE2+F2+G2+H2MME2+F2+G2+H2 M M
68 63 67 mpbird φE2+F2+G2+H2MM
69 17 68 eqbrtrid φRM
70 simpr φR=0R=0
71 17 70 eqtr3id φR=0E2+F2+G2+H2M=0
72 64 recnd φE2+F2+G2+H2
73 20 nnne0d φM0
74 72 61 73 diveq0ad φE2+F2+G2+H2M=0E2+F2+G2+H2=0
75 zsqcl2 EE20
76 22 75 syl φE20
77 zsqcl2 FF20
78 27 77 syl φF20
79 76 78 nn0addcld φE2+F20
80 79 nn0ge0d φ0E2+F2
81 zsqcl2 GG20
82 33 81 syl φG20
83 zsqcl2 HH20
84 38 83 syl φH20
85 82 84 nn0addcld φG2+H20
86 85 nn0ge0d φ0G2+H2
87 add20 E2+F20E2+F2G2+H20G2+H2E2+F2+G2+H2=0E2+F2=0G2+H2=0
88 31 80 42 86 87 syl22anc φE2+F2+G2+H2=0E2+F2=0G2+H2=0
89 74 88 bitrd φE2+F2+G2+H2M=0E2+F2=0G2+H2=0
90 89 biimpa φE2+F2+G2+H2M=0E2+F2=0G2+H2=0
91 71 90 syldan φR=0E2+F2=0G2+H2=0
92 91 simpld φR=0E2+F2=0
93 76 nn0ge0d φ0E2
94 78 nn0ge0d φ0F2
95 add20 E20E2F20F2E2+F2=0E2=0F2=0
96 25 93 30 94 95 syl22anc φE2+F2=0E2=0F2=0
97 96 biimpa φE2+F2=0E2=0F2=0
98 92 97 syldan φR=0E2=0F2=0
99 98 simpld φR=0E2=0
100 9 20 13 99 4sqlem9 φR=0M2A2
101 98 simprd φR=0F2=0
102 10 20 14 101 4sqlem9 φR=0M2B2
103 20 nnsqcld φM2
104 103 nnzd φM2
105 zsqcl AA2
106 9 105 syl φA2
107 zsqcl BB2
108 10 107 syl φB2
109 dvds2add M2A2B2M2A2M2B2M2A2+B2
110 104 106 108 109 syl3anc φM2A2M2B2M2A2+B2
111 110 adantr φR=0M2A2M2B2M2A2+B2
112 100 102 111 mp2and φR=0M2A2+B2
113 91 simprd φR=0G2+H2=0
114 82 nn0ge0d φ0G2
115 84 nn0ge0d φ0H2
116 add20 G20G2H20H2G2+H2=0G2=0H2=0
117 36 114 41 115 116 syl22anc φG2+H2=0G2=0H2=0
118 117 biimpa φG2+H2=0G2=0H2=0
119 113 118 syldan φR=0G2=0H2=0
120 119 simpld φR=0G2=0
121 11 20 15 120 4sqlem9 φR=0M2C2
122 119 simprd φR=0H2=0
123 12 20 16 122 4sqlem9 φR=0M2D2
124 zsqcl CC2
125 11 124 syl φC2
126 zsqcl DD2
127 12 126 syl φD2
128 dvds2add M2C2D2M2C2M2D2M2C2+D2
129 104 125 127 128 syl3anc φM2C2M2D2M2C2+D2
130 129 adantr φR=0M2C2M2D2M2C2+D2
131 121 123 130 mp2and φR=0M2C2+D2
132 106 108 zaddcld φA2+B2
133 125 127 zaddcld φC2+D2
134 dvds2add M2A2+B2C2+D2M2A2+B2M2C2+D2M2A2+B2+C2+D2
135 104 132 133 134 syl3anc φM2A2+B2M2C2+D2M2A2+B2+C2+D2
136 135 adantr φR=0M2A2+B2M2C2+D2M2A2+B2+C2+D2
137 112 131 136 mp2and φR=0M2A2+B2+C2+D2
138 104 adantr φR=MM2
139 132 adantr φR=MA2+B2
140 51 adantr φR=MM222+M222=M22
141 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 4sqlem15 φR=MM222E2=0M222F2=0M222G2=0M222H2=0
142 141 simpld φR=MM222E2=0M222F2=0
143 142 simpld φR=MM222E2=0
144 46 recnd φM222
145 24 zcnd φE2
146 144 145 subeq0ad φM222E2=0M222=E2
147 146 adantr φR=MM222E2=0M222=E2
148 143 147 mpbid φR=MM222=E2
149 24 adantr φR=ME2
150 148 149 eqeltrd φR=MM222
151 150 150 zaddcld φR=MM222+M222
152 140 151 eqeltrrd φR=MM22
153 139 152 zsubcld φR=MA2+B2-M22
154 133 adantr φR=MC2+D2
155 154 152 zsubcld φR=MC2+D2-M22
156 106 adantr φR=MA2
157 156 150 zsubcld φR=MA2M222
158 108 adantr φR=MB2
159 158 150 zsubcld φR=MB2M222
160 9 20 13 143 4sqlem10 φR=MM2A2M222
161 142 simprd φR=MM222F2=0
162 10 20 14 161 4sqlem10 φR=MM2B2M222
163 138 157 159 160 162 dvds2addd φR=MM2A2M222+B2-M222
164 106 zcnd φA2
165 108 zcnd φB2
166 164 165 144 144 addsub4d φA2+B2-M222+M222=A2M222+B2-M222
167 51 oveq2d φA2+B2-M222+M222=A2+B2-M22
168 166 167 eqtr3d φA2M222+B2-M222=A2+B2-M22
169 168 adantr φR=MA2M222+B2-M222=A2+B2-M22
170 163 169 breqtrd φR=MM2A2+B2-M22
171 125 adantr φR=MC2
172 171 150 zsubcld φR=MC2M222
173 127 adantr φR=MD2
174 173 150 zsubcld φR=MD2M222
175 141 simprd φR=MM222G2=0M222H2=0
176 175 simpld φR=MM222G2=0
177 11 20 15 176 4sqlem10 φR=MM2C2M222
178 175 simprd φR=MM222H2=0
179 12 20 16 178 4sqlem10 φR=MM2D2M222
180 138 172 174 177 179 dvds2addd φR=MM2C2M222+D2-M222
181 125 zcnd φC2
182 127 zcnd φD2
183 181 182 144 144 addsub4d φC2+D2-M222+M222=C2M222+D2-M222
184 51 oveq2d φC2+D2-M222+M222=C2+D2-M22
185 183 184 eqtr3d φC2M222+D2-M222=C2+D2-M22
186 185 adantr φR=MC2M222+D2-M222=C2+D2-M22
187 180 186 breqtrd φR=MM2C2+D2-M22
188 138 153 155 170 187 dvds2addd φR=MM2A2+B2-M22+C2+D2-M22
189 132 zcnd φA2+B2
190 133 zcnd φC2+D2
191 189 190 50 50 addsub4d φA2+B2+C2+D2-M22+M22=A2+B2-M22+C2+D2-M22
192 59 oveq2d φA2+B2+C2+D2-M22+M22=A2+B2+C2+D2-M2
193 191 192 eqtr3d φA2+B2-M22+C2+D2-M22=A2+B2+C2+D2-M2
194 193 adantr φR=MA2+B2-M22+C2+D2-M22=A2+B2+C2+D2-M2
195 188 194 breqtrd φR=MM2A2+B2+C2+D2-M2
196 132 133 zaddcld φA2+B2+C2+D2
197 196 adantr φR=MA2+B2+C2+D2
198 dvdssubr M2A2+B2+C2+D2M2A2+B2+C2+D2M2A2+B2+C2+D2-M2
199 138 197 198 syl2anc φR=MM2A2+B2+C2+D2M2A2+B2+C2+D2-M2
200 195 199 mpbird φR=MM2A2+B2+C2+D2
201 137 200 jaodan φR=0R=MM2A2+B2+C2+D2
202 18 adantr φR=0R=MMP=A2+B2+C2+D2
203 201 202 breqtrrd φR=0R=MM2MP
204 203 ex φR=0R=MM2MP
205 69 204 jca φRMR=0R=MM2MP