bezoutlem3

Description: Lemma for bezout . (Contributed by Mario Carneiro, 22-Feb-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	bezoutlem3	$⊢ φ \to (C \in M \to G ∥ C)$

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		simpr	$⊢ (φ \land C \in M) \to C \in M$
7		eqeq1	$⊢ z = C \to (z = A x + B y \leftrightarrow C = A x + B y)$
8	7	2rexbidv	$⊢ z = C \to (\exists x \in ℤ \exists y \in ℤ z = A x + B y \leftrightarrow \exists x \in ℤ \exists y \in ℤ C = A x + B y)$
9		oveq2	$⊢ x = s \to A x = A s$
10	9	oveq1d	$⊢ x = s \to A x + B y = A s + B y$
11	10	eqeq2d	$⊢ x = s \to (C = A x + B y \leftrightarrow C = A s + B y)$
12		oveq2	$⊢ y = t \to B y = B t$
13	12	oveq2d	$⊢ y = t \to A s + B y = A s + B t$
14	13	eqeq2d	$⊢ y = t \to (C = A s + B y \leftrightarrow C = A s + B t)$
15	11 14	cbvrex2vw	$⊢ \exists x \in ℤ \exists y \in ℤ C = A x + B y \leftrightarrow \exists s \in ℤ \exists t \in ℤ C = A s + B t$
16	8 15	bitrdi	$⊢ z = C \to (\exists x \in ℤ \exists y \in ℤ z = A x + B y \leftrightarrow \exists s \in ℤ \exists t \in ℤ C = A s + B t)$
17	16 1	elrab2	$⊢ C \in M \leftrightarrow (C \in ℕ \land \exists s \in ℤ \exists t \in ℤ C = A s + B t)$
18	6 17	sylib	$⊢ (φ \land C \in M) \to (C \in ℕ \land \exists s \in ℤ \exists t \in ℤ C = A s + B t)$
19	18	simpld	$⊢ (φ \land C \in M) \to C \in ℕ$
20	19	nnred	$⊢ (φ \land C \in M) \to C \in ℝ$
21	1 2 3 4 5	bezoutlem2	$⊢ φ \to G \in M$
22		oveq2	$⊢ x = u \to A x = A u$
23	22	oveq1d	$⊢ x = u \to A x + B y = A u + B y$
24	23	eqeq2d	$⊢ x = u \to (z = A x + B y \leftrightarrow z = A u + B y)$
25		oveq2	$⊢ y = v \to B y = B v$
26	25	oveq2d	$⊢ y = v \to A u + B y = A u + B v$
27	26	eqeq2d	$⊢ y = v \to (z = A u + B y \leftrightarrow z = A u + B v)$
28	24 27	cbvrex2vw	$⊢ \exists x \in ℤ \exists y \in ℤ z = A x + B y \leftrightarrow \exists u \in ℤ \exists v \in ℤ z = A u + B v$
29		eqeq1	$⊢ z = G \to (z = A u + B v \leftrightarrow G = A u + B v)$
30	29	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)$
31	28 30	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)$
32	31 1	elrab2	$⊢ G \in M \leftrightarrow (G \in ℕ \land \exists u \in ℤ \exists v \in ℤ G = A u + B v)$
33	21 32	sylib	$⊢ φ \to (G \in ℕ \land \exists u \in ℤ \exists v \in ℤ G = A u + B v)$
34	33	simpld	$⊢ φ \to G \in ℕ$
35	34	nnrpd	$⊢ φ \to G \in ℝ^{+}$
36	35	adantr	$⊢ (φ \land C \in M) \to G \in ℝ^{+}$
37		modlt	$⊢ (C \in ℝ \land G \in ℝ^{+}) \to C \mod G < G$
38	20 36 37	syl2anc	$⊢ (φ \land C \in M) \to C \mod G < G$
39	19	nnzd	$⊢ (φ \land C \in M) \to C \in ℤ$
40	34	adantr	$⊢ (φ \land C \in M) \to G \in ℕ$
41	39 40	zmodcld	$⊢ (φ \land C \in M) \to C \mod G \in ℕ_{0}$
42	41	nn0red	$⊢ (φ \land C \in M) \to C \mod G \in ℝ$
43	34	nnred	$⊢ φ \to G \in ℝ$
44	43	adantr	$⊢ (φ \land C \in M) \to G \in ℝ$
45	42 44	ltnled	$⊢ (φ \land C \in M) \to (C \mod G < G \leftrightarrow \neg G \leq C \mod G)$
46	38 45	mpbid	$⊢ (φ \land C \in M) \to \neg G \leq C \mod G$
47	18	simprd	$⊢ (φ \land C \in M) \to \exists s \in ℤ \exists t \in ℤ C = A s + B t$
48	33	simprd	$⊢ φ \to \exists u \in ℤ \exists v \in ℤ G = A u + B v$
49	48	ad2antrr	$⊢ ((φ \land C \in M) \land (s \in ℤ \land t \in ℤ)) \to \exists u \in ℤ \exists v \in ℤ G = A u + B v$
50		simprll	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to s \in ℤ$
51		simprrl	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to u \in ℤ$
52	20 40	nndivred	$⊢ (φ \land C \in M) \to \frac{C}{G} \in ℝ$
53	52	flcld	$⊢ (φ \land C \in M) \to ⌊\frac{C}{G}⌋ \in ℤ$
54	53	adantr	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to ⌊\frac{C}{G}⌋ \in ℤ$
55	51 54	zmulcld	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to u ⌊\frac{C}{G}⌋ \in ℤ$
56	50 55	zsubcld	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to s - u ⌊\frac{C}{G}⌋ \in ℤ$
57		simprlr	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to t \in ℤ$
58		simprrr	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to v \in ℤ$
59	58 54	zmulcld	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to v ⌊\frac{C}{G}⌋ \in ℤ$
60	57 59	zsubcld	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to t - v ⌊\frac{C}{G}⌋ \in ℤ$
61	2	zcnd	$⊢ φ \to A \in ℂ$
62	61	ad2antrr	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to A \in ℂ$
63	50	zcnd	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to s \in ℂ$
64	62 63	mulcld	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to A s \in ℂ$
65	3	zcnd	$⊢ φ \to B \in ℂ$
66	65	ad2antrr	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to B \in ℂ$
67	57	zcnd	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to t \in ℂ$
68	66 67	mulcld	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to B t \in ℂ$
69	55	zcnd	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to u ⌊\frac{C}{G}⌋ \in ℂ$
70	62 69	mulcld	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to A u ⌊\frac{C}{G}⌋ \in ℂ$
71	59	zcnd	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to v ⌊\frac{C}{G}⌋ \in ℂ$
72	66 71	mulcld	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to B v ⌊\frac{C}{G}⌋ \in ℂ$
73	64 68 70 72	addsub4d	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to A s + B t - (A u ⌊\frac{C}{G}⌋ + B v ⌊\frac{C}{G}⌋) = (A s - A u ⌊\frac{C}{G}⌋) + B t - B v ⌊\frac{C}{G}⌋$
74	51	zcnd	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to u \in ℂ$
75	62 74	mulcld	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to A u \in ℂ$
76	53	zcnd	$⊢ (φ \land C \in M) \to ⌊\frac{C}{G}⌋ \in ℂ$
77	76	adantr	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to ⌊\frac{C}{G}⌋ \in ℂ$
78	58	zcnd	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to v \in ℂ$
79	66 78	mulcld	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to B v \in ℂ$
80	62 74 77	mulassd	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to A u ⌊\frac{C}{G}⌋ = A u ⌊\frac{C}{G}⌋$
81	66 78 77	mulassd	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to B v ⌊\frac{C}{G}⌋ = B v ⌊\frac{C}{G}⌋$
82	80 81	oveq12d	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to A u ⌊\frac{C}{G}⌋ + B v ⌊\frac{C}{G}⌋ = A u ⌊\frac{C}{G}⌋ + B v ⌊\frac{C}{G}⌋$
83	75 77 79 82	joinlmuladdmuld	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to (A u + B v) ⌊\frac{C}{G}⌋ = A u ⌊\frac{C}{G}⌋ + B v ⌊\frac{C}{G}⌋$
84	83	oveq2d	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to A s + B t - (A u + B v) ⌊\frac{C}{G}⌋ = A s + B t - (A u ⌊\frac{C}{G}⌋ + B v ⌊\frac{C}{G}⌋)$
85	62 63 69	subdid	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to A (s - u ⌊\frac{C}{G}⌋) = A s - A u ⌊\frac{C}{G}⌋$
86	66 67 71	subdid	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to B (t - v ⌊\frac{C}{G}⌋) = B t - B v ⌊\frac{C}{G}⌋$
87	85 86	oveq12d	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to A (s - u ⌊\frac{C}{G}⌋) + B (t - v ⌊\frac{C}{G}⌋) = (A s - A u ⌊\frac{C}{G}⌋) + B t - B v ⌊\frac{C}{G}⌋$
88	73 84 87	3eqtr4d	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to A s + B t - (A u + B v) ⌊\frac{C}{G}⌋ = A (s - u ⌊\frac{C}{G}⌋) + B (t - v ⌊\frac{C}{G}⌋)$
89		oveq2	$⊢ x = s - u ⌊\frac{C}{G}⌋ \to A x = A (s - u ⌊\frac{C}{G}⌋)$
90	89	oveq1d	$⊢ x = s - u ⌊\frac{C}{G}⌋ \to A x + B y = A (s - u ⌊\frac{C}{G}⌋) + B y$
91	90	eqeq2d	$⊢ x = s - u ⌊\frac{C}{G}⌋ \to (A s + B t - (A u + B v) ⌊\frac{C}{G}⌋ = A x + B y \leftrightarrow A s + B t - (A u + B v) ⌊\frac{C}{G}⌋ = A (s - u ⌊\frac{C}{G}⌋) + B y)$
92		oveq2	$⊢ y = t - v ⌊\frac{C}{G}⌋ \to B y = B (t - v ⌊\frac{C}{G}⌋)$
93	92	oveq2d	$⊢ y = t - v ⌊\frac{C}{G}⌋ \to A (s - u ⌊\frac{C}{G}⌋) + B y = A (s - u ⌊\frac{C}{G}⌋) + B (t - v ⌊\frac{C}{G}⌋)$
94	93	eqeq2d	$⊢ y = t - v ⌊\frac{C}{G}⌋ \to (A s + B t - (A u + B v) ⌊\frac{C}{G}⌋ = A (s - u ⌊\frac{C}{G}⌋) + B y \leftrightarrow A s + B t - (A u + B v) ⌊\frac{C}{G}⌋ = A (s - u ⌊\frac{C}{G}⌋) + B (t - v ⌊\frac{C}{G}⌋))$
95	91 94	rspc2ev	$⊢ (s - u ⌊\frac{C}{G}⌋ \in ℤ \land t - v ⌊\frac{C}{G}⌋ \in ℤ \land A s + B t - (A u + B v) ⌊\frac{C}{G}⌋ = A (s - u ⌊\frac{C}{G}⌋) + B (t - v ⌊\frac{C}{G}⌋)) \to \exists x \in ℤ \exists y \in ℤ A s + B t - (A u + B v) ⌊\frac{C}{G}⌋ = A x + B y$
96	56 60 88 95	syl3anc	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to \exists x \in ℤ \exists y \in ℤ A s + B t - (A u + B v) ⌊\frac{C}{G}⌋ = A x + B y$
97		oveq1	$⊢ G = A u + B v \to G ⌊\frac{C}{G}⌋ = (A u + B v) ⌊\frac{C}{G}⌋$
98		oveq12	$⊢ (C = A s + B t \land G ⌊\frac{C}{G}⌋ = (A u + B v) ⌊\frac{C}{G}⌋) \to C - G ⌊\frac{C}{G}⌋ = A s + B t - (A u + B v) ⌊\frac{C}{G}⌋$
99	97 98	sylan2	$⊢ (C = A s + B t \land G = A u + B v) \to C - G ⌊\frac{C}{G}⌋ = A s + B t - (A u + B v) ⌊\frac{C}{G}⌋$
100	99	eqeq1d	$⊢ (C = A s + B t \land G = A u + B v) \to (C - G ⌊\frac{C}{G}⌋ = A x + B y \leftrightarrow A s + B t - (A u + B v) ⌊\frac{C}{G}⌋ = A x + B y)$
101	100	2rexbidv	$⊢ (C = A s + B t \land G = A u + B v) \to (\exists x \in ℤ \exists y \in ℤ C - G ⌊\frac{C}{G}⌋ = A x + B y \leftrightarrow \exists x \in ℤ \exists y \in ℤ A s + B t - (A u + B v) ⌊\frac{C}{G}⌋ = A x + B y)$
102	96 101	syl5ibrcom	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to ((C = A s + B t \land G = A u + B v) \to \exists x \in ℤ \exists y \in ℤ C - G ⌊\frac{C}{G}⌋ = A x + B y)$
103	102	expcomd	$⊢ ((φ \land C \in M) \land ((s \in ℤ \land t \in ℤ) \land (u \in ℤ \land v \in ℤ))) \to (G = A u + B v \to (C = A s + B t \to \exists x \in ℤ \exists y \in ℤ C - G ⌊\frac{C}{G}⌋ = A x + B y))$
104	103	expr	$⊢ ((φ \land C \in M) \land (s \in ℤ \land t \in ℤ)) \to ((u \in ℤ \land v \in ℤ) \to (G = A u + B v \to (C = A s + B t \to \exists x \in ℤ \exists y \in ℤ C - G ⌊\frac{C}{G}⌋ = A x + B y)))$
105	104	rexlimdvv	$⊢ ((φ \land C \in M) \land (s \in ℤ \land t \in ℤ)) \to (\exists u \in ℤ \exists v \in ℤ G = A u + B v \to (C = A s + B t \to \exists x \in ℤ \exists y \in ℤ C - G ⌊\frac{C}{G}⌋ = A x + B y))$
106	49 105	mpd	$⊢ ((φ \land C \in M) \land (s \in ℤ \land t \in ℤ)) \to (C = A s + B t \to \exists x \in ℤ \exists y \in ℤ C - G ⌊\frac{C}{G}⌋ = A x + B y)$
107	106	ex	$⊢ (φ \land C \in M) \to ((s \in ℤ \land t \in ℤ) \to (C = A s + B t \to \exists x \in ℤ \exists y \in ℤ C - G ⌊\frac{C}{G}⌋ = A x + B y))$
108	107	rexlimdvv	$⊢ (φ \land C \in M) \to (\exists s \in ℤ \exists t \in ℤ C = A s + B t \to \exists x \in ℤ \exists y \in ℤ C - G ⌊\frac{C}{G}⌋ = A x + B y)$
109	47 108	mpd	$⊢ (φ \land C \in M) \to \exists x \in ℤ \exists y \in ℤ C - G ⌊\frac{C}{G}⌋ = A x + B y$
110		modval	$⊢ (C \in ℝ \land G \in ℝ^{+}) \to C \mod G = C - G ⌊\frac{C}{G}⌋$
111	20 36 110	syl2anc	$⊢ (φ \land C \in M) \to C \mod G = C - G ⌊\frac{C}{G}⌋$
112	111	eqcomd	$⊢ (φ \land C \in M) \to C - G ⌊\frac{C}{G}⌋ = C \mod G$
113	112	eqeq1d	$⊢ (φ \land C \in M) \to (C - G ⌊\frac{C}{G}⌋ = A x + B y \leftrightarrow C \mod G = A x + B y)$
114	113	2rexbidv	$⊢ (φ \land C \in M) \to (\exists x \in ℤ \exists y \in ℤ C - G ⌊\frac{C}{G}⌋ = A x + B y \leftrightarrow \exists x \in ℤ \exists y \in ℤ C \mod G = A x + B y)$
115	109 114	mpbid	$⊢ (φ \land C \in M) \to \exists x \in ℤ \exists y \in ℤ C \mod G = A x + B y$
116		eqeq1	$⊢ z = C \mod G \to (z = A x + B y \leftrightarrow C \mod G = A x + B y)$
117	116	2rexbidv	$⊢ z = C \mod G \to (\exists x \in ℤ \exists y \in ℤ z = A x + B y \leftrightarrow \exists x \in ℤ \exists y \in ℤ C \mod G = A x + B y)$
118	117 1	elrab2	$⊢ C \mod G \in M \leftrightarrow (C \mod G \in ℕ \land \exists x \in ℤ \exists y \in ℤ C \mod G = A x + B y)$
119	118	simplbi2com	$⊢ \exists x \in ℤ \exists y \in ℤ C \mod G = A x + B y \to (C \mod G \in ℕ \to C \mod G \in M)$
120	115 119	syl	$⊢ (φ \land C \in M) \to (C \mod G \in ℕ \to C \mod G \in M)$
121	1	ssrab3	$⊢ M \subseteq ℕ$
122		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
123	121 122	sseqtri	$⊢ M \subseteq ℤ_{\geq 1}$
124		infssuzle	$⊢ (M \subseteq ℤ_{\geq 1} \land C \mod G \in M) \to inf (M ℝ <) \leq C \mod G$
125	123 124	mpan	$⊢ C \mod G \in M \to inf (M ℝ <) \leq C \mod G$
126	4 125	eqbrtrid	$⊢ C \mod G \in M \to G \leq C \mod G$
127	120 126	syl6	$⊢ (φ \land C \in M) \to (C \mod G \in ℕ \to G \leq C \mod G)$
128	46 127	mtod	$⊢ (φ \land C \in M) \to \neg C \mod G \in ℕ$
129		elnn0	$⊢ C \mod G \in ℕ_{0} \leftrightarrow (C \mod G \in ℕ \lor C \mod G = 0)$
130	41 129	sylib	$⊢ (φ \land C \in M) \to (C \mod G \in ℕ \lor C \mod G = 0)$
131	130	ord	$⊢ (φ \land C \in M) \to (\neg C \mod G \in ℕ \to C \mod G = 0)$
132	128 131	mpd	$⊢ (φ \land C \in M) \to C \mod G = 0$
133		dvdsval3	$⊢ (G \in ℕ \land C \in ℤ) \to (G ∥ C \leftrightarrow C \mod G = 0)$
134	40 39 133	syl2anc	$⊢ (φ \land C \in M) \to (G ∥ C \leftrightarrow C \mod G = 0)$
135	132 134	mpbird	$⊢ (φ \land C \in M) \to G ∥ C$
136	135	ex	$⊢ φ \to (C \in M \to G ∥ C)$

Metamath Proof Explorer

Theorem bezoutlem3

Proof