Axiom ax-flt

Description: This factoid is e.g. useful for nrt2irr . Andrew has a proof, I'll have a go at formalizing it after my coffee break. In the mean time let's add it as an axiom. (Contributed by Prof. Loof Lirpa, 1-Apr-2025) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-flt	|- ( ( N e. ( ZZ>= ` 3 ) /\ ( X e. NN /\ Y e. NN /\ Z e. NN ) ) -> ( ( X ^ N ) + ( Y ^ N ) ) =/= ( Z ^ N ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cN	|- N
1		cuz	|- ZZ>=
2		c3	|- 3
3	2 1	cfv	|- ( ZZ>= ` 3 )
4	0 3	wcel	|- N e. ( ZZ>= ` 3 )
5		cX	|- X
6		cn	|- NN
7	5 6	wcel	|- X e. NN
8		cY	|- Y
9	8 6	wcel	|- Y e. NN
10		cZ	|- Z
11	10 6	wcel	|- Z e. NN
12	7 9 11	w3a	|- ( X e. NN /\ Y e. NN /\ Z e. NN )
13	4 12	wa	|- ( N e. ( ZZ>= ` 3 ) /\ ( X e. NN /\ Y e. NN /\ Z e. NN ) )
14		cexp	|- ^
15	5 0 14	co	|- ( X ^ N )
16		caddc	|- +
17	8 0 14	co	|- ( Y ^ N )
18	15 17 16	co	|- ( ( X ^ N ) + ( Y ^ N ) )
19	10 0 14	co	|- ( Z ^ N )
20	18 19	wne	|- ( ( X ^ N ) + ( Y ^ N ) ) =/= ( Z ^ N )
21	13 20	wi	|- ( ( N e. ( ZZ>= ` 3 ) /\ ( X e. NN /\ Y e. NN /\ Z e. NN ) ) -> ( ( X ^ N ) + ( Y ^ N ) ) =/= ( Z ^ N ) )