Proof of Theorem zabsle1
Step | Hyp | Ref
| Expression |
1 | | eltpi 4603 |
. . 3
⊢ (𝑍 ∈ {-1, 0, 1} → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1)) |
2 | | fveq2 6717 |
. . . . 5
⊢ (𝑍 = -1 → (abs‘𝑍) =
(abs‘-1)) |
3 | | ax-1cn 10787 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
4 | 3 | absnegi 14964 |
. . . . . . 7
⊢
(abs‘-1) = (abs‘1) |
5 | | abs1 14861 |
. . . . . . 7
⊢
(abs‘1) = 1 |
6 | 4, 5 | eqtri 2765 |
. . . . . 6
⊢
(abs‘-1) = 1 |
7 | | 1le1 11460 |
. . . . . 6
⊢ 1 ≤
1 |
8 | 6, 7 | eqbrtri 5074 |
. . . . 5
⊢
(abs‘-1) ≤ 1 |
9 | 2, 8 | eqbrtrdi 5092 |
. . . 4
⊢ (𝑍 = -1 → (abs‘𝑍) ≤ 1) |
10 | | fveq2 6717 |
. . . . 5
⊢ (𝑍 = 0 → (abs‘𝑍) =
(abs‘0)) |
11 | | abs0 14849 |
. . . . . 6
⊢
(abs‘0) = 0 |
12 | | 0le1 11355 |
. . . . . 6
⊢ 0 ≤
1 |
13 | 11, 12 | eqbrtri 5074 |
. . . . 5
⊢
(abs‘0) ≤ 1 |
14 | 10, 13 | eqbrtrdi 5092 |
. . . 4
⊢ (𝑍 = 0 → (abs‘𝑍) ≤ 1) |
15 | | fveq2 6717 |
. . . . 5
⊢ (𝑍 = 1 → (abs‘𝑍) =
(abs‘1)) |
16 | 5, 7 | eqbrtri 5074 |
. . . . 5
⊢
(abs‘1) ≤ 1 |
17 | 15, 16 | eqbrtrdi 5092 |
. . . 4
⊢ (𝑍 = 1 → (abs‘𝑍) ≤ 1) |
18 | 9, 14, 17 | 3jaoi 1429 |
. . 3
⊢ ((𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1) → (abs‘𝑍) ≤ 1) |
19 | 1, 18 | syl 17 |
. 2
⊢ (𝑍 ∈ {-1, 0, 1} →
(abs‘𝑍) ≤
1) |
20 | | zre 12180 |
. . . 4
⊢ (𝑍 ∈ ℤ → 𝑍 ∈
ℝ) |
21 | | 1red 10834 |
. . . 4
⊢ (𝑍 ∈ ℤ → 1 ∈
ℝ) |
22 | 20, 21 | absled 14994 |
. . 3
⊢ (𝑍 ∈ ℤ →
((abs‘𝑍) ≤ 1
↔ (-1 ≤ 𝑍 ∧
𝑍 ≤
1))) |
23 | | elz 12178 |
. . . 4
⊢ (𝑍 ∈ ℤ ↔ (𝑍 ∈ ℝ ∧ (𝑍 = 0 ∨ 𝑍 ∈ ℕ ∨ -𝑍 ∈ ℕ))) |
24 | | 3mix2 1333 |
. . . . . . . . . 10
⊢ (𝑍 = 0 → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1)) |
25 | 24 | a1d 25 |
. . . . . . . . 9
⊢ (𝑍 = 0 → ((𝑍 ∈ ℝ ∧ (-1 ≤ 𝑍 ∧ 𝑍 ≤ 1)) → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
26 | | nnle1eq1 11860 |
. . . . . . . . . . . . . . 15
⊢ (𝑍 ∈ ℕ → (𝑍 ≤ 1 ↔ 𝑍 = 1)) |
27 | 26 | biimpac 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑍 ≤ 1 ∧ 𝑍 ∈ ℕ) → 𝑍 = 1) |
28 | 27 | 3mix3d 1340 |
. . . . . . . . . . . . 13
⊢ ((𝑍 ≤ 1 ∧ 𝑍 ∈ ℕ) → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1)) |
29 | 28 | ex 416 |
. . . . . . . . . . . 12
⊢ (𝑍 ≤ 1 → (𝑍 ∈ ℕ → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
30 | 29 | adantl 485 |
. . . . . . . . . . 11
⊢ ((-1 ≤
𝑍 ∧ 𝑍 ≤ 1) → (𝑍 ∈ ℕ → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
31 | 30 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑍 ∈ ℝ ∧ (-1 ≤
𝑍 ∧ 𝑍 ≤ 1)) → (𝑍 ∈ ℕ → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
32 | 31 | com12 32 |
. . . . . . . . 9
⊢ (𝑍 ∈ ℕ → ((𝑍 ∈ ℝ ∧ (-1 ≤
𝑍 ∧ 𝑍 ≤ 1)) → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
33 | | elnnz1 12203 |
. . . . . . . . . 10
⊢ (-𝑍 ∈ ℕ ↔ (-𝑍 ∈ ℤ ∧ 1 ≤
-𝑍)) |
34 | | 1red 10834 |
. . . . . . . . . . . . . . 15
⊢ (𝑍 ∈ ℝ → 1 ∈
ℝ) |
35 | | lenegcon2 11337 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ 𝑍
∈ ℝ) → (1 ≤ -𝑍 ↔ 𝑍 ≤ -1)) |
36 | 34, 35 | mpancom 688 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ ℝ → (1 ≤
-𝑍 ↔ 𝑍 ≤ -1)) |
37 | | neg1rr 11945 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ -1 ∈
ℝ |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑍 ∈ ℝ → -1 ∈
ℝ) |
39 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑍 ∈ ℝ → 𝑍 ∈
ℝ) |
40 | 38, 39 | letri3d 10974 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑍 ∈ ℝ → (-1 =
𝑍 ↔ (-1 ≤ 𝑍 ∧ 𝑍 ≤ -1))) |
41 | | 3mix1 1332 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑍 = -1 → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1)) |
42 | 41 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . 19
⊢ (-1 =
𝑍 → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1)) |
43 | 40, 42 | syl6bir 257 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑍 ∈ ℝ → ((-1 ≤
𝑍 ∧ 𝑍 ≤ -1) → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
44 | 43 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ((-1 ≤
𝑍 ∧ 𝑍 ≤ -1) → (𝑍 ∈ ℝ → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
45 | 44 | ex 416 |
. . . . . . . . . . . . . . . 16
⊢ (-1 ≤
𝑍 → (𝑍 ≤ -1 → (𝑍 ∈ ℝ → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1)))) |
46 | 45 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((-1 ≤
𝑍 ∧ 𝑍 ≤ 1) → (𝑍 ≤ -1 → (𝑍 ∈ ℝ → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1)))) |
47 | 46 | com13 88 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ ℝ → (𝑍 ≤ -1 → ((-1 ≤ 𝑍 ∧ 𝑍 ≤ 1) → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1)))) |
48 | 36, 47 | sylbid 243 |
. . . . . . . . . . . . 13
⊢ (𝑍 ∈ ℝ → (1 ≤
-𝑍 → ((-1 ≤ 𝑍 ∧ 𝑍 ≤ 1) → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1)))) |
49 | 48 | com12 32 |
. . . . . . . . . . . 12
⊢ (1 ≤
-𝑍 → (𝑍 ∈ ℝ → ((-1 ≤
𝑍 ∧ 𝑍 ≤ 1) → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1)))) |
50 | 49 | impd 414 |
. . . . . . . . . . 11
⊢ (1 ≤
-𝑍 → ((𝑍 ∈ ℝ ∧ (-1 ≤
𝑍 ∧ 𝑍 ≤ 1)) → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
51 | 50 | adantl 485 |
. . . . . . . . . 10
⊢ ((-𝑍 ∈ ℤ ∧ 1 ≤
-𝑍) → ((𝑍 ∈ ℝ ∧ (-1 ≤
𝑍 ∧ 𝑍 ≤ 1)) → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
52 | 33, 51 | sylbi 220 |
. . . . . . . . 9
⊢ (-𝑍 ∈ ℕ → ((𝑍 ∈ ℝ ∧ (-1 ≤
𝑍 ∧ 𝑍 ≤ 1)) → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
53 | 25, 32, 52 | 3jaoi 1429 |
. . . . . . . 8
⊢ ((𝑍 = 0 ∨ 𝑍 ∈ ℕ ∨ -𝑍 ∈ ℕ) → ((𝑍 ∈ ℝ ∧ (-1 ≤ 𝑍 ∧ 𝑍 ≤ 1)) → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
54 | 53 | imp 410 |
. . . . . . 7
⊢ (((𝑍 = 0 ∨ 𝑍 ∈ ℕ ∨ -𝑍 ∈ ℕ) ∧ (𝑍 ∈ ℝ ∧ (-1 ≤ 𝑍 ∧ 𝑍 ≤ 1))) → (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1)) |
55 | | eltpg 4601 |
. . . . . . . . 9
⊢ (𝑍 ∈ ℝ → (𝑍 ∈ {-1, 0, 1} ↔ (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
56 | 55 | adantr 484 |
. . . . . . . 8
⊢ ((𝑍 ∈ ℝ ∧ (-1 ≤
𝑍 ∧ 𝑍 ≤ 1)) → (𝑍 ∈ {-1, 0, 1} ↔ (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
57 | 56 | adantl 485 |
. . . . . . 7
⊢ (((𝑍 = 0 ∨ 𝑍 ∈ ℕ ∨ -𝑍 ∈ ℕ) ∧ (𝑍 ∈ ℝ ∧ (-1 ≤ 𝑍 ∧ 𝑍 ≤ 1))) → (𝑍 ∈ {-1, 0, 1} ↔ (𝑍 = -1 ∨ 𝑍 = 0 ∨ 𝑍 = 1))) |
58 | 54, 57 | mpbird 260 |
. . . . . 6
⊢ (((𝑍 = 0 ∨ 𝑍 ∈ ℕ ∨ -𝑍 ∈ ℕ) ∧ (𝑍 ∈ ℝ ∧ (-1 ≤ 𝑍 ∧ 𝑍 ≤ 1))) → 𝑍 ∈ {-1, 0, 1}) |
59 | 58 | exp32 424 |
. . . . 5
⊢ ((𝑍 = 0 ∨ 𝑍 ∈ ℕ ∨ -𝑍 ∈ ℕ) → (𝑍 ∈ ℝ → ((-1 ≤ 𝑍 ∧ 𝑍 ≤ 1) → 𝑍 ∈ {-1, 0, 1}))) |
60 | 59 | impcom 411 |
. . . 4
⊢ ((𝑍 ∈ ℝ ∧ (𝑍 = 0 ∨ 𝑍 ∈ ℕ ∨ -𝑍 ∈ ℕ)) → ((-1 ≤ 𝑍 ∧ 𝑍 ≤ 1) → 𝑍 ∈ {-1, 0, 1})) |
61 | 23, 60 | sylbi 220 |
. . 3
⊢ (𝑍 ∈ ℤ → ((-1 ≤
𝑍 ∧ 𝑍 ≤ 1) → 𝑍 ∈ {-1, 0, 1})) |
62 | 22, 61 | sylbid 243 |
. 2
⊢ (𝑍 ∈ ℤ →
((abs‘𝑍) ≤ 1
→ 𝑍 ∈ {-1, 0,
1})) |
63 | 19, 62 | impbid2 229 |
1
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ {-1, 0, 1} ↔
(abs‘𝑍) ≤
1)) |