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 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 ) ) ) )
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 )