Metamath Proof Explorer


Theorem bezoutlem4

Description: Lemma for bezout . (Contributed by Mario Carneiro, 22-Feb-2014)

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 bezoutlem4 φ A gcd B M

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