prove flt4g

flt4 is left as an easy exercise (hint: mteqand)

proving flt4g first shows that the structure of flt4lem and flt4lem6 is correct, subsequent commits will prove the lemmas

Author: icecream17

set.mm

@@ -643230,6 +643230,23 @@ D Fn ( I ... ( M - 1 ) ) /\
       ( wcel wrex rspcev syl2anc ) AEFJCBDFKHIBCDEFGLM $.
   $}
 
+  ${
+    $d ch x $.  $d th y $.  $d ta z $.  $d A x y z $.  $d B y z $.  $d C z $.
+    $d X x $.  $d Y x y $.  $d Z x y z $.
+    3rspcedvdw.1 $e |- ( x = A -> ( ps <-> ch ) ) $.
+    3rspcedvdw.2 $e |- ( y = B -> ( ch <-> th ) ) $.
+    3rspcedvdw.3 $e |- ( z = C -> ( th <-> ta ) ) $.
+    3rspcedvdw.a $e |- ( ph -> A e. X ) $.
+    3rspcedvdw.b $e |- ( ph -> B e. Y ) $.
+    3rspcedvdw.c $e |- ( ph -> C e. Z ) $.
+    3rspcedvdw.4 $e |- ( ph -> ta ) $.
+    $( Triple application of ~ rspcedvdw .  (Contributed by SN,
+       20-Aug-2024.) $)
+    3rspcedvdw $p |- ( ph -> E. x e. X E. y e. Y E. z e. Z ps ) $=
+      ( wrex cv wceq 2rexbidv rexbidv rspcedvdw ) ABHNUBGMUBCHNUBZGMUBFILFUCIUD
+      BCGHMNOUERAUHDHNUBGJMGUCJUDCDHNPUFSADEHKNQTUAUGUGUG $.
+  $}
+
   ${
     $d ph x y z $.  $d ch x $.  $d th y $.  $d ta z $.  $d D x y z $.
     $d A x y z $.  $d B y z $.  $d C z $.
@@ -645339,6 +645356,18 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
     $( $j usage 'nnmulcom' avoids 'ax-mulcom'; $)
   $}
 
+  ${
+    laddrotrd.a $e |- ( ph -> A e. CC ) $.
+    laddrotrd.b $e |- ( ph -> B e. CC ) $.
+    laddrotrd.c $e |- ( ph -> C e. CC ) $.
+    laddrotrd.1 $e |- ( ph -> ( A + B ) = C ) $.
+    $( Rotate the variables right in an equation with addition on the left,
+       converting it into a subtraction.  ~ mvlladdd commuted.  (Contributed by
+       SN, 21-Aug-2024.) $)
+    laddrotrd $p |- ( ph -> ( C - A ) = B ) $=
+      ( cmin co mvlladdd eqcomd ) ACDBIJABCDEFHKL $.
+  $}
+
   $( Relation between sums and differences.  (Contributed by Steven Nguyen,
      5-Jan-2023.) $)
   addsubeq4com $p |- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) ->
@@ -645582,6 +645611,18 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
       VMATUJVAVCVMUKULUMVGVOVJVIIVFBCPUNUOUPUQURUS $.
   $}
 
+  ${
+    dvdsexpad.1 $e |- ( ph -> A e. ZZ ) $.
+    dvdsexpad.2 $e |- ( ph -> B e. ZZ ) $.
+    dvdsexpad.3 $e |- ( ph -> N e. NN0 ) $.
+    dvdsexpad.5 $e |- ( ph -> A || B ) $.
+    $( Deduction associated with ~ dvdsexpim .  (Contributed by SN,
+       21-Aug-2024.) $)
+    dvdsexpad $p |- ( ph -> ( A ^ N ) || ( B ^ N ) ) $=
+      ( cdvds wbr cexp co cz wcel cn0 wi dvdsexpim syl3anc mpd ) ABCIJZBDKLCDKL
+      IJZHABMNCMNDONTUAPEFGBCDQRS $.
+  $}
+
   $( If ` A ` and ` B ` are relatively prime, then so are ` A ^ N ` and
      ` B ^ N ` . ~ rppwr extended to nonnegative integers.  (Contributed by
      Steven Nguyen, 4-Apr-2023.) $)
