make fltne more general

I've decided that when a general proof is easier to prove, the statement will be more general

Author: icecream17

set.mm

@@ -647524,7 +647524,7 @@ standardize vectors to a length (norm) of one, but such definitions require
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
-Equivalent formulations of Fermat's Last Theorem
+Basic reductions for Fermat's Last Theorem
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
 $)
 
@@ -647864,25 +647864,31 @@ standardize vectors to a length (norm) of one, but such definitions require
     fltne.a $e |- ( ph -> A e. NN ) $.
     fltne.b $e |- ( ph -> B e. NN ) $.
     fltne.c $e |- ( ph -> C e. NN ) $.
-    fltne.n $e |- ( ph -> N e. ( ZZ>= ` 3 ) ) $.
+    fltne.n $e |- ( ph -> N e. ( ZZ>= ` 2 ) ) $.
     fltne.1 $e |- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) ) $.
     $( If a counterexample to FLT exists, its addends are not equal.
-       (Contributed by Steven Nguyen, 1-Jun-2023.) $)
+       (Contributed by SN, 1-Jun-2023.) $)
     fltne $p |- ( ph -> A =/= B ) $=
-      ( c2 cdiv co cq wcel wne syl wceq adantr cexp c1 ccxp cprime cuz cfv cdif
-      wn cr 2prm a1i c3 uzuzle23 rtprmirr syl2anc eldifbd wi cz nnzd znq eleq1a
-      cn necon3bd mpd wa crp eluzge3nn nnrecred rpcxpcld nnrpd rpdivcld eluzelz
-      2rp simpl 3syl cc0 nnne0d cc nncnd nnnn0d 2cnd expne0d cmul caddc times2d
-      expcld simpr oveq1d oveq2d 3eqtrd mvllmuld cxproot expdivd 3eqtr4d exp11d
-      mteqand ) ABCKUAELMZUBMZDBLMZAWQNOZUGWQWRPAWQUHNAKUCOZEKUDUEOZWQUHNUFOWTA
-      UIUJAEUKUDUEOZXAIEULQKEUMUNUOAWSWQWRAWRNOZWQWRRWSUPADUQOBVAOXCADHURFDBUSU
-      NWRNWQUTQVBVCABCRZVDZWQWREAWQVEOXDAKWPKVEOAVLUJAEAXBEVAOZIEVFQZVGVHSAWRVE
-      OXDADBADHVIABFVIVJSXEAXBEUQOZAXDVMIUKEVKZVNAEVOPXDAEXGVPSXEKDETMZBETMZLMZ
-      WQETMZWRETMZXEXKKXJAXKVQOXDABEABFVRZAEXGVSZWESZXEVTZAXKVOPXDABEXOABFVPZAX
-      BXHIXIQWASXEXKKWBMXKXKWCMXKCETMZWCMZXJXEXKXQWDXEXKXTXKWCXEBCETAXDWFWGWHAY
-      AXJRXDJSWIWJXEKVQOXFXMKRXRAXFXDXGSKEWKUNAXNXLRXDADBEADHVRXOXSXPWLSWMWNWO
-      $.
-
+      ( c2 cdiv co cq wcel wceq cn adantr cexp nncnd c1 ccxp wne cprime cuz cfv
+      wn cr cdif 2prm rtprmirr sylancr eldifbd nnzd znq syl2anc eleq1a necon3bd
+      wi cz syl mpd crp 2rp a1i eluz2nn nnrecred rpcxpcld nnrpd rpdivcld nnne0d
+      wa nnnn0d nnexpcld 2cnd caddc times2d simpr oveq1d oveq2d 3eqtrd mvllmuld
+      cmul cc 2cn cxproot expdivd 3eqtr4d exp11d mteqand ) ABCKUAELMZUBMZDBLMZA
+      WLNOZUGWLWMUCAWLUHNAKUDOEKUEUFOZWLUHNUIOUJIKEUKULUMAWNWLWMAWMNOZWLWMPWNUS
+      ADUTOBQOWPADHUNFDBUOUPWMNWLUQVAURVBABCPZVLZWLWMEAWLVCOWQAKWKKVCOAVDVEAEAW
+      OEQOZIEVFVAZVGVHRAWMVCOWQADBADHVIABFVIVJRWREAWSWQWTRZUNWREXAVKWRKDESMZBES
+      MZLMZWLESMZWMESMZWRXCKXBWRXCAXCQOWQABEFAEWTVMZVNZRZTWRVOWRXCXIVKWRXCKWCMZ
+      XCXCVPMZXCCESMZVPMZXBAXJXKPWQAXCAXCXHTVQRWRXCXLXCVPWRBCESAWQVRVSVTAXMXBPW
+      QJRWAWBAXEKPZWQAKWDOWSXNWEWTKEWFULRAXFXDPWQADBEADHTABFTABFVKXGWGRWHWIWJ
+      $.
+  $}
+
+  ${
+    fltltc.a $e |- ( ph -> A e. NN ) $.
+    fltltc.b $e |- ( ph -> B e. NN ) $.
+    fltltc.c $e |- ( ph -> C e. NN ) $.
+    fltltc.n $e |- ( ph -> N e. ( ZZ>= ` 3 ) ) $.
+    fltltc.1 $e |- ( ph -> ( ( A ^ N ) + ( B ^ N ) ) = ( C ^ N ) ) $.
     $( ` ( C ^ N ) ` is the largest term and therefore ` B < C ` .
        (Contributed by Steven Nguyen, 22-Aug-2023.) $)
     fltltc $p |- ( ph -> B < C ) $=