Metamath Proof Explorer

Theorem bezoutlem2

Description: Lemma for bezout . (Contributed by Mario Carneiro, 15-Mar-2014) ( Revised by AV, 30-Sep-2020.)

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 bezoutlem2 
|- ( ph -> G 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 1 ssrab3 
 |-  M C_ NN
7 nnuz 
 |-  NN = ( ZZ>= ` 1 )
8 6 7 sseqtri 
 |-  M C_ ( ZZ>= ` 1 )
9 1 2 3 bezoutlem1 
 |-  ( ph -> ( A =/= 0 -> ( abs ` A ) e. M ) )
10 ne0i 
 |-  ( ( abs ` A ) e. M -> M =/= (/) )
11 9 10 syl6 
 |-  ( ph -> ( A =/= 0 -> M =/= (/) ) )
12 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 ) ) }
13 12 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 ) ) } ) )
14 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 ) ) )
15 2 zcnd 
 |-  ( ph -> A e. CC )
16 15 adantr 
 |-  ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> A e. CC )
17 zcn 
 |-  ( x e. ZZ -> x e. CC )
18 17 ad2antll 
 |-  ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> x e. CC )
19 16 18 mulcld 
 |-  ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> ( A x. x ) e. CC )
20 3 zcnd 
 |-  ( ph -> B e. CC )
21 20 adantr 
 |-  ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> B e. CC )
22 zcn 
 |-  ( y e. ZZ -> y e. CC )
23 22 ad2antrl 
 |-  ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> y e. CC )
24 21 23 mulcld 
 |-  ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> ( B x. y ) e. CC )
25 19 24 addcomd 
 |-  ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> ( ( A x. x ) + ( B x. y ) ) = ( ( B x. y ) + ( A x. x ) ) )
26 25 eqeq2d 
 |-  ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> ( z = ( ( A x. x ) + ( B x. y ) ) <-> z = ( ( B x. y ) + ( A x. x ) ) ) )
27 26 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 ) ) ) )
28 14 27 bitrid 
 |-  ( 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 ) ) ) )
29 28 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 ) ) } )
30 1 29 eqtrid 
 |-  ( ph -> M = { z e. NN | E. y e. ZZ E. x e. ZZ z = ( ( B x. y ) + ( A x. x ) ) } )
31 30 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 ) ) } ) )
32 13 31 sylibrd 
 |-  ( ph -> ( B =/= 0 -> ( abs ` B ) e. M ) )
33 ne0i 
 |-  ( ( abs ` B ) e. M -> M =/= (/) )
34 32 33 syl6 
 |-  ( ph -> ( B =/= 0 -> M =/= (/) ) )
35 neorian 
 |-  ( ( A =/= 0 \/ B =/= 0 ) <-> -. ( A = 0 /\ B = 0 ) )
36 5 35 sylibr 
 |-  ( ph -> ( A =/= 0 \/ B =/= 0 ) )
37 11 34 36 mpjaod 
 |-  ( ph -> M =/= (/) )
38 infssuzcl 
 |-  ( ( M C_ ( ZZ>= ` 1 ) /\ M =/= (/) ) -> inf ( M , RR , < ) e. M )
39 8 37 38 sylancr 
 |-  ( ph -> inf ( M , RR , < ) e. M )
40 4 39 eqeltrid 
 |-  ( ph -> G e. M )