Description: Lemma for logcn . (Contributed by Mario Carneiro, 25-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | logcn.d | |
|
logcnlem.s | |
||
logcnlem.t | |
||
logcnlem.a | |
||
logcnlem.r | |
||
logcnlem.b | |
||
logcnlem.l | |
||
Assertion | logcnlem4 | |