Add odzphi to iset.mm

Copied without change from set.mm.
metamath · Oct 3, 2024 · 74f3a86 · 74f3a86
1 parent 75176ad
commit 74f3a86
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/iset.mm b/iset.mm
@@ -135536,6 +135536,16 @@ and the outer argument selects the integer or equivalence class (if you
       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 $.
   $}