4sqlem18

Description: Lemma for 4sq . Inductive step, odd prime case. (Contributed by Mario Carneiro, 16-Jul-2014) (Revised by AV, 14-Sep-2020)

	Ref	Expression
Hypotheses	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}\}$
	4sq.2	$⊢ φ \to N \in ℕ$
	4sq.3	$⊢ φ \to P = 2 \cdot N + 1$
	4sq.4	$⊢ φ \to P \in ℙ$
	4sq.5	$⊢ φ \to (0 \dots 2 \cdot N) \subseteq S$
	4sq.6	$⊢ T = \{i \in ℕ \| i P \in S\}$
	4sq.7	$⊢ M = sup (T ℝ <)$
Assertion	4sqlem18	$⊢ φ \to P \in 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		4sq.2	$⊢ φ \to N \in ℕ$
3		4sq.3	$⊢ φ \to P = 2 \cdot N + 1$
4		4sq.4	$⊢ φ \to P \in ℙ$
5		4sq.5	$⊢ φ \to (0 \dots 2 \cdot N) \subseteq S$
6		4sq.6	$⊢ T = \{i \in ℕ \| i P \in S\}$
7		4sq.7	$⊢ M = sup (T ℝ <)$
8		prmnn	$⊢ P \in ℙ \to P \in ℕ$
9	4 8	syl	$⊢ φ \to P \in ℕ$
10	9	nncnd	$⊢ φ \to P \in ℂ$
11	10	mulid2d	$⊢ φ \to 1 P = P$
12	6	ssrab3	$⊢ T \subseteq ℕ$
13		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
14	12 13	sseqtri	$⊢ T \subseteq ℤ_{\geq 1}$
15	1 2 3 4 5 6 7	4sqlem13	$⊢ φ \to (T \neq \emptyset \land M < P)$
16	15	simpld	$⊢ φ \to T \neq \emptyset$
17		infssuzcl	$⊢ (T \subseteq ℤ_{\geq 1} \land T \neq \emptyset) \to sup (T ℝ <) \in T$
18	14 16 17	sylancr	$⊢ φ \to sup (T ℝ <) \in T$
19	7 18	eqeltrid	$⊢ φ \to M \in T$
20		oveq1	$⊢ i = M \to i P = M P$
21	20	eleq1d	$⊢ i = M \to (i P \in S \leftrightarrow M P \in S)$
22	21 6	elrab2	$⊢ M \in T \leftrightarrow (M \in ℕ \land M P \in S)$
23	19 22	sylib	$⊢ φ \to (M \in ℕ \land M P \in S)$
24	23	simprd	$⊢ φ \to M P \in S$
25	1	4sqlem2	$⊢ M P \in S \leftrightarrow \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ M P = a^{2} + b^{2} + c^{2} + d^{2}$
26	24 25	sylib	$⊢ φ \to \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ M P = a^{2} + b^{2} + c^{2} + d^{2}$
27	26	adantr	$⊢ (φ \land M \in ℤ_{\geq 2}) \to \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ M P = a^{2} + b^{2} + c^{2} + d^{2}$
28		simp1l	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \land M P = a^{2} + b^{2} + c^{2} + d^{2}) \to φ$
29	28 2	syl	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \land M P = a^{2} + b^{2} + c^{2} + d^{2}) \to N \in ℕ$
30	28 3	syl	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \land M P = a^{2} + b^{2} + c^{2} + d^{2}) \to P = 2 \cdot N + 1$
31	28 4	syl	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \land M P = a^{2} + b^{2} + c^{2} + d^{2}) \to P \in ℙ$
32	28 5	syl	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \land M P = a^{2} + b^{2} + c^{2} + d^{2}) \to (0 \dots 2 \cdot N) \subseteq S$
33		simp1r	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \land M P = a^{2} + b^{2} + c^{2} + d^{2}) \to M \in ℤ_{\geq 2}$
34		simp2ll	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \land M P = a^{2} + b^{2} + c^{2} + d^{2}) \to a \in ℤ$
35		simp2lr	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \land M P = a^{2} + b^{2} + c^{2} + d^{2}) \to b \in ℤ$
36		simp2rl	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \land M P = a^{2} + b^{2} + c^{2} + d^{2}) \to c \in ℤ$
37		simp2rr	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \land M P = a^{2} + b^{2} + c^{2} + d^{2}) \to d \in ℤ$
38		eqid	$⊢ ((a + (\frac{M}{2})) \mod M) - (\frac{M}{2}) = ((a + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
39		eqid	$⊢ ((b + (\frac{M}{2})) \mod M) - (\frac{M}{2}) = ((b + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
40		eqid	$⊢ ((c + (\frac{M}{2})) \mod M) - (\frac{M}{2}) = ((c + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
41		eqid	$⊢ ((d + (\frac{M}{2})) \mod M) - (\frac{M}{2}) = ((d + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
42		eqid	$⊢ \frac{{(((a + (\frac{M}{2})) \mod M) - (\frac{M}{2}))}^{2} + {(((b + (\frac{M}{2})) \mod M) - (\frac{M}{2}))}^{2} + {(((c + (\frac{M}{2})) \mod M) - (\frac{M}{2}))}^{2} + {(((d + (\frac{M}{2})) \mod M) - (\frac{M}{2}))}^{2}}{M} = \frac{{(((a + (\frac{M}{2})) \mod M) - (\frac{M}{2}))}^{2} + {(((b + (\frac{M}{2})) \mod M) - (\frac{M}{2}))}^{2} + {(((c + (\frac{M}{2})) \mod M) - (\frac{M}{2}))}^{2} + {(((d + (\frac{M}{2})) \mod M) - (\frac{M}{2}))}^{2}}{M}$
43		simp3	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \land M P = a^{2} + b^{2} + c^{2} + d^{2}) \to M P = a^{2} + b^{2} + c^{2} + d^{2}$
44	1 29 30 31 32 6 7 33 34 35 36 37 38 39 40 41 42 43	4sqlem17	$⊢ \neg ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \land M P = a^{2} + b^{2} + c^{2} + d^{2})$
45	44	pm2.21i	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ)) \land M P = a^{2} + b^{2} + c^{2} + d^{2}) \to \neg M \in ℤ_{\geq 2}$
46	45	3expia	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land ((a \in ℤ \land b \in ℤ) \land (c \in ℤ \land d \in ℤ))) \to (M P = a^{2} + b^{2} + c^{2} + d^{2} \to \neg M \in ℤ_{\geq 2})$
47	46	anassrs	$⊢ (((φ \land M \in ℤ_{\geq 2}) \land (a \in ℤ \land b \in ℤ)) \land (c \in ℤ \land d \in ℤ)) \to (M P = a^{2} + b^{2} + c^{2} + d^{2} \to \neg M \in ℤ_{\geq 2})$
48	47	rexlimdvva	$⊢ ((φ \land M \in ℤ_{\geq 2}) \land (a \in ℤ \land b \in ℤ)) \to (\exists c \in ℤ \exists d \in ℤ M P = a^{2} + b^{2} + c^{2} + d^{2} \to \neg M \in ℤ_{\geq 2})$
49	48	rexlimdvva	$⊢ (φ \land M \in ℤ_{\geq 2}) \to (\exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ M P = a^{2} + b^{2} + c^{2} + d^{2} \to \neg M \in ℤ_{\geq 2})$
50	27 49	mpd	$⊢ (φ \land M \in ℤ_{\geq 2}) \to \neg M \in ℤ_{\geq 2}$
51	50	pm2.01da	$⊢ φ \to \neg M \in ℤ_{\geq 2}$
52	23	simpld	$⊢ φ \to M \in ℕ$
53		elnn1uz2	$⊢ M \in ℕ \leftrightarrow (M = 1 \lor M \in ℤ_{\geq 2})$
54	52 53	sylib	$⊢ φ \to (M = 1 \lor M \in ℤ_{\geq 2})$
55	54	ord	$⊢ φ \to (\neg M = 1 \to M \in ℤ_{\geq 2})$
56	51 55	mt3d	$⊢ φ \to M = 1$
57	56 19	eqeltrrd	$⊢ φ \to 1 \in T$
58		oveq1	$⊢ i = 1 \to i P = 1 P$
59	58	eleq1d	$⊢ i = 1 \to (i P \in S \leftrightarrow 1 P \in S)$
60	59 6	elrab2	$⊢ 1 \in T \leftrightarrow (1 \in ℕ \land 1 P \in S)$
61	60	simprbi	$⊢ 1 \in T \to 1 P \in S$
62	57 61	syl	$⊢ φ \to 1 P \in S$
63	11 62	eqeltrrd	$⊢ φ \to P \in S$

Metamath Proof Explorer

Theorem 4sqlem18

Proof