2sqlem5

Description: Lemma for 2sq . If a number that is a sum of two squares is divisible by a prime that is a sum of two squares, then the quotient is a sum of two squares. (Contributed by Mario Carneiro, 20-Jun-2015)

	Ref	Expression
Hypotheses	2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
	2sqlem5.1	$⊢ φ \to N \in ℕ$
	2sqlem5.2	$⊢ φ \to P \in ℙ$
	2sqlem5.3	$⊢ φ \to N P \in S$
	2sqlem5.4	$⊢ φ \to P \in S$
Assertion	2sqlem5	$⊢ φ \to N \in S$

Proof

Step	Hyp	Ref	Expression
1		2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
2		2sqlem5.1	$⊢ φ \to N \in ℕ$
3		2sqlem5.2	$⊢ φ \to P \in ℙ$
4		2sqlem5.3	$⊢ φ \to N P \in S$
5		2sqlem5.4	$⊢ φ \to P \in S$
6	1	2sqlem2	$⊢ P \in S \leftrightarrow \exists p \in ℤ \exists q \in ℤ P = p^{2} + q^{2}$
7	5 6	sylib	$⊢ φ \to \exists p \in ℤ \exists q \in ℤ P = p^{2} + q^{2}$
8	1	2sqlem2	$⊢ N P \in S \leftrightarrow \exists x \in ℤ \exists y \in ℤ N P = x^{2} + y^{2}$
9	4 8	sylib	$⊢ φ \to \exists x \in ℤ \exists y \in ℤ N P = x^{2} + y^{2}$
10		reeanv	$⊢ \exists p \in ℤ \exists x \in ℤ (\exists q \in ℤ P = p^{2} + q^{2} \land \exists y \in ℤ N P = x^{2} + y^{2}) \leftrightarrow (\exists p \in ℤ \exists q \in ℤ P = p^{2} + q^{2} \land \exists x \in ℤ \exists y \in ℤ N P = x^{2} + y^{2})$
11		reeanv	$⊢ \exists q \in ℤ \exists y \in ℤ (P = p^{2} + q^{2} \land N P = x^{2} + y^{2}) \leftrightarrow (\exists q \in ℤ P = p^{2} + q^{2} \land \exists y \in ℤ N P = x^{2} + y^{2})$
12	2	ad2antrr	$⊢ ((φ \land (p \in ℤ \land x \in ℤ)) \land ((q \in ℤ \land y \in ℤ) \land (P = p^{2} + q^{2} \land N P = x^{2} + y^{2}))) \to N \in ℕ$
13	3	ad2antrr	$⊢ ((φ \land (p \in ℤ \land x \in ℤ)) \land ((q \in ℤ \land y \in ℤ) \land (P = p^{2} + q^{2} \land N P = x^{2} + y^{2}))) \to P \in ℙ$
14		simplrr	$⊢ ((φ \land (p \in ℤ \land x \in ℤ)) \land ((q \in ℤ \land y \in ℤ) \land (P = p^{2} + q^{2} \land N P = x^{2} + y^{2}))) \to x \in ℤ$
15		simprlr	$⊢ ((φ \land (p \in ℤ \land x \in ℤ)) \land ((q \in ℤ \land y \in ℤ) \land (P = p^{2} + q^{2} \land N P = x^{2} + y^{2}))) \to y \in ℤ$
16		simplrl	$⊢ ((φ \land (p \in ℤ \land x \in ℤ)) \land ((q \in ℤ \land y \in ℤ) \land (P = p^{2} + q^{2} \land N P = x^{2} + y^{2}))) \to p \in ℤ$
17		simprll	$⊢ ((φ \land (p \in ℤ \land x \in ℤ)) \land ((q \in ℤ \land y \in ℤ) \land (P = p^{2} + q^{2} \land N P = x^{2} + y^{2}))) \to q \in ℤ$
18		simprrr	$⊢ ((φ \land (p \in ℤ \land x \in ℤ)) \land ((q \in ℤ \land y \in ℤ) \land (P = p^{2} + q^{2} \land N P = x^{2} + y^{2}))) \to N P = x^{2} + y^{2}$
19		simprrl	$⊢ ((φ \land (p \in ℤ \land x \in ℤ)) \land ((q \in ℤ \land y \in ℤ) \land (P = p^{2} + q^{2} \land N P = x^{2} + y^{2}))) \to P = p^{2} + q^{2}$
20	1 12 13 14 15 16 17 18 19	2sqlem4	$⊢ ((φ \land (p \in ℤ \land x \in ℤ)) \land ((q \in ℤ \land y \in ℤ) \land (P = p^{2} + q^{2} \land N P = x^{2} + y^{2}))) \to N \in S$
21	20	expr	$⊢ ((φ \land (p \in ℤ \land x \in ℤ)) \land (q \in ℤ \land y \in ℤ)) \to ((P = p^{2} + q^{2} \land N P = x^{2} + y^{2}) \to N \in S)$
22	21	rexlimdvva	$⊢ (φ \land (p \in ℤ \land x \in ℤ)) \to (\exists q \in ℤ \exists y \in ℤ (P = p^{2} + q^{2} \land N P = x^{2} + y^{2}) \to N \in S)$
23	11 22	syl5bir	$⊢ (φ \land (p \in ℤ \land x \in ℤ)) \to ((\exists q \in ℤ P = p^{2} + q^{2} \land \exists y \in ℤ N P = x^{2} + y^{2}) \to N \in S)$
24	23	rexlimdvva	$⊢ φ \to (\exists p \in ℤ \exists x \in ℤ (\exists q \in ℤ P = p^{2} + q^{2} \land \exists y \in ℤ N P = x^{2} + y^{2}) \to N \in S)$
25	10 24	syl5bir	$⊢ φ \to ((\exists p \in ℤ \exists q \in ℤ P = p^{2} + q^{2} \land \exists x \in ℤ \exists y \in ℤ N P = x^{2} + y^{2}) \to N \in S)$
26	7 9 25	mp2and	$⊢ φ \to N \in S$

Metamath Proof Explorer

Theorem 2sqlem5

Proof