Metamath Proof Explorer

Theorem bezoutlem4

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

Ref Expression
Hypotheses bezout.1 
|- M = { z e. NN | E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) }
bezout.3 
|- ( ph -> A e. ZZ )
bezout.4 
|- ( ph -> B e. ZZ )
bezout.2 
|- G = inf ( M , RR , < )
bezout.5 
|- ( ph -> -. ( A = 0 /\ B = 0 ) )
Assertion bezoutlem4 
|- ( ph -> ( A gcd B ) e. M )

Proof

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