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.
