Metamath Proof Explorer


Theorem 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 | x y z = A x + B y
bezout.3 φ A
bezout.4 φ B
bezout.2 G = sup M <
bezout.5 φ ¬ A = 0 B = 0
Assertion bezoutlem3 φ C M G C

Proof

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