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	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) ) = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2		oveq1	⊢ ( 𝑎 = 𝑥 → ( 𝑎 gcd 𝑏 ) = ( 𝑥 gcd 𝑏 ) )
3	2	eqeq1d	⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 gcd 𝑏 ) = 1 ↔ ( 𝑥 gcd 𝑏 ) = 1 ) )
4		oveq1	⊢ ( 𝑎 = 𝑥 → ( 𝑎 ↑ 2 ) = ( 𝑥 ↑ 2 ) )
5	4	oveq1d	⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) )
6	5	eqeq2d	⊢ ( 𝑎 = 𝑥 → ( 𝑧 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ↔ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ) )
7	3 6	anbi12d	⊢ ( 𝑎 = 𝑥 → ( ( ( 𝑎 gcd 𝑏 ) = 1 ∧ 𝑧 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ) ↔ ( ( 𝑥 gcd 𝑏 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ) ) )
8		oveq2	⊢ ( 𝑏 = 𝑦 → ( 𝑥 gcd 𝑏 ) = ( 𝑥 gcd 𝑦 ) )
9	8	eqeq1d	⊢ ( 𝑏 = 𝑦 → ( ( 𝑥 gcd 𝑏 ) = 1 ↔ ( 𝑥 gcd 𝑦 ) = 1 ) )
10		oveq1	⊢ ( 𝑏 = 𝑦 → ( 𝑏 ↑ 2 ) = ( 𝑦 ↑ 2 ) )
11	10	oveq2d	⊢ ( 𝑏 = 𝑦 → ( ( 𝑥 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
12	11	eqeq2d	⊢ ( 𝑏 = 𝑦 → ( 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ↔ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
13	9 12	anbi12d	⊢ ( 𝑏 = 𝑦 → ( ( ( 𝑥 gcd 𝑏 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ) ↔ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) ) )
14	7 13	cbvrex2vw	⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( 𝑎 gcd 𝑏 ) = 1 ∧ 𝑧 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
15	14	abbii	⊢ { 𝑧 ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( 𝑎 gcd 𝑏 ) = 1 ∧ 𝑧 = ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) ) } = { 𝑧 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( 𝑥 gcd 𝑦 ) = 1 ∧ 𝑧 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) }
16	1 15	2sqlem11	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → 𝑃 ∈ ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) ) )
17	1	2sqlem2	⊢ ( 𝑃 ∈ ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
18	16 17	sylib	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 1 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝑃 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )