Nuprl - Proof: increasing le 1 2 1

(11steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: increasing le 1 2 1

1. k :

2. 0<k
3.

m:

. (

f:(

(k-1)

m). increasing(f;k-1))

k-1

m
4. m :

5. f :

k

m
6. increasing(f;k)
7. i :

(k-1)

f(i+1)-f(1)

(m-1)

By:	FwdThru Thm* k:, f:(k). increasing(f;k) (x,y:k. x<y f(x)<f(y)) [-2] THEN InstHyp [0;1] -1

Generated subgoal:

1 8. x,y:k. x<y f(x)<f(y)
9. f(0)<f(1)
f(i+1)-f(1) (m-1)
3 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(11steps total) PrintForm Definitions Lemmas mb nat Sections MarkB generic Doc