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 ⊢ 𝑍 = { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 }
Assertion lgslem3 ( ( 𝐴 ∈ 𝑍 ∧ 𝐵 ∈ 𝑍 ) → ( 𝐴 · 𝐵 ) ∈ 𝑍 )

Proof

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