2sqlem8a

	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})\}$
	2sqlem9.5	$⊢ φ \to \forall b \in (1 \dots M - 1) \forall a \in Y (b ∥ a \to b \in S)$
	2sqlem9.7	$⊢ φ \to M ∥ N$
	2sqlem8.n	$⊢ φ \to N \in ℕ$
	2sqlem8.m	$⊢ φ \to M \in ℤ_{\geq 2}$
	2sqlem8.1	$⊢ φ \to A \in ℤ$
	2sqlem8.2	$⊢ φ \to B \in ℤ$
	2sqlem8.3	$⊢ φ \to A \gcd B = 1$
	2sqlem8.4	$⊢ φ \to N = A^{2} + B^{2}$
	2sqlem8.c	$⊢ C = ((A + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
	2sqlem8.d	$⊢ D = ((B + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
Assertion	2sqlem8a	$⊢ φ \to C \gcd D \in ℕ$

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		2sqlem9.5	$⊢ φ \to \forall b \in (1 \dots M - 1) \forall a \in Y (b ∥ a \to b \in S)$
4		2sqlem9.7	$⊢ φ \to M ∥ N$
5		2sqlem8.n	$⊢ φ \to N \in ℕ$
6		2sqlem8.m	$⊢ φ \to M \in ℤ_{\geq 2}$
7		2sqlem8.1	$⊢ φ \to A \in ℤ$
8		2sqlem8.2	$⊢ φ \to B \in ℤ$
9		2sqlem8.3	$⊢ φ \to A \gcd B = 1$
10		2sqlem8.4	$⊢ φ \to N = A^{2} + B^{2}$
11		2sqlem8.c	$⊢ C = ((A + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
12		2sqlem8.d	$⊢ D = ((B + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
13		eluz2b3	$⊢ M \in ℤ_{\geq 2} \leftrightarrow (M \in ℕ \land M \neq 1)$
14	6 13	sylib	$⊢ φ \to (M \in ℕ \land M \neq 1)$
15	14	simpld	$⊢ φ \to M \in ℕ$
16	7 15 11	4sqlem5	$⊢ φ \to (C \in ℤ \land \frac{A - C}{M} \in ℤ)$
17	16	simpld	$⊢ φ \to C \in ℤ$
18	8 15 12	4sqlem5	$⊢ φ \to (D \in ℤ \land \frac{B - D}{M} \in ℤ)$
19	18	simpld	$⊢ φ \to D \in ℤ$
20	14	simprd	$⊢ φ \to M \neq 1$
21		simpr	$⊢ (φ \land C^{2} = 0) \to C^{2} = 0$
22	7 15 11 21	4sqlem9	$⊢ (φ \land C^{2} = 0) \to M^{2} ∥ A^{2}$
23	22	ex	$⊢ φ \to (C^{2} = 0 \to M^{2} ∥ A^{2})$
24		eluzelz	$⊢ M \in ℤ_{\geq 2} \to M \in ℤ$
25	6 24	syl	$⊢ φ \to M \in ℤ$
26		dvdssq	$⊢ (M \in ℤ \land A \in ℤ) \to (M ∥ A \leftrightarrow M^{2} ∥ A^{2})$
27	25 7 26	syl2anc	$⊢ φ \to (M ∥ A \leftrightarrow M^{2} ∥ A^{2})$
28	23 27	sylibrd	$⊢ φ \to (C^{2} = 0 \to M ∥ A)$
29		simpr	$⊢ (φ \land D^{2} = 0) \to D^{2} = 0$
30	8 15 12 29	4sqlem9	$⊢ (φ \land D^{2} = 0) \to M^{2} ∥ B^{2}$
31	30	ex	$⊢ φ \to (D^{2} = 0 \to M^{2} ∥ B^{2})$
32		dvdssq	$⊢ (M \in ℤ \land B \in ℤ) \to (M ∥ B \leftrightarrow M^{2} ∥ B^{2})$
33	25 8 32	syl2anc	$⊢ φ \to (M ∥ B \leftrightarrow M^{2} ∥ B^{2})$
34	31 33	sylibrd	$⊢ φ \to (D^{2} = 0 \to M ∥ B)$
35		ax-1ne0	$⊢ 1 \neq 0$
36	35	a1i	$⊢ φ \to 1 \neq 0$
37	9 36	eqnetrd	$⊢ φ \to A \gcd B \neq 0$
38	37	neneqd	$⊢ φ \to \neg A \gcd B = 0$
39		gcdeq0	$⊢ (A \in ℤ \land B \in ℤ) \to (A \gcd B = 0 \leftrightarrow (A = 0 \land B = 0))$
40	7 8 39	syl2anc	$⊢ φ \to (A \gcd B = 0 \leftrightarrow (A = 0 \land B = 0))$
41	38 40	mtbid	$⊢ φ \to \neg (A = 0 \land B = 0)$
42		dvdslegcd	$⊢ ((M \in ℤ \land A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to ((M ∥ A \land M ∥ B) \to M \leq A \gcd B)$
43	25 7 8 41 42	syl31anc	$⊢ φ \to ((M ∥ A \land M ∥ B) \to M \leq A \gcd B)$
44	28 34 43	syl2and	$⊢ φ \to ((C^{2} = 0 \land D^{2} = 0) \to M \leq A \gcd B)$
45	9	breq2d	$⊢ φ \to (M \leq A \gcd B \leftrightarrow M \leq 1)$
46		nnle1eq1	$⊢ M \in ℕ \to (M \leq 1 \leftrightarrow M = 1)$
47	15 46	syl	$⊢ φ \to (M \leq 1 \leftrightarrow M = 1)$
48	45 47	bitrd	$⊢ φ \to (M \leq A \gcd B \leftrightarrow M = 1)$
49	44 48	sylibd	$⊢ φ \to ((C^{2} = 0 \land D^{2} = 0) \to M = 1)$
50	49	necon3ad	$⊢ φ \to (M \neq 1 \to \neg (C^{2} = 0 \land D^{2} = 0))$
51	20 50	mpd	$⊢ φ \to \neg (C^{2} = 0 \land D^{2} = 0)$
52	17	zcnd	$⊢ φ \to C \in ℂ$
53		sqeq0	$⊢ C \in ℂ \to (C^{2} = 0 \leftrightarrow C = 0)$
54	52 53	syl	$⊢ φ \to (C^{2} = 0 \leftrightarrow C = 0)$
55	19	zcnd	$⊢ φ \to D \in ℂ$
56		sqeq0	$⊢ D \in ℂ \to (D^{2} = 0 \leftrightarrow D = 0)$
57	55 56	syl	$⊢ φ \to (D^{2} = 0 \leftrightarrow D = 0)$
58	54 57	anbi12d	$⊢ φ \to ((C^{2} = 0 \land D^{2} = 0) \leftrightarrow (C = 0 \land D = 0))$
59	51 58	mtbid	$⊢ φ \to \neg (C = 0 \land D = 0)$
60		gcdn0cl	$⊢ ((C \in ℤ \land D \in ℤ) \land \neg (C = 0 \land D = 0)) \to C \gcd D \in ℕ$
61	17 19 59 60	syl21anc	$⊢ φ \to C \gcd D \in ℕ$

Metamath Proof Explorer

Theorem 2sqlem8a

Proof