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