2sqnn

Description: All primes of the form 4 k + 1 are sums of squares of two positive integers. (Contributed by AV, 11-Jun-2023)

		Ref	Expression
	Assertion	2sqnn	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}$

Proof

Step	Hyp	Ref	Expression
1		2sqnn0	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists a \in ℕ_{0} \exists b \in ℕ_{0} P = a^{2} + b^{2}$
2		elnn0	$⊢ a \in ℕ_{0} \leftrightarrow (a \in ℕ \lor a = 0)$
3		elnn0	$⊢ b \in ℕ_{0} \leftrightarrow (b \in ℕ \lor b = 0)$
4		oveq1	$⊢ x = a \to x^{2} = a^{2}$
5	4	oveq1d	$⊢ x = a \to x^{2} + y^{2} = a^{2} + y^{2}$
6	5	eqeq2d	$⊢ x = a \to (P = x^{2} + y^{2} \leftrightarrow P = a^{2} + y^{2})$
7		oveq1	$⊢ y = b \to y^{2} = b^{2}$
8	7	oveq2d	$⊢ y = b \to a^{2} + y^{2} = a^{2} + b^{2}$
9	8	eqeq2d	$⊢ y = b \to (P = a^{2} + y^{2} \leftrightarrow P = a^{2} + b^{2})$
10	6 9	rspc2ev	$⊢ (a \in ℕ \land b \in ℕ \land P = a^{2} + b^{2}) \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}$
11	10	3expia	$⊢ (a \in ℕ \land b \in ℕ) \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})$
12	11	a1d	$⊢ (a \in ℕ \land b \in ℕ) \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
13	12	expcom	$⊢ b \in ℕ \to (a \in ℕ \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})))$
14		sq0i	$⊢ a = 0 \to a^{2} = 0$
15	14	adantr	$⊢ (a = 0 \land b \in ℕ) \to a^{2} = 0$
16	15	oveq1d	$⊢ (a = 0 \land b \in ℕ) \to a^{2} + b^{2} = 0 + b^{2}$
17		nncn	$⊢ b \in ℕ \to b \in ℂ$
18	17	sqcld	$⊢ b \in ℕ \to b^{2} \in ℂ$
19	18	addid2d	$⊢ b \in ℕ \to 0 + b^{2} = b^{2}$
20	19	adantl	$⊢ (a = 0 \land b \in ℕ) \to 0 + b^{2} = b^{2}$
21	16 20	eqtrd	$⊢ (a = 0 \land b \in ℕ) \to a^{2} + b^{2} = b^{2}$
22	21	eqeq2d	$⊢ (a = 0 \land b \in ℕ) \to (P = a^{2} + b^{2} \leftrightarrow P = b^{2})$
23		eleq1	$⊢ P = b^{2} \to (P \in ℙ \leftrightarrow b^{2} \in ℙ)$
24	23	adantl	$⊢ (b \in ℕ \land P = b^{2}) \to (P \in ℙ \leftrightarrow b^{2} \in ℙ)$
25		nnz	$⊢ b \in ℕ \to b \in ℤ$
26		sqnprm	$⊢ b \in ℤ \to \neg b^{2} \in ℙ$
27	25 26	syl	$⊢ b \in ℕ \to \neg b^{2} \in ℙ$
28	27	pm2.21d	$⊢ b \in ℕ \to (b^{2} \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})$
29	28	adantr	$⊢ (b \in ℕ \land P = b^{2}) \to (b^{2} \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})$
30	24 29	sylbid	$⊢ (b \in ℕ \land P = b^{2}) \to (P \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})$
31	30	ex	$⊢ b \in ℕ \to (P = b^{2} \to (P \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
32	31	adantl	$⊢ (a = 0 \land b \in ℕ) \to (P = b^{2} \to (P \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
33	22 32	sylbid	$⊢ (a = 0 \land b \in ℕ) \to (P = a^{2} + b^{2} \to (P \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
34	33	com23	$⊢ (a = 0 \land b \in ℕ) \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
35	34	expcom	$⊢ b \in ℕ \to (a = 0 \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})))$
36	13 35	jaod	$⊢ b \in ℕ \to ((a \in ℕ \lor a = 0) \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})))$
37		sq0i	$⊢ b = 0 \to b^{2} = 0$
38	37	adantr	$⊢ (b = 0 \land a \in ℕ) \to b^{2} = 0$
39	38	oveq2d	$⊢ (b = 0 \land a \in ℕ) \to a^{2} + b^{2} = a^{2} + 0$
40		nncn	$⊢ a \in ℕ \to a \in ℂ$
41	40	sqcld	$⊢ a \in ℕ \to a^{2} \in ℂ$
42	41	addid1d	$⊢ a \in ℕ \to a^{2} + 0 = a^{2}$
43	42	adantl	$⊢ (b = 0 \land a \in ℕ) \to a^{2} + 0 = a^{2}$
44	39 43	eqtrd	$⊢ (b = 0 \land a \in ℕ) \to a^{2} + b^{2} = a^{2}$
45	44	eqeq2d	$⊢ (b = 0 \land a \in ℕ) \to (P = a^{2} + b^{2} \leftrightarrow P = a^{2})$
46		eleq1	$⊢ P = a^{2} \to (P \in ℙ \leftrightarrow a^{2} \in ℙ)$
47	46	adantl	$⊢ (a \in ℕ \land P = a^{2}) \to (P \in ℙ \leftrightarrow a^{2} \in ℙ)$
48		nnz	$⊢ a \in ℕ \to a \in ℤ$
49		sqnprm	$⊢ a \in ℤ \to \neg a^{2} \in ℙ$
50	48 49	syl	$⊢ a \in ℕ \to \neg a^{2} \in ℙ$
51	50	pm2.21d	$⊢ a \in ℕ \to (a^{2} \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})$
52	51	adantr	$⊢ (a \in ℕ \land P = a^{2}) \to (a^{2} \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})$
53	47 52	sylbid	$⊢ (a \in ℕ \land P = a^{2}) \to (P \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})$
54	53	ex	$⊢ a \in ℕ \to (P = a^{2} \to (P \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
55	54	adantl	$⊢ (b = 0 \land a \in ℕ) \to (P = a^{2} \to (P \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
56	45 55	sylbid	$⊢ (b = 0 \land a \in ℕ) \to (P = a^{2} + b^{2} \to (P \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
57	56	com23	$⊢ (b = 0 \land a \in ℕ) \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
58	57	ex	$⊢ b = 0 \to (a \in ℕ \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})))$
59	14 37	oveqan12rd	$⊢ (b = 0 \land a = 0) \to a^{2} + b^{2} = 0 + 0$
60		00id	$⊢ 0 + 0 = 0$
61	59 60	eqtrdi	$⊢ (b = 0 \land a = 0) \to a^{2} + b^{2} = 0$
62	61	eqeq2d	$⊢ (b = 0 \land a = 0) \to (P = a^{2} + b^{2} \leftrightarrow P = 0)$
63		eleq1	$⊢ P = 0 \to (P \in ℙ \leftrightarrow 0 \in ℙ)$
64		0nprm	$⊢ \neg 0 \in ℙ$
65	64	pm2.21i	$⊢ 0 \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}$
66	63 65	syl6bi	$⊢ P = 0 \to (P \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})$
67	62 66	syl6bi	$⊢ (b = 0 \land a = 0) \to (P = a^{2} + b^{2} \to (P \in ℙ \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
68	67	com23	$⊢ (b = 0 \land a = 0) \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
69	68	ex	$⊢ b = 0 \to (a = 0 \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})))$
70	58 69	jaod	$⊢ b = 0 \to ((a \in ℕ \lor a = 0) \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})))$
71	36 70	jaoi	$⊢ (b \in ℕ \lor b = 0) \to ((a \in ℕ \lor a = 0) \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})))$
72	3 71	sylbi	$⊢ b \in ℕ_{0} \to ((a \in ℕ \lor a = 0) \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})))$
73	72	com12	$⊢ (a \in ℕ \lor a = 0) \to (b \in ℕ_{0} \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})))$
74	2 73	sylbi	$⊢ a \in ℕ_{0} \to (b \in ℕ_{0} \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})))$
75	74	imp	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to (P \in ℙ \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
76	75	com12	$⊢ P \in ℙ \to ((a \in ℕ_{0} \land b \in ℕ_{0}) \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
77	76	adantr	$⊢ (P \in ℙ \land P \mod 4 = 1) \to ((a \in ℕ_{0} \land b \in ℕ_{0}) \to (P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}))$
78	77	rexlimdvv	$⊢ (P \in ℙ \land P \mod 4 = 1) \to (\exists a \in ℕ_{0} \exists b \in ℕ_{0} P = a^{2} + b^{2} \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2})$
79	1 78	mpd	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists x \in ℕ \exists y \in ℕ P = x^{2} + y^{2}$

Metamath Proof Explorer

Theorem 2sqnn

Proof