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 S = n | x y z w n = x 2 + y 2 + z 2 + w 2
4sq.2 φ N
4sq.3 φ P = 2 N + 1
4sq.4 φ P
4sq.5 φ 0 2 N S
4sq.6 T = i | i P S
4sq.7 M = sup T <
4sq.m φ M 2
4sq.a φ A
4sq.b φ B
4sq.c φ C
4sq.d φ D
4sq.e E = A + M 2 mod M M 2
4sq.f F = B + M 2 mod M M 2
4sq.g G = C + M 2 mod M M 2
4sq.h H = D + M 2 mod M M 2
4sq.r R = E 2 + F 2 + G 2 + H 2 M
4sq.p φ M P = A 2 + B 2 + C 2 + D 2
Assertion 4sqlem15 φ R = M M 2 2 2 E 2 = 0 M 2 2 2 F 2 = 0 M 2 2 2 G 2 = 0 M 2 2 2 H 2 = 0

Proof

Step Hyp Ref Expression
1 4sq.1 S = n | x y z w n = x 2 + y 2 + z 2 + w 2
2 4sq.2 φ N
3 4sq.3 φ P = 2 N + 1
4 4sq.4 φ P
5 4sq.5 φ 0 2 N S
6 4sq.6 T = i | i P S
7 4sq.7 M = sup T <
8 4sq.m φ M 2
9 4sq.a φ A
10 4sq.b φ B
11 4sq.c φ C
12 4sq.d φ D
13 4sq.e E = A + M 2 mod M M 2
14 4sq.f F = B + M 2 mod M M 2
15 4sq.g G = C + M 2 mod M M 2
16 4sq.h H = D + M 2 mod M M 2
17 4sq.r R = E 2 + F 2 + G 2 + H 2 M
18 4sq.p φ M P = A 2 + B 2 + C 2 + D 2
19 eluz2nn M 2 M
20 8 19 syl φ M
21 20 nnred φ M
22 21 resqcld φ M 2
23 22 rehalfcld φ M 2 2
24 23 rehalfcld φ M 2 2 2
25 24 recnd φ M 2 2 2
26 9 20 13 4sqlem5 φ E A E M
27 26 simpld φ E
28 zsqcl E E 2
29 27 28 syl φ E 2
30 29 zred φ E 2
31 30 recnd φ E 2
32 10 20 14 4sqlem5 φ F B F M
33 32 simpld φ F
34 zsqcl F F 2
35 33 34 syl φ F 2
36 35 zred φ F 2
37 36 recnd φ F 2
38 25 25 31 37 addsub4d φ M 2 2 2 + M 2 2 2 - E 2 + F 2 = M 2 2 2 E 2 + M 2 2 2 - F 2
39 23 recnd φ M 2 2
40 39 2halvesd φ M 2 2 2 + M 2 2 2 = M 2 2
41 40 oveq1d φ M 2 2 2 + M 2 2 2 - E 2 + F 2 = M 2 2 E 2 + F 2
42 38 41 eqtr3d φ M 2 2 2 E 2 + M 2 2 2 - F 2 = M 2 2 E 2 + F 2
43 42 adantr φ R = M M 2 2 2 E 2 + M 2 2 2 - F 2 = M 2 2 E 2 + F 2
44 22 recnd φ M 2
45 44 2halvesd φ M 2 2 + M 2 2 = M 2
46 45 adantr φ R = M M 2 2 + M 2 2 = M 2
47 21 recnd φ M
48 47 sqvald φ M 2 = M M
49 48 adantr φ R = M M 2 = M M
50 simpr φ R = M R = M
51 17 50 eqtr3id φ R = M E 2 + F 2 + G 2 + H 2 M = M
52 51 oveq1d φ R = M E 2 + F 2 + G 2 + H 2 M M = M M
53 30 36 readdcld φ E 2 + F 2
54 11 20 15 4sqlem5 φ G C G M
55 54 simpld φ G
56 zsqcl G G 2
57 55 56 syl φ G 2
58 57 zred φ G 2
59 12 20 16 4sqlem5 φ H D H M
60 59 simpld φ H
61 zsqcl H H 2
62 60 61 syl φ H 2
63 62 zred φ H 2
64 58 63 readdcld φ G 2 + H 2
65 53 64 readdcld φ E 2 + F 2 + G 2 + H 2
66 65 recnd φ E 2 + F 2 + G 2 + H 2
67 20 nnne0d φ M 0
68 66 47 67 divcan1d φ E 2 + F 2 + G 2 + H 2 M M = E 2 + F 2 + G 2 + H 2
69 68 adantr φ R = M E 2 + F 2 + G 2 + H 2 M M = E 2 + F 2 + G 2 + H 2
70 49 52 69 3eqtr2rd φ R = M E 2 + F 2 + G 2 + H 2 = M 2
71 46 70 oveq12d φ R = M M 2 2 + M 2 2 - E 2 + F 2 + G 2 + H 2 = M 2 M 2
72 53 recnd φ E 2 + F 2
73 64 recnd φ G 2 + H 2
74 39 39 72 73 addsub4d φ M 2 2 + M 2 2 - E 2 + F 2 + G 2 + H 2 = M 2 2 E 2 + F 2 + M 2 2 - G 2 + H 2
75 74 adantr φ R = M M 2 2 + M 2 2 - E 2 + F 2 + G 2 + H 2 = M 2 2 E 2 + F 2 + M 2 2 - G 2 + H 2
76 44 subidd φ M 2 M 2 = 0
77 76 adantr φ R = M M 2 M 2 = 0
78 71 75 77 3eqtr3d φ R = M M 2 2 E 2 + F 2 + M 2 2 - G 2 + H 2 = 0
79 23 53 resubcld φ M 2 2 E 2 + F 2
80 9 20 13 4sqlem7 φ E 2 M 2 2 2
81 10 20 14 4sqlem7 φ F 2 M 2 2 2
82 30 36 24 24 80 81 le2addd φ E 2 + F 2 M 2 2 2 + M 2 2 2
83 82 40 breqtrd φ E 2 + F 2 M 2 2
84 23 53 subge0d φ 0 M 2 2 E 2 + F 2 E 2 + F 2 M 2 2
85 83 84 mpbird φ 0 M 2 2 E 2 + F 2
86 23 64 resubcld φ M 2 2 G 2 + H 2
87 11 20 15 4sqlem7 φ G 2 M 2 2 2
88 12 20 16 4sqlem7 φ H 2 M 2 2 2
89 58 63 24 24 87 88 le2addd φ G 2 + H 2 M 2 2 2 + M 2 2 2
90 89 40 breqtrd φ G 2 + H 2 M 2 2
91 23 64 subge0d φ 0 M 2 2 G 2 + H 2 G 2 + H 2 M 2 2
92 90 91 mpbird φ 0 M 2 2 G 2 + H 2
93 add20 M 2 2 E 2 + F 2 0 M 2 2 E 2 + F 2 M 2 2 G 2 + H 2 0 M 2 2 G 2 + H 2 M 2 2 E 2 + F 2 + M 2 2 - G 2 + H 2 = 0 M 2 2 E 2 + F 2 = 0 M 2 2 G 2 + H 2 = 0
94 79 85 86 92 93 syl22anc φ M 2 2 E 2 + F 2 + M 2 2 - G 2 + H 2 = 0 M 2 2 E 2 + F 2 = 0 M 2 2 G 2 + H 2 = 0
95 94 biimpa φ M 2 2 E 2 + F 2 + M 2 2 - G 2 + H 2 = 0 M 2 2 E 2 + F 2 = 0 M 2 2 G 2 + H 2 = 0
96 78 95 syldan φ R = M M 2 2 E 2 + F 2 = 0 M 2 2 G 2 + H 2 = 0
97 96 simpld φ R = M M 2 2 E 2 + F 2 = 0
98 43 97 eqtrd φ R = M M 2 2 2 E 2 + M 2 2 2 - F 2 = 0
99 24 30 resubcld φ M 2 2 2 E 2
100 24 30 subge0d φ 0 M 2 2 2 E 2 E 2 M 2 2 2
101 80 100 mpbird φ 0 M 2 2 2 E 2
102 24 36 resubcld φ M 2 2 2 F 2
103 24 36 subge0d φ 0 M 2 2 2 F 2 F 2 M 2 2 2
104 81 103 mpbird φ 0 M 2 2 2 F 2
105 add20 M 2 2 2 E 2 0 M 2 2 2 E 2 M 2 2 2 F 2 0 M 2 2 2 F 2 M 2 2 2 E 2 + M 2 2 2 - F 2 = 0 M 2 2 2 E 2 = 0 M 2 2 2 F 2 = 0
106 99 101 102 104 105 syl22anc φ M 2 2 2 E 2 + M 2 2 2 - F 2 = 0 M 2 2 2 E 2 = 0 M 2 2 2 F 2 = 0
107 106 biimpa φ M 2 2 2 E 2 + M 2 2 2 - F 2 = 0 M 2 2 2 E 2 = 0 M 2 2 2 F 2 = 0
108 98 107 syldan φ R = M M 2 2 2 E 2 = 0 M 2 2 2 F 2 = 0
109 58 recnd φ G 2
110 63 recnd φ H 2
111 25 25 109 110 addsub4d φ M 2 2 2 + M 2 2 2 - G 2 + H 2 = M 2 2 2 G 2 + M 2 2 2 - H 2
112 40 oveq1d φ M 2 2 2 + M 2 2 2 - G 2 + H 2 = M 2 2 G 2 + H 2
113 111 112 eqtr3d φ M 2 2 2 G 2 + M 2 2 2 - H 2 = M 2 2 G 2 + H 2
114 113 adantr φ R = M M 2 2 2 G 2 + M 2 2 2 - H 2 = M 2 2 G 2 + H 2
115 96 simprd φ R = M M 2 2 G 2 + H 2 = 0
116 114 115 eqtrd φ R = M M 2 2 2 G 2 + M 2 2 2 - H 2 = 0
117 24 58 resubcld φ M 2 2 2 G 2
118 24 58 subge0d φ 0 M 2 2 2 G 2 G 2 M 2 2 2
119 87 118 mpbird φ 0 M 2 2 2 G 2
120 24 63 resubcld φ M 2 2 2 H 2
121 24 63 subge0d φ 0 M 2 2 2 H 2 H 2 M 2 2 2
122 88 121 mpbird φ 0 M 2 2 2 H 2
123 add20 M 2 2 2 G 2 0 M 2 2 2 G 2 M 2 2 2 H 2 0 M 2 2 2 H 2 M 2 2 2 G 2 + M 2 2 2 - H 2 = 0 M 2 2 2 G 2 = 0 M 2 2 2 H 2 = 0
124 117 119 120 122 123 syl22anc φ M 2 2 2 G 2 + M 2 2 2 - H 2 = 0 M 2 2 2 G 2 = 0 M 2 2 2 H 2 = 0
125 124 biimpa φ M 2 2 2 G 2 + M 2 2 2 - H 2 = 0 M 2 2 2 G 2 = 0 M 2 2 2 H 2 = 0
126 116 125 syldan φ R = M M 2 2 2 G 2 = 0 M 2 2 2 H 2 = 0
127 108 126 jca φ R = M M 2 2 2 E 2 = 0 M 2 2 2 F 2 = 0 M 2 2 2 G 2 = 0 M 2 2 2 H 2 = 0