Metamath Proof Explorer

Theorem 2sqreuopb

Description: There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4 k + 1 . Alternate ordered pair variant of 2sqreunnltb . (Contributed by AV, 3-Jul-2023)

		Ref	Expression
	Assertion	2sqreuopb	$⊢ P \in ℙ \to (P \mod 4 = 1 \leftrightarrow \exists! p \in (ℕ \times ℕ) \exists a \exists b (p = ⟨a, b⟩ \land (a < b \land a^{2} + b^{2} = P)))$

Proof

Step	Hyp	Ref	Expression
1		2sqreuopnnltb	$⊢ P \in ℙ \to (P \mod 4 = 1 \leftrightarrow \exists! p \in (ℕ \times ℕ) (1^{st} (p) < 2^{nd} (p) \land {1^{st} (p)}^{2} + {2^{nd} (p)}^{2} = P))$
2		breq12	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to (a < b \leftrightarrow 1^{st} (p) < 2^{nd} (p))$
3		simpl	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to a = 1^{st} (p)$
4	3	oveq1d	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to a^{2} = {1^{st} (p)}^{2}$
5		simpr	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to b = 2^{nd} (p)$
6	5	oveq1d	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to b^{2} = {2^{nd} (p)}^{2}$
7	4 6	oveq12d	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to a^{2} + b^{2} = {1^{st} (p)}^{2} + {2^{nd} (p)}^{2}$
8	7	eqeq1d	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to (a^{2} + b^{2} = P \leftrightarrow {1^{st} (p)}^{2} + {2^{nd} (p)}^{2} = P)$
9	2 8	anbi12d	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to ((a < b \land a^{2} + b^{2} = P) \leftrightarrow (1^{st} (p) < 2^{nd} (p) \land {1^{st} (p)}^{2} + {2^{nd} (p)}^{2} = P))$
10	9	opreuopreu	$⊢ \exists! p \in (ℕ \times ℕ) (1^{st} (p) < 2^{nd} (p) \land {1^{st} (p)}^{2} + {2^{nd} (p)}^{2} = P) \leftrightarrow \exists! p \in (ℕ \times ℕ) \exists a \exists b (p = ⟨a, b⟩ \land (a < b \land a^{2} + b^{2} = P))$
11	1 10	syl6bb	$⊢ P \in ℙ \to (P \mod 4 = 1 \leftrightarrow \exists! p \in (ℕ \times ℕ) \exists a \exists b (p = ⟨a, b⟩ \land (a < b \land a^{2} + b^{2} = P)))$