bezoutlem2

Description: Lemma for bezout . (Contributed by Mario Carneiro, 15-Mar-2014) ( Revised by AV, 30-Sep-2020.)

	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 ℤ$
	bezout.2	$⊢ G = inf (M ℝ <)$
	bezout.5	$⊢ φ \to \neg (A = 0 \land B = 0)$
Assertion	bezoutlem2	$⊢ φ \to G \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		bezout.2	$⊢ G = inf (M ℝ <)$
5		bezout.5	$⊢ φ \to \neg (A = 0 \land B = 0)$
6	1	ssrab3	$⊢ M \subseteq ℕ$
7		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
8	6 7	sseqtri	$⊢ M \subseteq ℤ_{\geq 1}$
9	1 2 3	bezoutlem1	$⊢ φ \to (A \neq 0 \to \|A\| \in M)$
10		ne0i	$⊢ \|A\| \in M \to M \neq \emptyset$
11	9 10	syl6	$⊢ φ \to (A \neq 0 \to M \neq \emptyset)$
12		eqid	$⊢ \{z \in ℕ \| \exists y \in ℤ \exists x \in ℤ z = B y + A x\} = \{z \in ℕ \| \exists y \in ℤ \exists x \in ℤ z = B y + A x\}$
13	12 3 2	bezoutlem1	$⊢ φ \to (B \neq 0 \to \|B\| \in \{z \in ℕ \| \exists y \in ℤ \exists x \in ℤ z = B y + A x\})$
14		rexcom	$⊢ \exists x \in ℤ \exists y \in ℤ z = A x + B y \leftrightarrow \exists y \in ℤ \exists x \in ℤ z = A x + B y$
15	2	zcnd	$⊢ φ \to A \in ℂ$
16	15	adantr	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to A \in ℂ$
17		zcn	$⊢ x \in ℤ \to x \in ℂ$
18	17	ad2antll	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to x \in ℂ$
19	16 18	mulcld	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to A x \in ℂ$
20	3	zcnd	$⊢ φ \to B \in ℂ$
21	20	adantr	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to B \in ℂ$
22		zcn	$⊢ y \in ℤ \to y \in ℂ$
23	22	ad2antrl	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to y \in ℂ$
24	21 23	mulcld	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to B y \in ℂ$
25	19 24	addcomd	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to A x + B y = B y + A x$
26	25	eqeq2d	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to (z = A x + B y \leftrightarrow z = B y + A x)$
27	26	2rexbidva	$⊢ φ \to (\exists y \in ℤ \exists x \in ℤ z = A x + B y \leftrightarrow \exists y \in ℤ \exists x \in ℤ z = B y + A x)$
28	14 27	bitrid	$⊢ φ \to (\exists x \in ℤ \exists y \in ℤ z = A x + B y \leftrightarrow \exists y \in ℤ \exists x \in ℤ z = B y + A x)$
29	28	rabbidv	$⊢ φ \to \{z \in ℕ \| \exists x \in ℤ \exists y \in ℤ z = A x + B y\} = \{z \in ℕ \| \exists y \in ℤ \exists x \in ℤ z = B y + A x\}$
30	1 29	eqtrid	$⊢ φ \to M = \{z \in ℕ \| \exists y \in ℤ \exists x \in ℤ z = B y + A x\}$
31	30	eleq2d	$⊢ φ \to (\|B\| \in M \leftrightarrow \|B\| \in \{z \in ℕ \| \exists y \in ℤ \exists x \in ℤ z = B y + A x\})$
32	13 31	sylibrd	$⊢ φ \to (B \neq 0 \to \|B\| \in M)$
33		ne0i	$⊢ \|B\| \in M \to M \neq \emptyset$
34	32 33	syl6	$⊢ φ \to (B \neq 0 \to M \neq \emptyset)$
35		neorian	$⊢ (A \neq 0 \lor B \neq 0) \leftrightarrow \neg (A = 0 \land B = 0)$
36	5 35	sylibr	$⊢ φ \to (A \neq 0 \lor B \neq 0)$
37	11 34 36	mpjaod	$⊢ φ \to M \neq \emptyset$
38		infssuzcl	$⊢ (M \subseteq ℤ_{\geq 1} \land M \neq \emptyset) \to inf (M ℝ <) \in M$
39	8 37 38	sylancr	$⊢ φ \to inf (M ℝ <) \in M$
40	4 39	eqeltrid	$⊢ φ \to G \in M$

Metamath Proof Explorer

Theorem bezoutlem2

Proof