Proof of Theorem el1fzopredsuc
Step | Hyp | Ref
| Expression |
1 | | elfzelz 12213 |
. . 3
⊢ (𝐼 ∈ (0...𝑁) → 𝐼 ∈ ℤ) |
2 | | 1fzopredsuc 39947 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (0...𝑁) = (({0}
∪ (1..^𝑁)) ∪ {𝑁})) |
3 | 2 | eleq2d 2673 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ (0...𝑁) ↔ 𝐼 ∈ (({0} ∪ (1..^𝑁)) ∪ {𝑁}))) |
4 | | elun 3715 |
. . . . . . . . 9
⊢ (𝐼 ∈ (({0} ∪ (1..^𝑁)) ∪ {𝑁}) ↔ (𝐼 ∈ ({0} ∪ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁})) |
5 | | elun 3715 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ({0} ∪ (1..^𝑁)) ↔ (𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁))) |
6 | 5 | orbi1i 541 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ({0} ∪ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁}) ↔ ((𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁})) |
7 | 4, 6 | bitri 263 |
. . . . . . . 8
⊢ (𝐼 ∈ (({0} ∪ (1..^𝑁)) ∪ {𝑁}) ↔ ((𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁})) |
8 | | elsng 4139 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ ℤ → (𝐼 ∈ {0} ↔ 𝐼 = 0)) |
9 | 8 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝐼 ∈ ℤ)
→ (𝐼 ∈ {0} ↔
𝐼 = 0)) |
10 | 9 | orbi1d 735 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐼 ∈ ℤ)
→ ((𝐼 ∈ {0} ∨
𝐼 ∈ (1..^𝑁)) ↔ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁)))) |
11 | | elsng 4139 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ℤ → (𝐼 ∈ {𝑁} ↔ 𝐼 = 𝑁)) |
12 | 11 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐼 ∈ ℤ)
→ (𝐼 ∈ {𝑁} ↔ 𝐼 = 𝑁)) |
13 | 10, 12 | orbi12d 742 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐼 ∈ ℤ)
→ (((𝐼 ∈ {0} ∨
𝐼 ∈ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁}) ↔ ((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 = 𝑁))) |
14 | 7, 13 | syl5bb 271 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐼 ∈ ℤ)
→ (𝐼 ∈ (({0}
∪ (1..^𝑁)) ∪ {𝑁}) ↔ ((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 = 𝑁))) |
15 | | df-3or 1032 |
. . . . . . . 8
⊢ ((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁) ↔ ((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 = 𝑁)) |
16 | 15 | biimpri 217 |
. . . . . . 7
⊢ (((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 = 𝑁) → (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)) |
17 | 14, 16 | syl6bi 242 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐼 ∈ ℤ)
→ (𝐼 ∈ (({0}
∪ (1..^𝑁)) ∪ {𝑁}) → (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁))) |
18 | 17 | ex 449 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ ℤ
→ (𝐼 ∈ (({0}
∪ (1..^𝑁)) ∪ {𝑁}) → (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)))) |
19 | 18 | com23 84 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ (({0}
∪ (1..^𝑁)) ∪ {𝑁}) → (𝐼 ∈ ℤ → (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)))) |
20 | 3, 19 | sylbid 229 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ (0...𝑁) → (𝐼 ∈ ℤ → (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)))) |
21 | 1, 20 | mpdi 44 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ (0...𝑁) → (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁))) |
22 | | c0ex 9913 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
23 | 22 | snid 4155 |
. . . . . . . . . . 11
⊢ 0 ∈
{0} |
24 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐼 = 0 → 0 ∈
{0}) |
25 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝐼 = 0 → (𝐼 ∈ {0} ↔ 0 ∈
{0})) |
26 | 24, 25 | mpbird 246 |
. . . . . . . . 9
⊢ (𝐼 = 0 → 𝐼 ∈ {0}) |
27 | 26 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝐼 = 0 → 𝐼 ∈ {0})) |
28 | | idd 24 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ (1..^𝑁) → 𝐼 ∈ (1..^𝑁))) |
29 | | snidg 4153 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ {𝑁}) |
30 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝐼 = 𝑁 → (𝐼 ∈ {𝑁} ↔ 𝑁 ∈ {𝑁})) |
31 | 29, 30 | syl5ibrcom 236 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝐼 = 𝑁 → 𝐼 ∈ {𝑁})) |
32 | 27, 28, 31 | 3orim123d 1399 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁) → (𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 ∈ {𝑁}))) |
33 | 32 | imp 444 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)) → (𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 ∈ {𝑁})) |
34 | | df-3or 1032 |
. . . . . 6
⊢ ((𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 ∈ {𝑁}) ↔ ((𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁})) |
35 | 33, 34 | sylib 207 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)) → ((𝐼 ∈ {0} ∨ 𝐼 ∈ (1..^𝑁)) ∨ 𝐼 ∈ {𝑁})) |
36 | 35, 7 | sylibr 223 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)) → 𝐼 ∈ (({0} ∪ (1..^𝑁)) ∪ {𝑁})) |
37 | 3 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)) → (𝐼 ∈ (0...𝑁) ↔ 𝐼 ∈ (({0} ∪ (1..^𝑁)) ∪ {𝑁}))) |
38 | 36, 37 | mpbird 246 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)) → 𝐼 ∈ (0...𝑁)) |
39 | 38 | ex 449 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁) → 𝐼 ∈ (0...𝑁))) |
40 | 21, 39 | impbid 201 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝐼 ∈ (0...𝑁) ↔ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁))) |