Proof of Theorem fz0fzelfz0
Step | Hyp | Ref
| Expression |
1 | | elfz2nn0 13329 |
. . . 4
⊢ (𝑁 ∈ (0...𝑅) ↔ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅)) |
2 | | elfz2 13228 |
. . . . . 6
⊢ (𝑀 ∈ (𝑁...𝑅) ↔ ((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅))) |
3 | | simplr 765 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
∧ 𝑁 ≤ 𝑀) → 𝑀 ∈ ℤ) |
4 | | 0red 10962 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
→ 0 ∈ ℝ) |
5 | | nn0re 12225 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
6 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
→ 𝑁 ∈
ℝ) |
7 | | zre 12306 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
8 | 7 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
→ 𝑀 ∈
ℝ) |
9 | 4, 6, 8 | 3jca 1126 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
→ (0 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ)) |
10 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
∧ 𝑁 ≤ 𝑀) → (0 ∈ ℝ ∧
𝑁 ∈ ℝ ∧
𝑀 ∈
ℝ)) |
11 | | nn0ge0 12241 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
12 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
→ 0 ≤ 𝑁) |
13 | 12 | anim1i 614 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
∧ 𝑁 ≤ 𝑀) → (0 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)) |
14 | | letr 11052 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ ∧ 𝑁
∈ ℝ ∧ 𝑀
∈ ℝ) → ((0 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀) → 0 ≤ 𝑀)) |
15 | 10, 13, 14 | sylc 65 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
∧ 𝑁 ≤ 𝑀) → 0 ≤ 𝑀) |
16 | | elnn0z 12315 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℤ
∧ 0 ≤ 𝑀)) |
17 | 3, 15, 16 | sylanbrc 582 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈ ℤ)
∧ 𝑁 ≤ 𝑀) → 𝑀 ∈
ℕ0) |
18 | 17 | exp31 419 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ (𝑀 ∈ ℤ
→ (𝑁 ≤ 𝑀 → 𝑀 ∈
ℕ0))) |
19 | 18 | com23 86 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ≤ 𝑀 → (𝑀 ∈ ℤ → 𝑀 ∈
ℕ0))) |
20 | 19 | 3ad2ant1 1131 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈
ℕ0 ∧ 𝑁
≤ 𝑅) → (𝑁 ≤ 𝑀 → (𝑀 ∈ ℤ → 𝑀 ∈
ℕ0))) |
21 | 20 | com13 88 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → (𝑁 ≤ 𝑀 → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅) → 𝑀 ∈
ℕ0))) |
22 | 21 | adantrd 491 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℤ → ((𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅) → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅) → 𝑀 ∈
ℕ0))) |
23 | 22 | 3ad2ant3 1133 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅) → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅) → 𝑀 ∈
ℕ0))) |
24 | 23 | imp 406 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)) → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅) → 𝑀 ∈
ℕ0)) |
25 | 24 | imp 406 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅)) → 𝑀 ∈
ℕ0) |
26 | | simpr2 1193 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅)) → 𝑅 ∈
ℕ0) |
27 | | simplrr 774 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅)) → 𝑀 ≤ 𝑅) |
28 | 25, 26, 27 | 3jca 1126 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)) ∧ (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅)) → (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅)) |
29 | 28 | ex 412 |
. . . . . 6
⊢ (((𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑅)) → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅) → (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅))) |
30 | 2, 29 | sylbi 216 |
. . . . 5
⊢ (𝑀 ∈ (𝑁...𝑅) → ((𝑁 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑁 ≤ 𝑅) → (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅))) |
31 | 30 | com12 32 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈
ℕ0 ∧ 𝑁
≤ 𝑅) → (𝑀 ∈ (𝑁...𝑅) → (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅))) |
32 | 1, 31 | sylbi 216 |
. . 3
⊢ (𝑁 ∈ (0...𝑅) → (𝑀 ∈ (𝑁...𝑅) → (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅))) |
33 | 32 | imp 406 |
. 2
⊢ ((𝑁 ∈ (0...𝑅) ∧ 𝑀 ∈ (𝑁...𝑅)) → (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅)) |
34 | | elfz2nn0 13329 |
. 2
⊢ (𝑀 ∈ (0...𝑅) ↔ (𝑀 ∈ ℕ0 ∧ 𝑅 ∈ ℕ0
∧ 𝑀 ≤ 𝑅)) |
35 | 33, 34 | sylibr 233 |
1
⊢ ((𝑁 ∈ (0...𝑅) ∧ 𝑀 ∈ (𝑁...𝑅)) → 𝑀 ∈ (0...𝑅)) |