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