Axiom ax-flt 30491

Description: This factoid is e.g. useful for nrt2irr 30492. 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.)

Assertion

Ref	Expression
ax-flt	⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑋 ∈ ℕ ∧ 𝑌 ∈ ℕ ∧ 𝑍 ∈ ℕ)) → ((𝑋↑𝑁) + (𝑌↑𝑁)) ≠ (𝑍↑𝑁))

Detailed syntax breakdown of Axiom ax-flt

Step	Hyp	Ref	Expression
1		cN	. . . 4 class 𝑁
2		c3 12322	. . . . 5 class 3
3		cuz 12878	. . . . 5 class ℤ≥
4	2, 3	cfv 6561	. . . 4 class (ℤ≥‘3)
5	1, 4	wcel 2108	. . 3 wff 𝑁 ∈ (ℤ≥‘3)
6		cX	. . . . 5 class 𝑋
7		cn 12266	. . . . 5 class ℕ
8	6, 7	wcel 2108	. . . 4 wff 𝑋 ∈ ℕ
9		cY	. . . . 5 class 𝑌
10	9, 7	wcel 2108	. . . 4 wff 𝑌 ∈ ℕ
11		cZ	. . . . 5 class 𝑍
12	11, 7	wcel 2108	. . . 4 wff 𝑍 ∈ ℕ
13	8, 10, 12	w3a 1087	. . 3 wff (𝑋 ∈ ℕ ∧ 𝑌 ∈ ℕ ∧ 𝑍 ∈ ℕ)
14	5, 13	wa 395	. 2 wff (𝑁 ∈ (ℤ≥‘3) ∧ (𝑋 ∈ ℕ ∧ 𝑌 ∈ ℕ ∧ 𝑍 ∈ ℕ))
15		cexp 14102	. . . . 5 class ↑
16	6, 1, 15	co 7431	. . . 4 class (𝑋↑𝑁)
17	9, 1, 15	co 7431	. . . 4 class (𝑌↑𝑁)
18		caddc 11158	. . . 4 class +
19	16, 17, 18	co 7431	. . 3 class ((𝑋↑𝑁) + (𝑌↑𝑁))
20	11, 1, 15	co 7431	. . 3 class (𝑍↑𝑁)
21	19, 20	wne 2940	. 2 wff ((𝑋↑𝑁) + (𝑌↑𝑁)) ≠ (𝑍↑𝑁)
22	14, 21	wi 4	1 wff ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑋 ∈ ℕ ∧ 𝑌 ∈ ℕ ∧ 𝑍 ∈ ℕ)) → ((𝑋↑𝑁) + (𝑌↑𝑁)) ≠ (𝑍↑𝑁))

This axiom is referenced by:  nrt2irr  30492