2sqreultblem

Description: Lemma for 2sqreultb . (Contributed by AV, 10-Jun-2023) The prime needs not be odd, as observed by WL. (Revised by AV, 18-Jun-2023)

		Ref	Expression
	Assertion	2sqreultblem	$⊢ P \in ℙ \to (P \mod 4 = 1 \leftrightarrow \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P))$

Proof

Step	Hyp	Ref	Expression
1		2sqreultlem	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P)$
2	1	ex	$⊢ P \in ℙ \to (P \mod 4 = 1 \to \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P))$
3		2reu2rex	$⊢ \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P) \to \exists a \in ℕ_{0} \exists b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P)$
4		elsni	$⊢ P \in \{2\} \to P = 2$
5		eqeq2	$⊢ P = 2 \to (a^{2} + b^{2} = P \leftrightarrow a^{2} + b^{2} = 2)$
6	5	anbi2d	$⊢ P = 2 \to ((a < b \land a^{2} + b^{2} = P) \leftrightarrow (a < b \land a^{2} + b^{2} = 2))$
7	6	adantl	$⊢ ((a \in ℕ_{0} \land b \in ℕ_{0}) \land P = 2) \to ((a < b \land a^{2} + b^{2} = P) \leftrightarrow (a < b \land a^{2} + b^{2} = 2))$
8		2sq2	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to (a^{2} + b^{2} = 2 \leftrightarrow (a = 1 \land b = 1))$
9		breq12	$⊢ (a = 1 \land b = 1) \to (a < b \leftrightarrow 1 < 1)$
10		1re	$⊢ 1 \in ℝ$
11	10	ltnri	$⊢ \neg 1 < 1$
12	11	pm2.21i	$⊢ 1 < 1 \to P \mod 4 = 1$
13	9 12	biimtrdi	$⊢ (a = 1 \land b = 1) \to (a < b \to P \mod 4 = 1)$
14	8 13	biimtrdi	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to (a^{2} + b^{2} = 2 \to (a < b \to P \mod 4 = 1))$
15	14	impcomd	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to ((a < b \land a^{2} + b^{2} = 2) \to P \mod 4 = 1)$
16	15	adantr	$⊢ ((a \in ℕ_{0} \land b \in ℕ_{0}) \land P = 2) \to ((a < b \land a^{2} + b^{2} = 2) \to P \mod 4 = 1)$
17	7 16	sylbid	$⊢ ((a \in ℕ_{0} \land b \in ℕ_{0}) \land P = 2) \to ((a < b \land a^{2} + b^{2} = P) \to P \mod 4 = 1)$
18	17	ex	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to (P = 2 \to ((a < b \land a^{2} + b^{2} = P) \to P \mod 4 = 1))$
19	18	com23	$⊢ (a \in ℕ_{0} \land b \in ℕ_{0}) \to ((a < b \land a^{2} + b^{2} = P) \to (P = 2 \to P \mod 4 = 1))$
20	19	rexlimivv	$⊢ \exists a \in ℕ_{0} \exists b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P) \to (P = 2 \to P \mod 4 = 1)$
21	3 4 20	syl2imc	$⊢ P \in \{2\} \to (\exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P) \to P \mod 4 = 1)$
22	21	a1d	$⊢ P \in \{2\} \to (P \in ℙ \to (\exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P) \to P \mod 4 = 1))$
23		eldif	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land \neg P \in \{2\})$
24		eldifsnneq	$⊢ P \in (ℙ ∖ \{2\}) \to \neg P = 2$
25		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
26		id	$⊢ a^{2} + b^{2} = P \to a^{2} + b^{2} = P$
27	26	eqcomd	$⊢ a^{2} + b^{2} = P \to P = a^{2} + b^{2}$
28	27	adantl	$⊢ (a < b \land a^{2} + b^{2} = P) \to P = a^{2} + b^{2}$
29	28	reximi	$⊢ \exists b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P) \to \exists b \in ℕ_{0} P = a^{2} + b^{2}$
30	29	reximi	$⊢ \exists a \in ℕ_{0} \exists b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P) \to \exists a \in ℕ_{0} \exists b \in ℕ_{0} P = a^{2} + b^{2}$
31		ssrexv	$⊢ ℕ_{0} \subseteq ℤ \to (\exists b \in ℕ_{0} P = a^{2} + b^{2} \to \exists b \in ℤ P = a^{2} + b^{2})$
32	25 31	ax-mp	$⊢ \exists b \in ℕ_{0} P = a^{2} + b^{2} \to \exists b \in ℤ P = a^{2} + b^{2}$
33	32	reximi	$⊢ \exists a \in ℕ_{0} \exists b \in ℕ_{0} P = a^{2} + b^{2} \to \exists a \in ℕ_{0} \exists b \in ℤ P = a^{2} + b^{2}$
34	3 30 33	3syl	$⊢ \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P) \to \exists a \in ℕ_{0} \exists b \in ℤ P = a^{2} + b^{2}$
35		ssrexv	$⊢ ℕ_{0} \subseteq ℤ \to (\exists a \in ℕ_{0} \exists b \in ℤ P = a^{2} + b^{2} \to \exists a \in ℤ \exists b \in ℤ P = a^{2} + b^{2})$
36	25 34 35	mpsyl	$⊢ \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P) \to \exists a \in ℤ \exists b \in ℤ P = a^{2} + b^{2}$
37	36	adantl	$⊢ (P \in (ℙ ∖ \{2\}) \land \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P)) \to \exists a \in ℤ \exists b \in ℤ P = a^{2} + b^{2}$
38		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
39	38	adantr	$⊢ (P \in (ℙ ∖ \{2\}) \land \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P)) \to P \in ℙ$
40		2sqb	$⊢ P \in ℙ \to (\exists a \in ℤ \exists b \in ℤ P = a^{2} + b^{2} \leftrightarrow (P = 2 \lor P \mod 4 = 1))$
41	39 40	syl	$⊢ (P \in (ℙ ∖ \{2\}) \land \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P)) \to (\exists a \in ℤ \exists b \in ℤ P = a^{2} + b^{2} \leftrightarrow (P = 2 \lor P \mod 4 = 1))$
42	37 41	mpbid	$⊢ (P \in (ℙ ∖ \{2\}) \land \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P)) \to (P = 2 \lor P \mod 4 = 1)$
43	42	ord	$⊢ (P \in (ℙ ∖ \{2\}) \land \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P)) \to (\neg P = 2 \to P \mod 4 = 1)$
44	43	ex	$⊢ P \in (ℙ ∖ \{2\}) \to (\exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P) \to (\neg P = 2 \to P \mod 4 = 1))$
45	24 44	mpid	$⊢ P \in (ℙ ∖ \{2\}) \to (\exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P) \to P \mod 4 = 1)$
46	23 45	sylbir	$⊢ (P \in ℙ \land \neg P \in \{2\}) \to (\exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P) \to P \mod 4 = 1)$
47	46	expcom	$⊢ \neg P \in \{2\} \to (P \in ℙ \to (\exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P) \to P \mod 4 = 1))$
48	22 47	pm2.61i	$⊢ P \in ℙ \to (\exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P) \to P \mod 4 = 1)$
49	2 48	impbid	$⊢ P \in ℙ \to (P \mod 4 = 1 \leftrightarrow \exists! a \in ℕ_{0} \exists! b \in ℕ_{0} (a < b \land a^{2} + b^{2} = P))$

Metamath Proof Explorer

Theorem 2sqreultblem

Proof