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 \in ℤ_{\geq 3} \land (X \in ℕ \land Y \in ℕ \land Z \in ℕ)) \to X^{N} + Y^{N} \neq Z^{N}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cN	$class N$
1		cuz	$class ℤ_{\geq}$
2		c3	$class 3$
3	2 1	cfv	$class ℤ_{\geq 3}$
4	0 3	wcel	$wff N \in ℤ_{\geq 3}$
5		cX	$class X$
6		cn	$class ℕ$
7	5 6	wcel	$wff X \in ℕ$
8		cY	$class Y$
9	8 6	wcel	$wff Y \in ℕ$
10		cZ	$class Z$
11	10 6	wcel	$wff Z \in ℕ$
12	7 9 11	w3a	$wff (X \in ℕ \land Y \in ℕ \land Z \in ℕ)$
13	4 12	wa	$wff (N \in ℤ_{\geq 3} \land (X \in ℕ \land Y \in ℕ \land Z \in ℕ))$
14		cexp	$class^$
15	5 0 14	co	$class X^{N}$
16		caddc	$class +$
17	8 0 14	co	$class Y^{N}$
18	15 17 16	co	$class (X^{N} + Y^{N})$
19	10 0 14	co	$class Z^{N}$
20	18 19	wne	$wff X^{N} + Y^{N} \neq Z^{N}$
21	13 20	wi	$wff ((N \in ℤ_{\geq 3} \land (X \in ℕ \land Y \in ℕ \land Z \in ℕ)) \to X^{N} + Y^{N} \neq Z^{N})$

Metamath Proof Explorer

Axiom ax-flt

Detailed syntax breakdown