# 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}=\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\}$
Assertion 4sqlem19 ${⊢}{ℕ}_{0}={S}$

### 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 elnn0 ${⊢}{k}\in {ℕ}_{0}↔\left({k}\in ℕ\vee {k}=0\right)$
3 eleq1 ${⊢}{j}=1\to \left({j}\in {S}↔1\in {S}\right)$
4 eleq1 ${⊢}{j}={m}\to \left({j}\in {S}↔{m}\in {S}\right)$
5 eleq1 ${⊢}{j}={i}\to \left({j}\in {S}↔{i}\in {S}\right)$
6 eleq1 ${⊢}{j}={m}{i}\to \left({j}\in {S}↔{m}{i}\in {S}\right)$
7 eleq1 ${⊢}{j}={k}\to \left({j}\in {S}↔{k}\in {S}\right)$
8 abs1 ${⊢}\left|1\right|=1$
9 8 oveq1i ${⊢}{\left|1\right|}^{2}={1}^{2}$
10 sq1 ${⊢}{1}^{2}=1$
11 9 10 eqtri ${⊢}{\left|1\right|}^{2}=1$
12 abs0 ${⊢}\left|0\right|=0$
13 12 oveq1i ${⊢}{\left|0\right|}^{2}={0}^{2}$
14 sq0 ${⊢}{0}^{2}=0$
15 13 14 eqtri ${⊢}{\left|0\right|}^{2}=0$
16 11 15 oveq12i ${⊢}{\left|1\right|}^{2}+{\left|0\right|}^{2}=1+0$
17 1p0e1 ${⊢}1+0=1$
18 16 17 eqtri ${⊢}{\left|1\right|}^{2}+{\left|0\right|}^{2}=1$
19 1z ${⊢}1\in ℤ$
20 zgz ${⊢}1\in ℤ\to 1\in ℤ\left[i\right]$
21 19 20 ax-mp ${⊢}1\in ℤ\left[i\right]$
22 0z ${⊢}0\in ℤ$
23 zgz ${⊢}0\in ℤ\to 0\in ℤ\left[i\right]$
24 22 23 ax-mp ${⊢}0\in ℤ\left[i\right]$
25 1 4sqlem4a ${⊢}\left(1\in ℤ\left[i\right]\wedge 0\in ℤ\left[i\right]\right)\to {\left|1\right|}^{2}+{\left|0\right|}^{2}\in {S}$
26 21 24 25 mp2an ${⊢}{\left|1\right|}^{2}+{\left|0\right|}^{2}\in {S}$
27 18 26 eqeltrri ${⊢}1\in {S}$
28 eleq1 ${⊢}{j}=2\to \left({j}\in {S}↔2\in {S}\right)$
29 eldifsn ${⊢}{j}\in \left(ℙ\setminus \left\{2\right\}\right)↔\left({j}\in ℙ\wedge {j}\ne 2\right)$
30 oddprm ${⊢}{j}\in \left(ℙ\setminus \left\{2\right\}\right)\to \frac{{j}-1}{2}\in ℕ$
31 30 adantr ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to \frac{{j}-1}{2}\in ℕ$
32 eldifi ${⊢}{j}\in \left(ℙ\setminus \left\{2\right\}\right)\to {j}\in ℙ$
33 32 adantr ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to {j}\in ℙ$
34 prmnn ${⊢}{j}\in ℙ\to {j}\in ℕ$
35 nncn ${⊢}{j}\in ℕ\to {j}\in ℂ$
36 33 34 35 3syl ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to {j}\in ℂ$
37 ax-1cn ${⊢}1\in ℂ$
38 subcl ${⊢}\left({j}\in ℂ\wedge 1\in ℂ\right)\to {j}-1\in ℂ$
39 36 37 38 sylancl ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to {j}-1\in ℂ$
40 2cnd ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to 2\in ℂ$
41 2ne0 ${⊢}2\ne 0$
42 41 a1i ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to 2\ne 0$
43 39 40 42 divcan2d ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to 2\left(\frac{{j}-1}{2}\right)={j}-1$
44 43 oveq1d ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to 2\left(\frac{{j}-1}{2}\right)+1={j}-1+1$
45 npcan ${⊢}\left({j}\in ℂ\wedge 1\in ℂ\right)\to {j}-1+1={j}$
46 36 37 45 sylancl ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to {j}-1+1={j}$
47 44 46 eqtr2d ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to {j}=2\left(\frac{{j}-1}{2}\right)+1$
48 43 oveq2d ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to \left(0\dots 2\left(\frac{{j}-1}{2}\right)\right)=\left(0\dots {j}-1\right)$
49 nnm1nn0 ${⊢}{j}\in ℕ\to {j}-1\in {ℕ}_{0}$
50 33 34 49 3syl ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to {j}-1\in {ℕ}_{0}$
51 elnn0uz ${⊢}{j}-1\in {ℕ}_{0}↔{j}-1\in {ℤ}_{\ge 0}$
52 50 51 sylib ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to {j}-1\in {ℤ}_{\ge 0}$
53 eluzfz1 ${⊢}{j}-1\in {ℤ}_{\ge 0}\to 0\in \left(0\dots {j}-1\right)$
54 fzsplit ${⊢}0\in \left(0\dots {j}-1\right)\to \left(0\dots {j}-1\right)=\left(0\dots 0\right)\cup \left(0+1\dots {j}-1\right)$
55 52 53 54 3syl ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to \left(0\dots {j}-1\right)=\left(0\dots 0\right)\cup \left(0+1\dots {j}-1\right)$
56 48 55 eqtrd ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to \left(0\dots 2\left(\frac{{j}-1}{2}\right)\right)=\left(0\dots 0\right)\cup \left(0+1\dots {j}-1\right)$
57 fz0sn ${⊢}\left(0\dots 0\right)=\left\{0\right\}$
58 15 15 oveq12i ${⊢}{\left|0\right|}^{2}+{\left|0\right|}^{2}=0+0$
59 00id ${⊢}0+0=0$
60 58 59 eqtri ${⊢}{\left|0\right|}^{2}+{\left|0\right|}^{2}=0$
61 1 4sqlem4a ${⊢}\left(0\in ℤ\left[i\right]\wedge 0\in ℤ\left[i\right]\right)\to {\left|0\right|}^{2}+{\left|0\right|}^{2}\in {S}$
62 24 24 61 mp2an ${⊢}{\left|0\right|}^{2}+{\left|0\right|}^{2}\in {S}$
63 60 62 eqeltrri ${⊢}0\in {S}$
64 snssi ${⊢}0\in {S}\to \left\{0\right\}\subseteq {S}$
65 63 64 ax-mp ${⊢}\left\{0\right\}\subseteq {S}$
66 57 65 eqsstri ${⊢}\left(0\dots 0\right)\subseteq {S}$
67 66 a1i ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to \left(0\dots 0\right)\subseteq {S}$
68 0p1e1 ${⊢}0+1=1$
69 68 oveq1i ${⊢}\left(0+1\dots {j}-1\right)=\left(1\dots {j}-1\right)$
70 simpr ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}$
71 dfss3 ${⊢}\left(1\dots {j}-1\right)\subseteq {S}↔\forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}$
72 70 71 sylibr ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to \left(1\dots {j}-1\right)\subseteq {S}$
73 69 72 eqsstrid ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to \left(0+1\dots {j}-1\right)\subseteq {S}$
74 67 73 unssd ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to \left(0\dots 0\right)\cup \left(0+1\dots {j}-1\right)\subseteq {S}$
75 56 74 eqsstrd ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to \left(0\dots 2\left(\frac{{j}-1}{2}\right)\right)\subseteq {S}$
76 oveq1 ${⊢}{k}={i}\to {k}{j}={i}{j}$
77 76 eleq1d ${⊢}{k}={i}\to \left({k}{j}\in {S}↔{i}{j}\in {S}\right)$
78 77 cbvrabv ${⊢}\left\{{k}\in ℕ|{k}{j}\in {S}\right\}=\left\{{i}\in ℕ|{i}{j}\in {S}\right\}$
79 eqid ${⊢}sup\left(\left\{{k}\in ℕ|{k}{j}\in {S}\right\},ℝ,<\right)=sup\left(\left\{{k}\in ℕ|{k}{j}\in {S}\right\},ℝ,<\right)$
80 1 31 47 33 75 78 79 4sqlem18 ${⊢}\left({j}\in \left(ℙ\setminus \left\{2\right\}\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to {j}\in {S}$
81 29 80 sylanbr ${⊢}\left(\left({j}\in ℙ\wedge {j}\ne 2\right)\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to {j}\in {S}$
82 81 an32s ${⊢}\left(\left({j}\in ℙ\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\wedge {j}\ne 2\right)\to {j}\in {S}$
83 11 11 oveq12i ${⊢}{\left|1\right|}^{2}+{\left|1\right|}^{2}=1+1$
84 df-2 ${⊢}2=1+1$
85 83 84 eqtr4i ${⊢}{\left|1\right|}^{2}+{\left|1\right|}^{2}=2$
86 1 4sqlem4a ${⊢}\left(1\in ℤ\left[i\right]\wedge 1\in ℤ\left[i\right]\right)\to {\left|1\right|}^{2}+{\left|1\right|}^{2}\in {S}$
87 21 21 86 mp2an ${⊢}{\left|1\right|}^{2}+{\left|1\right|}^{2}\in {S}$
88 85 87 eqeltrri ${⊢}2\in {S}$
89 88 a1i ${⊢}\left({j}\in ℙ\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to 2\in {S}$
90 28 82 89 pm2.61ne ${⊢}\left({j}\in ℙ\wedge \forall {m}\in \left(1\dots {j}-1\right)\phantom{\rule{.4em}{0ex}}{m}\in {S}\right)\to {j}\in {S}$
91 1 mul4sq ${⊢}\left({m}\in {S}\wedge {i}\in {S}\right)\to {m}{i}\in {S}$
92 91 a1i ${⊢}\left({m}\in {ℤ}_{\ge 2}\wedge {i}\in {ℤ}_{\ge 2}\right)\to \left(\left({m}\in {S}\wedge {i}\in {S}\right)\to {m}{i}\in {S}\right)$
93 3 4 5 6 7 27 90 92 prmind2 ${⊢}{k}\in ℕ\to {k}\in {S}$
94 id ${⊢}{k}=0\to {k}=0$
95 94 63 syl6eqel ${⊢}{k}=0\to {k}\in {S}$
96 93 95 jaoi ${⊢}\left({k}\in ℕ\vee {k}=0\right)\to {k}\in {S}$
97 2 96 sylbi ${⊢}{k}\in {ℕ}_{0}\to {k}\in {S}$
98 97 ssriv ${⊢}{ℕ}_{0}\subseteq {S}$
99 1 4sqlem1 ${⊢}{S}\subseteq {ℕ}_{0}$
100 98 99 eqssi ${⊢}{ℕ}_{0}={S}$