# 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 )`
` |-  ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> A e. CC )`
17 zcn
` |-  ( x e. ZZ -> x e. CC )`
` |-  ( ( 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 )`
` |-  ( ( ph /\ ( y e. ZZ /\ x e. ZZ ) ) -> B e. CC )`
22 zcn
` |-  ( y e. ZZ -> y e. CC )`
` |-  ( ( 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 )`
` |-  ( ( 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 syl5eq
` |-  ( 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 )`