Proof of Theorem el1fzopredsuc
| Step | Hyp | Ref
| Expression |
| 1 | | elfzelz 13564 |
. . 3
⊢ (𝐼 ∈ (0...𝑁) → 𝐼 ∈ ℤ) |
| 2 | | 1fzopredsuc 47336 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (0...𝑁) = (({0}
∪ (1..^𝑁)) ∪ {𝑁})) |
| 3 | 2 | eleq2d 2827 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ (0...𝑁) ↔ 𝐼 ∈ (({0} ∪ (1..^𝑁)) ∪ {𝑁}))) |
| 4 | | elun 4153 |
. . . . . . . . 9
⊢ (𝐼 ∈ (({0} ∪ (1..^𝑁)) ∪ {𝑁}) ↔ (𝐼 ∈ ({0} ∪ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁})) |
| 5 | | elun 4153 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ({0} ∪ (1..^𝑁)) ↔ (𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁))) |
| 6 | 5 | orbi1i 914 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ({0} ∪ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁}) ↔ ((𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁})) |
| 7 | 4, 6 | bitri 275 |
. . . . . . . 8
⊢ (𝐼 ∈ (({0} ∪ (1..^𝑁)) ∪ {𝑁}) ↔ ((𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁})) |
| 8 | | elsng 4640 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ ℤ → (𝐼 ∈ {0} ↔ 𝐼 = 0)) |
| 9 | 8 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝐼 ∈ ℤ)
→ (𝐼 ∈ {0} ↔
𝐼 = 0)) |
| 10 | 9 | orbi1d 917 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐼 ∈ ℤ)
→ ((𝐼 ∈ {0} ∨
𝐼 ∈ (1..^𝑁)) ↔ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁)))) |
| 11 | | elsng 4640 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ℤ → (𝐼 ∈ {𝑁} ↔ 𝐼 = 𝑁)) |
| 12 | 11 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐼 ∈ ℤ)
→ (𝐼 ∈ {𝑁} ↔ 𝐼 = 𝑁)) |
| 13 | 10, 12 | orbi12d 919 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐼 ∈ ℤ)
→ (((𝐼 ∈ {0} ∨
𝐼 ∈ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁}) ↔ ((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 = 𝑁))) |
| 14 | 7, 13 | bitrid 283 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐼 ∈ ℤ)
→ (𝐼 ∈ (({0}
∪ (1..^𝑁)) ∪ {𝑁}) ↔ ((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 = 𝑁))) |
| 15 | | df-3or 1088 |
. . . . . . . 8
⊢ ((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁) ↔ ((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 = 𝑁)) |
| 16 | 15 | biimpri 228 |
. . . . . . 7
⊢ (((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 = 𝑁) → (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)) |
| 17 | 14, 16 | biimtrdi 253 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐼 ∈ ℤ)
→ (𝐼 ∈ (({0}
∪ (1..^𝑁)) ∪ {𝑁}) → (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁))) |
| 18 | 17 | ex 412 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ ℤ
→ (𝐼 ∈ (({0}
∪ (1..^𝑁)) ∪ {𝑁}) → (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)))) |
| 19 | 18 | com23 86 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ (({0}
∪ (1..^𝑁)) ∪ {𝑁}) → (𝐼 ∈ ℤ → (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)))) |
| 20 | 3, 19 | sylbid 240 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ (0...𝑁) → (𝐼 ∈ ℤ → (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)))) |
| 21 | 1, 20 | mpdi 45 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ (0...𝑁) → (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁))) |
| 22 | | c0ex 11255 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
| 23 | 22 | snid 4662 |
. . . . . . . . . . 11
⊢ 0 ∈
{0} |
| 24 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐼 = 0 → 0 ∈
{0}) |
| 25 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝐼 = 0 → (𝐼 ∈ {0} ↔ 0 ∈
{0})) |
| 26 | 24, 25 | mpbird 257 |
. . . . . . . . 9
⊢ (𝐼 = 0 → 𝐼 ∈ {0}) |
| 27 | 26 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝐼 = 0 → 𝐼 ∈ {0})) |
| 28 | | idd 24 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ (1..^𝑁) → 𝐼 ∈ (1..^𝑁))) |
| 29 | | snidg 4660 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ {𝑁}) |
| 30 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝐼 = 𝑁 → (𝐼 ∈ {𝑁} ↔ 𝑁 ∈ {𝑁})) |
| 31 | 29, 30 | syl5ibrcom 247 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝐼 = 𝑁 → 𝐼 ∈ {𝑁})) |
| 32 | 27, 28, 31 | 3orim123d 1446 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁) → (𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 ∈ {𝑁}))) |
| 33 | 32 | imp 406 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)) → (𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 ∈ {𝑁})) |
| 34 | | df-3or 1088 |
. . . . . 6
⊢ ((𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 ∈ {𝑁}) ↔ ((𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁})) |
| 35 | 33, 34 | sylib 218 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)) → ((𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁})) |
| 36 | 35, 7 | sylibr 234 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)) → 𝐼 ∈ (({0} ∪ (1..^𝑁)) ∪ {𝑁})) |
| 37 | 3 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)) → (𝐼 ∈ (0...𝑁) ↔ 𝐼 ∈ (({0} ∪ (1..^𝑁)) ∪ {𝑁}))) |
| 38 | 36, 37 | mpbird 257 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)) → 𝐼 ∈ (0...𝑁)) |
| 39 | 38 | ex 412 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁) → 𝐼 ∈ (0...𝑁))) |
| 40 | 21, 39 | impbid 212 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ (0...𝑁) ↔ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁))) |