If I'm not mistaken, a possible formalization of https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem
in set.mm would be |- -. E. a e. NN E. b e. NN E. c e. NN E. n e. ( ZZ>= ` 3 ) ( ( a ^ n ) + ( b ^ n ) ) = ( c ^ n ) or |- A. a e. NN A. b e. NN A. c e. NN A. n e. ( ZZ>= ` 3 ) ( ( a ^ n ) + ( b ^ n ) ) =/= ( c ^ n ) Glauco LM wrote: Would someone be so kind to at least formalize in the notation of metamath the final theorem? I would prefer to double check or modify the proof to the desired form. -- 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/8a71e210-07de-4223-a98f-95b5af6ff9dcn%40googlegroups.com.
