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 )`
` |-  ( ( ph /\ ( ( u e. ZZ /\ v e. ZZ ) /\ ( s e. ZZ /\ t e. ZZ ) ) ) -> ( ( s x. u ) + ( t x. v ) ) e. ZZ )`
` |-  ( ( 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 )`
` |-  ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> A e. CC )`
92 zcn
` |-  ( x e. ZZ -> x e. CC )`
` |-  ( ( 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 )`
` |-  ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> B e. CC )`
97 zcn
` |-  ( y e. ZZ -> y e. CC )`
` |-  ( ( 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 )`
` |-  ( ( 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 syl5eq
` |-  ( 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 )`