Step 
Hyp 
Ref 
Expression 
1 

biid 
⊢ ( ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) 
2 
1

2sqreu 
⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ( ∃! 𝑎 ∈ ℕ_{0} ∃ 𝑏 ∈ ℕ_{0} ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ∃! 𝑏 ∈ ℕ_{0} ∃ 𝑎 ∈ ℕ_{0} ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ) 
3 

fveq2 
⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 1^{st} ‘ 𝑝 ) = ( 1^{st} ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) 
4 

fveq2 
⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 2^{nd} ‘ 𝑝 ) = ( 2^{nd} ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) 
5 
3 4

breq12d 
⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 1^{st} ‘ 𝑝 ) ≤ ( 2^{nd} ‘ 𝑝 ) ↔ ( 1^{st} ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ≤ ( 2^{nd} ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ) ) 
6 

vex 
⊢ 𝑎 ∈ V 
7 

vex 
⊢ 𝑏 ∈ V 
8 
6 7

op1st 
⊢ ( 1^{st} ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑎 
9 
6 7

op2nd 
⊢ ( 2^{nd} ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑏 
10 
8 9

breq12i 
⊢ ( ( 1^{st} ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ≤ ( 2^{nd} ‘ ⟨ 𝑎 , 𝑏 ⟩ ) ↔ 𝑎 ≤ 𝑏 ) 
11 
5 10

syl6bb 
⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 1^{st} ‘ 𝑝 ) ≤ ( 2^{nd} ‘ 𝑝 ) ↔ 𝑎 ≤ 𝑏 ) ) 
12 
6 7

op1std 
⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 1^{st} ‘ 𝑝 ) = 𝑎 ) 
13 
12

oveq1d 
⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 1^{st} ‘ 𝑝 ) ↑ 2 ) = ( 𝑎 ↑ 2 ) ) 
14 
6 7

op2ndd 
⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( 2^{nd} ‘ 𝑝 ) = 𝑏 ) 
15 
14

oveq1d 
⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 2^{nd} ‘ 𝑝 ) ↑ 2 ) = ( 𝑏 ↑ 2 ) ) 
16 
13 15

oveq12d 
⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 1^{st} ‘ 𝑝 ) ↑ 2 ) + ( ( 2^{nd} ‘ 𝑝 ) ↑ 2 ) ) = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ) 
17 
16

eqeq1d 
⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( ( 1^{st} ‘ 𝑝 ) ↑ 2 ) + ( ( 2^{nd} ‘ 𝑝 ) ↑ 2 ) ) = 𝑃 ↔ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) 
18 
11 17

anbi12d 
⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 1^{st} ‘ 𝑝 ) ≤ ( 2^{nd} ‘ 𝑝 ) ∧ ( ( ( 1^{st} ‘ 𝑝 ) ↑ 2 ) + ( ( 2^{nd} ‘ 𝑝 ) ↑ 2 ) ) = 𝑃 ) ↔ ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ) 
19 
18

opreu2reurex 
⊢ ( ∃! 𝑝 ∈ ( ℕ_{0} × ℕ_{0} ) ( ( 1^{st} ‘ 𝑝 ) ≤ ( 2^{nd} ‘ 𝑝 ) ∧ ( ( ( 1^{st} ‘ 𝑝 ) ↑ 2 ) + ( ( 2^{nd} ‘ 𝑝 ) ↑ 2 ) ) = 𝑃 ) ↔ ( ∃! 𝑎 ∈ ℕ_{0} ∃ 𝑏 ∈ ℕ_{0} ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ∧ ∃! 𝑏 ∈ ℕ_{0} ∃ 𝑎 ∈ ℕ_{0} ( 𝑎 ≤ 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ) 
20 
2 19

sylibr 
⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃! 𝑝 ∈ ( ℕ_{0} × ℕ_{0} ) ( ( 1^{st} ‘ 𝑝 ) ≤ ( 2^{nd} ‘ 𝑝 ) ∧ ( ( ( 1^{st} ‘ 𝑝 ) ↑ 2 ) + ( ( 2^{nd} ‘ 𝑝 ) ↑ 2 ) ) = 𝑃 ) ) 