Proof of Theorem fzofzim
Step | Hyp | Ref
| Expression |
1 | | elfz2nn0 10055 |
. . . 4
⊢ (𝐾 ∈ (0...𝑀) ↔ (𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0
∧ 𝐾 ≤ 𝑀)) |
2 | | simpl1 995 |
. . . . . 6
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝐾
≤ 𝑀) ∧ 𝐾 ≠ 𝑀) → 𝐾 ∈
ℕ0) |
3 | | necom 2424 |
. . . . . . . . 9
⊢ (𝐾 ≠ 𝑀 ↔ 𝑀 ≠ 𝐾) |
4 | | nn0z 9219 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
5 | | nn0z 9219 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℤ) |
6 | | zltlen 9277 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐾 < 𝑀 ↔ (𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾))) |
7 | 4, 5, 6 | syl2an 287 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝐾 < 𝑀 ↔ (𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾))) |
8 | 7 | bicomd 140 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾) ↔ 𝐾 < 𝑀)) |
9 | | elnn0z 9212 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
↔ (𝐾 ∈ ℤ
∧ 0 ≤ 𝐾)) |
10 | | 0red 7908 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ 0 ∈ ℝ) |
11 | | zre 9203 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) |
12 | 11 | adantr 274 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ 𝐾 ∈
ℝ) |
13 | | nn0re 9131 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
14 | 13 | adantl 275 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ 𝑀 ∈
ℝ) |
15 | | lelttr 7995 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ ∧ 𝐾
∈ ℝ ∧ 𝑀
∈ ℝ) → ((0 ≤ 𝐾 ∧ 𝐾 < 𝑀) → 0 < 𝑀)) |
16 | 10, 12, 14, 15 | syl3anc 1233 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ ((0 ≤ 𝐾 ∧
𝐾 < 𝑀) → 0 < 𝑀)) |
17 | | elnnz 9209 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℤ ∧ 0 <
𝑀)) |
18 | 17 | simplbi2 383 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℤ → (0 <
𝑀 → 𝑀 ∈ ℕ)) |
19 | 5, 18 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ0
→ (0 < 𝑀 →
𝑀 ∈
ℕ)) |
20 | 19 | adantl 275 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (0 < 𝑀 →
𝑀 ∈
ℕ)) |
21 | 16, 20 | syld 45 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ ((0 ≤ 𝐾 ∧
𝐾 < 𝑀) → 𝑀 ∈ ℕ)) |
22 | 21 | expd 256 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℕ0)
→ (0 ≤ 𝐾 →
(𝐾 < 𝑀 → 𝑀 ∈ ℕ))) |
23 | 22 | impancom 258 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) → (𝑀 ∈ ℕ0
→ (𝐾 < 𝑀 → 𝑀 ∈ ℕ))) |
24 | 9, 23 | sylbi 120 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ0
→ (𝑀 ∈
ℕ0 → (𝐾 < 𝑀 → 𝑀 ∈ ℕ))) |
25 | 24 | imp 123 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝐾 < 𝑀 → 𝑀 ∈ ℕ)) |
26 | 8, 25 | sylbid 149 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾) → 𝑀 ∈ ℕ)) |
27 | 26 | expd 256 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝐾 ≤ 𝑀 → (𝑀 ≠ 𝐾 → 𝑀 ∈ ℕ))) |
28 | 3, 27 | syl7bi 164 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝐾 ≤ 𝑀 → (𝐾 ≠ 𝑀 → 𝑀 ∈ ℕ))) |
29 | 28 | 3impia 1195 |
. . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝐾
≤ 𝑀) → (𝐾 ≠ 𝑀 → 𝑀 ∈ ℕ)) |
30 | 29 | imp 123 |
. . . . . 6
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝐾
≤ 𝑀) ∧ 𝐾 ≠ 𝑀) → 𝑀 ∈ ℕ) |
31 | 8 | biimpd 143 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((𝐾 ≤ 𝑀 ∧ 𝑀 ≠ 𝐾) → 𝐾 < 𝑀)) |
32 | 31 | exp4b 365 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ (𝑀 ∈
ℕ0 → (𝐾 ≤ 𝑀 → (𝑀 ≠ 𝐾 → 𝐾 < 𝑀)))) |
33 | 32 | 3imp 1188 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝐾
≤ 𝑀) → (𝑀 ≠ 𝐾 → 𝐾 < 𝑀)) |
34 | 3, 33 | syl5bi 151 |
. . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝐾
≤ 𝑀) → (𝐾 ≠ 𝑀 → 𝐾 < 𝑀)) |
35 | 34 | imp 123 |
. . . . . 6
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝐾
≤ 𝑀) ∧ 𝐾 ≠ 𝑀) → 𝐾 < 𝑀) |
36 | 2, 30, 35 | 3jca 1172 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝐾
≤ 𝑀) ∧ 𝐾 ≠ 𝑀) → (𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀)) |
37 | 36 | ex 114 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0 ∧ 𝐾
≤ 𝑀) → (𝐾 ≠ 𝑀 → (𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀))) |
38 | 1, 37 | sylbi 120 |
. . 3
⊢ (𝐾 ∈ (0...𝑀) → (𝐾 ≠ 𝑀 → (𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀))) |
39 | 38 | impcom 124 |
. 2
⊢ ((𝐾 ≠ 𝑀 ∧ 𝐾 ∈ (0...𝑀)) → (𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀)) |
40 | | elfzo0 10125 |
. 2
⊢ (𝐾 ∈ (0..^𝑀) ↔ (𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐾 < 𝑀)) |
41 | 39, 40 | sylibr 133 |
1
⊢ ((𝐾 ≠ 𝑀 ∧ 𝐾 ∈ (0...𝑀)) → 𝐾 ∈ (0..^𝑀)) |