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 \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
	Assertion	4sqlem19	$⊢ ℕ_{0} = S$

Proof

Step	Hyp	Ref	Expression
1		4sq.1	$⊢ S = \{n \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
2		elnn0	$⊢ k \in ℕ_{0} \leftrightarrow (k \in ℕ \lor k = 0)$
3		eleq1	$⊢ j = 1 \to (j \in S \leftrightarrow 1 \in S)$
4		eleq1	$⊢ j = m \to (j \in S \leftrightarrow m \in S)$
5		eleq1	$⊢ j = i \to (j \in S \leftrightarrow i \in S)$
6		eleq1	$⊢ j = m i \to (j \in S \leftrightarrow m i \in S)$
7		eleq1	$⊢ j = k \to (j \in S \leftrightarrow k \in 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 \in ℤ$
20		zgz	$⊢ 1 \in ℤ \to 1 \in ℤ [i]$
21	19 20	ax-mp	$⊢ 1 \in ℤ [i]$
22		0z	$⊢ 0 \in ℤ$
23		zgz	$⊢ 0 \in ℤ \to 0 \in ℤ [i]$
24	22 23	ax-mp	$⊢ 0 \in ℤ [i]$
25	1	4sqlem4a	$⊢ (1 \in ℤ [i] \land 0 \in ℤ [i]) \to {\|1\|}^{2} + {\|0\|}^{2} \in S$
26	21 24 25	mp2an	$⊢ {\|1\|}^{2} + {\|0\|}^{2} \in S$
27	18 26	eqeltrri	$⊢ 1 \in S$
28		eleq1	$⊢ j = 2 \to (j \in S \leftrightarrow 2 \in S)$
29		eldifsn	$⊢ j \in (ℙ ∖ \{2\}) \leftrightarrow (j \in ℙ \land j \neq 2)$
30		oddprm	$⊢ j \in (ℙ ∖ \{2\}) \to \frac{j - 1}{2} \in ℕ$
31	30	adantr	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to \frac{j - 1}{2} \in ℕ$
32		eldifi	$⊢ j \in (ℙ ∖ \{2\}) \to j \in ℙ$
33	32	adantr	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to j \in ℙ$
34		prmnn	$⊢ j \in ℙ \to j \in ℕ$
35		nncn	$⊢ j \in ℕ \to j \in ℂ$
36	33 34 35	3syl	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to j \in ℂ$
37		ax-1cn	$⊢ 1 \in ℂ$
38		subcl	$⊢ (j \in ℂ \land 1 \in ℂ) \to j - 1 \in ℂ$
39	36 37 38	sylancl	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to j - 1 \in ℂ$
40		2cnd	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to 2 \in ℂ$
41		2ne0	$⊢ 2 \neq 0$
42	41	a1i	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to 2 \neq 0$
43	39 40 42	divcan2d	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to 2 (\frac{j - 1}{2}) = j - 1$
44	43	oveq1d	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to 2 (\frac{j - 1}{2}) + 1 = j - 1 + 1$
45		npcan	$⊢ (j \in ℂ \land 1 \in ℂ) \to j - 1 + 1 = j$
46	36 37 45	sylancl	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to j - 1 + 1 = j$
47	44 46	eqtr2d	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to j = 2 (\frac{j - 1}{2}) + 1$
48	43	oveq2d	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to (0 \dots 2 (\frac{j - 1}{2})) = (0 \dots j - 1)$
49		nnm1nn0	$⊢ j \in ℕ \to j - 1 \in ℕ_{0}$
50	33 34 49	3syl	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to j - 1 \in ℕ_{0}$
51		elnn0uz	$⊢ j - 1 \in ℕ_{0} \leftrightarrow j - 1 \in ℤ_{\geq 0}$
52	50 51	sylib	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to j - 1 \in ℤ_{\geq 0}$
53		eluzfz1	$⊢ j - 1 \in ℤ_{\geq 0} \to 0 \in (0 \dots j - 1)$
54		fzsplit	$⊢ 0 \in (0 \dots j - 1) \to (0 \dots j - 1) = (0 \dots 0) \cup (0 + 1 \dots j - 1)$
55	52 53 54	3syl	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to (0 \dots j - 1) = (0 \dots 0) \cup (0 + 1 \dots j - 1)$
56	48 55	eqtrd	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to (0 \dots 2 (\frac{j - 1}{2})) = (0 \dots 0) \cup (0 + 1 \dots j - 1)$
57		fz0sn	$⊢ (0 \dots 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 \in ℤ [i] \land 0 \in ℤ [i]) \to {\|0\|}^{2} + {\|0\|}^{2} \in S$
62	24 24 61	mp2an	$⊢ {\|0\|}^{2} + {\|0\|}^{2} \in S$
63	60 62	eqeltrri	$⊢ 0 \in S$
64		snssi	$⊢ 0 \in S \to \{0\} \subseteq S$
65	63 64	ax-mp	$⊢ \{0\} \subseteq S$
66	57 65	eqsstri	$⊢ (0 \dots 0) \subseteq S$
67	66	a1i	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to (0 \dots 0) \subseteq S$
68		0p1e1	$⊢ 0 + 1 = 1$
69	68	oveq1i	$⊢ (0 + 1 \dots j - 1) = (1 \dots j - 1)$
70		dfss3	$⊢ (1 \dots j - 1) \subseteq S \leftrightarrow \forall m \in (1 \dots j - 1) m \in S$
71	70	bilanri	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to (1 \dots j - 1) \subseteq S$
72	69 71	eqsstrid	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to (0 + 1 \dots j - 1) \subseteq S$
73	67 72	unssd	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to (0 \dots 0) \cup (0 + 1 \dots j - 1) \subseteq S$
74	56 73	eqsstrd	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to (0 \dots 2 (\frac{j - 1}{2})) \subseteq S$
75		oveq1	$⊢ k = i \to k j = i j$
76	75	eleq1d	$⊢ k = i \to (k j \in S \leftrightarrow i j \in S)$
77	76	cbvrabv	$⊢ \{k \in ℕ \| k j \in S\} = \{i \in ℕ \| i j \in S\}$
78		eqid	$⊢ inf (\{k \in ℕ \| k j \in S\} ℝ <) = inf (\{k \in ℕ \| k j \in S\} ℝ <)$
79	1 31 47 33 74 77 78	4sqlem18	$⊢ (j \in (ℙ ∖ \{2\}) \land \forall m \in (1 \dots j - 1) m \in S) \to j \in S$
80	29 79	sylanbr	$⊢ ((j \in ℙ \land j \neq 2) \land \forall m \in (1 \dots j - 1) m \in S) \to j \in S$
81	80	an32s	$⊢ ((j \in ℙ \land \forall m \in (1 \dots j - 1) m \in S) \land j \neq 2) \to j \in S$
82	11 11	oveq12i	$⊢ {\|1\|}^{2} + {\|1\|}^{2} = 1 + 1$
83		df-2	$⊢ 2 = 1 + 1$
84	82 83	eqtr4i	$⊢ {\|1\|}^{2} + {\|1\|}^{2} = 2$
85	1	4sqlem4a	$⊢ (1 \in ℤ [i] \land 1 \in ℤ [i]) \to {\|1\|}^{2} + {\|1\|}^{2} \in S$
86	21 21 85	mp2an	$⊢ {\|1\|}^{2} + {\|1\|}^{2} \in S$
87	84 86	eqeltrri	$⊢ 2 \in S$
88	87	a1i	$⊢ (j \in ℙ \land \forall m \in (1 \dots j - 1) m \in S) \to 2 \in S$
89	28 81 88	pm2.61ne	$⊢ (j \in ℙ \land \forall m \in (1 \dots j - 1) m \in S) \to j \in S$
90	1	mul4sq	$⊢ (m \in S \land i \in S) \to m i \in S$
91	90	a1i	$⊢ (m \in ℤ_{\geq 2} \land i \in ℤ_{\geq 2}) \to ((m \in S \land i \in S) \to m i \in S)$
92	3 4 5 6 7 27 89 91	prmind2	$⊢ k \in ℕ \to k \in S$
93		id	$⊢ k = 0 \to k = 0$
94	93 63	eqeltrdi	$⊢ k = 0 \to k \in S$
95	92 94	jaoi	$⊢ (k \in ℕ \lor k = 0) \to k \in S$
96	2 95	sylbi	$⊢ k \in ℕ_{0} \to k \in S$
97	96	ssriv	$⊢ ℕ_{0} \subseteq S$
98	1	4sqlem1	$⊢ S \subseteq ℕ_{0}$
99	97 98	eqssi	$⊢ ℕ_{0} = S$

Metamath Proof Explorer

Theorem 4sqlem19

Proof