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