Description: Lemma for unbnn . The value of the function F is less than its value at a successor. (Contributed by NM, 3-Dec-2003)
Ref | Expression | ||
---|---|---|---|
Hypothesis | unblem.2 | |
|
Assertion | unblem3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unblem.2 | |
|
2 | 1 | unblem2 | |
3 | 2 | imp | |
4 | omsson | |
|
5 | sstr | |
|
6 | 4 5 | mpan2 | |
7 | ssel | |
|
8 | 7 | anc2li | |
9 | 6 8 | syl | |
10 | 9 | ad2antrr | |
11 | 3 10 | mpd | |
12 | onmindif | |
|
13 | 11 12 | syl | |
14 | unblem1 | |
|
15 | 14 | ex | |
16 | 2 15 | syld | |
17 | suceq | |
|
18 | 17 | difeq2d | |
19 | 18 | inteqd | |
20 | suceq | |
|
21 | 20 | difeq2d | |
22 | 21 | inteqd | |
23 | 1 19 22 | frsucmpt2 | |
24 | 23 | ex | |
25 | 16 24 | sylcom | |
26 | 25 | imp | |
27 | 13 26 | eleqtrrd | |
28 | 27 | ex | |