In the future, you can prove it. Probably best as a lemma. Let ph -> T e. CC and ph -> T + 1 in ZZ
So, T + 1 - 1 in ZZ, and by cancellation, T in ZZ. You can see an example at https://us.metamath.org/mpeuni/readdrcl2d.html On Tue, Apr 29, 2025 at 1:21 PM Ender Ting <[email protected]> wrote: > I've managed to get unstuck, bringing one more antecedent into the > expression! Here's the script of my current progress. > > $( <MM> <PROOF_ASST> THEOREM=ormkglobd LOC_AFTER=et-sqrtnegnre > > h1::ormkglobd.1 |- ( ph -> R Or S ) > h2::ormkglobd.2 |- ( ph -> ran B C_ S ) > h3::ormkglobd.3 |- ( ph -> A. k e. ( 0 ..^ T ) ( B ` k ) R ( B ` ( k + 1 ) > ) ) > * bringing a hypothesis that <T e. ZZ> here looks unnecessary; theorem > still holds > even if non-integer T is substituted > > d2:3:r19.21bi |- ( ( ph /\ k e. ( 0 ..^ T ) ) -> ( B ` k ) R ( B ` ( k + 1 > ) ) ) > !d16:: |- ( a = ( k + 1 ) -> ( ( B ` k ) R ( B ` a ) <-> ( B ` k ) R > ( B ` ( k + 1 ) ) ) ) > !d17:: |- ( a = b -> ( ( B ` k ) R ( B ` a ) <-> ( B ` k ) R ( B ` b > ) ) ) > !d18:: |- ( a = ( b + 1 ) -> ( ( B ` k ) R ( B ` a ) <-> ( B ` k ) R > ( B ` ( b + 1 ) ) ) ) > !d19:: |- ( a = t -> ( ( B ` k ) R ( B ` a ) <-> ( B ` k ) R ( B ` t > ) ) ) > !d21:: |- ( ( ( ph /\ k e. ( 0 ..^ T ) ) > /\ ( b e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) > /\ ( B ` k ) R ( B ` b ) ) > -> ( B ` k ) R ( B ` ( b + 1 ) ) ) > d14::elfzoelz |- ( k e. ( 0 ..^ T ) -> k e. ZZ ) > d15::elfzoel2 |- ( k e. ( 0 ..^ T ) -> T e. ZZ ) > d4::elfzop1le2 |- ( k e. ( 0 ..^ T ) -> ( k + 1 ) <_ T ) > d25:d14:adantl |- ( ( ph /\ k e. ( 0 ..^ T ) ) -> k e. ZZ ) > d22:d25:peano2zd |- ( ( ph /\ k e. ( 0 ..^ T ) ) -> ( k + 1 ) e. ZZ ) > d23:d15:adantl |- ( ( ph /\ k e. ( 0 ..^ T ) ) -> T e. ZZ ) > d24:d4:adantl |- ( ( ph /\ k e. ( 0 ..^ T ) ) -> ( k + 1 ) <_ T ) > d3:d16,d17,d18,d19,d2,d21,d22,d23,d24:fzindd > |- ( ( ( ph /\ k e. ( 0 ..^ T ) ) > /\ ( t e. ZZ /\ ( k + 1 ) <_ t /\ t <_ T ) ) > -> ( B ` k ) R ( B ` t ) ) > > d30::elfzop1le2 |- ( t e. ( 1 ..^ ( T + 1 ) ) -> ( t + 1 ) <_ ( T + 1 ) ) > d33::leadd1 |- ( ( t e. RR /\ T e. RR /\ 1 e. RR ) > -> ( t <_ T <-> ( t + 1 ) <_ ( T + 1 ) ) ) > d40:d33:biimprd |- ( ( t e. RR /\ T e. RR /\ 1 e. RR ) > -> ( ( t + 1 ) <_ ( T + 1 ) -> t <_ T ) ) > d32:d30:adantl |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> ( t + 1 ) <_ ( T + 1 ) ) > * ******************************************************************** > here, I tried to prove <T e. ZZ> from <t e. ( 1 ..^ ( T + 1 ) )> > ******************************************************************** > d34:d15:adantr |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> T e. ZZ ) > d36::elfzoelz |- ( t e. ( 1 ..^ ( T + 1 ) ) -> t e. ZZ ) > d35:d36:adantl |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> t e. ZZ ) > d38:d34:zred |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) -> T e. > RR ) > d37:d35:zred |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) -> t e. > RR ) > d39::1red |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) -> 1 e. RR > ) > d41:d37,d38,d39:3jca |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> ( t e. RR /\ T e. RR /\ 1 e. RR ) ) > d31:d41,d32,d40:sylc |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> t <_ T ) > d42:d14:adantr |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> k e. ZZ ) > d43::zltp1le |- ( ( k e. ZZ /\ t e. ZZ ) -> ( k < t <-> ( k + 1 ) <_ t ) > ) > d44:d42,d35,d43:syl2anc |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) > ) ) > -> ( k < t <-> ( k + 1 ) <_ t ) ) > d45:d44:biimpd |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> ( k < t -> ( k + 1 ) <_ t ) ) > d46:d35:a1d |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> ( k < t -> t e. ZZ ) ) > d47:d31:a1d |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> ( k < t -> t <_ T ) ) > d48:d46,d45,d47:3jcad |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> ( k < t -> ( t e. ZZ /\ ( k + 1 ) <_ t /\ t <_ T ) ) ) > d52::2a1 |- ( ph -> ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> ( k < t -> ph ) ) ) > d53:d48:a1i |- ( ph -> ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> ( k < t -> ( t e. ZZ /\ ( k + 1 ) <_ t /\ t <_ T ) ) ) ) > d55::2a1 |- ( k e. ( 0 ..^ T ) -> ( t e. ( 1 ..^ ( T + 1 ) ) > -> ( k < t -> k e. ( 0 ..^ T ) ) ) ) > d54:d55:imp |- ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> ( k < t -> k e. ( 0 ..^ T ) ) ) > d51:d54:a1i |- ( ph -> ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> ( k < t -> k e. ( 0 ..^ T ) ) ) ) > !d56::jcad |- ( ph -> ( ( k e. ( 0 ..^ T ) /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> ( k < t -> ( ph /\ k e. ( 0 ..^ T ) ) ) ) ) > > d49:: |- ( ( ph /\ &W1 ) -> ( B ` k ) R ( B ` t ) ) > d50:: |- ( ph > -> ( ( k e. ( 0 ..^ T ) > /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> ( k < t -> ( ph /\ &W1 ) ) ) ) > > d1:d50,d49:syl8 |- ( ph > -> ( ( k e. ( 0 ..^ T ) > /\ t e. ( 1 ..^ ( T + 1 ) ) ) > -> ( k < t -> ( B ` k ) R ( B ` t ) ) ) ) > qed:d1:ralrimivv |- ( ph -> A. k e. ( 0 ..^ T ) A. t e. ( 1 ..^ ( T + 1 ) ) > ( k < t -> ( B ` k ) R ( B ` t ) ) ) > > $) > > Well, I get the reason: if addition was defined to return 0 or like on > non-integer arguments, then cancellation would not work. Thanks for the > answer! > вторник, 29 апреля 2025 г. в 21:05:51 UTC+3, Meta Kunt: > >> Yes and no. >> 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 numbers >> 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 [email protected] >> <http://metamath%2Bunsubscribe%40googlegroups.com>. >> To view this discussion visit >> https://groups.google.com/d/msgid/metamath/2f2c8474-0f90-4ef4-8afb-1b8ac06b1dc6n%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/2f2c8474-0f90-4ef4-8afb-1b8ac06b1dc6n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> >> >> >> >> ------------------------------ >> >> Your E-Mail. Your Cloud. Your Office. *eclipso Mail Europe >> <https://www.eclipso.eu>*. >> > -- > 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/f51f2ce5-fbb0-4f53-ab66-777aed9a1aa9n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/f51f2ce5-fbb0-4f53-ab66-777aed9a1aa9n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAAfCLni7Onnr2EVA_Ti26sZJFPT%3DtkRdu3oNxMfz8fsm8g-aPA%40mail.gmail.com.
