2sqlem11

	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	2sqlem11	$⊢ (P \in ℙ \land P \mod 4 = 1) \to P \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		simpr	$⊢ (P \in ℙ \land P \mod 4 = 1) \to P \mod 4 = 1$
4		simpl	$⊢ (P \in ℙ \land P \mod 4 = 1) \to P \in ℙ$
5		1ne2	$⊢ 1 \neq 2$
6	5	necomi	$⊢ 2 \neq 1$
7		oveq1	$⊢ P = 2 \to P \mod 4 = 2 \mod 4$
8		2re	$⊢ 2 \in ℝ$
9		4re	$⊢ 4 \in ℝ$
10		4pos	$⊢ 0 < 4$
11	9 10	elrpii	$⊢ 4 \in ℝ^{+}$
12		0le2	$⊢ 0 \leq 2$
13		2lt4	$⊢ 2 < 4$
14		modid	$⊢ ((2 \in ℝ \land 4 \in ℝ^{+}) \land (0 \leq 2 \land 2 < 4)) \to 2 \mod 4 = 2$
15	8 11 12 13 14	mp4an	$⊢ 2 \mod 4 = 2$
16	7 15	eqtrdi	$⊢ P = 2 \to P \mod 4 = 2$
17	16	neeq1d	$⊢ P = 2 \to (P \mod 4 \neq 1 \leftrightarrow 2 \neq 1)$
18	6 17	mpbiri	$⊢ P = 2 \to P \mod 4 \neq 1$
19	18	necon2i	$⊢ P \mod 4 = 1 \to P \neq 2$
20	3 19	syl	$⊢ (P \in ℙ \land P \mod 4 = 1) \to P \neq 2$
21		eldifsn	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land P \neq 2)$
22	4 20 21	sylanbrc	$⊢ (P \in ℙ \land P \mod 4 = 1) \to P \in (ℙ ∖ \{2\})$
23		m1lgs	$⊢ P \in (ℙ ∖ \{2\}) \to (-1 /_{L} P = 1 \leftrightarrow P \mod 4 = 1)$
24	22 23	syl	$⊢ (P \in ℙ \land P \mod 4 = 1) \to (-1 /_{L} P = 1 \leftrightarrow P \mod 4 = 1)$
25	3 24	mpbird	$⊢ (P \in ℙ \land P \mod 4 = 1) \to -1 /_{L} P = 1$
26		neg1z	$⊢ - 1 \in ℤ$
27		lgsqr	$⊢ (- 1 \in ℤ \land P \in (ℙ ∖ \{2\})) \to (-1 /_{L} P = 1 \leftrightarrow (\neg P ∥ -1 \land \exists n \in ℤ P ∥ (n^{2} - -1)))$
28	26 22 27	sylancr	$⊢ (P \in ℙ \land P \mod 4 = 1) \to (-1 /_{L} P = 1 \leftrightarrow (\neg P ∥ -1 \land \exists n \in ℤ P ∥ (n^{2} - -1)))$
29	25 28	mpbid	$⊢ (P \in ℙ \land P \mod 4 = 1) \to (\neg P ∥ -1 \land \exists n \in ℤ P ∥ (n^{2} - -1))$
30	29	simprd	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists n \in ℤ P ∥ (n^{2} - -1)$
31		simprl	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (n \in ℤ \land P ∥ (n^{2} - -1))) \to n \in ℤ$
32		1zzd	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (n \in ℤ \land P ∥ (n^{2} - -1))) \to 1 \in ℤ$
33		gcd1	$⊢ n \in ℤ \to n \gcd 1 = 1$
34	33	ad2antrl	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (n \in ℤ \land P ∥ (n^{2} - -1))) \to n \gcd 1 = 1$
35		eqidd	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (n \in ℤ \land P ∥ (n^{2} - -1))) \to n^{2} + 1 = n^{2} + 1$
36		oveq1	$⊢ x = n \to x \gcd y = n \gcd y$
37	36	eqeq1d	$⊢ x = n \to (x \gcd y = 1 \leftrightarrow n \gcd y = 1)$
38		oveq1	$⊢ x = n \to x^{2} = n^{2}$
39	38	oveq1d	$⊢ x = n \to x^{2} + y^{2} = n^{2} + y^{2}$
40	39	eqeq2d	$⊢ x = n \to (n^{2} + 1 = x^{2} + y^{2} \leftrightarrow n^{2} + 1 = n^{2} + y^{2})$
41	37 40	anbi12d	$⊢ x = n \to ((x \gcd y = 1 \land n^{2} + 1 = x^{2} + y^{2}) \leftrightarrow (n \gcd y = 1 \land n^{2} + 1 = n^{2} + y^{2}))$
42		oveq2	$⊢ y = 1 \to n \gcd y = n \gcd 1$
43	42	eqeq1d	$⊢ y = 1 \to (n \gcd y = 1 \leftrightarrow n \gcd 1 = 1)$
44		oveq1	$⊢ y = 1 \to y^{2} = 1^{2}$
45		sq1	$⊢ 1^{2} = 1$
46	44 45	eqtrdi	$⊢ y = 1 \to y^{2} = 1$
47	46	oveq2d	$⊢ y = 1 \to n^{2} + y^{2} = n^{2} + 1$
48	47	eqeq2d	$⊢ y = 1 \to (n^{2} + 1 = n^{2} + y^{2} \leftrightarrow n^{2} + 1 = n^{2} + 1)$
49	43 48	anbi12d	$⊢ y = 1 \to ((n \gcd y = 1 \land n^{2} + 1 = n^{2} + y^{2}) \leftrightarrow (n \gcd 1 = 1 \land n^{2} + 1 = n^{2} + 1))$
50	41 49	rspc2ev	$⊢ (n \in ℤ \land 1 \in ℤ \land (n \gcd 1 = 1 \land n^{2} + 1 = n^{2} + 1)) \to \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land n^{2} + 1 = x^{2} + y^{2})$
51	31 32 34 35 50	syl112anc	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (n \in ℤ \land P ∥ (n^{2} - -1))) \to \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land n^{2} + 1 = x^{2} + y^{2})$
52		ovex	$⊢ n^{2} + 1 \in V$
53		eqeq1	$⊢ z = n^{2} + 1 \to (z = x^{2} + y^{2} \leftrightarrow n^{2} + 1 = x^{2} + y^{2})$
54	53	anbi2d	$⊢ z = n^{2} + 1 \to ((x \gcd y = 1 \land z = x^{2} + y^{2}) \leftrightarrow (x \gcd y = 1 \land n^{2} + 1 = x^{2} + y^{2}))$
55	54	2rexbidv	$⊢ z = n^{2} + 1 \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^{2} + 1 = x^{2} + y^{2}))$
56	52 55 2	elab2	$⊢ n^{2} + 1 \in Y \leftrightarrow \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land n^{2} + 1 = x^{2} + y^{2})$
57	51 56	sylibr	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (n \in ℤ \land P ∥ (n^{2} - -1))) \to n^{2} + 1 \in Y$
58		prmnn	$⊢ P \in ℙ \to P \in ℕ$
59	58	ad2antrr	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (n \in ℤ \land P ∥ (n^{2} - -1))) \to P \in ℕ$
60		simprr	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (n \in ℤ \land P ∥ (n^{2} - -1))) \to P ∥ (n^{2} - -1)$
61	31	zcnd	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (n \in ℤ \land P ∥ (n^{2} - -1))) \to n \in ℂ$
62	61	sqcld	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (n \in ℤ \land P ∥ (n^{2} - -1))) \to n^{2} \in ℂ$
63		ax-1cn	$⊢ 1 \in ℂ$
64		subneg	$⊢ (n^{2} \in ℂ \land 1 \in ℂ) \to n^{2} - -1 = n^{2} + 1$
65	62 63 64	sylancl	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (n \in ℤ \land P ∥ (n^{2} - -1))) \to n^{2} - -1 = n^{2} + 1$
66	60 65	breqtrd	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (n \in ℤ \land P ∥ (n^{2} - -1))) \to P ∥ (n^{2} + 1)$
67	1 2	2sqlem10	$⊢ (n^{2} + 1 \in Y \land P \in ℕ \land P ∥ (n^{2} + 1)) \to P \in S$
68	57 59 66 67	syl3anc	$⊢ ((P \in ℙ \land P \mod 4 = 1) \land (n \in ℤ \land P ∥ (n^{2} - -1))) \to P \in S$
69	30 68	rexlimddv	$⊢ (P \in ℙ \land P \mod 4 = 1) \to P \in S$

Metamath Proof Explorer

Theorem 2sqlem11

Proof