Proof of Theorem fzo1fzo0n0
Step | Hyp | Ref
| Expression |
1 | | elfzo2 13132 |
. . 3
⊢ (𝐾 ∈ (1..^𝑁) ↔ (𝐾 ∈ (ℤ≥‘1)
∧ 𝑁 ∈ ℤ
∧ 𝐾 < 𝑁)) |
2 | | elnnuz 12364 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ ↔ 𝐾 ∈
(ℤ≥‘1)) |
3 | | nnnn0 11983 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) |
4 | 3 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 𝐾 ∈
ℕ0) |
5 | 4 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝑁) → 𝐾 ∈
ℕ0) |
6 | | nngt0 11747 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ → 0 <
𝐾) |
7 | | 0red 10722 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → 0 ∈
ℝ) |
8 | | nnre 11723 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℝ) |
9 | 8 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → 𝐾 ∈
ℝ) |
10 | | zre 12066 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
11 | 10 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → 𝑁 ∈
ℝ) |
12 | | lttr 10795 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ 𝐾
∈ ℝ ∧ 𝑁
∈ ℝ) → ((0 < 𝐾 ∧ 𝐾 < 𝑁) → 0 < 𝑁)) |
13 | 7, 9, 11, 12 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → ((0 <
𝐾 ∧ 𝐾 < 𝑁) → 0 < 𝑁)) |
14 | | elnnz 12072 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 <
𝑁)) |
15 | 14 | simplbi2 504 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → (0 <
𝑁 → 𝑁 ∈ ℕ)) |
16 | 15 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (0 <
𝑁 → 𝑁 ∈ ℕ)) |
17 | 13, 16 | syld 47 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → ((0 <
𝐾 ∧ 𝐾 < 𝑁) → 𝑁 ∈ ℕ)) |
18 | 17 | exp4b 434 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝐾 ∈ ℕ → (0 <
𝐾 → (𝐾 < 𝑁 → 𝑁 ∈ ℕ)))) |
19 | 18 | com13 88 |
. . . . . . . . . . 11
⊢ (0 <
𝐾 → (𝐾 ∈ ℕ → (𝑁 ∈ ℤ → (𝐾 < 𝑁 → 𝑁 ∈ ℕ)))) |
20 | 6, 19 | mpcom 38 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℕ → (𝑁 ∈ ℤ → (𝐾 < 𝑁 → 𝑁 ∈ ℕ))) |
21 | 20 | imp31 421 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝑁) → 𝑁 ∈ ℕ) |
22 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝑁) → 𝐾 < 𝑁) |
23 | 5, 21, 22 | 3jca 1129 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝑁) → (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) |
24 | 23 | exp31 423 |
. . . . . . 7
⊢ (𝐾 ∈ ℕ → (𝑁 ∈ ℤ → (𝐾 < 𝑁 → (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)))) |
25 | 2, 24 | sylbir 238 |
. . . . . 6
⊢ (𝐾 ∈
(ℤ≥‘1) → (𝑁 ∈ ℤ → (𝐾 < 𝑁 → (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)))) |
26 | 25 | 3imp 1112 |
. . . . 5
⊢ ((𝐾 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁) → (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) |
27 | | elfzo0 13169 |
. . . . 5
⊢ (𝐾 ∈ (0..^𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) |
28 | 26, 27 | sylibr 237 |
. . . 4
⊢ ((𝐾 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁) → 𝐾 ∈ (0..^𝑁)) |
29 | | nnne0 11750 |
. . . . . 6
⊢ (𝐾 ∈ ℕ → 𝐾 ≠ 0) |
30 | 2, 29 | sylbir 238 |
. . . . 5
⊢ (𝐾 ∈
(ℤ≥‘1) → 𝐾 ≠ 0) |
31 | 30 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐾 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁) → 𝐾 ≠ 0) |
32 | 28, 31 | jca 515 |
. . 3
⊢ ((𝐾 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁) → (𝐾 ∈ (0..^𝑁) ∧ 𝐾 ≠ 0)) |
33 | 1, 32 | sylbi 220 |
. 2
⊢ (𝐾 ∈ (1..^𝑁) → (𝐾 ∈ (0..^𝑁) ∧ 𝐾 ≠ 0)) |
34 | | elnnne0 11990 |
. . . . . 6
⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℕ0
∧ 𝐾 ≠
0)) |
35 | | nnge1 11744 |
. . . . . 6
⊢ (𝐾 ∈ ℕ → 1 ≤
𝐾) |
36 | 34, 35 | sylbir 238 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝐾 ≠ 0) → 1
≤ 𝐾) |
37 | 36 | 3ad2antl1 1186 |
. . . 4
⊢ (((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) ∧ 𝐾 ≠ 0) → 1 ≤ 𝐾) |
38 | | simpl3 1194 |
. . . 4
⊢ (((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) ∧ 𝐾 ≠ 0) → 𝐾 < 𝑁) |
39 | | nn0z 12086 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
40 | 39 | adantr 484 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝐾 ∈
ℤ) |
41 | | 1zzd 12094 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 1 ∈ ℤ) |
42 | | nnz 12085 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
43 | 42 | adantl 485 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑁 ∈
ℤ) |
44 | 40, 41, 43 | 3jca 1129 |
. . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝐾 ∈ ℤ
∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
45 | 44 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝐾 ∈ ℤ ∧ 1 ∈ ℤ ∧
𝑁 ∈
ℤ)) |
46 | 45 | adantr 484 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) ∧ 𝐾 ≠ 0) → (𝐾 ∈ ℤ ∧ 1 ∈ ℤ ∧
𝑁 ∈
ℤ)) |
47 | | elfzo 13131 |
. . . . 5
⊢ ((𝐾 ∈ ℤ ∧ 1 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝐾 ∈
(1..^𝑁) ↔ (1 ≤
𝐾 ∧ 𝐾 < 𝑁))) |
48 | 46, 47 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) ∧ 𝐾 ≠ 0) → (𝐾 ∈ (1..^𝑁) ↔ (1 ≤ 𝐾 ∧ 𝐾 < 𝑁))) |
49 | 37, 38, 48 | mpbir2and 713 |
. . 3
⊢ (((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) ∧ 𝐾 ≠ 0) → 𝐾 ∈ (1..^𝑁)) |
50 | 27, 49 | sylanb 584 |
. 2
⊢ ((𝐾 ∈ (0..^𝑁) ∧ 𝐾 ≠ 0) → 𝐾 ∈ (1..^𝑁)) |
51 | 33, 50 | impbii 212 |
1
⊢ (𝐾 ∈ (1..^𝑁) ↔ (𝐾 ∈ (0..^𝑁) ∧ 𝐾 ≠ 0)) |