Utility theorems for numbers

[Ender Ting]

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.

[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.

­ 

--
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+u...@googlegroups.com.
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.

[Ender Ting]

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:

[Steven Nguyen]

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

To view this discussion visit https://groups.google.com/d/msgid/metamath/f51f2ce5-fbb0-4f53-ab66-777aed9a1aa9n%40googlegroups.com.