Add dedekindeu to iset.mm

This is a bit like dedekind in set.mm although various details are different including that the lower and upper cuts have to be open (and thus the real corresponding to the Dedekind cut is not contained in either one). Includes lemmas dedekindeulemuub , dedekindeulemub , dedekindeulemloc , dedekindeulemlub , dedekindeulemlu , and dedekindeulemeu Expand dedekind entry in mmil.html to mention dedekindeu and differences.
metamath · Feb 5, 2024 · 1a068d5 · 1a068d5
1 parent 733f82e
commit 1a068d5
Show file tree

Hide file tree

Showing 2 changed files with 164 additions and 1 deletion.
diff --git a/iset.mm b/iset.mm
@@ -141800,6 +141800,165 @@ S C_ ( P ( ball ` D ) T ) ) $=
 $)
 
 
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Dedekind cuts
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+  ${
+    dedekindeu.lss $e |- ( ph -> L C_ RR ) $.
+    dedekindeu.uss $e |- ( ph -> U C_ RR ) $.
+    dedekindeu.lm $e |- ( ph -> E. q e. RR q e. L ) $.
+    dedekindeu.um $e |- ( ph -> E. r e. RR r e. U ) $.
+    dedekindeu.lr $e |- ( ph -> A. q e. RR (
+      q e. L <-> E. r e. L q < r ) ) $.
+    dedekindeu.ur $e |- ( ph -> A. r e. RR (
+      r e. U <-> E. q e. U q < r ) ) $.
+    dedekindeu.disj $e |- ( ph -> ( L i^i U ) = (/) ) $.
+    dedekindeu.loc $e |- ( ph -> A. q e. RR A. r e. RR (
+      q < r -> ( q e. L \/ r e. U ) ) ) $.
+
+    ${
+      $d A q r z $.  $d L q z $.  $d U a q z $.  $d U q r z $.  $d ph q z $.
+      dedekindeulemuub.u $e |- ( ph -> A e. U ) $.
+      $( Lemma for ~ dedekindeu .  Any element of the upper cut is an upper
+         bound for the lower cut.  (Contributed by Jim Kingdon, 2-Feb-2024.) $)
+      dedekindeulemuub $p |- ( ph -> A. z e. L z < A ) $=
+        ( clt wbr wcel cr va cv wral wrex wb eleq1 breq2 rexbidv bibi12d sseldd
+        wceq rspcdva mpbid wa ad2antrr simpr simplrl breq1 rspcev sylan cbvrexv
+        wss sylib ad3antrrr adantr mpbird wn simplll cin disj r19.21bi pm2.65da
+        c0 syl2anc nltled simplrr lelttrd ralrimiva rexlimddv ) AGUBZCQRZBUBZCQ
+        RZBEUCGDACDSZWAGDUDZPAFUBZDSZVTWFQRZGDUDZUEZWDWEUEFTCWFCUKZWGWDWIWEWFCD
+        UFWKWHWAGDWFCVTQUGUHUIMADTCIPUJZULUMAVTDSZWAUNZUNZWCBEWOWBESZUNZWBVTCWQ
+        ETWBAETVBWNWPHUOWOWPUPZUJZWQDTVTADTVBWNWPIUOAWMWAWPUQZUJZACTSWNWPWLUOWQ
+        WBVTWSXAWQVTWBQRZWBDSZWQXBUNZXCXBGDUDZXDUAUBZWBQRZUADUDZXEWQWMXBXHWTXGX
+        BUAVTDXFVTWBQURZUSUTXGXBUAGDXIVAVCXDWJXCXEUEFTWBWFWBUKZWGXCWIXEWFWBDUFX
+        JWHXBGDWFWBVTQUGUHUIAWJFTUCWNWPXBMVDWQWBTSXBWSVEULVFXDAWPXCVGZAWNWPXBVH
+        WQWPXBWRVEAXKBEAEDVIVMUKXKBEUCNBEDVJVCVKVNVLVOAWMWAWPVPVQVRVS $.
+    $}
+
+    ${
+      $d L a q r y $.  $d L a r x y $.  $d U a q r y $.  $d a ph q r y $.
+      $( Lemma for ~ dedekindeu .  The lower cut has an upper bound.
+         (Contributed by Jim Kingdon, 31-Jan-2024.) $)
+      dedekindeulemub $p |- ( ph -> E. x e. RR A. y e. L y < x ) $=
+        ( va wral cr wrex adantr cv wcel clt wbr eleq1w cbvrexv sylib wa simprl
+        wss wb cin c0 wceq wo wi dedekindeulemuub brralrspcev syl2anc rexlimddv
+        simprr ) APUAZDUBZCUAZBUAUCUDCEQBRSZPRAFUAZDUBZFRSZVCPRSKVGVCFPRFPDUEUF
+        UGAVBRUBZVCUHZUHZVIVDVBUCUDCEQVEAVIVCUIVKCVBDEFGAERUJVJHTADRUJVJITAGUAZ
+        EUBZGRSVJJTAVHVJKTAVMVLVFUCUDZFESUKGRQVJLTAVGVNGDSUKFRQVJMTAEDULUMUNVJN
+        TAVNVMVGUOUPFRQGRQVJOTAVIVCVAUQBCVDVBUCREURUSUT $.
+    $}
+
+    ${
+      $d L q r z $.  $d U q r z $.  $d ph q x y z $.  $d r x y z $.
+      $( Lemma for ~ dedekindeu .  The set L is located.  (Contributed by Jim
+         Kingdon, 31-Jan-2024.) $)
+      dedekindeulemloc $p |- ( ph -> A. x e. RR A. y e. RR ( x < y
+          -> ( E. z e. L x < z \/ A. z e. L z < y ) ) ) $=
+        ( clt wrex cr ad2antrr cv wbr wral wo wi wcel weq eleq1w orbi2d imbi12d
+        breq2 breq1 orbi1d ralbidv adantr simprl rspcdva simprr rexbidv bibi12d
+        wa simpr wb mpbid cbvrexv sylib ex wss c0 wceq dedekindeulemuub orim12d
+        cin syld ralrimivva ) ABUAZCUAZQUBZVPDUAZQUBZDFRZVSVQQUBDFUCZUDZUEBCSSA
+        VPSUFZVQSUFZVAZVAZVRVPFUFZVQEUFZUDZWCWGVPGUAZQUBZWHWKEUFZUDZUEZVRWJUEGS
+        VQGCUGZWLVRWNWJWKVQVPQUKWPWMWIWHGCEUHUIUJWGHUAZWKQUBZWQFUFZWMUDZUEZGSUC
+        ZWOGSUCHSVPHBUGZXAWOGSXCWRWLWTWNWQVPWKQULZXCWSWHWMHBFUHZUMUJUNAXBHSUCZW
+        FPUOAWDWEUPZUQAWDWEURUQWGWHWAWIWBWGWHWAWGWHVAZWLGFRZWAXHWHXIWGWHVBXHWSW
+        RGFRZVCZWHXIVCHSVPXCWSWHXJXIXEXCWRWLGFXDUSUTAXKHSUCZWFWHMTWGWDWHXGUOUQV
+        DWLVTGDFWKVSVPQUKVEVFVGWGWIWBWGWIVADVQEFGHAFSVHWFWIITAESVHWFWIJTAWSHSRW
+        FWIKTAWMGSRWFWILTAXLWFWIMTAWMWRHERVCGSUCWFWINTAFEVMVIVJWFWIOTAXFWFWIPTW
+        GWIVBVKVGVLVNVO $.
+    $}
+
+    ${
+      $d L q r x y z $.  $d U q r y z $.  $d ph q r x y z $.
+      $( Lemma for ~ dedekindeu .  The set L has a least upper bound.
+         (Contributed by Jim Kingdon, 31-Jan-2024.) $)
+      dedekindeulemlub $p |- ( ph -> E. x e. RR ( A. y e. L -. x < y
+          /\ A. y e. RR ( y < x -> E. z e. L y < z ) ) ) $=
+        ( cr clt wral wrex wss cv wcel wex wbr wo wi wn wa eleq1w cbvrexv rexex
+        sylbi syl dedekindeulemub dedekindeulemloc axsuploc syl22anc ) AFQUABUB
+        ZFUCZBUDZCUBZUSRUEZCFSBQTUSVBRUEZUSDUBZRUEDFTVEVBRUEDFSUFUGCQSBQSVDUHCF
+        SVCVBVERUEDFTUGCQSUIBQTIAHUBFUCZHQTZVAKVGUTBQTVAVFUTHBQHBFUJUKUTBQULUMU
+        NABCEFGHIJKLMNOPUOABCDEFGHIJKLMNOPUPBCDFUQUR $.
+    $}
+
+    ${
+      $d L q r x y z $.  $d U q r y z $.  $d ph q r x y z $.
+      $( Lemma for ~ dedekindeu .  There is a number which separates the lower
+         and upper cuts.  (Contributed by Jim Kingdon, 31-Jan-2024.) $)
+      dedekindeulemlu $p |- ( ph -> E. x e. RR (
+          A. q e. L q < x /\ A. r e. U x < r ) ) $=
+        ( clt wbr wral cr wa wcel vy vz cv wn wrex wi dedekindeulemlub simpr wb
+        wss ad3antrrr sseldd rsp syl mpd mpbid adantr simprl simp-4r wceq breq2
+        simprr notbid ad2antrr rspcdva ltletrd rexlimddv ralrimiva simplll sylc
+        nltled breq1 rexbidv imbi12d cbvrexv sylib mpbird disj r19.21bi syl2anc
+        cin c0 pm2.65da lelttrd jca ex reximdva ) ABUCZUAUCZOPZUDZUADQZWIWHOPZW
+        IUBUCZOPZUBDUEZUFZUARQZSZBRUEFUCZWHOPZFDQZWHEUCZOPZECQZSZBRUEABUAUBCDEF
+        GHIJKLMNUGAWSXFBRAWHRTZSZWSXFXHWSSZXBXEXIXAFDXIWTDTZSZWTXCOPZXAEDXKXJXL
+        EDUEZXIXJUHZXKWTRTZXJXMUIZXKDRWTADRUJZXGWSXJGUKZXNULZAXOXPUFZXGWSXJAXPF
+        RQXTKXPFRUMUNZUKUOUPXKXCDTZXLSZSZWTXCWHXKXOYCXSUQYDDRXCXKXQYCXRUQXKYBXL
+        URZULZAXGWSXJYCUSZXKYBXLVBYDXCWHYFYGYDWKXDUDUADXCWIXCUTWJXDWIXCWHOVAVCX
+        IWLXJYCXHWLWRURVDYEVEVKVFVGVHXIXDECXIXCCTZSZXLXDFCYIYHXLFCUEZXIYHUHZYIA
+        XCRTZYHYJUIZAXGWSYHVIZYICRXCYIACRUJZYNHUNZYKULZAYMERQYLYMUFLYMERUMUNVJU
+        PYIWTCTZXLSZSZWHWTXCAXGWSYHYSUSZYTCRWTYIYOYSYPUQYIYRXLURZULZYIYLYSYQUQY
+        TWHWTUUAUUCYTXAYRYTYRXAUUBUQYTXASZAXJYRUDZYIAYSXAYNVDZUUDXJXMUUDWTWNOPZ
+        UBDUEZXMUUDXAUUHYTXAUHUUDWQXAUUHUFUARWTWIWTUTZWMXAWPUUHWIWTWHOVLUUIWOUU
+        GUBDWIWTWNOVLVMVNXIWRYHYSXAXHWLWRVBUKYTXOXAUUCUQZVEUOUUGXLUBEDWNXCWTOVA
+        VOVPUUDAXOXPUUFUUJYAVJVQAUUEFDADCWAWBUTUUEFDQMFDCVRVPVSVTWCVKYIYRXLVBWD
+        VGVHWEWFWGUO $.
+    $}
+
+    ${
+      $d A q r $.  $d B r $.  $d L q r $.  $d U q r $.
+      dedekindeulemeu.are $e |- ( ph -> A e. RR ) $.
+      dedekindeulemeu.ac $e |- ( ph
+        -> ( A. q e. L q < A /\ A. r e. U A < r ) ) $.
+      dedekindeulemeu.bre $e |- ( ph -> B e. RR ) $.
+      dedekindeulemeu.bc $e |- ( ph
+        -> ( A. q e. L q < B /\ A. r e. U B < r ) ) $.
+      dedekindeulemeu.lt $e |- ( ph -> A < B ) $.
+      $( Lemma for ~ dedekindeu .  Part of proving uniqueness.  (Contributed by
+         Jim Kingdon, 31-Jan-2024.) $)
+      dedekindeulemeu $p |- ( ph -> F. ) $=
+        ( wcel wfal wa clt wbr breq1 wral simpld adantr simpr rspcdva pm2.21fal
+        cv wn ltnrd breq2 simprd wo wi wceq eleq1 orbi2d imbi12d orbi1d ralbidv
+        cr mpd mpjaodan ) ABEUAZUBCDUAZAVIUCZBBUDUEZVKGUMZBUDUEZVLGEBVMBBUDUFAV
+        NGEUGZVIAVOBFUMZUDUEZFDUGQUHUIAVIUJUKAVLUNVIABPUOUIULAVJUCZCCUDUEZVRCVP
+        UDUEZVSFDCVPCCUDUPAVTFDUGZVJAVMCUDUEGEUGWASUQUIAVJUJUKAVSUNVJACRUOUIULA
+        BCUDUEZVIVJURZTAVQVIVPDUAZURZUSZWBWCUSFVFCVPCUTZVQWBWEWCVPCBUDUPWGWDVJV
+        IVPCDVAVBVCAVMVPUDUEZVMEUAZWDURZUSZFVFUGWFFVFUGGVFBVMBUTZWKWFFVFWLWHVQW
+        JWEVMBVPUDUFWLWIVIWDVMBEVAVDVCVEOPUKRUKVGVH $.
+    $}
+
+    $d L q r x y $.  $d U q r x y $.  $d ph q r x y $.
+    $( A Dedekind cut identifies a unique real number.  Similar to ~ df-inp
+       except that the the Dedekind cut is formed by sets of reals (rather than
+       positive rationals).  But in both cases the defining property of a
+       Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and
+       located.  (Contributed by Jim Kingdon, 5-Jan-2024.) $)
+    dedekindeu $p |- ( ph -> E! x e. RR (
+        A. q e. L q < x /\ A. r e. U x < r ) ) $=
+      ( clt wbr wral wa cr ad4antr vy cv wrex wrmo wreu dedekindeulemlu wceq wi
+      wcel cap wn wfal wss wb cin simprl ad2antrr adantr simprr dedekindeulemeu
+      c0 wo simpr reaplt syl2anc mpbid mpjaodan inegd cc simplrl simplrr mpbird
+      recnd apti ex ralrimivva breq2 ralbidv breq1 anbi12d rmo4 sylibr sylanbrc
+      reu5 ) AFUBZBUBZOPZFDQZWFEUBZOPZECQZRZBSUCWLBSUDZWLBSUEABCDEFGHIJKLMNUFAW
+      LWEUAUBZOPZFDQZWNWIOPZECQZRZRZWFWNUGZUHZUASQBSQWMAXBBUASSAWFSUIZWNSUIZRZR
+      ZWTXAXFWTRZXAWFWNUJPZUKZXGXHXGXHRZWFWNOPZULWNWFOPZXJXKRWFWNCDEFADSUMZXEWT
+      XHXKGTACSUMZXEWTXHXKHTAWEDUIZFSUCZXEWTXHXKITAWICUIZESUCZXEWTXHXKJTAXOWEWI
+      OPZEDUCUNFSQZXEWTXHXKKTAXQXSFCUCUNESQZXEWTXHXKLTADCUOVAUGZXEWTXHXKMTAXSXO
+      XQVBUHESQFSQZXEWTXHXKNTXJXCXKXFXCWTXHAXCXDUPUQZURXGWLXHXKXFWLWSUPZUQXJXDX
+      KXFXDWTXHAXCXDUSUQZURXGWSXHXKXFWLWSUSZUQXJXKVCUTXJXLRWNWFCDEFAXMXEWTXHXLG
+      TAXNXEWTXHXLHTAXPXEWTXHXLITAXRXEWTXHXLJTAXTXEWTXHXLKTAYAXEWTXHXLLTAYBXEWT
+      XHXLMTAYCXEWTXHXLNTXJXDXLYFURXGWSXHXLYGUQXJXCXLYDURXGWLXHXLYEUQXJXLVCUTXJ
+      XHXKXLVBZXGXHVCXJXCXDXHYHUNYDYFWFWNVDVEVFVGVHXGWFVIUIWNVIUIXAXIUNXGWFAXCX
+      DWTVJVMXGWNAXCXDWTVKVMWFWNVNVEVLVOVPWLWSBUASXAWHWPWKWRXAWGWOFDWFWNWEOVQVR
+      XAWJWQECWFWNWIOVSVRVTWAWBWLBSWDWC $.
+  $}
+
+
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
   Derivatives

diff --git a/mmil.raw.html b/mmil.raw.html
@@ -5679,7 +5679,11 @@
 
 <TR>
 <TD>dedekind , dedekindle</TD>
-<TD><I>none</I></TD>
+<TD>~ dedekindeu</TD>
+<TD>various details are different including that in ~ dedekindeu
+the lower and upper cuts have to be open (and thus the real
+corresponding to the Dedekind cut is not contained in either the
+lower or upper cut)</TD>
 </TR>
 
 <TR>