@@ -645719,7 +645760,7 @@ number axioms (add ~ ax-10 , ~ ax-11 , ~ ax-13 , ~ ax-nul , and remove
 
   $( ~ dvdssqlem generalized to positive integer exponents.  (Contributed by
      SN, 20-Aug-2024.) $)
-  dvdsexplem $p |- ( ( A e. NN /\ B e. NN /\ N e. NN ) ->
+  dvdsexpnn $p |- ( ( A e. NN /\ B e. NN /\ N e. NN ) ->
                                     ( A || B <-> ( A ^ N ) || ( B ^ N ) ) ) $=
     ( cn wcel w3a cdvds wbr cexp co cz cn0 nnz wa nnrpd 3adant3 adantr nnexpcld
     cgcd wceq wi nnnn0 dvdsexpim syl3an crp gcdnncl simpl1 simpl3 nnne0d expgcd
@@ -647782,45 +647823,44 @@ standardize vectors to a length (norm) of one, but such definitions require
       ( 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 imp nnexpcld ad2antrr dvds2sub mpd nncnd expcld caddc eqcomd mvrladdd
-      nnzd breqtrd simplr flt0 dvdsexplem jca ex imim1d ralimdva mpbid ) ANUAZB
-      OPZWBDOPZUBZWBUCUDZUEZNQUFZBDUGRUCUDZAWCWBCOPZUBZWFUEZNQUFZWHAWMBCUGRUCUD
-      ZMABQSZCQSZWMWNUJHIBCNUHUIUKAWLWGNQAWBQSZUBZWEWKWFWRWEWKWRWEUBZWCWJWRWCWD
-      ULWSWJWBFUMRZCFUMRZOPZWSWTDFUMRZBFUMRZUNRZXAOWSWTXCOPZWTXDOPZUBZWTXEOPZWR
-      WEXHWRWDWCXHWRWDXFWCXGWRWBTSZDTSZFVASZWDXFUEWRWBAWQUOZVLZAXKWQADJVLUPAXLW
-      QKUPZWBDFUQURWRXJBTSZXLWCXGUEXNAXPWQABHVLUPXOWBBFUQURUSUTVBWSWTTSZXCTSZXD
-      TSZXHXIUEWRXQWEWRWTWRWBFXMXOVCVLUPAXRWQWEAXCADFJKVCVLVDAXSWQWEAXDABFHKVCV
-      LVDWTXCXDVEURVFAXEXAUDWQWEAXCXDXAABFABHVGZKVHACFACIVGZKVHAXDXAVIRXCLVJVKV
-      DVMWSWQWPFQSZWJXBUJAWQWEVNAWPWQWEIVDAYBWQWEABCDFXTYAADJVGKLVOVDWBCFVPURUK
-      VQVRVSVTVFAWODQSWHWIUJHJBDNUHUIWA $.
-  $}
-
-  ${
-    $d ph x z $.  $d ps x z $.  $d ch y $.  $d th y $.  $d A y z $.
-    $d S x y z $.
-    flt4lem.1 $e |- ( y = x -> ( ps <-> ch ) ) $.
-    flt4lem.2 $e |- ( y = A -> ( ps <-> th ) ) $.
-    flt4lem.3 $e |- ( ph -> S C_ ( ZZ>= ` M ) ) $.
-    flt4lem.4 $e |- ( ( ph /\ ( x e. S /\ ch ) ) -> A e. S ) $.
-    flt4lem.5 $e |- ( ( ph /\ ( x e. S /\ ch ) ) -> th ) $.
-    flt4lem.6 $e |- ( ( ph /\ ( x e. S /\ ch ) ) -> A < x ) $.
+      nnzd breqtrd simplr flt0 dvdsexpnn jca ex imim1d ralimdva mpbid ) ANUAZBO
+      PZWBDOPZUBZWBUCUDZUEZNQUFZBDUGRUCUDZAWCWBCOPZUBZWFUEZNQUFZWHAWMBCUGRUCUDZ
+      MABQSZCQSZWMWNUJHIBCNUHUIUKAWLWGNQAWBQSZUBZWEWKWFWRWEWKWRWEUBZWCWJWRWCWDU
+      LWSWJWBFUMRZCFUMRZOPZWSWTDFUMRZBFUMRZUNRZXAOWSWTXCOPZWTXDOPZUBZWTXEOPZWRW
+      EXHWRWDWCXHWRWDXFWCXGWRWBTSZDTSZFVASZWDXFUEWRWBAWQUOZVLZAXKWQADJVLUPAXLWQ
+      KUPZWBDFUQURWRXJBTSZXLWCXGUEXNAXPWQABHVLUPXOWBBFUQURUSUTVBWSWTTSZXCTSZXDT
+      SZXHXIUEWRXQWEWRWTWRWBFXMXOVCVLUPAXRWQWEAXCADFJKVCVLVDAXSWQWEAXDABFHKVCVL
+      VDWTXCXDVEURVFAXEXAUDWQWEAXCXDXAABFABHVGZKVHACFACIVGZKVHAXDXAVIRXCLVJVKVD
+      VMWSWQWPFQSZWJXBUJAWQWEVNAWPWQWEIVDAYBWQWEABCDFXTYAADJVGKLVOVDWBCFVPURUKV
+      QVRVSVTVFAWODQSWHWIUJHJBDNUHUIWA $.
+  $}
+
+  ${
+    $d ph x z $.  $d ps x z $.  $d ch y $.  $d th y $.  $d S x y z $.
+    flt4lem.x $e |- ( y = x -> ( ps <-> ch ) ) $.
+    flt4lem.z $e |- ( y = z -> ( ps <-> th ) ) $.
+    flt4lem.s $e |- ( ph -> S C_ ( ZZ>= ` M ) ) $.
+    flt4lem.1 $e |-
+        ( ( ph /\ ( x e. S /\ ch ) ) -> E. z e. S ( th /\ z < x ) ) $.
     $( Infinite descent.  The hypotheses say that ` S ` is lower bounded, and
        that if ` ps ` holds for an integer in ` S ` , it holds for a smaller
        integer in ` S ` .  By infinite descent, eventually we cannot go any
        smaller, therefore ` ps ` holds for no integer in ` S ` .  (Contributed
        by SN, 20-Aug-2024.)  $)
     flt4lem $p |- ( ph -> { y e. S | ps } = (/) ) $=
-      ( vz c0 wn wa cr crab wceq wne df-ne cle wbr wral wrex cuz cfv wss ssrab2
-      sstrid uzwo sylan wcel elrab breq2 notbid elrabd clt uzssre sstrdi adantr
-      cv sseldd sselda adantrr ltnled rspcedvdw sylan2b ralrimiva rexnal ralbii
-      mpbid ralnex bitri sylib pm2.21dd sylan2br pm2.18da ) ABFHUAZQUBZWCRAWBQU
-      CZWCWBQUDAWDSEVEZPVEZUEUFZPWBUGZEWBUHZWCAWBIUIUJZUKWDWIAWBHWJBFHULLUMWBEP
-      IUNUOAWIRZWDAWGRZPWBUHZEWBUGZWKAWMEWBWEWBUPAWEHUPZCSZWMBCFWEHJUQAWPSZWLWE
-      GUEUFZRZPGWBWFGUBWGWRWFGWEUEURUSWQBDFGHKMNUTWQGWEVAUFWSOWQGWEWQHTGAHTUKWP
-      AHWJTLIVBVCZVDMVFAWOWETUPCAHTWEWTVGVHVIVOVJVKVLWNWHRZEWBUGWKWMXAEWBWGPWBV
-      MVNWHEWBVPVQVRVDVSVTWA $.
+      ( c0 wn wa wral wrex wcel cr crab wne df-ne cv cle wbr cuz cfv wss ssrab2
+      wceq sstrid uzwo sylan elrab wb uzssre sstrdi adantr sselda ltnled anbi2d
+      clt rexbidva adantrr sylan2b rexrab sylibr ralrimiva rexnal ralbii ralnex
+      mpbid bitri sylib pm2.21dd sylan2br pm2.18da ) ABFHUAZNUKZVTOAVSNUBZVTVSN
+      UCAWAPEUDZGUDZUEUFZGVSQZEVSRZVTAVSIUGUHZUIWAWFAVSHWGBFHUJLULVSEGIUMUNAWFO
+      ZWAAWDOZGVSRZEVSQZWHAWJEVSAWBVSSZPDWIPZGHRZWJWLAWBHSZCPZWNBCFWBHJUOAWPPDW
+      CWBVCUFZPZGHRZWNMAWOWSWNUPCAWOPZWRWMGHWTWCHSZPZWQWIDXBWCWBWTHTWCAHTUIWOAH
+      WGTLIUQURZUSUTWTWBTSXAAHTWBXCUTUSVAVBVDVEVMVFBDWIGFHKVGVHVIWKWEOZEVSQWHWJ
+      XDEVSWDGVSVJVKWEEVSVLVNVOUSVPVQVR $.
   $}
 
   ${
+    $d ph k m n $.  $d A k m n $.  $d B k m n $.  $d C k m n $.
     flt4lem2.a $e |- ( ph -> A e. NN ) $.
     flt4lem2.b $e |- ( ph -> B e. NN ) $.
     flt4lem2.c $e |- ( ph -> C e. NN ) $.
@@ -647848,10 +647888,10 @@ standardize vectors to a length (norm) of one, but such definitions require
     flt4lem3.b $e |- ( ph -> B e. NN ) $.
     flt4lem3.c $e |- ( ph -> C e. NN ) $.
     flt4lem3.1 $e |- ( ph -> A < B ) $.
-    flt4lem3.2 $e |- ( ph -> ( A gcd B ) = 1 ) $.
-    $( Add a coprime requirement, converting ~ pythagtrip into a
-       characterization of primitive Pythagorean triples.  (Contributed by SN,
-       20-Aug-2024.) $)
+    flt4lem3.2 $e |- ( ph -> ( A gcd C ) = 1 ) $.
+    $( Add a coprime requirement (between ` A , C ` to correspond with
+       ~ flt4lem6 ), converting ~ pythagtrip into a characterization of
+       primitive Pythagorean triples.  (Contributed by SN, 20-Aug-2024.) $)
     flt4lem3 $p |- ( ph -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) <->
        E. n e. NN E. m e. NN (
          A = ( ( m ^ 2 ) - ( n ^ 2 ) /\
@@ -647860,6 +647900,23 @@ standardize vectors to a length (norm) of one, but such definitions require
       ? $.
   $}
 
+  ${
+    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 < B ) $.
+    flt4lem4.2 $e |- ( ph -> ( A gcd C ) = 1 ) $.
+    $( In the characterization of primitive Pythagorean triples, ` m , n ` are
+       coprime (otherwise ` A , C ` would not be coprime).  (Contributed by SN,
+       20-Aug-2024.) $)
+    flt4lem4 $p |- ( ph -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) <->
+       E. n e. NN E. m e. NN ( ( n gcd m ) = 1 /\ (
+         A = ( ( m ^ 2 ) - ( n ^ 2 ) /\
+         B = ( 2 x. ( m x. n ) ) /\
+         C = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) ) $=
+      ? $.
+  $}
+
   ${
     fltne.a $e |- ( ph -> A e. NN ) $.
     fltne.b $e |- ( ph -> B e. NN ) $.
@@ -647883,6 +647940,123 @@ standardize vectors to a length (norm) of one, but such definitions require
       $.
   $}
 
+  ${
+    flt4lem5.a $e |- ( ph -> A e. NN ) $.
+    flt4lem5.b $e |- ( ph -> B e. NN ) $.
+    flt4lem5.c $e |- ( ph -> C e. NN ) $.
+    flt4lem5.2 $e |- ( ph -> ( A gcd C ) = 1 ) $.
+    flt4lem5.3 $e |- ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( C ^ 2 ) ) $.
+    $( By ~ fltne , we can assume ` A < B ` without loss of generality,
+       eliminating the hypothesis from ~ flt4lem2 .  (Contributed by SN,
+       20-Aug-2024.) $)
+    flt4lem5 $p |- ( ph -> E. n e. NN E. m e. NN ( ( n gcd m ) = 1 /\ (
+         A = ( ( m ^ 2 ) - ( n ^ 2 ) /\
+         B = ( 2 x. ( m x. n ) ) /\
+         C = ( ( m ^ 2 ) + ( n ^ 2 ) ) ) ) ) $=
+      ? $.
+  $}
+
+  ${
+    flt4lem6.a $e |- ( ph -> A e. NN ) $.
+    flt4lem6.b $e |- ( ph -> B e. NN ) $.
+    flt4lem6.c $e |- ( ph -> C e. NN ) $.
+    flt4lem6.2 $e |- ( ph -> ( A gcd C ) = 1 ) $.
+    flt4lem6.3 $e |- ( ph -> ( ( A ^ 4 ) + ( B ^ 2 ) ) = ( C ^ 4 ) ) $.
+    $( Given a solution to ` A ^ 4 + B ^ 2 = C ^ 4 ` , provide a smaller
+       solution.  This satisfies the infinite descent condition.  (Contributed
+       by SN, 20-Aug-2024.) $)
+    flt4lem6 $p |- ( ph -> E. n e. NN E. m e. NN (
+         ( n gcd m ) = 1 /\
+         m < C /\
+         ( ( n ^ 4 ) + ( ( A x. C ) ^ 2 ) ) = ( m ^ 4 ) ) ) $=
+      ? $.
+  $}
+
+  ${
+    $d ph a c $.  $d ph b $.  $d A a $.  $d A c $.  $d B a $.  $d B b c $.
+    $d C c $.  $d a b d e f $.  $d c d e f $.  $d e g h $.   $d e f x z $.
+    $d ph d g h x z $.
+    flt4g.a $e |- ( ph -> A e. NN ) $.
+    flt4g.b $e |- ( ph -> B e. NN ) $.
+    flt4g.c $e |- ( ph -> C e. NN ) $.
+    $( Fermat's last theorem for the exponent four, generalized.  This is
+       equivalent to Fermat's right triangle theorem.  (Contributed by SN,
+       20-Aug-2024.) $)
+    flt4g $p |- ( ph -> ( ( A ^ 4 ) + ( B ^ 2 ) ) =/= ( C ^ 4 ) ) $=
+      ( vd ve c4 cexp co c2 caddc wceq cn wrex wcel wa nncnd vc va vb vf vx wne
+      vz vg vh cv wn oveq1 eqeq2d necon3bbid crab c0 wss oveq1d eqeq1d ad2antrr
+      wral simpr rspcedvdw ex ss2rabdv oveq2d ad3antrrr reximdva cgcd weq oveq2
+      anbi12d 2rexbidv cuz cfv nnuz eqimssi a1i clt wbr rexbidv cbvrexvw anbi2d
+      c1 rexbii cmul w3a simprll simprlr simplr simprrl simprrr flt4lem6 rexcom
+      bitri anbi1d simp-5r nnmulcld simpr1 simpr3 simpr2 jca31 r19.40 reximi id
+      rexlimivw anim2i 3syl syl6 syl5bi expr rexlimdvva impr flt4lem cz simplrl
+      mpd cdiv simplrr nnzd divgcdnnr syl2anc divgcdnn cdvds cmin cn0 dvdsexpad
+      nnexpcld 2t2e4 oveq2i 2nn0 expmuld syl5eqr nnsqcld wb nnne0d sqdivd rabn0
+      3eqtr4d sseq0 gcdnncl 4nn0 gcddvds simprd simpld dvds2subd simprl 3brtr3d
+      simprr laddrotrd dvdssqlem mpbird nndivdvds mpbid cc0 divgcdcoprm0 biimpd
+      syl3anc eqeq12d fltdiv 3rspcedvdw rexlimdvaa 3imtr4g necon4d rabeq0 sylib
+      jca rspcdva ) ABJKLZCMKLZNLZUAUJZJKLZOZUKZUVKDJKLZUFUAPDUVLDOZUVNUVKUVPUV
+      QUVMUVPUVKUVLDJKULUMUNAUVNUAPUOZUPOZUVOUAPVAAUVRUBUJZJKLZUVJNLZUVMOZUBPQZ
+      UAPUOZUQUWEUPOZUVSAUVNUWDUAPAUVLPRZSZUVNUWDUWHUVNSUWCUVNUBBPUVTBOZUWBUVKU
+      VMUWIUWAUVIUVJNUVTBJKULURUSABPRUWGUVNEUTUWHUVNVBVCVDVEAUWEUWAUCUJZMKLZNLZ
+      UVMOZUCPQZUBPQZUAPUOZUQUWPUPOZUWFAUWDUWOUAPUWHUWCUWNUBPUWHUVTPRZSZUWCUWNU
+      WSUWCSUWMUWCUCCPUWJCOZUWLUWBUVMUWTUWKUVJUWANUWJCMKULVFUSACPRUWGUWRUWCFVGU
+      WSUWCVBVCVDVHVEAHUJZUDUJZVILZWDOZUXAJKLZIUJZMKLZNLZUXBJKLZOZSZIPQHPQZUDPU
+      OZUPOUWQAUXLUXAUEUJZVILZWDOZUXHUXNJKLZOZSZIPQZHPQZUXAUGUJZVILZWDOZUXHUYBJ
+      KLZOZSZIPQZHPQZUEUDUGPWDUDUEVJZUXKUXSHIPPUYJUXDUXPUXJUXRUYJUXCUXOWDUXBUXN
+      UXAVIVKUSUYJUXIUXQUXHUXBUXNJKULUMVLVMUDUGVJZUXKUYGHIPPUYKUXDUYDUXJUYFUYKU
+      XCUYCWDUXBUYBUXAVIVKUSUYKUXIUYEUXHUXBUYBJKULUMVLVMPWDVNVOZUQAPUYLVPVQVRAU
+      XNPRZUYAUYIUYBUXNVSVTZSZUGPQZUYAUHUJZUXNVILZWDOZUYQJKLZUIUJZMKLZNLZUXQOZS
+      ZUIPQZUHPQZAUYMSZUYPUYAUYSUYTUXGNLZUXQOZSZIPQZUHPQVUGUXTVULHUHPHUHVJZUXSV
+      UKIPVUMUXPUYSUXRVUJVUMUXOUYRWDUXAUYQUXNVIULUSVUMUXHVUIUXQVUMUXEUYTUXGNUXA
+      UYQJKULURUSVLWAWBVULVUFUHPVUKVUEIUIPIUIVJZVUJVUDUYSVUNVUIVUCUXQVUNUXGVUBU
+      YTNUXFVUAMKULVFUSWCWBWEWOVUHVUEUYPUHUIPPVUHUYQPRZVUAPRZSZVUEUYPVUHVUQVUES
+      ZSZUYDUYNUXEUYQUXNWFLZMKLZNLZUYEOZWGZUGPQHPQZUYPVUSUYQVUAUXNUGHVUHVUOVUPV
+      UEWHZVUHVUOVUPVUEWIAUYMVURWJVUHVUQUYSVUDWKVUHVUQUYSVUDWLWMVVEVVDHPQZUGPQV
+      USUYPVVDHUGPPWNVUSVVGUYOUGPVUSUYBPRZSZVVGUYGUYNSZIPQZHPQZUYOVVIVVDVVKHPVV
+      IUXAPRZSZVVDVVKVVNVVDSZVVJUYDVVCSZUYNSIVUTPUXFVUTOZUYGVVPUYNVVQUYFVVCUYDV
+      VQUXHVVBUYEVVQUXGVVAUXENUXFVUTMKULVFUSWCWPVVOUYQUXNVUSVUOVVHVVMVVDVVFVGAU
+      YMVURVVHVVMVVDWQWRVVOUYDVVCUYNVVNUYDUYNVVCWSVVNUYDUYNVVCWTVVNUYDUYNVVCXAX
+      BVCVDVHVVLUYHUYNIPQZSZHPQUYIVVRHPQZSUYOVVKVVSHPUYGUYNIPXCXDUYHVVRHPXCVVTU
+      YNUYIVVRUYNHPUYNUYNIPUYNXEXFXFXGXHXIVHXJXQXKXLXJXMXNAUWPUPUXMUPAUWOUAPQUX
+      LUDPQZUWPUPUFUXMUPUFAUWNVWAUAUBPPAUWGUWRSSZUWMVWAUCPVWBUWJPRZUWMSZSZUXKUX
+      AUVLUVTUVLVILZXRLZVILZWDOZUXHVWGJKLZOZSUVTVWFXRLZVWGVILZWDOZVWLJKLZUXGNLZ
+      VWJOZSVWNVWOUWJVWFMKLZXRLZMKLZNLZVWJOZSUDHIVWGVWLVWSPPPUXBVWGOZUXDVWIUXJV
+      WKVXCUXCVWHWDUXBVWGUXAVIVKUSVXCUXIVWJUXHUXBVWGJKULUMVLUXAVWLOZVWIVWNVWKVW
+      QVXDVWHVWMWDUXAVWLVWGVIULUSVXDUXHVWPVWJVXDUXEVWOUXGNUXAVWLJKULURUSVLUXFVW
+      SOZVWQVXBVWNVXEVWPVXAVWJVXEUXGVWTVWONUXFVWSMKULVFUSWCVWEUWGUVTXORZVWGPRAU
+      WGUWRVWDXPZVWEUVTAUWGUWRVWDXSZXTZUVLUVTYAYBZVWEUWRUVLXORZVWLPRVXHVWEUVLVX
+      GXTZUVTUVLYCYBZVWEVWRUWJYDVTZVWSPRZVWEVXNVWRMKLZUWKYDVTZVWEVWFJKLZUVMUWAY
+      ELVXPUWKYDVWEVXRUVMUWAVWEVXRVWEVWFJVWEUWRUWGVWFPRVXHVXGUVTUVLUUAYBZJYFRVW
+      EUUBVRZYHXTVWEVWFUVLJVWEVWFVXSXTZVXLVXTVWEVWFUVTYDVTZVWFUVLYDVTZVWEVXFVXK
+      VYBVYCSVXIVXLUVTUVLUUCYBZUUDYGVWEVWFUVTJVYAVXIVXTVWEVYBVYCVYDUUEYGVWEUVMV
+      WEUVLJVXGVXTYHZXTVWEUWAVWEUVTJVXHVXTYHZXTUUFVWEVXRVWFMMWFLZKLVXPVYGJVWFKY
+      IYJVWEVWFMMVWEVWFVXSTZMYFRZVWEYKVRZVYJYLYMVWEUWAUWKUVMVWEUWAVYFTVWEUWKVWE
+      UWJVWBVWCUWMUUGZYNTVWEUVMVYETVWBVWCUWMUUIUUJUUHVWEVWRPRZVWCVXNVXQYOVWEVWF
+      VXSYNZVYKVWRUWJUUKYBUULVWEVWCVYLVXNVXOYOVYKVYMUWJVWRUUMYBUUNVWEVWNVXBVWEV
+      XFVXKUVLUUOUFVWNVXIVXLVWEUVLVXGYPUVTUVLUUPUURVWEVWLMKLZMKLZVWTNLZVWGMKLZM
+      KLZVXAVWJVWEUVTMKLZVWRXRLZMKLZVWTNLUVLMKLZVWRXRLZMKLVYPVYRVWEVYSUWJWUBVWR
+      MVWEVWRVYMTVWEVWRVYMYPVWEVYSVWEUVTVXHYNTVWEUWJVYKTVWEWUBVWEUVLVXGYNTVYJVW
+      BVWCUWMVYSMKLZUWKNLZWUBMKLZOZVWBVWCSZUWMWUGWUHUWLWUEUVMWUFWUHUWAWUDUWKNWU
+      HUWAUVTVYGKLWUDVYGJUVTKYIYJWUHUVTMMWUHUVTAUWGUWRVWCXSTVYIWUHYKVRZWUIYLYMU
+      RWUHUVMUVLVYGKLWUFVYGJUVLKYIYJWUHUVLMMWUHUVLAUWGUWRVWCXPTWUIWUIYLYMUUSUUQ
+      XMUUTVWEVYOWUAVWTNVWEVYNVYTMKVWEUVTVWFVWEUVTVXHTVYHVWEVWFVXSYPZYQURURVWEV
+      YQWUCMKVWEUVLVWFVWEUVLVXGTVYHWUJYQURYSVWEVWOVYOVWTNVWEVWOVWLVYGKLVYOVYGJV
+      WLKYIYJVWEVWLMMVWEVWLVXMTVYJVYJYLYMURVWEVWJVWGVYGKLVYRVYGJVWGKYIYJVWEVWGM
+      MVWEVWGVXJTVYJVYJYLYMYSUVGUVAUVBXLUWOUAPYRUXLUDPYRUVCUVDXQUWEUWPYTYBUVRUW
+      EYTYBUVNUAPUVEUVFGUVH $.
+  $}
+
+  $(
+    flt4.a @e |- ( ph -> A e. NN ) @.
+    flt4.b @e |- ( ph -> B e. NN ) @.
+    flt4.c @e |- ( ph -> C e. NN ) @.
+    @( Fermat's last theorem for the exponent four.  (Contributed by ??,
+       ??-???-????.) @)
+    flt4 @p |- ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) =/= ( C ^ 4 ) ) @=
+      ? @.
+  $)
+
   ${
     fltltc.a $e |- ( ph -> A e. NN ) $.
     fltltc.b $e |- ( ph -> B e. NN ) $.