Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fzofzp1 | Structured version Visualization version Unicode version |
Description: If a point is in a half-open range, the next point is in the closed range. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
Ref | Expression |
---|---|
fzofzp1 | ..^ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzoel1 12468 | . . . 4 ..^ | |
2 | uzid 11702 | . . . 4 | |
3 | peano2uz 11741 | . . . 4 | |
4 | fzoss1 12495 | . . . 4 ..^ ..^ | |
5 | 1, 2, 3, 4 | 4syl 19 | . . 3 ..^ ..^ ..^ |
6 | 1z 11407 | . . . 4 | |
7 | fzoaddel 12520 | . . . 4 ..^ ..^ | |
8 | 6, 7 | mpan2 707 | . . 3 ..^ ..^ |
9 | 5, 8 | sseldd 3604 | . 2 ..^ ..^ |
10 | elfzoel2 12469 | . . 3 ..^ | |
11 | fzval3 12536 | . . 3 ..^ | |
12 | 10, 11 | syl 17 | . 2 ..^ ..^ |
13 | 9, 12 | eleqtrrd 2704 | 1 ..^ |
Copyright terms: Public domain | W3C validator |