Theorem lgslem2

Description: The set Z of all integers with absolute value at most 1 contains { -u 1 , 0 , 1 } . (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Hypothesis	lgslem2.z	⊢ 𝑍 = { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 }
Assertion	lgslem2	⊢ ( - 1 ∈ 𝑍 ∧ 0 ∈ 𝑍 ∧ 1 ∈ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		lgslem2.z	⊢ 𝑍 = { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 }
2		neg1z	⊢ - 1 ∈ ℤ
3		1le1	⊢ 1 ≤ 1
4		fveq2	⊢ ( 𝑥 = - 1 → ( abs ‘ 𝑥 ) = ( abs ‘ - 1 ) )
5		ax-1cn	⊢ 1 ∈ ℂ
6	5	absnegi	⊢ ( abs ‘ - 1 ) = ( abs ‘ 1 )
7		abs1	⊢ ( abs ‘ 1 ) = 1
8	6 7	eqtri	⊢ ( abs ‘ - 1 ) = 1
9	4 8	eqtrdi	⊢ ( 𝑥 = - 1 → ( abs ‘ 𝑥 ) = 1 )
10	9	breq1d	⊢ ( 𝑥 = - 1 → ( ( abs ‘ 𝑥 ) ≤ 1 ↔ 1 ≤ 1 ) )
11	10 1	elrab2	⊢ ( - 1 ∈ 𝑍 ↔ ( - 1 ∈ ℤ ∧ 1 ≤ 1 ) )
12	2 3 11	mpbir2an	⊢ - 1 ∈ 𝑍
13		0z	⊢ 0 ∈ ℤ
14		0le1	⊢ 0 ≤ 1
15		fveq2	⊢ ( 𝑥 = 0 → ( abs ‘ 𝑥 ) = ( abs ‘ 0 ) )
16		abs0	⊢ ( abs ‘ 0 ) = 0
17	15 16	eqtrdi	⊢ ( 𝑥 = 0 → ( abs ‘ 𝑥 ) = 0 )
18	17	breq1d	⊢ ( 𝑥 = 0 → ( ( abs ‘ 𝑥 ) ≤ 1 ↔ 0 ≤ 1 ) )
19	18 1	elrab2	⊢ ( 0 ∈ 𝑍 ↔ ( 0 ∈ ℤ ∧ 0 ≤ 1 ) )
20	13 14 19	mpbir2an	⊢ 0 ∈ 𝑍
21		1z	⊢ 1 ∈ ℤ
22		fveq2	⊢ ( 𝑥 = 1 → ( abs ‘ 𝑥 ) = ( abs ‘ 1 ) )
23	22 7	eqtrdi	⊢ ( 𝑥 = 1 → ( abs ‘ 𝑥 ) = 1 )
24	23	breq1d	⊢ ( 𝑥 = 1 → ( ( abs ‘ 𝑥 ) ≤ 1 ↔ 1 ≤ 1 ) )
25	24 1	elrab2	⊢ ( 1 ∈ 𝑍 ↔ ( 1 ∈ ℤ ∧ 1 ≤ 1 ) )
26	21 3 25	mpbir2an	⊢ 1 ∈ 𝑍
27	12 20 26	3pm3.2i	⊢ ( - 1 ∈ 𝑍 ∧ 0 ∈ 𝑍 ∧ 1 ∈ 𝑍 )