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	33 39	raleqtrrdv	$⊢ ((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)$
41		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$
42		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
43	42	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 ℕ$
44		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$
45	1 2 40 41 43 44	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$
46	45	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)$
47	46	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)$
48	47	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))$
49		breq2	$⊢ a = m \to ((n + 1) ∥ a \leftrightarrow (n + 1) ∥ m)$
50	49	imbi1d	$⊢ a = m \to (((n + 1) ∥ a \to n + 1 \in S) \leftrightarrow ((n + 1) ∥ m \to n + 1 \in S))$
51	50	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)$
52	48 51	imbitrrdi	$⊢ 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))$
53		ovex	$⊢ n + 1 \in V$
54		breq1	$⊢ b = n + 1 \to (b ∥ a \leftrightarrow (n + 1) ∥ a)$
55		eleq1	$⊢ b = n + 1 \to (b \in S \leftrightarrow n + 1 \in S)$
56	54 55	imbi12d	$⊢ b = n + 1 \to ((b ∥ a \to b \in S) \leftrightarrow ((n + 1) ∥ a \to n + 1 \in S))$
57	56	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))$
58	53 57	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)$
59	52 58	imbitrrdi	$⊢ 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))$
60	59	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)))$
61		elnnuz	$⊢ n \in ℕ \leftrightarrow n \in ℤ_{\geq 1}$
62		fzsuc	$⊢ n \in ℤ_{\geq 1} \to (1 \dots n + 1) = (1 \dots n) \cup \{n + 1\}$
63	61 62	sylbi	$⊢ n \in ℕ \to (1 \dots n + 1) = (1 \dots n) \cup \{n + 1\}$
64	63	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))$
65		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))$
66	64 65	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)))$
67	60 66	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))$
68	8 10 12 14 32 67	nnind	$⊢ B \in ℕ \to \forall b \in (1 \dots B) \forall a \in Y (b ∥ a \to b \in S)$
69		elfz1end	$⊢ B \in ℕ \leftrightarrow B \in (1 \dots B)$
70	69	biimpi	$⊢ B \in ℕ \to B \in (1 \dots B)$
71	6 68 70	rspcdva	$⊢ B \in ℕ \to \forall a \in Y (B ∥ a \to B \in S)$
72		breq2	$⊢ a = A \to (B ∥ a \leftrightarrow B ∥ A)$
73	72	imbi1d	$⊢ a = A \to ((B ∥ a \to B \in S) \leftrightarrow (B ∥ A \to B \in S))$
74	73	rspcv	$⊢ A \in Y \to (\forall a \in Y (B ∥ a \to B \in S) \to (B ∥ A \to B \in S))$
75	71 74	syl5	$⊢ A \in Y \to (B \in ℕ \to (B ∥ A \to B \in S))$
76	75	3imp	$⊢ (A \in Y \land B \in ℕ \land B ∥ A) \to B \in S$

Metamath Proof Explorer

Theorem 2sqlem10

Proof