4sqlem13

Description: Lemma for 4sq . (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 = inf (T ℝ <)$
Assertion	4sqlem13	$⊢ φ \to (T \neq \emptyset \land M < P)$

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 = inf (T ℝ <)$
8		eqid	$⊢ \{u \| \exists m \in (0 \dots N) u = m^{2} \mod P\} = \{u \| \exists m \in (0 \dots N) u = m^{2} \mod P\}$
9		eqid	$⊢ (v \in \{u \| \exists m \in (0 \dots N) u = m^{2} \mod P\} ⟼ P - 1 - v) = (v \in \{u \| \exists m \in (0 \dots N) u = m^{2} \mod P\} ⟼ P - 1 - v)$
10	1 2 3 4 8 9	4sqlem12	$⊢ φ \to \exists k \in (1 \dots P - 1) \exists u \in ℤ [i] {\|u\|}^{2} + 1 = k P$
11		simplrl	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to k \in (1 \dots P - 1)$
12		elfznn	$⊢ k \in (1 \dots P - 1) \to k \in ℕ$
13	11 12	syl	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to k \in ℕ$
14		simpr	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to {\|u\|}^{2} + 1 = k P$
15		abs1	$⊢ \|1\| = 1$
16	15	oveq1i	$⊢ {\|1\|}^{2} = 1^{2}$
17		sq1	$⊢ 1^{2} = 1$
18	16 17	eqtri	$⊢ {\|1\|}^{2} = 1$
19	18	oveq2i	$⊢ {\|u\|}^{2} + {\|1\|}^{2} = {\|u\|}^{2} + 1$
20		simplrr	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to u \in ℤ [i]$
21		1z	$⊢ 1 \in ℤ$
22		zgz	$⊢ 1 \in ℤ \to 1 \in ℤ [i]$
23	21 22	ax-mp	$⊢ 1 \in ℤ [i]$
24	1	4sqlem4a	$⊢ (u \in ℤ [i] \land 1 \in ℤ [i]) \to {\|u\|}^{2} + {\|1\|}^{2} \in S$
25	20 23 24	sylancl	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to {\|u\|}^{2} + {\|1\|}^{2} \in S$
26	19 25	eqeltrrid	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to {\|u\|}^{2} + 1 \in S$
27	14 26	eqeltrrd	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to k P \in S$
28		oveq1	$⊢ i = k \to i P = k P$
29	28	eleq1d	$⊢ i = k \to (i P \in S \leftrightarrow k P \in S)$
30	29 6	elrab2	$⊢ k \in T \leftrightarrow (k \in ℕ \land k P \in S)$
31	13 27 30	sylanbrc	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to k \in T$
32	31	ne0d	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to T \neq \emptyset$
33	6	ssrab3	$⊢ T \subseteq ℕ$
34		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
35	33 34	sseqtri	$⊢ T \subseteq ℤ_{\geq 1}$
36		infssuzcl	$⊢ (T \subseteq ℤ_{\geq 1} \land T \neq \emptyset) \to inf (T ℝ <) \in T$
37	35 32 36	sylancr	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to inf (T ℝ <) \in T$
38	7 37	eqeltrid	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to M \in T$
39	33 38	sselid	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to M \in ℕ$
40	39	nnred	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to M \in ℝ$
41	13	nnred	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to k \in ℝ$
42	4	ad2antrr	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to P \in ℙ$
43		prmnn	$⊢ P \in ℙ \to P \in ℕ$
44	42 43	syl	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to P \in ℕ$
45	44	nnred	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to P \in ℝ$
46		infssuzle	$⊢ (T \subseteq ℤ_{\geq 1} \land k \in T) \to inf (T ℝ <) \leq k$
47	35 31 46	sylancr	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to inf (T ℝ <) \leq k$
48	7 47	eqbrtrid	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to M \leq k$
49		prmz	$⊢ P \in ℙ \to P \in ℤ$
50	42 49	syl	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to P \in ℤ$
51		elfzm11	$⊢ (1 \in ℤ \land P \in ℤ) \to (k \in (1 \dots P - 1) \leftrightarrow (k \in ℤ \land 1 \leq k \land k < P))$
52	21 50 51	sylancr	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to (k \in (1 \dots P - 1) \leftrightarrow (k \in ℤ \land 1 \leq k \land k < P))$
53	11 52	mpbid	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to (k \in ℤ \land 1 \leq k \land k < P)$
54	53	simp3d	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to k < P$
55	40 41 45 48 54	lelttrd	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to M < P$
56	32 55	jca	$⊢ ((φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \land {\|u\|}^{2} + 1 = k P) \to (T \neq \emptyset \land M < P)$
57	56	ex	$⊢ (φ \land (k \in (1 \dots P - 1) \land u \in ℤ [i])) \to ({\|u\|}^{2} + 1 = k P \to (T \neq \emptyset \land M < P))$
58	57	rexlimdvva	$⊢ φ \to (\exists k \in (1 \dots P - 1) \exists u \in ℤ [i] {\|u\|}^{2} + 1 = k P \to (T \neq \emptyset \land M < P))$
59	10 58	mpd	$⊢ φ \to (T \neq \emptyset \land M < P)$

Metamath Proof Explorer

Theorem 4sqlem13

Proof