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 )
37 36 adantr 
 |-  ( ( 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 )
44 43 addid1d 
 |-  ( ( 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 ) )