Add odZ to iset.mm

iset.mm

@@ -39115,6 +39115,14 @@ rather than an implication (but the two are equivalent by ~ bm1.3ii ),
       BNAHOPFNAIJNCKLM $.
   $}
 
+  ${
+    uniexd.1 $e |- ( ph -> A e. V ) $.
+    $( Deduction version of the ZF Axiom of Union in class notation.
+       (Contributed by Glauco Siliprandi, 26-Jun-2021.) $)
+    uniexd $p |- ( ph -> U. A e. _V ) $=
+      ( wcel cuni cvv uniexg syl ) ABCEBFGEDBCHI $.
+  $}
+
   ${
     unex.1 $e |- A e. _V $.
     unex.2 $e |- B e. _V $.
@@ -51601,6 +51609,26 @@ We use their notation ("onto" under the arrow).  (Contributed by NM,
       ( cvv wcel cmpt mptexg ax-mp ) BEFABCGEFDABCEHI $.
   $}
 
+  ${
+    $d A x $.
+    mptexd.1 $e |- ( ph -> A e. V ) $.
+    $( If the domain of a function given by maps-to notation is a set, the
+       function is a set.  Deduction version of ~ mptexg .  (Contributed by
+       Glauco Siliprandi, 24-Dec-2020.) $)
+    mptexd $p |- ( ph -> ( x e. A |-> B ) e. _V ) $=
+      ( wcel cmpt cvv mptexg syl ) ACEGBCDHIGFBCDEJK $.
+  $}
+
+  ${
+    $d x y A $.  $d x ph $.
+    mptrabex.1 $e |- A e. _V $.
+    $( If the domain of a function given by maps-to notation is a class
+       abstraction based on a set, the function is a set.  (Contributed by AV,
+       16-Jul-2019.)  (Revised by AV, 26-Mar-2021.) $)
+    mptrabex $p |- ( x e. { y e. A | ph } |-> B ) e. _V $=
+      ( crab rabex mptex ) BACDGEACDFHI $.
+  $}
+
   $( If the domain of a mapping is a set, the function is a set.  (Contributed
      by NM, 3-Oct-1999.) $)
   fex $p |- ( ( F : A --> B /\ A e. C ) -> F e. _V ) $=
@@ -68439,6 +68467,22 @@ all reals (greatest real number) for which all positive reals are greater.
       GHUMULLUBMGHJKLUCUDNABCDGIJOUEAEFGJPUFUIUKHKUGUOUNLIGJUGUHUJ $.
   $}
 
+  ${
+    $d A x y z $.  $d B x y z $.  $d C x y z $.  $d R x y z $.
+    $( Existence of supremum.  (Contributed by Jeff Madsen, 2-Sep-2009.) $)
+    supex2g $p |- ( A e. C -> sup ( B , A , R ) e. _V ) $=
+      ( vx vy vz wcel csup cv wbr wn wral wrex wi wa crab cuni cvv df-sup
+      rabexg uniexd eqeltrid ) ACHZBADIEJZFJZDKLFBMUFUEDKUFGJDKGBNOFAMPZEAQZRSE
+      FGBADTUDUHSUGEACUAUBUC $.
+  $}
+
+  ${
+    $( Existence of infimum.  (Contributed by Jim Kingdon, 1-Oct-2024.) $)
+    infex2g $p |- ( A e. C -> inf ( B , A , R ) e. _V ) $=
+      ( wcel cinf ccnv csup cvv df-inf supex2g eqeltrid ) ACEBADFBADGZHIBADJABC
+      MKL $.
+  $}
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -134498,13 +134542,24 @@ reduced fraction representation (no common factors, denominator
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
 $)
 
+  $c odZ $.
   $c phi $.
 
