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 \in ℙ \land P \mod 4 = 1) \to \exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2}$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ran (w \in ℤ [i] ⟼ {\|w\|}^{2}) = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
2		oveq1	$⊢ a = x \to a \gcd b = x \gcd b$
3	2	eqeq1d	$⊢ a = x \to (a \gcd b = 1 \leftrightarrow x \gcd b = 1)$
4		oveq1	$⊢ a = x \to a^{2} = x^{2}$
5	4	oveq1d	$⊢ a = x \to a^{2} + b^{2} = x^{2} + b^{2}$
6	5	eqeq2d	$⊢ a = x \to (z = a^{2} + b^{2} \leftrightarrow z = x^{2} + b^{2})$
7	3 6	anbi12d	$⊢ a = x \to ((a \gcd b = 1 \land z = a^{2} + b^{2}) \leftrightarrow (x \gcd b = 1 \land z = x^{2} + b^{2}))$
8		oveq2	$⊢ b = y \to x \gcd b = x \gcd y$
9	8	eqeq1d	$⊢ b = y \to (x \gcd b = 1 \leftrightarrow x \gcd y = 1)$
10		oveq1	$⊢ b = y \to b^{2} = y^{2}$
11	10	oveq2d	$⊢ b = y \to x^{2} + b^{2} = x^{2} + y^{2}$
12	11	eqeq2d	$⊢ b = y \to (z = x^{2} + b^{2} \leftrightarrow z = x^{2} + y^{2})$
13	9 12	anbi12d	$⊢ b = y \to ((x \gcd b = 1 \land z = x^{2} + b^{2}) \leftrightarrow (x \gcd y = 1 \land z = x^{2} + y^{2}))$
14	7 13	cbvrex2vw	$⊢ \exists a \in ℤ \exists b \in ℤ (a \gcd b = 1 \land z = a^{2} + b^{2}) \leftrightarrow \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2})$
15	14	abbii	$⊢ \{z \| \exists a \in ℤ \exists b \in ℤ (a \gcd b = 1 \land z = a^{2} + b^{2})\} = \{z \| \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2})\}$
16	1 15	2sqlem11	$⊢ (P \in ℙ \land P \mod 4 = 1) \to P \in ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
17	1	2sqlem2	$⊢ P \in ran (w \in ℤ [i] ⟼ {\|w\|}^{2}) \leftrightarrow \exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2}$
18	16 17	sylib	$⊢ (P \in ℙ \land P \mod 4 = 1) \to \exists x \in ℤ \exists y \in ℤ P = x^{2} + y^{2}$