Metamath Proof Explorer

Theorem 2sqreuopnnltb

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 . Ordered pair variant of 2sqreunnltb . (Contributed by AV, 3-Jul-2023)

Ref Expression
Assertion 2sqreuopnnltb ⊢P∈ℙ→Pmod4=1↔∃!p∈ℕ×ℕ1st⁡p<2nd⁡p∧1st⁡p2+2nd⁡p2=P

Proof

Step Hyp Ref Expression
1 biid ⊢a<b∧a2+b2=P↔a<b∧a2+b2=P
2 1 2sqreunnltb ⊢P∈ℙ→Pmod4=1↔∃!a∈ℕ∃b∈ℕa<b∧a2+b2=P∧∃!b∈ℕ∃a∈ℕa<b∧a2+b2=P
3 fveq2 ⊢p=ab→1st⁡p=1st⁡ab
4 fveq2 ⊢p=ab→2nd⁡p=2nd⁡ab
5 3 4 breq12d ⊢p=ab→1st⁡p<2nd⁡p↔1st⁡ab<2nd⁡ab
6 vex ⊢a∈V
7 vex ⊢b∈V
8 6 7 op1st ⊢1st⁡ab=a
9 6 7 op2nd ⊢2nd⁡ab=b
10 8 9 breq12i ⊢1st⁡ab<2nd⁡ab↔a<b
11 5 10 bitrdi ⊢p=ab→1st⁡p<2nd⁡p↔a<b
12 6 7 op1std ⊢p=ab→1st⁡p=a
13 12 oveq1d ⊢p=ab→1st⁡p2=a2
14 6 7 op2ndd ⊢p=ab→2nd⁡p=b
15 14 oveq1d ⊢p=ab→2nd⁡p2=b2
16 13 15 oveq12d ⊢p=ab→1st⁡p2+2nd⁡p2=a2+b2
17 16 eqeq1d ⊢p=ab→1st⁡p2+2nd⁡p2=P↔a2+b2=P
18 11 17 anbi12d ⊢p=ab→1st⁡p<2nd⁡p∧1st⁡p2+2nd⁡p2=P↔a<b∧a2+b2=P
19 18 opreu2reurex ⊢∃!p∈ℕ×ℕ1st⁡p<2nd⁡p∧1st⁡p2+2nd⁡p2=P↔∃!a∈ℕ∃b∈ℕa<b∧a2+b2=P∧∃!b∈ℕ∃a∈ℕa<b∧a2+b2=P
20 2 19 bitr4di ⊢P∈ℙ→Pmod4=1↔∃!p∈ℕ×ℕ1st⁡p<2nd⁡p∧1st⁡p2+2nd⁡p2=P