2sqlem10

Description: Lemma for 2sq . Every factor of a "proper" sum of two squares (where the summands are coprime) is a sum of two squares. (Contributed by Mario Carneiro, 19-Jun-2015)

	Ref	Expression
Hypotheses	2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
	2sqlem7.2	$⊢ Y = \{z \| \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2})\}$
Assertion	2sqlem10	$⊢ (A \in Y \land B \in ℕ \land B ∥ A) \to B \in S$

Proof

Step	Hyp	Ref	Expression
1		2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
2		2sqlem7.2	$⊢ Y = \{z \| \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2})\}$
3		breq1	$⊢ b = B \to (b ∥ a \leftrightarrow B ∥ a)$
4		eleq1	$⊢ b = B \to (b \in S \leftrightarrow B \in S)$
5	3 4	imbi12d	$⊢ b = B \to ((b ∥ a \to b \in S) \leftrightarrow (B ∥ a \to B \in S))$
6	5	ralbidv	$⊢ b = B \to (\forall a \in Y (b ∥ a \to b \in S) \leftrightarrow \forall a \in Y (B ∥ a \to B \in S))$
7		oveq2	$⊢ m = 1 \to (1 \dots m) = (1 \dots 1)$
8	7	raleqdv	$⊢ m = 1 \to (\forall b \in (1 \dots m) \forall a \in Y (b ∥ a \to b \in S) \leftrightarrow \forall b \in (1 \dots 1) \forall a \in Y (b ∥ a \to b \in S))$
9		oveq2	$⊢ m = n \to (1 \dots m) = (1 \dots n)$
10	9	raleqdv	$⊢ m = n \to (\forall b \in (1 \dots m) \forall a \in Y (b ∥ a \to b \in S) \leftrightarrow \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S))$
11		oveq2	$⊢ m = n + 1 \to (1 \dots m) = (1 \dots n + 1)$
12	11	raleqdv	$⊢ m = n + 1 \to (\forall b \in (1 \dots m) \forall a \in Y (b ∥ a \to b \in S) \leftrightarrow \forall b \in (1 \dots n + 1) \forall a \in Y (b ∥ a \to b \in S))$
13		oveq2	$⊢ m = B \to (1 \dots m) = (1 \dots B)$
14	13	raleqdv	$⊢ m = B \to (\forall b \in (1 \dots m) \forall a \in Y (b ∥ a \to b \in S) \leftrightarrow \forall b \in (1 \dots B) \forall a \in Y (b ∥ a \to b \in S))$
15		elfz1eq	$⊢ b \in (1 \dots 1) \to b = 1$
16		1z	$⊢ 1 \in ℤ$
17		zgz	$⊢ 1 \in ℤ \to 1 \in ℤ [i]$
18	16 17	ax-mp	$⊢ 1 \in ℤ [i]$
19		sq1	$⊢ 1^{2} = 1$
20	19	eqcomi	$⊢ 1 = 1^{2}$
21		fveq2	$⊢ x = 1 \to \|x\| = \|1\|$
22		abs1	$⊢ \|1\| = 1$
23	21 22	eqtrdi	$⊢ x = 1 \to \|x\| = 1$
24	23	oveq1d	$⊢ x = 1 \to {\|x\|}^{2} = 1^{2}$
25	24	rspceeqv	$⊢ (1 \in ℤ [i] \land 1 = 1^{2}) \to \exists x \in ℤ [i] 1 = {\|x\|}^{2}$
26	18 20 25	mp2an	$⊢ \exists x \in ℤ [i] 1 = {\|x\|}^{2}$
27	1	2sqlem1	$⊢ 1 \in S \leftrightarrow \exists x \in ℤ [i] 1 = {\|x\|}^{2}$
28	26 27	mpbir	$⊢ 1 \in S$
29	15 28	eqeltrdi	$⊢ b \in (1 \dots 1) \to b \in S$
30	29	a1d	$⊢ b \in (1 \dots 1) \to (b ∥ a \to b \in S)$
31	30	ralrimivw	$⊢ b \in (1 \dots 1) \to \forall a \in Y (b ∥ a \to b \in S)$
32	31	rgen	$⊢ \forall b \in (1 \dots 1) \forall a \in Y (b ∥ a \to b \in S)$
33		simplr	$⊢ ((n \in ℕ \land \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S)) \land (m \in Y \land (n + 1) ∥ m)) \to \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S)$
34		nncn	$⊢ n \in ℕ \to n \in ℂ$
35	34	ad2antrr	$⊢ ((n \in ℕ \land \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S)) \land (m \in Y \land (n + 1) ∥ m)) \to n \in ℂ$
36		ax-1cn	$⊢ 1 \in ℂ$
37		pncan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n + 1 - 1 = n$
38	35 36 37	sylancl	$⊢ ((n \in ℕ \land \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S)) \land (m \in Y \land (n + 1) ∥ m)) \to n + 1 - 1 = n$
39	38	oveq2d	$⊢ ((n \in ℕ \land \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S)) \land (m \in Y \land (n + 1) ∥ m)) \to (1 \dots n + 1 - 1) = (1 \dots n)$
40	39	raleqdv	$⊢ ((n \in ℕ \land \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S)) \land (m \in Y \land (n + 1) ∥ m)) \to (\forall b \in (1 \dots n + 1 - 1) \forall a \in Y (b ∥ a \to b \in S) \leftrightarrow \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S))$
41	33 40	mpbird	$⊢ ((n \in ℕ \land \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S)) \land (m \in Y \land (n + 1) ∥ m)) \to \forall b \in (1 \dots n + 1 - 1) \forall a \in Y (b ∥ a \to b \in S)$
42		simprr	$⊢ ((n \in ℕ \land \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S)) \land (m \in Y \land (n + 1) ∥ m)) \to (n + 1) ∥ m$
43		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
44	43	ad2antrr	$⊢ ((n \in ℕ \land \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S)) \land (m \in Y \land (n + 1) ∥ m)) \to n + 1 \in ℕ$
45		simprl	$⊢ ((n \in ℕ \land \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S)) \land (m \in Y \land (n + 1) ∥ m)) \to m \in Y$
46	1 2 41 42 44 45	2sqlem9	$⊢ ((n \in ℕ \land \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S)) \land (m \in Y \land (n + 1) ∥ m)) \to n + 1 \in S$
47	46	expr	$⊢ ((n \in ℕ \land \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S)) \land m \in Y) \to ((n + 1) ∥ m \to n + 1 \in S)$
48	47	ralrimiva	$⊢ (n \in ℕ \land \forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S)) \to \forall m \in Y ((n + 1) ∥ m \to n + 1 \in S)$
49	48	ex	$⊢ n \in ℕ \to (\forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S) \to \forall m \in Y ((n + 1) ∥ m \to n + 1 \in S))$
50		breq2	$⊢ a = m \to ((n + 1) ∥ a \leftrightarrow (n + 1) ∥ m)$
51	50	imbi1d	$⊢ a = m \to (((n + 1) ∥ a \to n + 1 \in S) \leftrightarrow ((n + 1) ∥ m \to n + 1 \in S))$
52	51	cbvralvw	$⊢ \forall a \in Y ((n + 1) ∥ a \to n + 1 \in S) \leftrightarrow \forall m \in Y ((n + 1) ∥ m \to n + 1 \in S)$
53	49 52	syl6ibr	$⊢ n \in ℕ \to (\forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S) \to \forall a \in Y ((n + 1) ∥ a \to n + 1 \in S))$
54		ovex	$⊢ n + 1 \in V$
55		breq1	$⊢ b = n + 1 \to (b ∥ a \leftrightarrow (n + 1) ∥ a)$
56		eleq1	$⊢ b = n + 1 \to (b \in S \leftrightarrow n + 1 \in S)$
57	55 56	imbi12d	$⊢ b = n + 1 \to ((b ∥ a \to b \in S) \leftrightarrow ((n + 1) ∥ a \to n + 1 \in S))$
58	57	ralbidv	$⊢ b = n + 1 \to (\forall a \in Y (b ∥ a \to b \in S) \leftrightarrow \forall a \in Y ((n + 1) ∥ a \to n + 1 \in S))$
59	54 58	ralsn	$⊢ \forall b \in \{n + 1\} \forall a \in Y (b ∥ a \to b \in S) \leftrightarrow \forall a \in Y ((n + 1) ∥ a \to n + 1 \in S)$
60	53 59	syl6ibr	$⊢ n \in ℕ \to (\forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S) \to \forall b \in \{n + 1\} \forall a \in Y (b ∥ a \to b \in S))$
61	60	ancld	$⊢ n \in ℕ \to (\forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S) \to (\forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S) \land \forall b \in \{n + 1\} \forall a \in Y (b ∥ a \to b \in S)))$
62		elnnuz	$⊢ n \in ℕ \leftrightarrow n \in ℤ_{\geq 1}$
63		fzsuc	$⊢ n \in ℤ_{\geq 1} \to (1 \dots n + 1) = (1 \dots n) \cup \{n + 1\}$
64	62 63	sylbi	$⊢ n \in ℕ \to (1 \dots n + 1) = (1 \dots n) \cup \{n + 1\}$
65	64	raleqdv	$⊢ n \in ℕ \to (\forall b \in (1 \dots n + 1) \forall a \in Y (b ∥ a \to b \in S) \leftrightarrow \forall b \in ((1 \dots n) \cup \{n + 1\}) \forall a \in Y (b ∥ a \to b \in S))$
66		ralunb	$⊢ \forall b \in ((1 \dots n) \cup \{n + 1\}) \forall a \in Y (b ∥ a \to b \in S) \leftrightarrow (\forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S) \land \forall b \in \{n + 1\} \forall a \in Y (b ∥ a \to b \in S))$
67	65 66	bitrdi	$⊢ n \in ℕ \to (\forall b \in (1 \dots n + 1) \forall a \in Y (b ∥ a \to b \in S) \leftrightarrow (\forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S) \land \forall b \in \{n + 1\} \forall a \in Y (b ∥ a \to b \in S)))$
68	61 67	sylibrd	$⊢ n \in ℕ \to (\forall b \in (1 \dots n) \forall a \in Y (b ∥ a \to b \in S) \to \forall b \in (1 \dots n + 1) \forall a \in Y (b ∥ a \to b \in S))$
69	8 10 12 14 32 68	nnind	$⊢ B \in ℕ \to \forall b \in (1 \dots B) \forall a \in Y (b ∥ a \to b \in S)$
70		elfz1end	$⊢ B \in ℕ \leftrightarrow B \in (1 \dots B)$
71	70	biimpi	$⊢ B \in ℕ \to B \in (1 \dots B)$
72	6 69 71	rspcdva	$⊢ B \in ℕ \to \forall a \in Y (B ∥ a \to B \in S)$
73		breq2	$⊢ a = A \to (B ∥ a \leftrightarrow B ∥ A)$
74	73	imbi1d	$⊢ a = A \to ((B ∥ a \to B \in S) \leftrightarrow (B ∥ A \to B \in S))$
75	74	rspcv	$⊢ A \in Y \to (\forall a \in Y (B ∥ a \to B \in S) \to (B ∥ A \to B \in S))$
76	72 75	syl5	$⊢ A \in Y \to (B \in ℕ \to (B ∥ A \to B \in S))$
77	76	3imp	$⊢ (A \in Y \land B \in ℕ \land B ∥ A) \to B \in S$

Metamath Proof Explorer

Theorem 2sqlem10

Proof