Yes you can prove it, but it involves internal details of how addition is defined. Reverse closure laws are explicitly not proven for addition.
Why do you have this assertion? If you know that ( ph -> ( T + 1 ) e. ZZ ) why not just say that ( ph -> T e. ZZ ).
Also if you could paste your proof script that would be nice so that we could see where you are stuck.
Von: Ender Ting <[email protected]>
Datum: 29.04.2025 19:49:26
An: Metamath <[email protected]>
Betreff: [Metamath] Utility theorems for numbersHi! 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 TingP.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 [email protected].
To view this discussion visit https://groups.google.com/d/msgid/metamath/2f2c8474-0f90-4ef4-8afb-1b8ac06b1dc6n%40googlegroups.com.
Your E-Mail. Your Cloud. Your Office. eclipso Mail Europe.
--
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 [email protected].
To view this discussion visit https://groups.google.com/d/msgid/metamath/2b9fda92d155eaaa2dcc549e0ee797a7%40mail.eclipso.de.
