Metamath Proof Explorer

Theorem lgslem3

Description: The set Z of all integers with absolute value at most 1 is closed under multiplication. (Contributed by Mario Carneiro, 4-Feb-2015)

Ref Expression
Hypothesis lgslem2.z 
|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }
Assertion lgslem3 
|- ( ( A e. Z /\ B e. Z ) -> ( A x. B ) e. Z )

Proof

Step Hyp Ref Expression
1 lgslem2.z 
 |-  Z = { x e. ZZ | ( abs ` x ) <_ 1 }
2 zmulcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A x. B ) e. ZZ )
3 2 ad2ant2r 
 |-  ( ( ( A e. ZZ /\ ( abs ` A ) <_ 1 ) /\ ( B e. ZZ /\ ( abs ` B ) <_ 1 ) ) -> ( A x. B ) e. ZZ )
4 zcn 
 |-  ( A e. ZZ -> A e. CC )
5 zcn 
 |-  ( B e. ZZ -> B e. CC )
6 absmul 
 |-  ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) ) )
7 4 5 6 syl2an 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) ) )
8 7 ad2ant2r 
 |-  ( ( ( A e. ZZ /\ ( abs ` A ) <_ 1 ) /\ ( B e. ZZ /\ ( abs ` B ) <_ 1 ) ) -> ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) ) )
9 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
10 absge0 
 |-  ( A e. CC -> 0 <_ ( abs ` A ) )
11 9 10 jca 
 |-  ( A e. CC -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
12 4 11 syl 
 |-  ( A e. ZZ -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
13 12 adantr 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) )
14 1red 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> 1 e. RR )
15 abscl 
 |-  ( B e. CC -> ( abs ` B ) e. RR )
16 absge0 
 |-  ( B e. CC -> 0 <_ ( abs ` B ) )
17 15 16 jca 
 |-  ( B e. CC -> ( ( abs ` B ) e. RR /\ 0 <_ ( abs ` B ) ) )
18 5 17 syl 
 |-  ( B e. ZZ -> ( ( abs ` B ) e. RR /\ 0 <_ ( abs ` B ) ) )
19 18 adantl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( abs ` B ) e. RR /\ 0 <_ ( abs ` B ) ) )
20 lemul12a 
 |-  ( ( ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) /\ 1 e. RR ) /\ ( ( ( abs ` B ) e. RR /\ 0 <_ ( abs ` B ) ) /\ 1 e. RR ) ) -> ( ( ( abs ` A ) <_ 1 /\ ( abs ` B ) <_ 1 ) -> ( ( abs ` A ) x. ( abs ` B ) ) <_ ( 1 x. 1 ) ) )
21 13 14 19 14 20 syl22anc 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( ( abs ` A ) <_ 1 /\ ( abs ` B ) <_ 1 ) -> ( ( abs ` A ) x. ( abs ` B ) ) <_ ( 1 x. 1 ) ) )
22 21 imp 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( ( abs ` A ) <_ 1 /\ ( abs ` B ) <_ 1 ) ) -> ( ( abs ` A ) x. ( abs ` B ) ) <_ ( 1 x. 1 ) )
23 22 an4s 
 |-  ( ( ( A e. ZZ /\ ( abs ` A ) <_ 1 ) /\ ( B e. ZZ /\ ( abs ` B ) <_ 1 ) ) -> ( ( abs ` A ) x. ( abs ` B ) ) <_ ( 1 x. 1 ) )
24 1t1e1 
 |-  ( 1 x. 1 ) = 1
25 23 24 breqtrdi 
 |-  ( ( ( A e. ZZ /\ ( abs ` A ) <_ 1 ) /\ ( B e. ZZ /\ ( abs ` B ) <_ 1 ) ) -> ( ( abs ` A ) x. ( abs ` B ) ) <_ 1 )
26 8 25 eqbrtrd 
 |-  ( ( ( A e. ZZ /\ ( abs ` A ) <_ 1 ) /\ ( B e. ZZ /\ ( abs ` B ) <_ 1 ) ) -> ( abs ` ( A x. B ) ) <_ 1 )
27 3 26 jca 
 |-  ( ( ( A e. ZZ /\ ( abs ` A ) <_ 1 ) /\ ( B e. ZZ /\ ( abs ` B ) <_ 1 ) ) -> ( ( A x. B ) e. ZZ /\ ( abs ` ( A x. B ) ) <_ 1 ) )
28 fveq2 
 |-  ( x = A -> ( abs ` x ) = ( abs ` A ) )
29 28 breq1d 
 |-  ( x = A -> ( ( abs ` x ) <_ 1 <-> ( abs ` A ) <_ 1 ) )
30 29 1 elrab2 
 |-  ( A e. Z <-> ( A e. ZZ /\ ( abs ` A ) <_ 1 ) )
31 fveq2 
 |-  ( x = B -> ( abs ` x ) = ( abs ` B ) )
32 31 breq1d 
 |-  ( x = B -> ( ( abs ` x ) <_ 1 <-> ( abs ` B ) <_ 1 ) )
33 32 1 elrab2 
 |-  ( B e. Z <-> ( B e. ZZ /\ ( abs ` B ) <_ 1 ) )
34 30 33 anbi12i 
 |-  ( ( A e. Z /\ B e. Z ) <-> ( ( A e. ZZ /\ ( abs ` A ) <_ 1 ) /\ ( B e. ZZ /\ ( abs ` B ) <_ 1 ) ) )
35 fveq2 
 |-  ( x = ( A x. B ) -> ( abs ` x ) = ( abs ` ( A x. B ) ) )
36 35 breq1d 
 |-  ( x = ( A x. B ) -> ( ( abs ` x ) <_ 1 <-> ( abs ` ( A x. B ) ) <_ 1 ) )
37 36 1 elrab2 
 |-  ( ( A x. B ) e. Z <-> ( ( A x. B ) e. ZZ /\ ( abs ` ( A x. B ) ) <_ 1 ) )
38 27 34 37 3imtr4i 
 |-  ( ( A e. Z /\ B e. Z ) -> ( A x. B ) e. Z )