Proof of Theorem elfzo0
| Step | Hyp | Ref
| Expression |
| 1 | | elfzouz 13703 |
. . . 4
⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 ∈
(ℤ≥‘0)) |
| 2 | | elnn0uz 12923 |
. . . 4
⊢ (𝐴 ∈ ℕ0
↔ 𝐴 ∈
(ℤ≥‘0)) |
| 3 | 1, 2 | sylibr 234 |
. . 3
⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 ∈
ℕ0) |
| 4 | | elfzolt3b 13711 |
. . . 4
⊢ (𝐴 ∈ (0..^𝐵) → 0 ∈ (0..^𝐵)) |
| 5 | | lbfzo0 13739 |
. . . 4
⊢ (0 ∈
(0..^𝐵) ↔ 𝐵 ∈
ℕ) |
| 6 | 4, 5 | sylib 218 |
. . 3
⊢ (𝐴 ∈ (0..^𝐵) → 𝐵 ∈ ℕ) |
| 7 | | elfzolt2 13708 |
. . 3
⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 < 𝐵) |
| 8 | 3, 6, 7 | 3jca 1129 |
. 2
⊢ (𝐴 ∈ (0..^𝐵) → (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵)) |
| 9 | | simp1 1137 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐴 ∈
ℕ0) |
| 10 | 9, 2 | sylib 218 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐴 ∈
(ℤ≥‘0)) |
| 11 | | nnz 12634 |
. . . 4
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℤ) |
| 12 | 11 | 3ad2ant2 1135 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐵 ∈ ℤ) |
| 13 | | simp3 1139 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) |
| 14 | | elfzo2 13702 |
. . 3
⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ (ℤ≥‘0)
∧ 𝐵 ∈ ℤ
∧ 𝐴 < 𝐵)) |
| 15 | 10, 12, 13, 14 | syl3anbrc 1344 |
. 2
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐴 ∈ (0..^𝐵)) |
| 16 | 8, 15 | impbii 209 |
1
⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵)) |