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=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 4sqlem14 φR0

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 6 ssrab3 T
20 nnuz =1
21 19 20 sseqtri T1
22 1 2 3 4 5 6 7 4sqlem13 φTM<P
23 22 simpld φT
24 infssuzcl T1TsupT<T
25 21 23 24 sylancr φsupT<T
26 7 25 eqeltrid φMT
27 19 26 sselid φM
28 27 nnzd φM
29 prmz PP
30 4 29 syl φP
31 28 30 zmulcld φMP
32 9 27 13 4sqlem5 φEAEM
33 32 simpld φE
34 zsqcl2 EE20
35 33 34 syl φE20
36 10 27 14 4sqlem5 φFBFM
37 36 simpld φF
38 zsqcl2 FF20
39 37 38 syl φF20
40 35 39 nn0addcld φE2+F20
41 40 nn0zd φE2+F2
42 11 27 15 4sqlem5 φGCGM
43 42 simpld φG
44 zsqcl2 GG20
45 43 44 syl φG20
46 12 27 16 4sqlem5 φHDHM
47 46 simpld φH
48 zsqcl2 HH20
49 47 48 syl φH20
50 45 49 nn0addcld φG2+H20
51 50 nn0zd φG2+H2
52 41 51 zaddcld φE2+F2+G2+H2
53 31 52 zsubcld φMPE2+F2+G2+H2
54 dvdsmul1 MPMMP
55 28 30 54 syl2anc φMMP
56 zsqcl AA2
57 9 56 syl φA2
58 zsqcl BB2
59 10 58 syl φB2
60 57 59 zaddcld φA2+B2
61 60 41 zsubcld φA2+B2-E2+F2
62 zsqcl CC2
63 11 62 syl φC2
64 zsqcl DD2
65 12 64 syl φD2
66 63 65 zaddcld φC2+D2
67 66 51 zsubcld φC2+D2-G2+H2
68 35 nn0zd φE2
69 57 68 zsubcld φA2E2
70 39 nn0zd φF2
71 59 70 zsubcld φB2F2
72 9 27 13 4sqlem8 φMA2E2
73 10 27 14 4sqlem8 φMB2F2
74 28 69 71 72 73 dvds2addd φMA2E2+B2-F2
75 9 zcnd φA
76 75 sqcld φA2
77 10 zcnd φB
78 77 sqcld φB2
79 33 zcnd φE
80 79 sqcld φE2
81 37 zcnd φF
82 81 sqcld φF2
83 76 78 80 82 addsub4d φA2+B2-E2+F2=A2E2+B2-F2
84 74 83 breqtrrd φMA2+B2-E2+F2
85 45 nn0zd φG2
86 63 85 zsubcld φC2G2
87 49 nn0zd φH2
88 65 87 zsubcld φD2H2
89 11 27 15 4sqlem8 φMC2G2
90 12 27 16 4sqlem8 φMD2H2
91 28 86 88 89 90 dvds2addd φMC2G2+D2-H2
92 11 zcnd φC
93 92 sqcld φC2
94 12 zcnd φD
95 94 sqcld φD2
96 43 zcnd φG
97 96 sqcld φG2
98 47 zcnd φH
99 98 sqcld φH2
100 93 95 97 99 addsub4d φC2+D2-G2+H2=C2G2+D2-H2
101 91 100 breqtrrd φMC2+D2-G2+H2
102 28 61 67 84 101 dvds2addd φMA2+B2-E2+F2+C2+D2-G2+H2
103 18 oveq1d φMPE2+F2+G2+H2=A2+B2+C2+D2-E2+F2+G2+H2
104 76 78 addcld φA2+B2
105 93 95 addcld φC2+D2
106 80 82 addcld φE2+F2
107 97 99 addcld φG2+H2
108 104 105 106 107 addsub4d φA2+B2+C2+D2-E2+F2+G2+H2=A2+B2-E2+F2+C2+D2-G2+H2
109 103 108 eqtrd φMPE2+F2+G2+H2=A2+B2-E2+F2+C2+D2-G2+H2
110 102 109 breqtrrd φMMPE2+F2+G2+H2
111 28 31 53 55 110 dvds2subd φMMPMPE2+F2+G2+H2
112 27 nncnd φM
113 prmnn PP
114 4 113 syl φP
115 114 nncnd φP
116 112 115 mulcld φMP
117 106 107 addcld φE2+F2+G2+H2
118 116 117 nncand φMPMPE2+F2+G2+H2=E2+F2+G2+H2
119 111 118 breqtrd φME2+F2+G2+H2
120 27 nnne0d φM0
121 40 50 nn0addcld φE2+F2+G2+H20
122 121 nn0zd φE2+F2+G2+H2
123 dvdsval2 MM0E2+F2+G2+H2ME2+F2+G2+H2E2+F2+G2+H2M
124 28 120 122 123 syl3anc φME2+F2+G2+H2E2+F2+G2+H2M
125 119 124 mpbid φE2+F2+G2+H2M
126 121 nn0red φE2+F2+G2+H2
127 121 nn0ge0d φ0E2+F2+G2+H2
128 27 nnred φM
129 27 nngt0d φ0<M
130 divge0 E2+F2+G2+H20E2+F2+G2+H2M0<M0E2+F2+G2+H2M
131 126 127 128 129 130 syl22anc φ0E2+F2+G2+H2M
132 elnn0z E2+F2+G2+H2M0E2+F2+G2+H2M0E2+F2+G2+H2M
133 125 131 132 sylanbrc φE2+F2+G2+H2M0
134 17 133 eqeltrid φR0