bezoutlem1

	Ref	Expression
Hypotheses	bezout.1	$⊢ M = \{z \in ℕ \| \exists x \in ℤ \exists y \in ℤ z = A x + B y\}$
	bezout.3	$⊢ φ \to A \in ℤ$
	bezout.4	$⊢ φ \to B \in ℤ$
Assertion	bezoutlem1	$⊢ φ \to (A \neq 0 \to \|A\| \in M)$

Proof

Step	Hyp	Ref	Expression
1		bezout.1	$⊢ M = \{z \in ℕ \| \exists x \in ℤ \exists y \in ℤ z = A x + B y\}$
2		bezout.3	$⊢ φ \to A \in ℤ$
3		bezout.4	$⊢ φ \to B \in ℤ$
4		fveq2	$⊢ z = A \to \|z\| = \|A\|$
5		oveq1	$⊢ z = A \to z x = A x$
6	4 5	eqeq12d	$⊢ z = A \to (\|z\| = z x \leftrightarrow \|A\| = A x)$
7	6	rexbidv	$⊢ z = A \to (\exists x \in ℤ \|z\| = z x \leftrightarrow \exists x \in ℤ \|A\| = A x)$
8		zre	$⊢ z \in ℤ \to z \in ℝ$
9		1z	$⊢ 1 \in ℤ$
10		ax-1rid	$⊢ z \in ℝ \to z \cdot 1 = z$
11	10	eqcomd	$⊢ z \in ℝ \to z = z \cdot 1$
12		oveq2	$⊢ x = 1 \to z x = z \cdot 1$
13	12	rspceeqv	$⊢ (1 \in ℤ \land z = z \cdot 1) \to \exists x \in ℤ z = z x$
14	9 11 13	sylancr	$⊢ z \in ℝ \to \exists x \in ℤ z = z x$
15		eqeq1	$⊢ \|z\| = z \to (\|z\| = z x \leftrightarrow z = z x)$
16	15	rexbidv	$⊢ \|z\| = z \to (\exists x \in ℤ \|z\| = z x \leftrightarrow \exists x \in ℤ z = z x)$
17	14 16	syl5ibrcom	$⊢ z \in ℝ \to (\|z\| = z \to \exists x \in ℤ \|z\| = z x)$
18		neg1z	$⊢ - 1 \in ℤ$
19		recn	$⊢ z \in ℝ \to z \in ℂ$
20	19	mulm1d	$⊢ z \in ℝ \to -1 z = - z$
21		neg1cn	$⊢ - 1 \in ℂ$
22		mulcom	$⊢ (- 1 \in ℂ \land z \in ℂ) \to -1 z = z -1$
23	21 19 22	sylancr	$⊢ z \in ℝ \to -1 z = z -1$
24	20 23	eqtr3d	$⊢ z \in ℝ \to - z = z -1$
25		oveq2	$⊢ x = - 1 \to z x = z -1$
26	25	rspceeqv	$⊢ (- 1 \in ℤ \land - z = z -1) \to \exists x \in ℤ - z = z x$
27	18 24 26	sylancr	$⊢ z \in ℝ \to \exists x \in ℤ - z = z x$
28		eqeq1	$⊢ \|z\| = - z \to (\|z\| = z x \leftrightarrow - z = z x)$
29	28	rexbidv	$⊢ \|z\| = - z \to (\exists x \in ℤ \|z\| = z x \leftrightarrow \exists x \in ℤ - z = z x)$
30	27 29	syl5ibrcom	$⊢ z \in ℝ \to (\|z\| = - z \to \exists x \in ℤ \|z\| = z x)$
31		absor	$⊢ z \in ℝ \to (\|z\| = z \lor \|z\| = - z)$
32	17 30 31	mpjaod	$⊢ z \in ℝ \to \exists x \in ℤ \|z\| = z x$
33	8 32	syl	$⊢ z \in ℤ \to \exists x \in ℤ \|z\| = z x$
34	7 33	vtoclga	$⊢ A \in ℤ \to \exists x \in ℤ \|A\| = A x$
35	2 34	syl	$⊢ φ \to \exists x \in ℤ \|A\| = A x$
36	3	zcnd	$⊢ φ \to B \in ℂ$
37	36	adantr	$⊢ (φ \land x \in ℤ) \to B \in ℂ$
38	37	mul01d	$⊢ (φ \land x \in ℤ) \to B \cdot 0 = 0$
39	38	oveq2d	$⊢ (φ \land x \in ℤ) \to A x + B \cdot 0 = A x + 0$
40	2	zcnd	$⊢ φ \to A \in ℂ$
41		zcn	$⊢ x \in ℤ \to x \in ℂ$
42		mulcl	$⊢ (A \in ℂ \land x \in ℂ) \to A x \in ℂ$
43	40 41 42	syl2an	$⊢ (φ \land x \in ℤ) \to A x \in ℂ$
44	43	addridd	$⊢ (φ \land x \in ℤ) \to A x + 0 = A x$
45	39 44	eqtrd	$⊢ (φ \land x \in ℤ) \to A x + B \cdot 0 = A x$
46	45	eqeq2d	$⊢ (φ \land x \in ℤ) \to (\|A\| = A x + B \cdot 0 \leftrightarrow \|A\| = A x)$
47		0z	$⊢ 0 \in ℤ$
48		oveq2	$⊢ y = 0 \to B y = B \cdot 0$
49	48	oveq2d	$⊢ y = 0 \to A x + B y = A x + B \cdot 0$
50	49	rspceeqv	$⊢ (0 \in ℤ \land \|A\| = A x + B \cdot 0) \to \exists y \in ℤ \|A\| = A x + B y$
51	47 50	mpan	$⊢ \|A\| = A x + B \cdot 0 \to \exists y \in ℤ \|A\| = A x + B y$
52	46 51	syl6bir	$⊢ (φ \land x \in ℤ) \to (\|A\| = A x \to \exists y \in ℤ \|A\| = A x + B y)$
53	52	reximdva	$⊢ φ \to (\exists x \in ℤ \|A\| = A x \to \exists x \in ℤ \exists y \in ℤ \|A\| = A x + B y)$
54	35 53	mpd	$⊢ φ \to \exists x \in ℤ \exists y \in ℤ \|A\| = A x + B y$
55		nnabscl	$⊢ (A \in ℤ \land A \neq 0) \to \|A\| \in ℕ$
56	55	ex	$⊢ A \in ℤ \to (A \neq 0 \to \|A\| \in ℕ)$
57	2 56	syl	$⊢ φ \to (A \neq 0 \to \|A\| \in ℕ)$
58		eqeq1	$⊢ z = \|A\| \to (z = A x + B y \leftrightarrow \|A\| = A x + B y)$
59	58	2rexbidv	$⊢ z = \|A\| \to (\exists x \in ℤ \exists y \in ℤ z = A x + B y \leftrightarrow \exists x \in ℤ \exists y \in ℤ \|A\| = A x + B y)$
60	59 1	elrab2	$⊢ \|A\| \in M \leftrightarrow (\|A\| \in ℕ \land \exists x \in ℤ \exists y \in ℤ \|A\| = A x + B y)$
61	60	simplbi2com	$⊢ \exists x \in ℤ \exists y \in ℤ \|A\| = A x + B y \to (\|A\| \in ℕ \to \|A\| \in M)$
62	54 57 61	sylsyld	$⊢ φ \to (A \neq 0 \to \|A\| \in M)$

Metamath Proof Explorer

Theorem bezoutlem1

Proof