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