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	⊢ ( ( 𝐴 ∈ 𝑍 ∧ 𝐵 ∈ 𝑍 ) → ( 𝐴 · 𝐵 ) ∈ 𝑍 )