It's commented out, but you can search set.mm for "Fermat's Last Theorem"
and it's currently given like this:
$(
$@
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Fermat's Last Theorem
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$@
flt @p |- ( ( N e. ( ZZ>= ` 3 ) /\ ( X e. NN /\ Y e. NN /\ Z e. NN ) )
-> ( ( X ^ N ) + ( Y ^ N ) ) =/= ( Z ^ N ) ) @=
? @.
$)
Not that that makes this one particular way of stating it binding or
anything.
On Mon, Apr 17, 2023 at 1:54 PM Paul Chapman <[email protected]>
wrote:
> On 17/04/2023 12:59, Glauco wrote:
> |- A. a e. NN A. b e. NN A. c e. NN A. n e. ( ZZ>= ` 3 )
> ( ( a ^ n ) + ( b ^ n ) ) =/= ( c ^ n )
>
> I think I'd prefer
>
> |- A. a e. NN A. b e. NN A. c e. NN A. n e. NN
> ( ( ( a ^ n ) + ( b ^ n ) ) = ( c ^ n ) -> n <= 2 )
>
> since it shows where the cutoff occurs.
>
> Cheers, Paul
>
> --
> You received this message because you are subscribed to the Google Groups
> "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [email protected].
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/f4db70b5-ef66-fdc6-cea6-44c321cbe804%40igblan.free-online.co.uk
> .
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAJ48g%2BBEBy%3DxFbR41-Cfy8-ZLt1w4OD3gkTpin4kORBKhU%2B-EA%40mail.gmail.com.
