Step |
Hyp |
Ref |
Expression |
1 |
|
2sqreult.1 |
⊢ ( 𝜑 ↔ ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) |
2 |
|
2sqreultblem |
⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 ↔ ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ) ) |
3 |
1
|
bicomi |
⊢ ( ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ 𝜑 ) |
4 |
3
|
reubii |
⊢ ( ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ∃! 𝑏 ∈ ℕ0 𝜑 ) |
5 |
4
|
reubii |
⊢ ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 𝜑 ) |
6 |
5
|
a1i |
⊢ ( 𝑃 ∈ ℙ → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 ( 𝑎 < 𝑏 ∧ ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = 𝑃 ) ↔ ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 𝜑 ) ) |
7 |
1
|
2sqreulem4 |
⊢ ∀ 𝑎 ∈ ℕ0 ∃* 𝑏 ∈ ℕ0 𝜑 |
8 |
|
2reu1 |
⊢ ( ∀ 𝑎 ∈ ℕ0 ∃* 𝑏 ∈ ℕ0 𝜑 → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 𝜑 ↔ ( ∃! 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 𝜑 ∧ ∃! 𝑏 ∈ ℕ0 ∃ 𝑎 ∈ ℕ0 𝜑 ) ) ) |
9 |
7 8
|
mp1i |
⊢ ( 𝑃 ∈ ℙ → ( ∃! 𝑎 ∈ ℕ0 ∃! 𝑏 ∈ ℕ0 𝜑 ↔ ( ∃! 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 𝜑 ∧ ∃! 𝑏 ∈ ℕ0 ∃ 𝑎 ∈ ℕ0 𝜑 ) ) ) |
10 |
2 6 9
|
3bitrd |
⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 mod 4 ) = 1 ↔ ( ∃! 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℕ0 𝜑 ∧ ∃! 𝑏 ∈ ℕ0 ∃ 𝑎 ∈ ℕ0 𝜑 ) ) ) |