bezoutlem4

	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	bezoutlem4	$⊢ φ \to A \gcd B \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		gcddvds	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
7	2 3 6	syl2anc	$⊢ φ \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
8	7	simpld	$⊢ φ \to (A \gcd B) ∥ A$
9	2 3	gcdcld	$⊢ φ \to A \gcd B \in ℕ_{0}$
10	9	nn0zd	$⊢ φ \to A \gcd B \in ℤ$
11		divides	$⊢ (A \gcd B \in ℤ \land A \in ℤ) \to ((A \gcd B) ∥ A \leftrightarrow \exists s \in ℤ s (A \gcd B) = A)$
12	10 2 11	syl2anc	$⊢ φ \to ((A \gcd B) ∥ A \leftrightarrow \exists s \in ℤ s (A \gcd B) = A)$
13	8 12	mpbid	$⊢ φ \to \exists s \in ℤ s (A \gcd B) = A$
14	7	simprd	$⊢ φ \to (A \gcd B) ∥ B$
15		divides	$⊢ (A \gcd B \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ B \leftrightarrow \exists t \in ℤ t (A \gcd B) = B)$
16	10 3 15	syl2anc	$⊢ φ \to ((A \gcd B) ∥ B \leftrightarrow \exists t \in ℤ t (A \gcd B) = B)$
17	14 16	mpbid	$⊢ φ \to \exists t \in ℤ t (A \gcd B) = B$
18		reeanv	$⊢ \exists s \in ℤ \exists t \in ℤ (s (A \gcd B) = A \land t (A \gcd B) = B) \leftrightarrow (\exists s \in ℤ s (A \gcd B) = A \land \exists t \in ℤ t (A \gcd B) = B)$
19	1 2 3 4 5	bezoutlem2	$⊢ φ \to G \in M$
20		oveq2	$⊢ x = u \to A x = A u$
21	20	oveq1d	$⊢ x = u \to A x + B y = A u + B y$
22	21	eqeq2d	$⊢ x = u \to (z = A x + B y \leftrightarrow z = A u + B y)$
23		oveq2	$⊢ y = v \to B y = B v$
24	23	oveq2d	$⊢ y = v \to A u + B y = A u + B v$
25	24	eqeq2d	$⊢ y = v \to (z = A u + B y \leftrightarrow z = A u + B v)$
26	22 25	cbvrex2vw	$⊢ \exists x \in ℤ \exists y \in ℤ z = A x + B y \leftrightarrow \exists u \in ℤ \exists v \in ℤ z = A u + B v$
27		eqeq1	$⊢ z = G \to (z = A u + B v \leftrightarrow G = A u + B v)$
28	27	2rexbidv	$⊢ z = G \to (\exists u \in ℤ \exists v \in ℤ z = A u + B v \leftrightarrow \exists u \in ℤ \exists v \in ℤ G = A u + B v)$
29	26 28	bitrid	$⊢ z = G \to (\exists x \in ℤ \exists y \in ℤ z = A x + B y \leftrightarrow \exists u \in ℤ \exists v \in ℤ G = A u + B v)$
30	29 1	elrab2	$⊢ G \in M \leftrightarrow (G \in ℕ \land \exists u \in ℤ \exists v \in ℤ G = A u + B v)$
31	19 30	sylib	$⊢ φ \to (G \in ℕ \land \exists u \in ℤ \exists v \in ℤ G = A u + B v)$
32	31	simprd	$⊢ φ \to \exists u \in ℤ \exists v \in ℤ G = A u + B v$
33		simprrl	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to s \in ℤ$
34		simprll	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to u \in ℤ$
35	33 34	zmulcld	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to s u \in ℤ$
36		simprrr	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to t \in ℤ$
37		simprlr	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to v \in ℤ$
38	36 37	zmulcld	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to t v \in ℤ$
39	35 38	zaddcld	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to s u + t v \in ℤ$
40	10	adantr	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to A \gcd B \in ℤ$
41		dvdsmul2	$⊢ (s u + t v \in ℤ \land A \gcd B \in ℤ) \to (A \gcd B) ∥ (s u + t v) (A \gcd B)$
42	39 40 41	syl2anc	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to (A \gcd B) ∥ (s u + t v) (A \gcd B)$
43	35	zcnd	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to s u \in ℂ$
44	40	zcnd	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to A \gcd B \in ℂ$
45	38	zcnd	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to t v \in ℂ$
46	33	zcnd	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to s \in ℂ$
47	34	zcnd	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to u \in ℂ$
48	46 47 44	mul32d	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to s u (A \gcd B) = s (A \gcd B) u$
49	36	zcnd	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to t \in ℂ$
50	37	zcnd	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to v \in ℂ$
51	49 50 44	mul32d	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to t v (A \gcd B) = t (A \gcd B) v$
52	48 51	oveq12d	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to s u (A \gcd B) + t v (A \gcd B) = s (A \gcd B) u + t (A \gcd B) v$
53	43 44 45 52	joinlmuladdmuld	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to (s u + t v) (A \gcd B) = s (A \gcd B) u + t (A \gcd B) v$
54	42 53	breqtrd	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to (A \gcd B) ∥ (s (A \gcd B) u + t (A \gcd B) v)$
55		oveq1	$⊢ s (A \gcd B) = A \to s (A \gcd B) u = A u$
56		oveq1	$⊢ t (A \gcd B) = B \to t (A \gcd B) v = B v$
57	55 56	oveqan12d	$⊢ (s (A \gcd B) = A \land t (A \gcd B) = B) \to s (A \gcd B) u + t (A \gcd B) v = A u + B v$
58	57	breq2d	$⊢ (s (A \gcd B) = A \land t (A \gcd B) = B) \to ((A \gcd B) ∥ (s (A \gcd B) u + t (A \gcd B) v) \leftrightarrow (A \gcd B) ∥ (A u + B v))$
59	54 58	syl5ibcom	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to ((s (A \gcd B) = A \land t (A \gcd B) = B) \to (A \gcd B) ∥ (A u + B v))$
60		breq2	$⊢ G = A u + B v \to ((A \gcd B) ∥ G \leftrightarrow (A \gcd B) ∥ (A u + B v))$
61	60	imbi2d	$⊢ G = A u + B v \to (((s (A \gcd B) = A \land t (A \gcd B) = B) \to (A \gcd B) ∥ G) \leftrightarrow ((s (A \gcd B) = A \land t (A \gcd B) = B) \to (A \gcd B) ∥ (A u + B v)))$
62	59 61	syl5ibrcom	$⊢ (φ \land ((u \in ℤ \land v \in ℤ) \land (s \in ℤ \land t \in ℤ))) \to (G = A u + B v \to ((s (A \gcd B) = A \land t (A \gcd B) = B) \to (A \gcd B) ∥ G))$
63	62	expr	$⊢ (φ \land (u \in ℤ \land v \in ℤ)) \to ((s \in ℤ \land t \in ℤ) \to (G = A u + B v \to ((s (A \gcd B) = A \land t (A \gcd B) = B) \to (A \gcd B) ∥ G)))$
64	63	com23	$⊢ (φ \land (u \in ℤ \land v \in ℤ)) \to (G = A u + B v \to ((s \in ℤ \land t \in ℤ) \to ((s (A \gcd B) = A \land t (A \gcd B) = B) \to (A \gcd B) ∥ G)))$
65	64	rexlimdvva	$⊢ φ \to (\exists u \in ℤ \exists v \in ℤ G = A u + B v \to ((s \in ℤ \land t \in ℤ) \to ((s (A \gcd B) = A \land t (A \gcd B) = B) \to (A \gcd B) ∥ G)))$
66	32 65	mpd	$⊢ φ \to ((s \in ℤ \land t \in ℤ) \to ((s (A \gcd B) = A \land t (A \gcd B) = B) \to (A \gcd B) ∥ G))$
67	66	rexlimdvv	$⊢ φ \to (\exists s \in ℤ \exists t \in ℤ (s (A \gcd B) = A \land t (A \gcd B) = B) \to (A \gcd B) ∥ G)$
68	18 67	biimtrrid	$⊢ φ \to ((\exists s \in ℤ s (A \gcd B) = A \land \exists t \in ℤ t (A \gcd B) = B) \to (A \gcd B) ∥ G)$
69	13 17 68	mp2and	$⊢ φ \to (A \gcd B) ∥ G$
70	31	simpld	$⊢ φ \to G \in ℕ$
71		dvdsle	$⊢ (A \gcd B \in ℤ \land G \in ℕ) \to ((A \gcd B) ∥ G \to A \gcd B \leq G)$
72	10 70 71	syl2anc	$⊢ φ \to ((A \gcd B) ∥ G \to A \gcd B \leq G)$
73	69 72	mpd	$⊢ φ \to A \gcd B \leq G$
74		breq2	$⊢ A = 0 \to (G ∥ A \leftrightarrow G ∥ 0)$
75	1 2 3	bezoutlem1	$⊢ φ \to (A \neq 0 \to \|A\| \in M)$
76	1 2 3 4 5	bezoutlem3	$⊢ φ \to (\|A\| \in M \to G ∥ \|A\|)$
77	75 76	syld	$⊢ φ \to (A \neq 0 \to G ∥ \|A\|)$
78	70	nnzd	$⊢ φ \to G \in ℤ$
79		dvdsabsb	$⊢ (G \in ℤ \land A \in ℤ) \to (G ∥ A \leftrightarrow G ∥ \|A\|)$
80	78 2 79	syl2anc	$⊢ φ \to (G ∥ A \leftrightarrow G ∥ \|A\|)$
81	77 80	sylibrd	$⊢ φ \to (A \neq 0 \to G ∥ A)$
82	81	imp	$⊢ (φ \land A \neq 0) \to G ∥ A$
83		dvds0	$⊢ G \in ℤ \to G ∥ 0$
84	78 83	syl	$⊢ φ \to G ∥ 0$
85	74 82 84	pm2.61ne	$⊢ φ \to G ∥ A$
86		breq2	$⊢ B = 0 \to (G ∥ B \leftrightarrow G ∥ 0)$
87		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\}$
88	87 3 2	bezoutlem1	$⊢ φ \to (B \neq 0 \to \|B\| \in \{z \in ℕ \| \exists y \in ℤ \exists x \in ℤ z = B y + A x\})$
89		rexcom	$⊢ \exists x \in ℤ \exists y \in ℤ z = A x + B y \leftrightarrow \exists y \in ℤ \exists x \in ℤ z = A x + B y$
90	2	zcnd	$⊢ φ \to A \in ℂ$
91	90	adantr	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to A \in ℂ$
92		zcn	$⊢ x \in ℤ \to x \in ℂ$
93	92	ad2antll	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to x \in ℂ$
94	91 93	mulcld	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to A x \in ℂ$
95	3	zcnd	$⊢ φ \to B \in ℂ$
96	95	adantr	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to B \in ℂ$
97		zcn	$⊢ y \in ℤ \to y \in ℂ$
98	97	ad2antrl	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to y \in ℂ$
99	96 98	mulcld	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to B y \in ℂ$
100	94 99	addcomd	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to A x + B y = B y + A x$
101	100	eqeq2d	$⊢ (φ \land (y \in ℤ \land x \in ℤ)) \to (z = A x + B y \leftrightarrow z = B y + A x)$
102	101	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)$
103	89 102	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)$
104	103	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\}$
105	1 104	eqtrid	$⊢ φ \to M = \{z \in ℕ \| \exists y \in ℤ \exists x \in ℤ z = B y + A x\}$
106	105	eleq2d	$⊢ φ \to (\|B\| \in M \leftrightarrow \|B\| \in \{z \in ℕ \| \exists y \in ℤ \exists x \in ℤ z = B y + A x\})$
107	88 106	sylibrd	$⊢ φ \to (B \neq 0 \to \|B\| \in M)$
108	1 2 3 4 5	bezoutlem3	$⊢ φ \to (\|B\| \in M \to G ∥ \|B\|)$
109	107 108	syld	$⊢ φ \to (B \neq 0 \to G ∥ \|B\|)$
110		dvdsabsb	$⊢ (G \in ℤ \land B \in ℤ) \to (G ∥ B \leftrightarrow G ∥ \|B\|)$
111	78 3 110	syl2anc	$⊢ φ \to (G ∥ B \leftrightarrow G ∥ \|B\|)$
112	109 111	sylibrd	$⊢ φ \to (B \neq 0 \to G ∥ B)$
113	112	imp	$⊢ (φ \land B \neq 0) \to G ∥ B$
114	86 113 84	pm2.61ne	$⊢ φ \to G ∥ B$
115		dvdslegcd	$⊢ ((G \in ℤ \land A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to ((G ∥ A \land G ∥ B) \to G \leq A \gcd B)$
116	78 2 3 5 115	syl31anc	$⊢ φ \to ((G ∥ A \land G ∥ B) \to G \leq A \gcd B)$
117	85 114 116	mp2and	$⊢ φ \to G \leq A \gcd B$
118	9	nn0red	$⊢ φ \to A \gcd B \in ℝ$
119	70	nnred	$⊢ φ \to G \in ℝ$
120	118 119	letri3d	$⊢ φ \to (A \gcd B = G \leftrightarrow (A \gcd B \leq G \land G \leq A \gcd B))$
121	73 117 120	mpbir2and	$⊢ φ \to A \gcd B = G$
122	121 19	eqeltrd	$⊢ φ \to A \gcd B \in M$

Metamath Proof Explorer

Theorem bezoutlem4

Proof