(7steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
factors
smaller2
1
1
1.
k
:
2.
i
: {2..
k
}
3.
j
:
4.
i
j
=
k
2
j
By:
FwdThru:
Thm*
a
,
b
:
.
a
b
>0
a
>0 &
b
>0
a
<0 &
b
<0 on [ 0<
i
j
]
THEN
Analyze-1
Generated subgoal:
1
5.
i
>0
6.
j
>0
2
j
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
}
j = k
2
j
}
j = k
2j
a,b:. ab>0 
a>0 & b>0 
a<0 & b<0 on [ 0<ij ]
2j
