Proof of Theorem elfz0fzfz0
Step | Hyp | Ref
| Expression |
1 | | elfz2nn0 13216 |
. . . 4
⊢ (𝑀 ∈ (0...𝐿) ↔ (𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿)) |
2 | | elfz2 13115 |
. . . . . 6
⊢ (𝑁 ∈ (𝐿...𝑋) ↔ ((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋))) |
3 | | nn0re 12112 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
4 | | nn0re 12112 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐿 ∈ ℕ0
→ 𝐿 ∈
ℝ) |
5 | | zre 12193 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
6 | 3, 4, 5 | 3anim123i 1153 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑁
∈ ℤ) → (𝑀
∈ ℝ ∧ 𝐿
∈ ℝ ∧ 𝑁
∈ ℝ)) |
7 | 6 | 3expa 1120 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
8 | | letr 10939 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁) → 𝑀 ≤ 𝑁)) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) ∧ 𝑁 ∈ ℤ) → ((𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁) → 𝑀 ≤ 𝑁)) |
10 | | simplll 775 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈
ℕ0) |
11 | | simpr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ) |
12 | 11 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈ ℤ) |
13 | | elnn0z 12202 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℤ
∧ 0 ≤ 𝑀)) |
14 | | 0red 10849 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 0 ∈
ℝ) |
15 | | zre 12193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
16 | 15 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈
ℝ) |
17 | 5 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℝ) |
18 | | letr 10939 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((0
∈ ℝ ∧ 𝑀
∈ ℝ ∧ 𝑁
∈ ℝ) → ((0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁) → 0 ≤ 𝑁)) |
19 | 14, 16, 17, 18 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((0 ≤
𝑀 ∧ 𝑀 ≤ 𝑁) → 0 ≤ 𝑁)) |
20 | 19 | exp4b 434 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ ℤ → (0 ≤
𝑀 → (𝑀 ≤ 𝑁 → 0 ≤ 𝑁)))) |
21 | 20 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℤ → (0 ≤
𝑀 → (𝑁 ∈ ℤ → (𝑀 ≤ 𝑁 → 0 ≤ 𝑁)))) |
22 | 21 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℤ ∧ 0 ≤
𝑀) → (𝑁 ∈ ℤ → (𝑀 ≤ 𝑁 → 0 ≤ 𝑁))) |
23 | 13, 22 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ0
→ (𝑁 ∈ ℤ
→ (𝑀 ≤ 𝑁 → 0 ≤ 𝑁))) |
24 | 23 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝑁 ∈ ℤ → (𝑀 ≤ 𝑁 → 0 ≤ 𝑁))) |
25 | 24 | imp 410 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 → 0 ≤ 𝑁)) |
26 | 25 | imp 410 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 0 ≤ 𝑁) |
27 | | elnn0z 12202 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℤ
∧ 0 ≤ 𝑁)) |
28 | 12, 26, 27 | sylanbrc 586 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈
ℕ0) |
29 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ 𝑁) |
30 | 10, 28, 29 | 3jca 1130 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
31 | 30 | ex 416 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) |
32 | 9, 31 | syld 47 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) ∧ 𝑁 ∈ ℤ) → ((𝑀 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) |
33 | 32 | exp4b 434 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝑁 ∈ ℤ → (𝑀 ≤ 𝐿 → (𝐿 ≤ 𝑁 → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))))) |
34 | 33 | com23 86 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝑀 ≤ 𝐿 → (𝑁 ∈ ℤ → (𝐿 ≤ 𝑁 → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))))) |
35 | 34 | 3impia 1119 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → (𝑁 ∈ ℤ → (𝐿 ≤ 𝑁 → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)))) |
36 | 35 | com13 88 |
. . . . . . . . . 10
⊢ (𝐿 ≤ 𝑁 → (𝑁 ∈ ℤ → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)))) |
37 | 36 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋) → (𝑁 ∈ ℤ → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)))) |
38 | 37 | com12 32 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → ((𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)))) |
39 | 38 | 3ad2ant3 1137 |
. . . . . . 7
⊢ ((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)))) |
40 | 39 | imp 410 |
. . . . . 6
⊢ (((𝐿 ∈ ℤ ∧ 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿 ≤ 𝑁 ∧ 𝑁 ≤ 𝑋)) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) |
41 | 2, 40 | sylbi 220 |
. . . . 5
⊢ (𝑁 ∈ (𝐿...𝑋) → ((𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝑀 ≤ 𝐿) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) |
42 | 41 | com12 32 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0 ∧ 𝑀
≤ 𝐿) → (𝑁 ∈ (𝐿...𝑋) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) |
43 | 1, 42 | sylbi 220 |
. . 3
⊢ (𝑀 ∈ (0...𝐿) → (𝑁 ∈ (𝐿...𝑋) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) |
44 | 43 | imp 410 |
. 2
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
45 | | elfz2nn0 13216 |
. 2
⊢ (𝑀 ∈ (0...𝑁) ↔ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
46 | 44, 45 | sylibr 237 |
1
⊢ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...𝑋)) → 𝑀 ∈ (0...𝑁)) |