Metamath Proof Explorer

Theorem 2sq

Description: All primes of the form 4 k + 1 are sums of two squares. This is Metamath 100 proof #20. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Assertion 2sq ⊢ P ∈ ℙ ∧ P mod 4 = 1 → ∃ x ∈ ℤ ∃ y ∈ ℤ P = x 2 + y 2

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran ⁡ w ∈ ℤ i ⟼ w 2 = ran ⁡ w ∈ ℤ i ⟼ w 2
2 oveq1 ⊢ a = x → a gcd b = x gcd b
3 2 eqeq1d ⊢ a = x → a gcd b = 1 ↔ x gcd b = 1
4 oveq1 ⊢ a = x → a 2 = x 2
5 4 oveq1d ⊢ a = x → a 2 + b 2 = x 2 + b 2
6 5 eqeq2d ⊢ a = x → z = a 2 + b 2 ↔ z = x 2 + b 2
7 3 6 anbi12d ⊢ a = x → a gcd b = 1 ∧ z = a 2 + b 2 ↔ x gcd b = 1 ∧ z = x 2 + b 2
8 oveq2 ⊢ b = y → x gcd b = x gcd y
9 8 eqeq1d ⊢ b = y → x gcd b = 1 ↔ x gcd y = 1
10 oveq1 ⊢ b = y → b 2 = y 2
11 10 oveq2d ⊢ b = y → x 2 + b 2 = x 2 + y 2
12 11 eqeq2d ⊢ b = y → z = x 2 + b 2 ↔ z = x 2 + y 2
13 9 12 anbi12d ⊢ b = y → x gcd b = 1 ∧ z = x 2 + b 2 ↔ x gcd y = 1 ∧ z = x 2 + y 2
14 7 13 cbvrex2vw ⊢ ∃ a ∈ ℤ ∃ b ∈ ℤ a gcd b = 1 ∧ z = a 2 + b 2 ↔ ∃ x ∈ ℤ ∃ y ∈ ℤ x gcd y = 1 ∧ z = x 2 + y 2
15 14 abbii ⊢ z | ∃ a ∈ ℤ ∃ b ∈ ℤ a gcd b = 1 ∧ z = a 2 + b 2 = z | ∃ x ∈ ℤ ∃ y ∈ ℤ x gcd y = 1 ∧ z = x 2 + y 2
16 1 15 2sqlem11 ⊢ P ∈ ℙ ∧ P mod 4 = 1 → P ∈ ran ⁡ w ∈ ℤ i ⟼ w 2
17 1 2sqlem2 ⊢ P ∈ ran ⁡ w ∈ ℤ i ⟼ w 2 ↔ ∃ x ∈ ℤ ∃ y ∈ ℤ P = x 2 + y 2
18 16 17 sylib ⊢ P ∈ ℙ ∧ P mod 4 = 1 → ∃ x ∈ ℤ ∃ y ∈ ℤ P = x 2 + y 2