Proof of Theorem elfzo0
Step | Hyp | Ref
| Expression |
1 | | elfzouz 12474 |
. . . 4
⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 ∈
(ℤ≥‘0)) |
2 | | elnn0uz 11725 |
. . . 4
⊢ (𝐴 ∈ ℕ0
↔ 𝐴 ∈
(ℤ≥‘0)) |
3 | 1, 2 | sylibr 224 |
. . 3
⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 ∈
ℕ0) |
4 | | elfzolt3b 12482 |
. . . 4
⊢ (𝐴 ∈ (0..^𝐵) → 0 ∈ (0..^𝐵)) |
5 | | lbfzo0 12507 |
. . . 4
⊢ (0 ∈
(0..^𝐵) ↔ 𝐵 ∈
ℕ) |
6 | 4, 5 | sylib 208 |
. . 3
⊢ (𝐴 ∈ (0..^𝐵) → 𝐵 ∈ ℕ) |
7 | | elfzolt2 12479 |
. . 3
⊢ (𝐴 ∈ (0..^𝐵) → 𝐴 < 𝐵) |
8 | 3, 6, 7 | 3jca 1242 |
. 2
⊢ (𝐴 ∈ (0..^𝐵) → (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵)) |
9 | | simp1 1061 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐴 ∈
ℕ0) |
10 | 9, 2 | sylib 208 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐴 ∈
(ℤ≥‘0)) |
11 | | nnz 11399 |
. . . 4
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℤ) |
12 | 11 | 3ad2ant2 1083 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐵 ∈ ℤ) |
13 | | simp3 1063 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) |
14 | | elfzo2 12473 |
. . 3
⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ (ℤ≥‘0)
∧ 𝐵 ∈ ℤ
∧ 𝐴 < 𝐵)) |
15 | 10, 12, 13, 14 | syl3anbrc 1246 |
. 2
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ
∧ 𝐴 < 𝐵) → 𝐴 ∈ (0..^𝐵)) |
16 | 8, 15 | impbii 199 |
1
⊢ (𝐴 ∈ (0..^𝐵) ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵)) |