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∈ℤ|x≤1
Assertion lgslem3 ⊢A∈Z∧B∈Z→A⁢B∈Z

Proof

Step Hyp Ref Expression
1 lgslem2.z ⊢Z=x∈ℤ|x≤1
2 zmulcl ⊢A∈ℤ∧B∈ℤ→A⁢B∈ℤ
3 2 ad2ant2r ⊢A∈ℤ∧A≤1∧B∈ℤ∧B≤1→A⁢B∈ℤ
4 zcn ⊢A∈ℤ→A∈ℂ
5 zcn ⊢B∈ℤ→B∈ℂ
6 absmul ⊢A∈ℂ∧B∈ℂ→A⁢B=A⁢B
7 4 5 6 syl2an ⊢A∈ℤ∧B∈ℤ→A⁢B=A⁢B
8 7 ad2ant2r ⊢A∈ℤ∧A≤1∧B∈ℤ∧B≤1→A⁢B=A⁢B
9 abscl ⊢A∈ℂ→A∈ℝ
10 absge0 ⊢A∈ℂ→0≤A
11 9 10 jca ⊢A∈ℂ→A∈ℝ∧0≤A
12 4 11 syl ⊢A∈ℤ→A∈ℝ∧0≤A
13 12 adantr ⊢A∈ℤ∧B∈ℤ→A∈ℝ∧0≤A
14 1red ⊢A∈ℤ∧B∈ℤ→1∈ℝ
15 abscl ⊢B∈ℂ→B∈ℝ
16 absge0 ⊢B∈ℂ→0≤B
17 15 16 jca ⊢B∈ℂ→B∈ℝ∧0≤B
18 5 17 syl ⊢B∈ℤ→B∈ℝ∧0≤B
19 18 adantl ⊢A∈ℤ∧B∈ℤ→B∈ℝ∧0≤B
20 lemul12a ⊢A∈ℝ∧0≤A∧1∈ℝ∧B∈ℝ∧0≤B∧1∈ℝ→A≤1∧B≤1→A⁢B≤1⋅1
21 13 14 19 14 20 syl22anc ⊢A∈ℤ∧B∈ℤ→A≤1∧B≤1→A⁢B≤1⋅1
22 21 imp ⊢A∈ℤ∧B∈ℤ∧A≤1∧B≤1→A⁢B≤1⋅1
23 22 an4s ⊢A∈ℤ∧A≤1∧B∈ℤ∧B≤1→A⁢B≤1⋅1
24 1t1e1 ⊢1⋅1=1
25 23 24 breqtrdi ⊢A∈ℤ∧A≤1∧B∈ℤ∧B≤1→A⁢B≤1
26 8 25 eqbrtrd ⊢A∈ℤ∧A≤1∧B∈ℤ∧B≤1→A⁢B≤1
27 3 26 jca ⊢A∈ℤ∧A≤1∧B∈ℤ∧B≤1→A⁢B∈ℤ∧A⁢B≤1
28 fveq2 ⊢x=A→x=A
29 28 breq1d ⊢x=A→x≤1↔A≤1
30 29 1 elrab2 ⊢A∈Z↔A∈ℤ∧A≤1
31 fveq2 ⊢x=B→x=B
32 31 breq1d ⊢x=B→x≤1↔B≤1
33 32 1 elrab2 ⊢B∈Z↔B∈ℤ∧B≤1
34 30 33 anbi12i ⊢A∈Z∧B∈Z↔A∈ℤ∧A≤1∧B∈ℤ∧B≤1
35 fveq2 ⊢x=A⁢B→x=A⁢B
36 35 breq1d ⊢x=A⁢B→x≤1↔A⁢B≤1
37 36 1 elrab2 ⊢A⁢B∈Z↔A⁢B∈ℤ∧A⁢B≤1
38 27 34 37 3imtr4i ⊢A∈Z∧B∈Z→A⁢B∈Z