Metamath Proof Explorer

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 ∈ ℤ ≥ 3 ∧ X ∈ ℕ ∧ Y ∈ ℕ ∧ Z ∈ ℕ → X N + Y N ≠ Z N

Detailed syntax breakdown

Step Hyp Ref Expression
0 cN class N
1 cuz class ℤ ≥
2 c3 class 3
3 2 1 cfv class ℤ ≥ 3
4 0 3 wcel wff N ∈ ℤ ≥ 3
5 cX class X
6 cn class ℕ
7 5 6 wcel wff X ∈ ℕ
8 cY class Y
9 8 6 wcel wff Y ∈ ℕ
10 cZ class Z
11 10 6 wcel wff Z ∈ ℕ
12 7 9 11 w3a wff X ∈ ℕ ∧ Y ∈ ℕ ∧ Z ∈ ℕ
13 4 12 wa wff N ∈ ℤ ≥ 3 ∧ X ∈ ℕ ∧ Y ∈ ℕ ∧ Z ∈ ℕ
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 ≠ Z N
21 13 20 wi wff N ∈ ℤ ≥ 3 ∧ X ∈ ℕ ∧ Y ∈ ℕ ∧ Z ∈ ℕ → X N + Y N ≠ Z N