Metamath Proof Explorer

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 ⊢Z=x∈ℤ|x≤1
Assertion lgslem2 ⊢−1∈Z∧0∈Z∧1∈Z

Proof

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