2sqlem9

	Ref	Expression
Hypotheses	2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
	2sqlem7.2	$⊢ Y = \{z \| \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2})\}$
	2sqlem9.5	$⊢ φ \to \forall b \in (1 \dots M - 1) \forall a \in Y (b ∥ a \to b \in S)$
	2sqlem9.7	$⊢ φ \to M ∥ N$
	2sqlem9.6	$⊢ φ \to M \in ℕ$
	2sqlem9.4	$⊢ φ \to N \in Y$
Assertion	2sqlem9	$⊢ φ \to M \in S$

Proof

Step	Hyp	Ref	Expression
1		2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
2		2sqlem7.2	$⊢ Y = \{z \| \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2})\}$
3		2sqlem9.5	$⊢ φ \to \forall b \in (1 \dots M - 1) \forall a \in Y (b ∥ a \to b \in S)$
4		2sqlem9.7	$⊢ φ \to M ∥ N$
5		2sqlem9.6	$⊢ φ \to M \in ℕ$
6		2sqlem9.4	$⊢ φ \to N \in Y$
7		eqeq1	$⊢ z = N \to (z = x^{2} + y^{2} \leftrightarrow N = x^{2} + y^{2})$
8	7	anbi2d	$⊢ z = N \to ((x \gcd y = 1 \land z = x^{2} + y^{2}) \leftrightarrow (x \gcd y = 1 \land N = x^{2} + y^{2}))$
9	8	2rexbidv	$⊢ z = N \to (\exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2}) \leftrightarrow \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land N = x^{2} + y^{2}))$
10		oveq1	$⊢ x = u \to x \gcd y = u \gcd y$
11	10	eqeq1d	$⊢ x = u \to (x \gcd y = 1 \leftrightarrow u \gcd y = 1)$
12		oveq1	$⊢ x = u \to x^{2} = u^{2}$
13	12	oveq1d	$⊢ x = u \to x^{2} + y^{2} = u^{2} + y^{2}$
14	13	eqeq2d	$⊢ x = u \to (N = x^{2} + y^{2} \leftrightarrow N = u^{2} + y^{2})$
15	11 14	anbi12d	$⊢ x = u \to ((x \gcd y = 1 \land N = x^{2} + y^{2}) \leftrightarrow (u \gcd y = 1 \land N = u^{2} + y^{2}))$
16		oveq2	$⊢ y = v \to u \gcd y = u \gcd v$
17	16	eqeq1d	$⊢ y = v \to (u \gcd y = 1 \leftrightarrow u \gcd v = 1)$
18		oveq1	$⊢ y = v \to y^{2} = v^{2}$
19	18	oveq2d	$⊢ y = v \to u^{2} + y^{2} = u^{2} + v^{2}$
20	19	eqeq2d	$⊢ y = v \to (N = u^{2} + y^{2} \leftrightarrow N = u^{2} + v^{2})$
21	17 20	anbi12d	$⊢ y = v \to ((u \gcd y = 1 \land N = u^{2} + y^{2}) \leftrightarrow (u \gcd v = 1 \land N = u^{2} + v^{2}))$
22	15 21	cbvrex2vw	$⊢ \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land N = x^{2} + y^{2}) \leftrightarrow \exists u \in ℤ \exists v \in ℤ (u \gcd v = 1 \land N = u^{2} + v^{2})$
23	9 22	bitrdi	$⊢ z = N \to (\exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2}) \leftrightarrow \exists u \in ℤ \exists v \in ℤ (u \gcd v = 1 \land N = u^{2} + v^{2}))$
24	23 2	elab2g	$⊢ N \in Y \to (N \in Y \leftrightarrow \exists u \in ℤ \exists v \in ℤ (u \gcd v = 1 \land N = u^{2} + v^{2}))$
25	24	ibi	$⊢ N \in Y \to \exists u \in ℤ \exists v \in ℤ (u \gcd v = 1 \land N = u^{2} + v^{2})$
26	6 25	syl	$⊢ φ \to \exists u \in ℤ \exists v \in ℤ (u \gcd v = 1 \land N = u^{2} + v^{2})$
27		simpr	$⊢ (((φ \land (u \in ℤ \land v \in ℤ)) \land (u \gcd v = 1 \land N = u^{2} + v^{2})) \land M = 1) \to M = 1$
28		1z	$⊢ 1 \in ℤ$
29		zgz	$⊢ 1 \in ℤ \to 1 \in ℤ [i]$
30	28 29	ax-mp	$⊢ 1 \in ℤ [i]$
31		sq1	$⊢ 1^{2} = 1$
32	31	eqcomi	$⊢ 1 = 1^{2}$
33		fveq2	$⊢ x = 1 \to \|x\| = \|1\|$
34		abs1	$⊢ \|1\| = 1$
35	33 34	eqtrdi	$⊢ x = 1 \to \|x\| = 1$
36	35	oveq1d	$⊢ x = 1 \to {\|x\|}^{2} = 1^{2}$
37	36	rspceeqv	$⊢ (1 \in ℤ [i] \land 1 = 1^{2}) \to \exists x \in ℤ [i] 1 = {\|x\|}^{2}$
38	30 32 37	mp2an	$⊢ \exists x \in ℤ [i] 1 = {\|x\|}^{2}$
39	1	2sqlem1	$⊢ 1 \in S \leftrightarrow \exists x \in ℤ [i] 1 = {\|x\|}^{2}$
40	38 39	mpbir	$⊢ 1 \in S$
41	27 40	eqeltrdi	$⊢ (((φ \land (u \in ℤ \land v \in ℤ)) \land (u \gcd v = 1 \land N = u^{2} + v^{2})) \land M = 1) \to M \in S$
42	3	ad2antrr	$⊢ ((φ \land (u \in ℤ \land v \in ℤ)) \land ((u \gcd v = 1 \land N = u^{2} + v^{2}) \land M \neq 1)) \to \forall b \in (1 \dots M - 1) \forall a \in Y (b ∥ a \to b \in S)$
43	4	ad2antrr	$⊢ ((φ \land (u \in ℤ \land v \in ℤ)) \land ((u \gcd v = 1 \land N = u^{2} + v^{2}) \land M \neq 1)) \to M ∥ N$
44	1 2	2sqlem7	$⊢ Y \subseteq S \cap ℕ$
45		inss2	$⊢ S \cap ℕ \subseteq ℕ$
46	44 45	sstri	$⊢ Y \subseteq ℕ$
47	46 6	sselid	$⊢ φ \to N \in ℕ$
48	47	ad2antrr	$⊢ ((φ \land (u \in ℤ \land v \in ℤ)) \land ((u \gcd v = 1 \land N = u^{2} + v^{2}) \land M \neq 1)) \to N \in ℕ$
49	5	ad2antrr	$⊢ ((φ \land (u \in ℤ \land v \in ℤ)) \land ((u \gcd v = 1 \land N = u^{2} + v^{2}) \land M \neq 1)) \to M \in ℕ$
50		simprr	$⊢ ((φ \land (u \in ℤ \land v \in ℤ)) \land ((u \gcd v = 1 \land N = u^{2} + v^{2}) \land M \neq 1)) \to M \neq 1$
51		eluz2b3	$⊢ M \in ℤ_{\geq 2} \leftrightarrow (M \in ℕ \land M \neq 1)$
52	49 50 51	sylanbrc	$⊢ ((φ \land (u \in ℤ \land v \in ℤ)) \land ((u \gcd v = 1 \land N = u^{2} + v^{2}) \land M \neq 1)) \to M \in ℤ_{\geq 2}$
53		simplrl	$⊢ ((φ \land (u \in ℤ \land v \in ℤ)) \land ((u \gcd v = 1 \land N = u^{2} + v^{2}) \land M \neq 1)) \to u \in ℤ$
54		simplrr	$⊢ ((φ \land (u \in ℤ \land v \in ℤ)) \land ((u \gcd v = 1 \land N = u^{2} + v^{2}) \land M \neq 1)) \to v \in ℤ$
55		simprll	$⊢ ((φ \land (u \in ℤ \land v \in ℤ)) \land ((u \gcd v = 1 \land N = u^{2} + v^{2}) \land M \neq 1)) \to u \gcd v = 1$
56		simprlr	$⊢ ((φ \land (u \in ℤ \land v \in ℤ)) \land ((u \gcd v = 1 \land N = u^{2} + v^{2}) \land M \neq 1)) \to N = u^{2} + v^{2}$
57		eqid	$⊢ ((u + (\frac{M}{2})) \mod M) - (\frac{M}{2}) = ((u + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
58		eqid	$⊢ ((v + (\frac{M}{2})) \mod M) - (\frac{M}{2}) = ((v + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
59		eqid	$⊢ \frac{((u + (\frac{M}{2})) \mod M) - (\frac{M}{2})}{(((u + (\frac{M}{2})) \mod M) - (\frac{M}{2})) \gcd (((v + (\frac{M}{2})) \mod M) - (\frac{M}{2}))} = \frac{((u + (\frac{M}{2})) \mod M) - (\frac{M}{2})}{(((u + (\frac{M}{2})) \mod M) - (\frac{M}{2})) \gcd (((v + (\frac{M}{2})) \mod M) - (\frac{M}{2}))}$
60		eqid	$⊢ \frac{((v + (\frac{M}{2})) \mod M) - (\frac{M}{2})}{(((u + (\frac{M}{2})) \mod M) - (\frac{M}{2})) \gcd (((v + (\frac{M}{2})) \mod M) - (\frac{M}{2}))} = \frac{((v + (\frac{M}{2})) \mod M) - (\frac{M}{2})}{(((u + (\frac{M}{2})) \mod M) - (\frac{M}{2})) \gcd (((v + (\frac{M}{2})) \mod M) - (\frac{M}{2}))}$
61	1 2 42 43 48 52 53 54 55 56 57 58 59 60	2sqlem8	$⊢ ((φ \land (u \in ℤ \land v \in ℤ)) \land ((u \gcd v = 1 \land N = u^{2} + v^{2}) \land M \neq 1)) \to M \in S$
62	61	anassrs	$⊢ (((φ \land (u \in ℤ \land v \in ℤ)) \land (u \gcd v = 1 \land N = u^{2} + v^{2})) \land M \neq 1) \to M \in S$
63	41 62	pm2.61dane	$⊢ ((φ \land (u \in ℤ \land v \in ℤ)) \land (u \gcd v = 1 \land N = u^{2} + v^{2})) \to M \in S$
64	63	ex	$⊢ (φ \land (u \in ℤ \land v \in ℤ)) \to ((u \gcd v = 1 \land N = u^{2} + v^{2}) \to M \in S)$
65	64	rexlimdvva	$⊢ φ \to (\exists u \in ℤ \exists v \in ℤ (u \gcd v = 1 \land N = u^{2} + v^{2}) \to M \in S)$
66	26 65	mpd	$⊢ φ \to M \in S$

Metamath Proof Explorer

Theorem 2sqlem9

Proof