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