Metamath Proof Explorer

Theorem el1fzopredsuc

Description: An element of an open integer interval starting at 1 joined by 0 and a successor at the beginning and the end is either 0 or an element of the open integer interval or the successor. (Contributed by AV, 14-Jul-2020)

Ref Expression
Assertion el1fzopredsuc ⊢ N ∈ ℕ 0 → I ∈ 0 … N ↔ I = 0 ∨ I ∈ 1 ..^ N ∨ I = N

Proof

Step Hyp Ref Expression
1 elfzelz ⊢ I ∈ 0 … N → I ∈ ℤ
2 1fzopredsuc ⊢ N ∈ ℕ 0 → 0 … N = 0 ∪ 1 ..^ N ∪ N
3 2 eleq2d ⊢ N ∈ ℕ 0 → I ∈ 0 … N ↔ I ∈ 0 ∪ 1 ..^ N ∪ N
4 elun ⊢ I ∈ 0 ∪ 1 ..^ N ∪ N ↔ I ∈ 0 ∪ 1 ..^ N ∨ I ∈ N
5 elun ⊢ I ∈ 0 ∪ 1 ..^ N ↔ I ∈ 0 ∨ I ∈ 1 ..^ N
6 5 orbi1i ⊢ I ∈ 0 ∪ 1 ..^ N ∨ I ∈ N ↔ I ∈ 0 ∨ I ∈ 1 ..^ N ∨ I ∈ N
7 4 6 bitri ⊢ I ∈ 0 ∪ 1 ..^ N ∪ N ↔ I ∈ 0 ∨ I ∈ 1 ..^ N ∨ I ∈ N
8 elsng ⊢ I ∈ ℤ → I ∈ 0 ↔ I = 0
9 8 adantl ⊢ N ∈ ℕ 0 ∧ I ∈ ℤ → I ∈ 0 ↔ I = 0
10 9 orbi1d ⊢ N ∈ ℕ 0 ∧ I ∈ ℤ → I ∈ 0 ∨ I ∈ 1 ..^ N ↔ I = 0 ∨ I ∈ 1 ..^ N
11 elsng ⊢ I ∈ ℤ → I ∈ N ↔ I = N
12 11 adantl ⊢ N ∈ ℕ 0 ∧ I ∈ ℤ → I ∈ N ↔ I = N
13 10 12 orbi12d ⊢ N ∈ ℕ 0 ∧ I ∈ ℤ → I ∈ 0 ∨ I ∈ 1 ..^ N ∨ I ∈ N ↔ I = 0 ∨ I ∈ 1 ..^ N ∨ I = N
14 7 13 syl5bb ⊢ N ∈ ℕ 0 ∧ I ∈ ℤ → I ∈ 0 ∪ 1 ..^ N ∪ N ↔ I = 0 ∨ I ∈ 1 ..^ N ∨ I = N
15 df-3or ⊢ I = 0 ∨ I ∈ 1 ..^ N ∨ I = N ↔ I = 0 ∨ I ∈ 1 ..^ N ∨ I = N
16 15 biimpri ⊢ I = 0 ∨ I ∈ 1 ..^ N ∨ I = N → I = 0 ∨ I ∈ 1 ..^ N ∨ I = N
17 14 16 syl6bi ⊢ N ∈ ℕ 0 ∧ I ∈ ℤ → I ∈ 0 ∪ 1 ..^ N ∪ N → I = 0 ∨ I ∈ 1 ..^ N ∨ I = N
18 17 ex ⊢ N ∈ ℕ 0 → I ∈ ℤ → I ∈ 0 ∪ 1 ..^ N ∪ N → I = 0 ∨ I ∈ 1 ..^ N ∨ I = N
19 18 com23 ⊢ N ∈ ℕ 0 → I ∈ 0 ∪ 1 ..^ N ∪ N → I ∈ ℤ → I = 0 ∨ I ∈ 1 ..^ N ∨ I = N
20 3 19 sylbid ⊢ N ∈ ℕ 0 → I ∈ 0 … N → I ∈ ℤ → I = 0 ∨ I ∈ 1 ..^ N ∨ I = N
21 1 20 mpdi ⊢ N ∈ ℕ 0 → I ∈ 0 … N → I = 0 ∨ I ∈ 1 ..^ N ∨ I = N
22 c0ex ⊢ 0 ∈ V
23 22 snid ⊢ 0 ∈ 0
24 23 a1i ⊢ I = 0 → 0 ∈ 0
25 eleq1 ⊢ I = 0 → I ∈ 0 ↔ 0 ∈ 0
26 24 25 mpbird ⊢ I = 0 → I ∈ 0
27 26 a1i ⊢ N ∈ ℕ 0 → I = 0 → I ∈ 0
28 idd ⊢ N ∈ ℕ 0 → I ∈ 1 ..^ N → I ∈ 1 ..^ N
29 snidg ⊢ N ∈ ℕ 0 → N ∈ N
30 eleq1 ⊢ I = N → I ∈ N ↔ N ∈ N
31 29 30 syl5ibrcom ⊢ N ∈ ℕ 0 → I = N → I ∈ N
32 27 28 31 3orim123d ⊢ N ∈ ℕ 0 → I = 0 ∨ I ∈ 1 ..^ N ∨ I = N → I ∈ 0 ∨ I ∈ 1 ..^ N ∨ I ∈ N
33 32 imp ⊢ N ∈ ℕ 0 ∧ I = 0 ∨ I ∈ 1 ..^ N ∨ I = N → I ∈ 0 ∨ I ∈ 1 ..^ N ∨ I ∈ N
34 df-3or ⊢ I ∈ 0 ∨ I ∈ 1 ..^ N ∨ I ∈ N ↔ I ∈ 0 ∨ I ∈ 1 ..^ N ∨ I ∈ N
35 33 34 sylib ⊢ N ∈ ℕ 0 ∧ I = 0 ∨ I ∈ 1 ..^ N ∨ I = N → I ∈ 0 ∨ I ∈ 1 ..^ N ∨ I ∈ N
36 35 7 sylibr ⊢ N ∈ ℕ 0 ∧ I = 0 ∨ I ∈ 1 ..^ N ∨ I = N → I ∈ 0 ∪ 1 ..^ N ∪ N
37 3 adantr ⊢ N ∈ ℕ 0 ∧ I = 0 ∨ I ∈ 1 ..^ N ∨ I = N → I ∈ 0 … N ↔ I ∈ 0 ∪ 1 ..^ N ∪ N
38 36 37 mpbird ⊢ N ∈ ℕ 0 ∧ I = 0 ∨ I ∈ 1 ..^ N ∨ I = N → I ∈ 0 … N
39 38 ex ⊢ N ∈ ℕ 0 → I = 0 ∨ I ∈ 1 ..^ N ∨ I = N → I ∈ 0 … N
40 21 39 impbid ⊢ N ∈ ℕ 0 → I ∈ 0 … N ↔ I = 0 ∨ I ∈ 1 ..^ N ∨ I = N