# Metamath Proof Explorer

## Theorem bezoutlem1

Description: Lemma for bezout . (Contributed by Mario Carneiro, 15-Mar-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 )`
Assertion bezoutlem1
`|- ( ph -> ( A =/= 0 -> ( abs ` A ) 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 fveq2
` |-  ( z = A -> ( abs ` z ) = ( abs ` A ) )`
5 oveq1
` |-  ( z = A -> ( z x. x ) = ( A x. x ) )`
6 4 5 eqeq12d
` |-  ( z = A -> ( ( abs ` z ) = ( z x. x ) <-> ( abs ` A ) = ( A x. x ) ) )`
7 6 rexbidv
` |-  ( z = A -> ( E. x e. ZZ ( abs ` z ) = ( z x. x ) <-> E. x e. ZZ ( abs ` A ) = ( A x. x ) ) )`
8 zre
` |-  ( z e. ZZ -> z e. RR )`
9 1z
` |-  1 e. ZZ`
10 ax-1rid
` |-  ( z e. RR -> ( z x. 1 ) = z )`
11 10 eqcomd
` |-  ( z e. RR -> z = ( z x. 1 ) )`
12 oveq2
` |-  ( x = 1 -> ( z x. x ) = ( z x. 1 ) )`
13 12 rspceeqv
` |-  ( ( 1 e. ZZ /\ z = ( z x. 1 ) ) -> E. x e. ZZ z = ( z x. x ) )`
14 9 11 13 sylancr
` |-  ( z e. RR -> E. x e. ZZ z = ( z x. x ) )`
15 eqeq1
` |-  ( ( abs ` z ) = z -> ( ( abs ` z ) = ( z x. x ) <-> z = ( z x. x ) ) )`
16 15 rexbidv
` |-  ( ( abs ` z ) = z -> ( E. x e. ZZ ( abs ` z ) = ( z x. x ) <-> E. x e. ZZ z = ( z x. x ) ) )`
17 14 16 syl5ibrcom
` |-  ( z e. RR -> ( ( abs ` z ) = z -> E. x e. ZZ ( abs ` z ) = ( z x. x ) ) )`
18 neg1z
` |-  -u 1 e. ZZ`
19 recn
` |-  ( z e. RR -> z e. CC )`
20 19 mulm1d
` |-  ( z e. RR -> ( -u 1 x. z ) = -u z )`
21 neg1cn
` |-  -u 1 e. CC`
22 mulcom
` |-  ( ( -u 1 e. CC /\ z e. CC ) -> ( -u 1 x. z ) = ( z x. -u 1 ) )`
23 21 19 22 sylancr
` |-  ( z e. RR -> ( -u 1 x. z ) = ( z x. -u 1 ) )`
24 20 23 eqtr3d
` |-  ( z e. RR -> -u z = ( z x. -u 1 ) )`
25 oveq2
` |-  ( x = -u 1 -> ( z x. x ) = ( z x. -u 1 ) )`
26 25 rspceeqv
` |-  ( ( -u 1 e. ZZ /\ -u z = ( z x. -u 1 ) ) -> E. x e. ZZ -u z = ( z x. x ) )`
27 18 24 26 sylancr
` |-  ( z e. RR -> E. x e. ZZ -u z = ( z x. x ) )`
28 eqeq1
` |-  ( ( abs ` z ) = -u z -> ( ( abs ` z ) = ( z x. x ) <-> -u z = ( z x. x ) ) )`
29 28 rexbidv
` |-  ( ( abs ` z ) = -u z -> ( E. x e. ZZ ( abs ` z ) = ( z x. x ) <-> E. x e. ZZ -u z = ( z x. x ) ) )`
30 27 29 syl5ibrcom
` |-  ( z e. RR -> ( ( abs ` z ) = -u z -> E. x e. ZZ ( abs ` z ) = ( z x. x ) ) )`
31 absor
` |-  ( z e. RR -> ( ( abs ` z ) = z \/ ( abs ` z ) = -u z ) )`
32 17 30 31 mpjaod
` |-  ( z e. RR -> E. x e. ZZ ( abs ` z ) = ( z x. x ) )`
33 8 32 syl
` |-  ( z e. ZZ -> E. x e. ZZ ( abs ` z ) = ( z x. x ) )`
34 7 33 vtoclga
` |-  ( A e. ZZ -> E. x e. ZZ ( abs ` A ) = ( A x. x ) )`
35 2 34 syl
` |-  ( ph -> E. x e. ZZ ( abs ` A ) = ( A x. x ) )`
36 3 zcnd
` |-  ( ph -> B e. CC )`
` |-  ( ( ph /\ x e. ZZ ) -> B e. CC )`
38 37 mul01d
` |-  ( ( ph /\ x e. ZZ ) -> ( B x. 0 ) = 0 )`
39 38 oveq2d
` |-  ( ( ph /\ x e. ZZ ) -> ( ( A x. x ) + ( B x. 0 ) ) = ( ( A x. x ) + 0 ) )`
40 2 zcnd
` |-  ( ph -> A e. CC )`
41 zcn
` |-  ( x e. ZZ -> x e. CC )`
42 mulcl
` |-  ( ( A e. CC /\ x e. CC ) -> ( A x. x ) e. CC )`
43 40 41 42 syl2an
` |-  ( ( ph /\ x e. ZZ ) -> ( A x. x ) e. CC )`
` |-  ( ( ph /\ x e. ZZ ) -> ( ( A x. x ) + 0 ) = ( A x. x ) )`
45 39 44 eqtrd
` |-  ( ( ph /\ x e. ZZ ) -> ( ( A x. x ) + ( B x. 0 ) ) = ( A x. x ) )`
46 45 eqeq2d
` |-  ( ( ph /\ x e. ZZ ) -> ( ( abs ` A ) = ( ( A x. x ) + ( B x. 0 ) ) <-> ( abs ` A ) = ( A x. x ) ) )`
47 0z
` |-  0 e. ZZ`
48 oveq2
` |-  ( y = 0 -> ( B x. y ) = ( B x. 0 ) )`
49 48 oveq2d
` |-  ( y = 0 -> ( ( A x. x ) + ( B x. y ) ) = ( ( A x. x ) + ( B x. 0 ) ) )`
50 49 rspceeqv
` |-  ( ( 0 e. ZZ /\ ( abs ` A ) = ( ( A x. x ) + ( B x. 0 ) ) ) -> E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) )`
51 47 50 mpan
` |-  ( ( abs ` A ) = ( ( A x. x ) + ( B x. 0 ) ) -> E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) )`
52 46 51 syl6bir
` |-  ( ( ph /\ x e. ZZ ) -> ( ( abs ` A ) = ( A x. x ) -> E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) ) )`
53 52 reximdva
` |-  ( ph -> ( E. x e. ZZ ( abs ` A ) = ( A x. x ) -> E. x e. ZZ E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) ) )`
54 35 53 mpd
` |-  ( ph -> E. x e. ZZ E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) )`
55 nnabscl
` |-  ( ( A e. ZZ /\ A =/= 0 ) -> ( abs ` A ) e. NN )`
56 55 ex
` |-  ( A e. ZZ -> ( A =/= 0 -> ( abs ` A ) e. NN ) )`
57 2 56 syl
` |-  ( ph -> ( A =/= 0 -> ( abs ` A ) e. NN ) )`
58 eqeq1
` |-  ( z = ( abs ` A ) -> ( z = ( ( A x. x ) + ( B x. y ) ) <-> ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) ) )`
59 58 2rexbidv
` |-  ( z = ( abs ` A ) -> ( E. x e. ZZ E. y e. ZZ z = ( ( A x. x ) + ( B x. y ) ) <-> E. x e. ZZ E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) ) )`
60 59 1 elrab2
` |-  ( ( abs ` A ) e. M <-> ( ( abs ` A ) e. NN /\ E. x e. ZZ E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) ) )`
61 60 simplbi2com
` |-  ( E. x e. ZZ E. y e. ZZ ( abs ` A ) = ( ( A x. x ) + ( B x. y ) ) -> ( ( abs ` A ) e. NN -> ( abs ` A ) e. M ) )`
62 54 57 61 sylsyld
` |-  ( ph -> ( A =/= 0 -> ( abs ` A ) e. M ) )`