Metamath Proof Explorer


Theorem 4sqlem19

Description: Lemma for 4sq . The proof is by strong induction - we show that if all the integers less than k are in S , then k is as well. In this part of the proof we do the induction argument and dispense with all the cases except the odd prime case, which is sent to 4sqlem18 . If k is 0 , 1 , 2 , we show k e. S directly; otherwise if k is composite, k is the product of two numbers less than it (and hence in S by assumption), so by mul4sq k e. S . (Contributed by Mario Carneiro, 14-Jul-2014) (Revised by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypothesis 4sq.1 S = n | x y z w n = x 2 + y 2 + z 2 + w 2
Assertion 4sqlem19 0 = S

Proof

Step Hyp Ref Expression
1 4sq.1 S = n | x y z w n = x 2 + y 2 + z 2 + w 2
2 elnn0 k 0 k k = 0
3 eleq1 j = 1 j S 1 S
4 eleq1 j = m j S m S
5 eleq1 j = i j S i S
6 eleq1 j = m i j S m i S
7 eleq1 j = k j S k S
8 abs1 1 = 1
9 8 oveq1i 1 2 = 1 2
10 sq1 1 2 = 1
11 9 10 eqtri 1 2 = 1
12 abs0 0 = 0
13 12 oveq1i 0 2 = 0 2
14 sq0 0 2 = 0
15 13 14 eqtri 0 2 = 0
16 11 15 oveq12i 1 2 + 0 2 = 1 + 0
17 1p0e1 1 + 0 = 1
18 16 17 eqtri 1 2 + 0 2 = 1
19 1z 1
20 zgz 1 1 i
21 19 20 ax-mp 1 i
22 0z 0
23 zgz 0 0 i
24 22 23 ax-mp 0 i
25 1 4sqlem4a 1 i 0 i 1 2 + 0 2 S
26 21 24 25 mp2an 1 2 + 0 2 S
27 18 26 eqeltrri 1 S
28 eleq1 j = 2 j S 2 S
29 eldifsn j 2 j j 2
30 oddprm j 2 j 1 2
31 30 adantr j 2 m 1 j 1 m S j 1 2
32 eldifi j 2 j
33 32 adantr j 2 m 1 j 1 m S j
34 prmnn j j
35 nncn j j
36 33 34 35 3syl j 2 m 1 j 1 m S j
37 ax-1cn 1
38 subcl j 1 j 1
39 36 37 38 sylancl j 2 m 1 j 1 m S j 1
40 2cnd j 2 m 1 j 1 m S 2
41 2ne0 2 0
42 41 a1i j 2 m 1 j 1 m S 2 0
43 39 40 42 divcan2d j 2 m 1 j 1 m S 2 j 1 2 = j 1
44 43 oveq1d j 2 m 1 j 1 m S 2 j 1 2 + 1 = j - 1 + 1
45 npcan j 1 j - 1 + 1 = j
46 36 37 45 sylancl j 2 m 1 j 1 m S j - 1 + 1 = j
47 44 46 eqtr2d j 2 m 1 j 1 m S j = 2 j 1 2 + 1
48 43 oveq2d j 2 m 1 j 1 m S 0 2 j 1 2 = 0 j 1
49 nnm1nn0 j j 1 0
50 33 34 49 3syl j 2 m 1 j 1 m S j 1 0
51 elnn0uz j 1 0 j 1 0
52 50 51 sylib j 2 m 1 j 1 m S j 1 0
53 eluzfz1 j 1 0 0 0 j 1
54 fzsplit 0 0 j 1 0 j 1 = 0 0 0 + 1 j 1
55 52 53 54 3syl j 2 m 1 j 1 m S 0 j 1 = 0 0 0 + 1 j 1
56 48 55 eqtrd j 2 m 1 j 1 m S 0 2 j 1 2 = 0 0 0 + 1 j 1
57 fz0sn 0 0 = 0
58 15 15 oveq12i 0 2 + 0 2 = 0 + 0
59 00id 0 + 0 = 0
60 58 59 eqtri 0 2 + 0 2 = 0
61 1 4sqlem4a 0 i 0 i 0 2 + 0 2 S
62 24 24 61 mp2an 0 2 + 0 2 S
63 60 62 eqeltrri 0 S
64 snssi 0 S 0 S
65 63 64 ax-mp 0 S
66 57 65 eqsstri 0 0 S
67 66 a1i j 2 m 1 j 1 m S 0 0 S
68 0p1e1 0 + 1 = 1
69 68 oveq1i 0 + 1 j 1 = 1 j 1
70 simpr j 2 m 1 j 1 m S m 1 j 1 m S
71 dfss3 1 j 1 S m 1 j 1 m S
72 70 71 sylibr j 2 m 1 j 1 m S 1 j 1 S
73 69 72 eqsstrid j 2 m 1 j 1 m S 0 + 1 j 1 S
74 67 73 unssd j 2 m 1 j 1 m S 0 0 0 + 1 j 1 S
75 56 74 eqsstrd j 2 m 1 j 1 m S 0 2 j 1 2 S
76 oveq1 k = i k j = i j
77 76 eleq1d k = i k j S i j S
78 77 cbvrabv k | k j S = i | i j S
79 eqid sup k | k j S < = sup k | k j S <
80 1 31 47 33 75 78 79 4sqlem18 j 2 m 1 j 1 m S j S
81 29 80 sylanbr j j 2 m 1 j 1 m S j S
82 81 an32s j m 1 j 1 m S j 2 j S
83 11 11 oveq12i 1 2 + 1 2 = 1 + 1
84 df-2 2 = 1 + 1
85 83 84 eqtr4i 1 2 + 1 2 = 2
86 1 4sqlem4a 1 i 1 i 1 2 + 1 2 S
87 21 21 86 mp2an 1 2 + 1 2 S
88 85 87 eqeltrri 2 S
89 88 a1i j m 1 j 1 m S 2 S
90 28 82 89 pm2.61ne j m 1 j 1 m S j S
91 1 mul4sq m S i S m i S
92 91 a1i m 2 i 2 m S i S m i S
93 3 4 5 6 7 27 90 92 prmind2 k k S
94 id k = 0 k = 0
95 94 63 syl6eqel k = 0 k S
96 93 95 jaoi k k = 0 k S
97 2 96 sylbi k 0 k S
98 97 ssriv 0 S
99 1 4sqlem1 S 0
100 98 99 eqssi 0 = S