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	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑋 ∈ ℕ ∧ 𝑌 ∈ ℕ ∧ 𝑍 ∈ ℕ ) ) → ( ( 𝑋 ↑ 𝑁 ) + ( 𝑌 ↑ 𝑁 ) ) ≠ ( 𝑍 ↑ 𝑁 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cN	⊢ 𝑁
1		cuz	⊢ ℤ≥
2		c3	⊢ 3
3	2 1	cfv	⊢ ( ℤ≥ ‘ 3 )
4	0 3	wcel	⊢ 𝑁 ∈ ( ℤ≥ ‘ 3 )
5		cX	⊢ 𝑋
6		cn	⊢ ℕ
7	5 6	wcel	⊢ 𝑋 ∈ ℕ
8		cY	⊢ 𝑌
9	8 6	wcel	⊢ 𝑌 ∈ ℕ
10		cZ	⊢ 𝑍
11	10 6	wcel	⊢ 𝑍 ∈ ℕ
12	7 9 11	w3a	⊢ ( 𝑋 ∈ ℕ ∧ 𝑌 ∈ ℕ ∧ 𝑍 ∈ ℕ )
13	4 12	wa	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑋 ∈ ℕ ∧ 𝑌 ∈ ℕ ∧ 𝑍 ∈ ℕ ) )
14		cexp	⊢ ↑
15	5 0 14	co	⊢ ( 𝑋 ↑ 𝑁 )
16		caddc	⊢ +
17	8 0 14	co	⊢ ( 𝑌 ↑ 𝑁 )
18	15 17 16	co	⊢ ( ( 𝑋 ↑ 𝑁 ) + ( 𝑌 ↑ 𝑁 ) )
19	10 0 14	co	⊢ ( 𝑍 ↑ 𝑁 )
20	18 19	wne	⊢ ( ( 𝑋 ↑ 𝑁 ) + ( 𝑌 ↑ 𝑁 ) ) ≠ ( 𝑍 ↑ 𝑁 )
21	13 20	wi	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑋 ∈ ℕ ∧ 𝑌 ∈ ℕ ∧ 𝑍 ∈ ℕ ) ) → ( ( 𝑋 ↑ 𝑁 ) + ( 𝑌 ↑ 𝑁 ) ) ≠ ( 𝑍 ↑ 𝑁 ) )