Proof of Theorem elfzo0
Step | Hyp | Ref
| Expression |
1 | | elfzouz 13720 |
. . . 4
⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 ∈
(ℤ≥‘0)) |
2 | | elnn0uz 12948 |
. . . 4
⊢ (𝐴 ∈ ℕ0
↔ 𝐴 ∈
(ℤ≥‘0)) |
3 | 1, 2 | sylibr 234 |
. . 3
⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 ∈
ℕ0) |
4 | | elfzolt3b 13728 |
. . . 4
⊢ (𝐴 ∈ (0..^𝐵) → 0 ∈ (0..^𝐵)) |
5 | | lbfzo0 13756 |
. . . 4
⊢ (0 ∈
(0..^𝐵) ↔ 𝐵 ∈
ℕ) |
6 | 4, 5 | sylib 218 |
. . 3
⊢ (𝐴 ∈ (0..^𝐵) → 𝐵 ∈ ℕ) |
7 | | elfzolt2 13725 |
. . 3
⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 < 𝐵) |
8 | 3, 6, 7 | 3jca 1128 |
. 2
⊢ (𝐴 ∈ (0..^𝐵) → (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵)) |
9 | | simp1 1136 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐴 ∈
ℕ0) |
10 | 9, 2 | sylib 218 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐴 ∈
(ℤ≥‘0)) |
11 | | nnz 12660 |
. . . 4
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℤ) |
12 | 11 | 3ad2ant2 1134 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐵 ∈ ℤ) |
13 | | simp3 1138 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) |
14 | | elfzo2 13719 |
. . 3
⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ (ℤ≥‘0)
∧ 𝐵 ∈ ℤ
∧ 𝐴 < 𝐵)) |
15 | 10, 12, 13, 14 | syl3anbrc 1343 |
. 2
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐴 ∈ (0..^𝐵)) |
16 | 8, 15 | impbii 209 |
1
⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵)) |