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

Metamath Proof Explorer

Theorem bezoutlem3

Proof