Hi! I've tried to reprove my ~ natglobalincr in a more general way, and managed to hit a problem.
I have a "( ph -> ( T + 1 ) e. ZZ )" assertion. It turns out there are zero theorems which allow to go from that to "( ph -> T e. ZZ )", while it seems there really should be some. Is there a way to prove it? Thanks! --- Ender Ting P.S. I can work around this because the final theorem contains "A. k e. ( 0 ..^ T )" which would generalize over empty set if T is not integer, but that makes proof very much cumbersome. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/metamath/2f2c8474-0f90-4ef4-8afb-1b8ac06b1dc6n%40googlegroups.com.
