2sqb

Description: The converse to 2sq . (Contributed by Mario Carneiro, 20-Jun-2015)

		Ref	Expression
	Assertion	2sqb	$⊢ P \in ℙ \to (\exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2} \leftrightarrow (P = 2 \lor P \mod 4 = 1))$

Proof

Step	Hyp	Ref	Expression
1		df-ne	$⊢ P \neq 2 \leftrightarrow \neg P = 2$
2		prmz	$⊢ P \in ℙ \to P \in ℤ$
3	2	ad3antrrr	$⊢ (((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \land P = x^{2} + y^{2}) \to P \in ℤ$
4		simplrr	$⊢ (((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \land P = x^{2} + y^{2}) \to y \in ℤ$
5		bezout	$⊢ (P \in ℤ \land y \in ℤ) \to \exists a \in ℤ \exists b \in ℤ P \gcd y = P a + y b$
6	3 4 5	syl2anc	$⊢ (((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \land P = x^{2} + y^{2}) \to \exists a \in ℤ \exists b \in ℤ P \gcd y = P a + y b$
7		simplll	$⊢ ((((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \land P = x^{2} + y^{2}) \land ((a \in ℤ \land b \in ℤ) \land P \gcd y = P a + y b)) \to (P \in ℙ \land P \neq 2)$
8		simpllr	$⊢ ((((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \land P = x^{2} + y^{2}) \land ((a \in ℤ \land b \in ℤ) \land P \gcd y = P a + y b)) \to (x \in ℤ \land y \in ℤ)$
9		simplr	$⊢ ((((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \land P = x^{2} + y^{2}) \land ((a \in ℤ \land b \in ℤ) \land P \gcd y = P a + y b)) \to P = x^{2} + y^{2}$
10		simprll	$⊢ ((((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \land P = x^{2} + y^{2}) \land ((a \in ℤ \land b \in ℤ) \land P \gcd y = P a + y b)) \to a \in ℤ$
11		simprlr	$⊢ ((((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \land P = x^{2} + y^{2}) \land ((a \in ℤ \land b \in ℤ) \land P \gcd y = P a + y b)) \to b \in ℤ$
12		simprr	$⊢ ((((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \land P = x^{2} + y^{2}) \land ((a \in ℤ \land b \in ℤ) \land P \gcd y = P a + y b)) \to P \gcd y = P a + y b$
13	7 8 9 10 11 12	2sqblem	$⊢ ((((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \land P = x^{2} + y^{2}) \land ((a \in ℤ \land b \in ℤ) \land P \gcd y = P a + y b)) \to P \mod 4 = 1$
14	13	expr	$⊢ ((((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \land P = x^{2} + y^{2}) \land (a \in ℤ \land b \in ℤ)) \to (P \gcd y = P a + y b \to P \mod 4 = 1)$
15	14	rexlimdvva	$⊢ (((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \land P = x^{2} + y^{2}) \to (\exists a \in ℤ \exists b \in ℤ P \gcd y = P a + y b \to P \mod 4 = 1)$
16	6 15	mpd	$⊢ (((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \land P = x^{2} + y^{2}) \to P \mod 4 = 1$
17	16	ex	$⊢ ((P \in ℙ \land P \neq 2) \land (x \in ℤ \land y \in ℤ)) \to (P = x^{2} + y^{2} \to P \mod 4 = 1)$
18	17	rexlimdvva	$⊢ (P \in ℙ \land P \neq 2) \to (\exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2} \to P \mod 4 = 1)$
19	18	impancom	$⊢ (P \in ℙ \land \exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2}) \to (P \neq 2 \to P \mod 4 = 1)$
20	1 19	biimtrrid	$⊢ (P \in ℙ \land \exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2}) \to (\neg P = 2 \to P \mod 4 = 1)$
21	20	orrd	$⊢ (P \in ℙ \land \exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2}) \to (P = 2 \lor P \mod 4 = 1)$
22		1z	$⊢ 1 \in ℤ$
23		oveq1	$⊢ x = 1 \to x^{2} = 1^{2}$
24		sq1	$⊢ 1^{2} = 1$
25	23 24	eqtrdi	$⊢ x = 1 \to x^{2} = 1$
26	25	oveq1d	$⊢ x = 1 \to x^{2} + y^{2} = 1 + y^{2}$
27	26	eqeq2d	$⊢ x = 1 \to (P = x^{2} + y^{2} \leftrightarrow P = 1 + y^{2})$
28		oveq1	$⊢ y = 1 \to y^{2} = 1^{2}$
29	28 24	eqtrdi	$⊢ y = 1 \to y^{2} = 1$
30	29	oveq2d	$⊢ y = 1 \to 1 + y^{2} = 1 + 1$
31		1p1e2	$⊢ 1 + 1 = 2$
32	30 31	eqtrdi	$⊢ y = 1 \to 1 + y^{2} = 2$
33	32	eqeq2d	$⊢ y = 1 \to (P = 1 + y^{2} \leftrightarrow P = 2)$
34	27 33	rspc2ev	$⊢ (1 \in ℤ \land 1 \in ℤ \land P = 2) \to \exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2}$
35	22 22 34	mp3an12	$⊢ P = 2 \to \exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2}$
36	35	adantl	$⊢ (P \in ℙ \land P = 2) \to \exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2}$
37		2sq	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2}$
38	36 37	jaodan	$⊢ (P \in ℙ \land (P = 2 \lor P \mod 4 = 1)) \to \exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2}$
39	21 38	impbida	$⊢ P \in ℙ \to (\exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2} \leftrightarrow (P = 2 \lor P \mod 4 = 1))$

Metamath Proof Explorer

Theorem 2sqb

Proof