Description: If there is a partition, then all intermediate points and the upper bound are strictly greater than the lower bound. (Contributed by AV, 14-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | iccpartgtprec.m | |
|
iccpartgtprec.p | |
||
Assertion | iccpartgtl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iccpartgtprec.m | |
|
2 | iccpartgtprec.p | |
|
3 | elnnuz | |
|
4 | 1 3 | sylib | |
5 | fzisfzounsn | |
|
6 | 4 5 | syl | |
7 | 6 | eleq2d | |
8 | elun | |
|
9 | 8 | a1i | |
10 | velsn | |
|
11 | 10 | a1i | |
12 | 11 | orbi2d | |
13 | 7 9 12 | 3bitrd | |
14 | fveq2 | |
|
15 | 14 | breq2d | |
16 | 15 | rspccv | |
17 | 1 2 | iccpartigtl | |
18 | 16 17 | syl11 | |
19 | 1 2 | iccpartlt | |
20 | 19 | adantl | |
21 | fveq2 | |
|
22 | 21 | adantr | |
23 | 20 22 | breqtrrd | |
24 | 23 | ex | |
25 | 18 24 | jaoi | |
26 | 25 | com12 | |
27 | 13 26 | sylbid | |
28 | 27 | ralrimiv | |