suggestion, fix hypotheses [skip ci]

two trivial shortenings

---

I started working towards proving case B:
https://en.wikipedia.org/wiki/Proof_of_Fermat%27s_Last_Theorem_for_specific_exponents#Proof_for_case_B

However, it's at least three times as long as case A. So I'm stopping and committing a few fixes before switching to https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html

Author: icecream17

set.mm

@@ -131737,8 +131737,8 @@ nonnegative integers (cont.)". $)
   $( Membership of the least member in an upper set of integers.  (Contributed
      by NM, 2-Sep-2005.) $)
   uzid $p |- ( M e. ZZ -> M e. ( ZZ>= ` M ) ) $=
-    ( cz wcel cuz cfv cle wbr wa zre leidd ancli eluz1 mpbird ) ABCZAADECNAAFGZ
-    HNONAAIJKAALM $.
+    ( cz wcel cuz cfv cle wbr id zre leidd eluz1 mpbir2and ) ABCZAADECMAAFGMHMA
+    AIJAAKL $.
 
   ${
     uzidd.1 $e |- ( ph -> M e. ZZ ) $.
@@ -523485,9 +523485,9 @@ Real and complex numbers (cont.)
      Fenton, 8-Apr-2014.)  (Revised by Mario Carneiro, 19-Apr-2014.) $)
   gcd32 $p |- ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ->
     ( ( A gcd B ) gcd C ) = ( ( A gcd C ) gcd B ) ) $=
-    ( cz wcel w3a cgcd co wceq wa gcdcom oveq2d 3adant1 gcdass 3com23 3eqtr4d )
-    ADEZBDEZCDEZFABCGHZGHZACBGHZGHZABGHCGHACGHBGHZRSUAUCIQRSJTUBAGBCKLMCBANQSRU
-    DUCIBCANOP $.
+    ( cz wcel w3a cgcd co wceq gcdcom 3adant1 oveq2d gcdass 3com23 3eqtr4d ) AD
+    EZBDEZCDEZFZABCGHZGHACBGHZGHZABGHCGHACGHBGHZSTUAAGQRTUAIPBCJKLCBAMPRQUCUBIB
+    CAMNO $.
 
   $( Absorption law for gcd.  (Contributed by Scott Fenton, 8-Apr-2014.)
      (Revised by Mario Carneiro, 19-Apr-2014.) $)
@@ -647581,7 +647581,7 @@ standardize vectors to a length (norm) of one, but such definitions require
 
     prjspnenm1.f $e |- F = ??? $.
     prjspnenm1.g $e |- G = ??? $.
-    @( The canonical bijection between an n-dimensional projective K-space and
+    @( The canonical bijection from an n-dimensional projective K-space onto
        the disjoint union of the n-dimensional affine K-space and the
        (n-1)-dimensional projective space (its "hypersurface at infinity").
        (Contributed by SN, ??-???-202?.) @)
@@ -647843,59 +647843,78 @@ standardize vectors to a length (norm) of one, but such definitions require
   $}
 
   ${
-    fltdvdsabdvdsc.s $e |- ( ph -> S e. NN ) $.
     fltdvdsabdvdsc.a $e |- ( ph -> A e. NN ) $.
     fltdvdsabdvdsc.b $e |- ( ph -> B e. NN ) $.
     fltdvdsabdvdsc.c $e |- ( ph -> C e. NN ) $.
     fltdvdsabdvdsc.n $e |- ( ph -> N e. NN ) $.
     fltdvdsabdvdsc.1 $e |- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) ) $.
     $( Any factor of both ` A ` and ` B ` also divides ` C ` .  This
-       establishes the validity of ~ fltabcoprm .  (Contributed by SN,
+       establishes the validity of ~ fltabcoprmex .  (Contributed by SN,
        21-Aug-2024.) $)
     fltdvdsabdvdsc $p |- ( ph -> ( A gcd B ) || C ) $=
-      ( co cdvds wbr cexp cn wcel nnexpcld nnzd caddc gcdnncl syl2anc nnnn0d cz
+      ( co cdvds wbr cexp cn wcel syl2anc nnexpcld nnzd cz caddc gcdnncl nnnn0d
       wa gcddvds simpld dvdsexpad simprd dvds2addd breqtrd wb dvdsexpnn syl3anc
-      cgcd mpbird ) ABCUPMZDNOZURFPMZDFPMZNOZAUTBFPMZCFPMZUAMVANAUTVCVDAUTAURFA
-      BQRCQRURQRZHIBCUBUCZAFKUDZSTAURBFAURVFTZABHTZVGAURBNOZURCNOZABUERCUERVJVK
-      UFVIACITZBCUGUCZUHUIAURCFVHVLVGAVJVKVMUJUIAVCABFHVGSTAVDACFIVGSTUKLULAVED
-      QRFQRUSVBUMVFJKURDFUNUOUQ $.
+      cgcd mpbird ) ABCUNKZDLMZUPENKZDENKZLMZAURBENKZCENKZUAKUSLAURVAVBAURAUPEA
+      BOPCOPUPOPZFGBCUBQZAEIUCZRSAUPBEAUPVDSZABFSZVEAUPBLMZUPCLMZABTPCTPVHVIUDV
+      GACGSZBCUEQZUFUGAUPCEVFVJVEAVHVIVKUHUGAVAABEFVERSAVBACEGVERSUIJUJAVCDOPEO
+      PUQUTUKVDHIUPDEULUMUO $.
   $}
 
   ${
-    fltabcoprm.s $e |- ( ph -> S e. NN ) $.
-    fltabcoprm.a $e |- ( ph -> A e. NN ) $.
-    fltabcoprm.b $e |- ( ph -> B e. NN ) $.
-    fltabcoprm.c $e |- ( ph -> C e. NN ) $.
-    fltabcoprm.n $e |- ( ph -> N e. NN0 ) $.
-    fltabcoprm.1 $e |- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) ) $.
+    fltabcoprmex.a $e |- ( ph -> A e. NN ) $.
+    fltabcoprmex.b $e |- ( ph -> B e. NN ) $.
+    fltabcoprmex.c $e |- ( ph -> C e. NN ) $.
+    fltabcoprmex.n $e |- ( ph -> N e. NN0 ) $.
+    fltabcoprmex.1 $e |- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) ) $.
     $( A counterexample to FLT implies a counterexample to FLT with ` A , B `
        (assigned to ` A / ( A gcd B ) ` and ` B / ( A gcd B ) ` ) coprime (by
        ~ divgcdcoprm0 ).  (Contributed by SN, 20-Aug-2024.) $)
-    fltabcoprm $p |- ( ph -> ( ( ( A / ( A gcd B ) ) ^ N )
+    fltabcoprmex $p |- ( ph -> ( ( ( A / ( A gcd B ) ) ^ N )
                              + ( ( B / ( A gcd B ) ) ^ N ) )
                              = ( ( C / ( A gcd B ) ) ^ N ) ) $=
-      ( cgcd co cn wcel gcdnncl syl2anc nncnd nnne0d fltdiv ) ABCDBCMNZFAUBABOP
-      COPUBOPHIBCQRZSAUBUCTABHSACISADJSKLUA $.
+      ( cgcd co cn wcel gcdnncl syl2anc nncnd nnne0d fltdiv ) ABCDBCKLZEATABMNC
+      MNTMNFGBCOPZQATUARABFQACGQADHQIJS $.
 
     $d A i $.  $d B i $.  $d C i $.  $d ph i $.
     fltaccoprm.1 $e |- ( ph -> ( A gcd B ) = 1 ) $.
     $( A counterexample to FLT with ` A , B ` coprime also has ` A , C `
        coprime (and by commutativity, ` B , C ` ).  (Contributed by SN,
        20-Aug-2024.) $)
     fltaccoprm $p |- ( ph -> ( A gcd C ) = 1 ) $=
-      ( vi cdvds wbr cn co wcel cz cv wa c1 wceq wi wral cgcd coprmgcdb syl2anc
-      wb mpbird simprl cexp cmin simpr adantr dvdsexpim syl3anc anim12d ancomsd
-      cn0 nnzd imp nnexpcld ad2antrr dvds2sub mpd nncnd expcld laddrotrd simplr
-      breqtrd flt0 dvdsexpnn jca ex imim1d ralimdva mpbid ) ANUAZBOPZVTDOPZUBZV
-      TUCUDZUEZNQUFZBDUGRUCUDZAWAVTCOPZUBZWDUEZNQUFZWFAWKBCUGRUCUDZMABQSZCQSZWK
-      WLUJHIBCNUHUIUKAWJWENQAVTQSZUBZWCWIWDWPWCWIWPWCUBZWAWHWPWAWBULWQWHVTFUMRZ
-      CFUMRZOPZWQWRDFUMRZBFUMRZUNRZWSOWQWRXAOPZWRXBOPZUBZWRXCOPZWPWCXFWPWBWAXFW
-      PWBXDWAXEWPVTTSZDTSZFVASZWBXDUEWPVTAWOUOZVBZAXIWOADJVBUPAXJWOKUPZVTDFUQUR
-      WPXHBTSZXJWAXEUEXLAXNWOABHVBUPXMVTBFUQURUSUTVCWQWRTSZXATSZXBTSZXFXGUEWPXO
-      WCWPWRWPVTFXKXMVDVBUPAXPWOWCAXAADFJKVDVBVEAXQWOWCAXBABFHKVDVBVEWRXAXBVFUR
-      VGAXCWSUDWOWCAXBWSXAABFABHVHZKVIACFACIVHZKVILVJVEVLWQWOWNFQSZWHWTUJAWOWCV
-      KAWNWOWCIVEAXTWOWCABCDFXRXSADJVHKLVMVEVTCFVNURUKVOVPVQVRVGAWMDQSWFWGUJHJB
-      DNUHUIVS $.
+      ( vi cdvds wbr wa cn co wcel cz nnzd cv c1 wceq wi wral cgcd wb coprmgcdb
+      syl2anc mpbird simprl cexp simpr adantr dvdsexpim syl3anc anim12d ancomsd
+      cmin cn0 imp nnexpcld ad2antrr dvds2sub mpd nncnd expcld laddrotrd simplr
+      breqtrd flt0 dvdsexpnn jca ex imim1d ralimdva mpbid ) ALUAZBMNZVRDMNZOZVR
+      UBUCZUDZLPUEZBDUFQUBUCZAVSVRCMNZOZWBUDZLPUEZWDAWIBCUFQUBUCZKABPRZCPRZWIWJ
+      UGFGBCLUHUIUJAWHWCLPAVRPRZOZWAWGWBWNWAWGWNWAOZVSWFWNVSVTUKWOWFVREULQZCEUL
+      QZMNZWOWPDEULQZBEULQZUSQZWQMWOWPWSMNZWPWTMNZOZWPXAMNZWNWAXDWNVTVSXDWNVTXB
+      VSXCWNVRSRZDSRZEUTRZVTXBUDWNVRAWMUMZTZAXGWMADHTUNAXHWMIUNZVRDEUOUPWNXFBSR
+      ZXHVSXCUDXJAXLWMABFTUNXKVRBEUOUPUQURVAWOWPSRZWSSRZWTSRZXDXEUDWNXMWAWNWPWN
+      VREXIXKVBTUNAXNWMWAAWSADEHIVBTVCAXOWMWAAWTABEFIVBTVCWPWSWTVDUPVEAXAWQUCWM
+      WAAWTWQWSABEABFVFZIVGACEACGVFZIVGJVHVCVJWOWMWLEPRZWFWRUGAWMWAVIAWLWMWAGVC
+      AXRWMWAABCDEXPXQADHVFIJVKVCVRCEVLUPUJVMVNVOVPVEAWKDPRWDWEUGFHBDLUHUIVQ $.
+  $}
+
+  ${
+    $d A i $.  $d B i $.  $d C i $.  $d ph i $.
+    fltabcoprm.a $e |- ( ph -> A e. NN ) $.
+    fltabcoprm.b $e |- ( ph -> B e. NN ) $.
+    fltabcoprm.c $e |- ( ph -> C e. NN ) $.
+    fltabcoprm.2 $e |- ( ph -> ( A gcd C ) = 1 ) $.
+    fltabcoprm.3 $e |- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) $.
+    $( A counterexample to FLT with ` A , C ` coprime also has ` A , B `
+       coprime.  Converse of ~ fltaccoprm . (Contributed by SN,
+       22-Aug-2024.) $)
+    fltabcoprm $p |- ( ph -> ( A gcd B ) = 1 ) $=
+      ( vi cdvds wbr wa wceq cn co wcel wb syl2anc c2 cv c1 wral cgcd coprmgcdb
+      wi mpbird simprl cexp caddc simplr nnsqcld nnzd ad2antrr dvdssqlem simprr
+      mpbid dvds2addd breqtrd jca ex imim1d ralimdva mpd ) AJUAZBKLZVECKLZMZVEU
+      BNZUFZJOUCZBCUDPUBNZAVFVEDKLZMZVIUFZJOUCZVKAVPBDUDPUBNZHABOQZDOQZVPVQREGB
+      DJUESUGAVOVJJOAVEOQZMZVHVNVIWAVHVNWAVHMZVFVMWAVFVGUHZWBVMVETUIPZDTUIPZKLZ
+      WBWDBTUIPZCTUIPZUJPZWEKWBWDWGWHWBWDWBVEAVTVHUKZULUMWBVFWDWGKLZWCWBVTVRVFW
+      KRWJAVRVTVHEUNZVEBUOSUQWBVGWDWHKLZWAVFVGUPWBVTCOQZVGWMRWJAWNVTVHFUNZVECUO
+      SUQWBWGWBBWLULUMWBWHWBCWOULUMURAWIWENVTVHIUNUSWBVTVSVMWFRWJAVSVTVHGUNVEDU
+      OSUGUTVAVBVCVDAVRWNVKVLREFBCJUESUQ $.
   $}
 
   ${
@@ -647955,7 +647974,6 @@ standardize vectors to a length (norm) of one, but such definitions require
   $}
 
   ${
-    $d A i $.  $d B i $.  $d C i $.  $d ph i $.
     flt4lem1.a $e |- ( ph -> A e. NN ) $.
     flt4lem1.b $e |- ( ph -> B e. NN ) $.
     flt4lem1.c $e |- ( ph -> C e. NN ) $.
@@ -647968,20 +647986,69 @@ standardize vectors to a length (norm) of one, but such definitions require
     flt4lem1 $p |- ( ph -> ( ( A e. NN /\ B e. NN /\ C e. NN ) /\
                            ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) /\
                            ( ( A gcd B ) = 1 /\ -. 2 || A ) ) ) $=
-      ( vi cn wcel c2 co cdvds wbr wa wb syl2anc w3a cexp caddc wceq cgcd c1 wn
-      3jca cv wi wral coprmgcdb mpbird simprl simplr nnsqcld ad2antrr dvdssqlem
-      nnzd mpbid simprr dvds2addd breqtrd jca ex imim1d ralimdva mpd ) ABLMZCLM
-      ZDLMZUABNUBOZCNUBOZUCOZDNUBOZUDZBCUEOUFUDZNBPQUGZRAVIVJVKEFGUHJAVQVRAKUIZ
-      BPQZVSCPQZRZVSUFUDZUJZKLUKZVQAVTVSDPQZRZWCUJZKLUKZWEAWIBDUEOUFUDZIAVIVKWI
-      WJSEGBDKULTUMAWHWDKLAVSLMZRZWBWGWCWLWBWGWLWBRZVTWFWLVTWAUNZWMWFVSNUBOZVOP
-      QZWMWOVNVOPWMWOVLVMWMWOWMVSAWKWBUOZUPUSWMVTWOVLPQZWNWMWKVIVTWRSWQAVIWKWBE
-      UQZVSBURTUTWMWAWOVMPQZWLVTWAVAWMWKVJWAWTSWQAVJWKWBFUQZVSCURTUTWMVLWMBWSUP
-      USWMVMWMCXAUPUSVBAVPWKWBJUQVCWMWKVKWFWPSWQAVKWKWBGUQVSDURTUMVDVEVFVGVHAVI
-      VJWEVQSEFBCKULTUTHVDUH $.
+      ( cn wcel w3a c2 cexp co caddc wceq cgcd 3jca c1 cdvds wbr fltabcoprm jca
+      wn wa ) ABKLZCKLZDKLZMBNOPCNOPQPDNOPRBCSPUARZNBUBUCUFZUGAUHUIUJEFGTJAUKUL
+      ABCDEFGIJUDHUET $.
   $}
 
   ${
     $d A i $.  $d B i $.  $d C i $.  $d ph i $.
+    flt4lem2.a $e |- ( ph -> A e. NN ) $.
+    flt4lem2.b $e |- ( ph -> B e. NN ) $.
+    flt4lem2.c $e |- ( ph -> C e. NN ) $.
+    flt4lem2.1 $e |- ( ph -> 2 || A ) $.
+    flt4lem2.2 $e |- ( ph -> ( A gcd C ) = 1 ) $.
+    flt4lem2.3 $e |- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) $.
+    $( If ` A ` is even, ` B ` is odd.  (Contributed by SN, 22-Aug-2024.) $)
+    flt4lem2 $p |- ( ph -> -. 2 || B ) $=
+      ( vi c2 cdvds wbr wa wcel cz adantr cn nnzd cgcd co c1 wceq wn wne cv cuz
+      cfv wrex breq1 anbi12d 2z uzid ax-mp a1i simpr dvdsgcd syl3anc mp2and 2nn
+      wi fltdvdsabdvdsc gcdnncl syl2anc dvdstr rspcedvdw wb ncoprmgcdne1b mpbid
+      jca ex necon2bd mpd ) ABDUAUBZUCUDLCMNZUEIAVPVOUCAVPVOUCUFZAVPOZKUGZBMNZV
+      SDMNZOZKLUHUIZUJZVQVRWBLBMNZLDMNZOKLWCVSLUDVTWEWAWFVSLBMUKVSLDMUKULLWCPZV
+      RLQPZWGUMLUNUOUPVRWEWFAWEVPHRZVRLBCUAUBZMNZWJDMNZWFVRWEVPWKWIAVPUQVRWHBQP
+      CQPZWEVPOWKVBWHVRUMUPZVRBABSPZVPERZTAWMVPACFTRLBCURUSUTAWLVPABCDLEFGLSPAV
+      AUPJVCRVRWHWJQPZDQPWKWLOWFVBWNAWQVPAWJAWOCSPWJSPEFBCVDVETRVRDADSPZVPGRZTL
+      WJDVFUSUTVKVGVRWOWRWDVQVHWPWSBDKVIVEVJVLVMVN $.
+  $}
+
+  ${
+    flt4lem3.a $e |- ( ph -> A e. NN ) $.
+    flt4lem3.b $e |- ( ph -> B e. NN ) $.
+    flt4lem3.c $e |- ( ph -> C e. NN ) $.
+    flt4lem3.1 $e |- ( ph -> 2 || A ) $.
+    flt4lem3.2 $e |- ( ph -> ( A gcd C ) = 1 ) $.
+    flt4lem3.3 $e |- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) $.
+    $( Equivalent to ~ pythagtriplem4 .  Show that ` C + A ` and ` C - A ` are
+       coprime.  (Contributed by SN, 22-Aug-2024.) $)
+    flt4lem3 $p |- ( ph -> ( ( C + A ) gcd ( C - A ) ) = 1 ) $=
+      ( caddc co cgcd c1 cz wcel wceq cn c2 cexp zaddcld zsubcld gcdcom syl2anc
+      cmin nnzd w3a cdvds wbr wn wa flt4lem2 flt4lem1 pythagtriplem4 syl eqtrd
+      ) ADBKLZDBUELZMLZURUQMLZNAUQOPUROPUSUTQADBADGUFZABEUFZUAADBVAVBUBUQURUCUD
+      ACRPBRPDRPUGCSTLBSTLKLDSTLQCBMLNQSCUHUIUJUKUGUTNQACBDFEGABCDEFGHIJUL??UMC
+      BDUNUOUP $.
+  $}
+
+  ${
+    $d ph s $.  $d ph t $.
+    flt4lem4.a $e |- ( ph -> A e. NN ) $.
+    flt4lem4.b $e |- ( ph -> B e. NN ) $.
+    flt4lem4.c $e |- ( ph -> C e. NN ) $.
+    flt4lem4.1 $e |- ( ph -> ( A gcd B ) = 1 ) $.
+    flt4lem4.2 $e |- ( ph -> ( A x. B ) = ( C ^ 2 ) ) $.
+    $( If the product of two coprime factors is a perfect square, the factors
+       are perfect squares.  (Contributed by SN, 22-Aug-2024.) $)
+    flt4lem4 $p |-
+      ( ph -> ( A = ( ( A gcd C ) ^ 2 ) /\ B = ( ( B gcd C ) ^ 2 ) ) ) $=
+      ( cgcd co c2 cexp wceq cn0 wcel cz c1 wi nnnn0d eqcomd nn0zd oveq1d eqtrd
+      cmul 1gcd syl coprimeprodsq syl31anc mpd nnzd coprimeprodsq2 jca ) ABBDJK
+      LMKNZCCDJKLMKNZADLMKZBCUEKZNZUNAUQUPIUAZABOPCQPDOPZBCJKZDJKZRNZURUNSABETA
+      CACFTZUBADGTZAVBRDJKZRAVARDJHUCADQPVFRNADVEUBDUFUGUDZBCDUHUIUJAURUOUSABQP
+      COPUTVCURUOSABEUKVDVEVGBCDULUIUJUM $.
+  $}
+
+
+  ${
     flt4lem6a.a $e |- ( ph -> A e. NN ) $.
     flt4lem6a.b $e |- ( ph -> B e. NN ) $.
     flt4lem6a.c $e |- ( ph -> C e. NN ) $.
@@ -648038,7 +648105,7 @@ standardize vectors to a length (norm) of one, but such definitions require
     $( Construct a smaller counterexample when ` A ` is even.  (Contributed by
        SN, 21-Aug-2024.) $)
     flt4lem6b $p |- ( ph -> ? ) $=
-      ? $.
+      (  ) ? $.
   $}
 
   ${
@@ -648052,8 +648119,8 @@ standardize vectors to a length (norm) of one, but such definitions require
        by SN, 20-Aug-2024.) $)
     flt4lem6 $p |- ( ph -> E. z e. NN ( E. d e. NN E. e e. NN (
          ( d gcd z ) = 1 /\ ( ( d ^ 4 ) + ( e ^ 2 ) ) = ( z ^ 4 ) ) /\
-         z < C ) $=
-      ? $.
+         z < C ) ) $=
+      (  ) ? $.
   $}
 
   ${