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.

Reply via email to