+  $( Extend class notation with the order function on the class of integers
+     modulo N. $)
+  codz $a class odZ $.
+
   $( Extend class notation with the Euler phi function. $)
   cphi $a class phi $.
 
   ${
-    $d n x $.
+    $d m n x $.
+    $( Define the order function on the class of integers modulo N.
+       (Contributed by Mario Carneiro, 23-Feb-2014.)  (Revised by AV,
+       26-Sep-2020.) $)
+    df-odz $a |- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |->
+                   inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) ) $.
+
     $( Define the Euler phi function (also called "Euler totient function"),
        which counts the number of integers less than ` n ` and coprime to it,
        see definition in [ApostolNT] p. 25.  (Contributed by Mario Carneiro,
@@ -135352,6 +135407,115 @@ reduced fraction representation (no common factors, denominator
       YDWMYEYFDYTUUEYGYHVPUWNEUUHYIYJYKYLYQBYMHUWMBOBYOBYPVLUPUP $.
   $}
 
+  ${
+    $d m n x N $.  $d n x A $.  $d n K $.
+    $( Value of the order function.  This is a function of functions; the inner
+       argument selects the base (i.e., mod ` N ` for some ` N ` , often prime)
+       and the outer argument selects the integer or equivalence class (if you
+       want to think about it that way) from the integers mod ` N ` .  In order
+       to ensure the supremum is well-defined, we only define the expression
+       when ` A ` and ` N ` are coprime.  (Contributed by Mario Carneiro,
+       23-Feb-2014.)  (Revised by AV, 26-Sep-2020.) $)
+    odzval $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
+                  ( ( odZ ` N ) ` A ) = inf ( { n e. NN |
+                    N || ( ( A ^ n ) - 1 ) } , RR , < ) ) $=
+      ( vx vm cn wcel cz cgcd co c1 wceq cfv cv cexp cmin cdvds crab cr clt wbr
+      codz cinf cmpt oveq2 eqeq1d rabbidv oveq1 cbvrabv eqtr4di breq1 mpteq12dv
+      wa infeq1d df-odz zex mptrabex fvmpt fveq1d elrab oveq1d breq2d eqid reex
+      cvv infex2g ax-mp sylbir sylan9eq 3impb ) CFGZAHGZACIJZKLZACUBMZMZCABNZOJ
+      ZKPJZQUAZBFRZSTUCZLVKVLVNUMZVPADVQCIJZKLZBHRZCDNZVQOJZKPJZQUAZBFRZSTUCZUD
+      ZMZWBVKAVOWMECDWGENZIJZKLZDHRZWOWIQUAZBFRZSTUCZUDWMFUBWOCLZDWRXAWFWLXBWRW
+      GCIJZKLZDHRWFXBWQXDDHXBWPXCKWOCWGIUEUFUGWEXDBDHVQWGLWDXCKVQWGCIUHUFUIUJXB
+      SWTWKTXBWSWJBFWOCWIQUKUGUNULDBEUOWEDBHWLUPUQURUSWCAWFGWNWBLWEVNBAHVQALWDV
+      MKVQACIUHUFUTDAWLWBWFWMWGALZSWKWATXEWJVTBFXEWIVSCQXEWHVRKPWGAVQOUHVAVBUGU
+      NWMVCSVEGWBVEGVDSWAVETVFVGURVHVIVJ $.
+
+    $( - Lemma for ~ odzcl , showing existence of a recurrent point for the
+       exponential.  (Contributed by Mario Carneiro, 28-Feb-2014.)  (Proof
+       shortened by AV, 26-Sep-2020.) $)
+    odzcllem $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
+                    ( ( ( odZ ` N ) ` A ) e. NN /\
+                      N || ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) ) ) $=
+      ( vn cn wcel cz co c1 wceq cfv cexp cmin cdvds wbr wa oveq2 oveq1d breq2d
+      cmo cn0 cgcd w3a codz cv crab cr clt cinf odzval cphi 1zzd cuz nnuz phicl
+      rabeqi 3ad2ant1 eulerth wb simp1 simp2 nnnn0d zexpcl syl2anc mp3an3 mpbid
+      1z moddvds elrabd cfz wdc elfznn adantl syl2an2r peano2zm syl infssuzcldc
+      dvdsdc eqeltrd elrab sylib ) BDEZAFEZABUAGHIZUBZABUCJJZBACUDZKGZHLGZMNZCD
+      UEZEWEDEBAWEKGZHLGZMNZOWDWEWJUFUGUHWJACBUIWDWIBUJJZWJCHWDUKWICDHULJUMUOWD
+      WIBAWNKGZHLGZMNZCWNDWFWNIZWHWPBMWRWGWOHLWFWNAKPQRWAWBWNDEWCBUNUPZWDWOBSGH
+      BSGIZWQABUQWDWAWOFEZWTWQURZWAWBWCUSZWDWBWNTEXAWAWBWCUTZWDWNWSVAAWNVBVCWAX
+      AHFEXBVFWOHBVGVDVCVEVHWDWAWFHWNVIGEZWHFEZWIVJXCWDXEOZWGFEZXFWDWBXEWFTEXHX
+      DXGWFXEWFDEWDWFWNVKVLVAAWFVBVMWGVNVOBWHVQVMVPVRWIWMCWEDWFWEIZWHWLBMXIWGWK
+      HLWFWEAKPQRVSVT $.
+
+    $( The order of a group element is an integer.  (Contributed by Mario
+       Carneiro, 28-Feb-2014.) $)
+    odzcl $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
+                 ( ( odZ ` N ) ` A ) e. NN ) $=
+      ( cn wcel cz cgcd co c1 wceq w3a codz cfv cexp cmin cdvds odzcllem simpld
+      wbr ) BCDAEDABFGHIJABKLLZCDBASMGHNGORABPQ $.
+
+    $( Any element raised to the power of its order is ` 1 ` .  (Contributed by
+       Mario Carneiro, 28-Feb-2014.) $)
+    odzid $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
+                      N || ( ( A ^ ( ( odZ ` N ) ` A ) ) - 1 ) ) $=
+      ( cn wcel cz cgcd co c1 wceq w3a codz cfv cexp cmin cdvds odzcllem simprd
+      wbr ) BCDAEDABFGHIJABKLLZCDBASMGHNGORABPQ $.
+
+    $( The only powers of ` A ` that are congruent to ` 1 ` are the multiples
+       of the order of ` A ` .  (Contributed by Mario Carneiro, 28-Feb-2014.)
+       (Proof shortened by AV, 26-Sep-2020.) $)
+    odzdvds $p |- ( ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) /\ K e. NN0 )
+      -> ( N || ( ( A ^ K ) - 1 ) <-> ( ( odZ ` N ) ` A ) || K ) ) $=
+      ( vn cn wcel cz co c1 wceq cn0 cmo cexp cmin cdvds wbr cc0 syl2anc oveq1d
+      syl cgcd w3a wa codz cfv wn wi cle clt cq nn0z zq adantl odzcl adantr nnq
+      nngt0d modqlt syl3anc wb zmodcld nn0zd nnzd zltnle mpbid cv crab cinf cuz
+      1zzd nnuz rabeqi oveq2 breq2d elrab biimpri cfz wdc simp1 ad3antrrr simp2
+      cr elfznn nnnn0d zexpcl peano2zm dvdsdc infssuzledc ancomsd odzval breq1d
+      ex sylibrd mtod imnan sylibr wo elnn0 sylib syld simpl1 dvds0 simpl2 zcnd
+      ord exp0d 1m1e0 eqtrdi breqtrrd syl5ibrcom impbid cdiv cfl cmul znq nn0re
+      nn0ge0 nnred ge0div flqge0nn0 nn0mulcld mp1i expmuld odzid moddvds mpbird
+      1z modqexp flqcld 1exp 3eqtrd modqmul1 caddc expaddd modqval oveq2d recnd
+      nn0cnd pncan3d eqtrd mulid2d 3eqtr3d sylancom 3bitr3d dvdsval3 3bitr4d
+      eqtr3d eqeq1d ) CEFZAGFZACUAHIJZUBZBKFZUCZCABACUDUEUEZLHZMHZINHZOPZUUPQJZ
+      CABMHZINHOPZUUOBOPZUUNUUSUUTUUNUUSUUPEFZUFZUUTUUNUUSUVDUCZUFUUSUVEUGUUNUV
+      FUUOUUPUHPZUUNUUPUUOUIPZUVGUFZUUNBUJFZUUOUJFZQUUOUIPZUVHUUMUVJUULUUMBGFZU
+      VJBUKZBULTUMZUUNUUOEFZUVKUULUVPUUMACUNUOZUUOUPTZUUNUUOUVQUQZBUUOURUSUUNUU
+      PGFUUOGFUVHUVIUTUUNUUPUUNBUUOUUMUVMUULUVNUMZUVQVAZVBUUNUUOUVQVCUUPUUOVDRV
+      EUUNUVFCADVFZMHZINHZOPZDEVGZWBUIVHZUUPUHPZUVGUUNUVDUUSUWHUUNUVDUUSUCZUWHU
+      UNUWIUCZUWEUUPUWFDIUWJVJUWEDEIVIUEVKVLUWIUUPUWFFZUUNUWKUWIUWEUUSDUUPEUWBU
+      UPJZUWDUURCOUWLUWCUUQINUWBUUPAMVMSVNVOVPUMUWJUWBIUUPVQHFZUCZUUIUWDGFZUWEV
+      RUULUUIUUMUWIUWMUUIUUJUUKVSVTUWNUWCGFZUWOUWNUUJUWBKFZUWPUULUUJUUMUWIUWMUU
+      IUUJUUKWAVTUWMUWQUWJUWMUWBUWBUUPWCWDUMAUWBWERUWCWFTCUWDWGRWHWLWIUUNUUOUWG
+      UUPUHUULUUOUWGJUUMADCWJUOWKWMWNUUSUVDWOWPUUNUVDUUTUUNUUPKFZUVDUUTWQUWAUUP
+      WRWSXEWTUUNUUSUUTCAQMHZINHZOPUUNCQUWTOUUNCGFCQOPUUNCUUIUUJUUKUUMXAZVCCXBT
+      UUNUWTIINHQUUNUWSIINUUNAUUNAUUIUUJUUKUUMXCZXDZXFSXGXHXIUUTUURUWTCOUUTUUQU
+      WSINUUPQAMVMSVNXJXKUUNUVACLHZICLHZJZUUQCLHZUXEJZUVBUUSUUNUXDUXGUXEUUNAUUO
+      BUUOXLHZXMUEZXNHZMHZUUQXNHZCLHIUUQXNHZCLHUXDUXGUUNUXLIUUQCUUNUXLGFZUXLUJF
+      UUNUUJUXKKFUXOUXBUUNUUOUXJUUNUUOUVQWDZUUNUXIUJFZQUXIUHPZUXJKFUUNUVMUVPUXQ
+      UVTUVQBUUOXORZUUNQBUHPZUXRUUMUXTUULBXQUMUUNBWBFZUUOWBFUVLUXTUXRUTUUMUYAUU
+      LBXPUMZUUNUUOUVQXRUVSBUUOXSUSVEUXIXTRZYAZAUXKWERUXLULTIGFZIUJFUUNYGIULYBU
+      UNUUJUWRUUQGFZUXBUWAAUUPWERZUUNUUICUJFUXACUPTZUUNCUXAUQZUUNUXLCLHAUUOMHZU
+      XJMHZCLHIUXJMHZCLHUXEUUNUXLUYKCLUUNAUUOUXJUXCUYCUXPYCSUUNUYJIUXJCUUNUUJUU
+      OKFUYJGFZUXBUXPAUUOWERZUUNVJZUYCUYHUYIUUNUYJCLHUXEJZCUYJINHOPZUULUYQUUMAC
+      YDUOUUNUUIUYMUYEUYPUYQUTUXAUYNUYOUYJICYEUSYFYHUUNUYLICLUUNUXJGFUYLIJUUNUX
+      IUXSYIUXJYJTSYKYLUUNUXMUVACLUUNAUXKUUPYMHZMHUXMUVAUUNAUXKUUPUXCUWAUYDYNUU
+      NUYRBAMUUNUYRUXKBUXKNHZYMHBUUNUUPUYSUXKYMUUNUVJUVKUVLUUPUYSJUVOUVRUVSBUUO
+      YOUSYPUUNUXKBUUNUXKUYDYRUUNBUYBYQYSYTYPUUGSUUNUXNUUQCLUUNUUQUUNUUQUYGXDUU
+      ASUUBUUHUUNUUIUVAGFZUYEUXFUVBUTUXAUULUUMUUJUYTUXBABWEUUCUYOUVAICYEUSUUNUU
+      IUYFUYEUXHUUSUTUXAUYGUYOUUQICYEUSUUDUUNUVPUVMUVCUUTUTUVQUVTUUOBUUERUUF $.
+
+    $( The order of any group element is a divisor of the Euler ` phi `
+       function.  (Contributed by Mario Carneiro, 28-Feb-2014.) $)
+    odzphi $p |- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) ->
+                  ( ( odZ ` N ) ` A ) || ( phi ` N ) ) $=
+      ( cn wcel cz cgcd co c1 wceq w3a cphi cfv cexp cmin cdvds wbr codz cmo wb
+      mpbid eulerth simp1 cn0 phicld nnnn0d zexpcl syl2anc 1zzd moddvds syl3anc
+      simp2 odzdvds mpdan ) BCDZAEDZABFGHIZJZBABKLZMGZHNGOPZABQLLUROPZUQUSBRGHB
+      RGIZUTABUAUQUNUSEDZHEDVBUTSUNUOUPUBZUQUOURUCDZVCUNUOUPUKUQURUQBVDUDUEZAUR
+      UFUGUQUHUSHBUIUJTUQVEUTVASVFAURBULUMT $.
+  $}
+
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
@@ -154144,6 +154308,12 @@ Norman Megill (2007) section 1.1.3.  Megill then states, "A number of
   althtmldef "Prime" as "&#8473;";
     /* 2-Jan-2016 reverted sans-serif */
   latexdef "Prime" as "\mathbb{P}";
+htmldef "odZ" as
+    "<IMG SRC='_od.gif' WIDTH=15 HEIGHT=19 ALT=' od' TITLE='od'>" +
+    "<IMG SRC='__subbbz.gif' WIDTH=8 HEIGHT=19 ALT='Z' TITLE='Z'>";
+  althtmldef "odZ" as "od<SUB>&#8484;</SUB>";
+    /* 2-Jan-2016 reverted sans-serif */
+  latexdef "odZ" as "\mathrm{od}_\mathbb{Z}";
 htmldef "phi" as
     "<IMG SRC='phi.gif' WIDTH=10 HEIGHT=19 ALT=' phi' TITLE='phi'>";
   althtmldef "phi" as '&#981;';

mmil.raw.html

@@ -4431,8 +4431,8 @@
 
 <TR>
   <TD>supexd , supex</TD>
-  <TD><I>none</I></TD>
-  <TD>The set.mm proof uses rmorabex</TD>
+  <TD>~ supex2g</TD>
+  <TD>The set.mm proof of supexd uses rmorabex</TD>
 </TR>
 
 <TR>
@@ -4523,8 +4523,7 @@
 
 <TR>
   <TD>infexd , infex</TD>
-  <TD><I>none</I></TD>
-  <TD>See supexd</TD>
+  <TD>~ infex2g</TD>
 </TR>
 
 <TR>