Proof of Theorem fzo1fzo0n0
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfzo2 13703 | . . 3
⊢ (𝐾 ∈ (1..^𝑁) ↔ (𝐾 ∈ (ℤ≥‘1)
∧ 𝑁 ∈ ℤ
∧ 𝐾 < 𝑁)) | 
| 2 |  | elnnuz 12923 | . . . . . . 7
⊢ (𝐾 ∈ ℕ ↔ 𝐾 ∈
(ℤ≥‘1)) | 
| 3 |  | nnnn0 12535 | . . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) | 
| 4 | 3 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 𝐾 ∈
ℕ0) | 
| 5 | 4 | adantr 480 | . . . . . . . . 9
⊢ (((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝑁) → 𝐾 ∈
ℕ0) | 
| 6 |  | nngt0 12298 | . . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ → 0 <
𝐾) | 
| 7 |  | 0red 11265 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → 0 ∈
ℝ) | 
| 8 |  | nnre 12274 | . . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℝ) | 
| 9 | 8 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → 𝐾 ∈
ℝ) | 
| 10 |  | zre 12619 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) | 
| 11 | 10 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → 𝑁 ∈
ℝ) | 
| 12 |  | lttr 11338 | . . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ 𝐾
∈ ℝ ∧ 𝑁
∈ ℝ) → ((0 < 𝐾 ∧ 𝐾 < 𝑁) → 0 < 𝑁)) | 
| 13 | 7, 9, 11, 12 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → ((0 <
𝐾 ∧ 𝐾 < 𝑁) → 0 < 𝑁)) | 
| 14 |  | elnnz 12625 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 <
𝑁)) | 
| 15 | 14 | simplbi2 500 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → (0 <
𝑁 → 𝑁 ∈ ℕ)) | 
| 16 | 15 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → (0 <
𝑁 → 𝑁 ∈ ℕ)) | 
| 17 | 13, 16 | syld 47 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ) → ((0 <
𝐾 ∧ 𝐾 < 𝑁) → 𝑁 ∈ ℕ)) | 
| 18 | 17 | exp4b 430 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝐾 ∈ ℕ → (0 <
𝐾 → (𝐾 < 𝑁 → 𝑁 ∈ ℕ)))) | 
| 19 | 18 | com13 88 | . . . . . . . . . . 11
⊢ (0 <
𝐾 → (𝐾 ∈ ℕ → (𝑁 ∈ ℤ → (𝐾 < 𝑁 → 𝑁 ∈ ℕ)))) | 
| 20 | 6, 19 | mpcom 38 | . . . . . . . . . 10
⊢ (𝐾 ∈ ℕ → (𝑁 ∈ ℤ → (𝐾 < 𝑁 → 𝑁 ∈ ℕ))) | 
| 21 | 20 | imp31 417 | . . . . . . . . 9
⊢ (((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝑁) → 𝑁 ∈ ℕ) | 
| 22 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝑁) → 𝐾 < 𝑁) | 
| 23 | 5, 21, 22 | 3jca 1128 | . . . . . . . 8
⊢ (((𝐾 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 < 𝑁) → (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) | 
| 24 | 23 | exp31 419 | . . . . . . 7
⊢ (𝐾 ∈ ℕ → (𝑁 ∈ ℤ → (𝐾 < 𝑁 → (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)))) | 
| 25 | 2, 24 | sylbir 235 | . . . . . 6
⊢ (𝐾 ∈
(ℤ≥‘1) → (𝑁 ∈ ℤ → (𝐾 < 𝑁 → (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)))) | 
| 26 | 25 | 3imp 1110 | . . . . 5
⊢ ((𝐾 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁) → (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) | 
| 27 |  | elfzo0 13741 | . . . . 5
⊢ (𝐾 ∈ (0..^𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝐾 < 𝑁)) | 
| 28 | 26, 27 | sylibr 234 | . . . 4
⊢ ((𝐾 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁) → 𝐾 ∈ (0..^𝑁)) | 
| 29 |  | nnne0 12301 | . . . . . 6
⊢ (𝐾 ∈ ℕ → 𝐾 ≠ 0) | 
| 30 | 2, 29 | sylbir 235 | . . . . 5
⊢ (𝐾 ∈
(ℤ≥‘1) → 𝐾 ≠ 0) | 
| 31 | 30 | 3ad2ant1 1133 | . . . 4
⊢ ((𝐾 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁) → 𝐾 ≠ 0) | 
| 32 | 28, 31 | jca 511 | . . 3
⊢ ((𝐾 ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁) → (𝐾 ∈ (0..^𝑁) ∧ 𝐾 ≠ 0)) | 
| 33 | 1, 32 | sylbi 217 | . 2
⊢ (𝐾 ∈ (1..^𝑁) → (𝐾 ∈ (0..^𝑁) ∧ 𝐾 ≠ 0)) | 
| 34 |  | elnnne0 12542 | . . . . . 6
⊢ (𝐾 ∈ ℕ ↔ (𝐾 ∈ ℕ0
∧ 𝐾 ≠
0)) | 
| 35 |  | nnge1 12295 | . . . . . 6
⊢ (𝐾 ∈ ℕ → 1 ≤
𝐾) | 
| 36 | 34, 35 | sylbir 235 | . . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝐾 ≠ 0) → 1
≤ 𝐾) | 
| 37 | 36 | 3ad2antl1 1185 | . . . 4
⊢ (((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) ∧ 𝐾 ≠ 0) → 1 ≤ 𝐾) | 
| 38 |  | simpl3 1193 | . . . 4
⊢ (((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) ∧ 𝐾 ≠ 0) → 𝐾 < 𝑁) | 
| 39 |  | nn0z 12640 | . . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) | 
| 40 | 39 | adantr 480 | . . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝐾 ∈
ℤ) | 
| 41 |  | 1zzd 12650 | . . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 1 ∈ ℤ) | 
| 42 |  | nnz 12636 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) | 
| 43 | 42 | adantl 481 | . . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ 𝑁 ∈
ℤ) | 
| 44 | 40, 41, 43 | 3jca 1128 | . . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝐾 ∈ ℤ
∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ)) | 
| 45 | 44 | 3adant3 1132 | . . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) → (𝐾 ∈ ℤ ∧ 1 ∈ ℤ ∧
𝑁 ∈
ℤ)) | 
| 46 | 45 | adantr 480 | . . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝐾 < 𝑁) ∧ 𝐾 ≠ 0) → (𝐾 ∈ ℤ ∧ 1 ∈ ℤ ∧
𝑁 ∈
ℤ)) | 
| 47 |  | elfzo 13702 | . . . . 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 581 | . 2
⊢ ((𝐾 ∈ (0..^𝑁) ∧ 𝐾 ≠ 0) → 𝐾 ∈ (1..^𝑁)) | 
| 51 | 33, 50 | impbii 209 | 1
⊢ (𝐾 ∈ (1..^𝑁) ↔ (𝐾 ∈ (0..^𝑁) ∧ 𝐾 ≠ 0)) |