Metamath Proof Explorer

Theorem fzostep1

Description: Two possibilities for a number one greater than a number in a half-open range. (Contributed by Stefan O'Rear, 23-Aug-2015)

Ref Expression
Assertion fzostep1 ⊢ A ∈ B ..^ C → A + 1 ∈ B ..^ C ∨ A + 1 = C

Proof

Step Hyp Ref Expression
1 elfzoel1 ⊢ A ∈ B ..^ C → B ∈ ℤ
2 uzid ⊢ B ∈ ℤ → B ∈ ℤ ≥ B
3 peano2uz ⊢ B ∈ ℤ ≥ B → B + 1 ∈ ℤ ≥ B
4 fzoss1 ⊢ B + 1 ∈ ℤ ≥ B → B + 1 ..^ C + 1 ⊆ B ..^ C + 1
5 1 2 3 4 4syl ⊢ A ∈ B ..^ C → B + 1 ..^ C + 1 ⊆ B ..^ C + 1
6 1z ⊢ 1 ∈ ℤ
7 fzoaddel ⊢ A ∈ B ..^ C ∧ 1 ∈ ℤ → A + 1 ∈ B + 1 ..^ C + 1
8 6 7 mpan2 ⊢ A ∈ B ..^ C → A + 1 ∈ B + 1 ..^ C + 1
9 5 8 sseldd ⊢ A ∈ B ..^ C → A + 1 ∈ B ..^ C + 1
10 elfzoel2 ⊢ A ∈ B ..^ C → C ∈ ℤ
11 elfzolt3 ⊢ A ∈ B ..^ C → B < C
12 zre ⊢ B ∈ ℤ → B ∈ ℝ
13 zre ⊢ C ∈ ℤ → C ∈ ℝ
14 ltle ⊢ B ∈ ℝ ∧ C ∈ ℝ → B < C → B ≤ C
15 12 13 14 syl2an ⊢ B ∈ ℤ ∧ C ∈ ℤ → B < C → B ≤ C
16 1 10 15 syl2anc ⊢ A ∈ B ..^ C → B < C → B ≤ C
17 11 16 mpd ⊢ A ∈ B ..^ C → B ≤ C
18 eluz2 ⊢ C ∈ ℤ ≥ B ↔ B ∈ ℤ ∧ C ∈ ℤ ∧ B ≤ C
19 1 10 17 18 syl3anbrc ⊢ A ∈ B ..^ C → C ∈ ℤ ≥ B
20 fzosplitsni ⊢ C ∈ ℤ ≥ B → A + 1 ∈ B ..^ C + 1 ↔ A + 1 ∈ B ..^ C ∨ A + 1 = C
21 19 20 syl ⊢ A ∈ B ..^ C → A + 1 ∈ B ..^ C + 1 ↔ A + 1 ∈ B ..^ C ∨ A + 1 = C
22 9 21 mpbid ⊢ A ∈ B ..^ C → A + 1 ∈ B ..^ C ∨ A + 1 = C