2sqlem7

	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})\}$
Assertion	2sqlem7	$⊢ Y \subseteq S \cap ℕ$

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		simpr	$⊢ (x \gcd y = 1 \land z = x^{2} + y^{2}) \to z = x^{2} + y^{2}$
4	3	reximi	$⊢ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2}) \to \exists y \in ℤ z = x^{2} + y^{2}$
5	4	reximi	$⊢ \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2}) \to \exists x \in ℤ \exists y \in ℤ z = x^{2} + y^{2}$
6	1	2sqlem2	$⊢ z \in S \leftrightarrow \exists x \in ℤ \exists y \in ℤ z = x^{2} + y^{2}$
7	5 6	sylibr	$⊢ \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2}) \to z \in S$
8		ax-1ne0	$⊢ 1 \neq 0$
9		gcdeq0	$⊢ (x \in ℤ \land y \in ℤ) \to (x \gcd y = 0 \leftrightarrow (x = 0 \land y = 0))$
10	9	adantr	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to (x \gcd y = 0 \leftrightarrow (x = 0 \land y = 0))$
11		simpr	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to x \gcd y = 1$
12	11	eqeq1d	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to (x \gcd y = 0 \leftrightarrow 1 = 0)$
13	10 12	bitr3d	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to ((x = 0 \land y = 0) \leftrightarrow 1 = 0)$
14	13	necon3bbid	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to (\neg (x = 0 \land y = 0) \leftrightarrow 1 \neq 0)$
15	8 14	mpbiri	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to \neg (x = 0 \land y = 0)$
16		zsqcl2	$⊢ x \in ℤ \to x^{2} \in ℕ_{0}$
17	16	ad2antrr	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to x^{2} \in ℕ_{0}$
18	17	nn0red	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to x^{2} \in ℝ$
19	17	nn0ge0d	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to 0 \leq x^{2}$
20		zsqcl2	$⊢ y \in ℤ \to y^{2} \in ℕ_{0}$
21	20	ad2antlr	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to y^{2} \in ℕ_{0}$
22	21	nn0red	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to y^{2} \in ℝ$
23	21	nn0ge0d	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to 0 \leq y^{2}$
24		add20	$⊢ ((x^{2} \in ℝ \land 0 \leq x^{2}) \land (y^{2} \in ℝ \land 0 \leq y^{2})) \to (x^{2} + y^{2} = 0 \leftrightarrow (x^{2} = 0 \land y^{2} = 0))$
25	18 19 22 23 24	syl22anc	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to (x^{2} + y^{2} = 0 \leftrightarrow (x^{2} = 0 \land y^{2} = 0))$
26		zcn	$⊢ x \in ℤ \to x \in ℂ$
27	26	ad2antrr	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to x \in ℂ$
28		zcn	$⊢ y \in ℤ \to y \in ℂ$
29	28	ad2antlr	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to y \in ℂ$
30		sqeq0	$⊢ x \in ℂ \to (x^{2} = 0 \leftrightarrow x = 0)$
31		sqeq0	$⊢ y \in ℂ \to (y^{2} = 0 \leftrightarrow y = 0)$
32	30 31	bi2anan9	$⊢ (x \in ℂ \land y \in ℂ) \to ((x^{2} = 0 \land y^{2} = 0) \leftrightarrow (x = 0 \land y = 0))$
33	27 29 32	syl2anc	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to ((x^{2} = 0 \land y^{2} = 0) \leftrightarrow (x = 0 \land y = 0))$
34	25 33	bitrd	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to (x^{2} + y^{2} = 0 \leftrightarrow (x = 0 \land y = 0))$
35	15 34	mtbird	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to \neg x^{2} + y^{2} = 0$
36		nn0addcl	$⊢ (x^{2} \in ℕ_{0} \land y^{2} \in ℕ_{0}) \to x^{2} + y^{2} \in ℕ_{0}$
37	16 20 36	syl2an	$⊢ (x \in ℤ \land y \in ℤ) \to x^{2} + y^{2} \in ℕ_{0}$
38	37	adantr	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to x^{2} + y^{2} \in ℕ_{0}$
39		elnn0	$⊢ x^{2} + y^{2} \in ℕ_{0} \leftrightarrow (x^{2} + y^{2} \in ℕ \lor x^{2} + y^{2} = 0)$
40	38 39	sylib	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to (x^{2} + y^{2} \in ℕ \lor x^{2} + y^{2} = 0)$
41	40	ord	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to (\neg x^{2} + y^{2} \in ℕ \to x^{2} + y^{2} = 0)$
42	35 41	mt3d	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to x^{2} + y^{2} \in ℕ$
43		eleq1	$⊢ z = x^{2} + y^{2} \to (z \in ℕ \leftrightarrow x^{2} + y^{2} \in ℕ)$
44	42 43	syl5ibrcom	$⊢ ((x \in ℤ \land y \in ℤ) \land x \gcd y = 1) \to (z = x^{2} + y^{2} \to z \in ℕ)$
45	44	expimpd	$⊢ (x \in ℤ \land y \in ℤ) \to ((x \gcd y = 1 \land z = x^{2} + y^{2}) \to z \in ℕ)$
46	45	rexlimivv	$⊢ \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2}) \to z \in ℕ$
47	7 46	elind	$⊢ \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2}) \to z \in (S \cap ℕ)$
48	47	abssi	$⊢ \{z \| \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2})\} \subseteq S \cap ℕ$
49	2 48	eqsstri	$⊢ Y \subseteq S \cap ℕ$

Metamath Proof Explorer

Theorem 2sqlem7

Proof