dffltz

Description: Fermat's Last Theorem (FLT) for nonzero integers is equivalent to the original scope of natural numbers. The backwards direction takes ( a ^ n ) + ( b ^ n ) = ( c ^ n ) , and adds the negative of any negative term to both sides, thus creating the corresponding equation with only positive integers. There are six combinations of negativity, so the proof is particularly long. (Contributed by Steven Nguyen, 27-Feb-2023)

		Ref	Expression
	Assertion	dffltz	$⊢ \forall n \in ℤ_{\geq 3} \forall x \in ℕ \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n} \leftrightarrow \forall n \in ℤ_{\geq 3} \forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$

Proof

Step	Hyp	Ref	Expression
1		simp-4r	$⊢ ((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \to a \in (ℤ ∖ \{0\})$
2		eldifi	$⊢ a \in (ℤ ∖ \{0\}) \to a \in ℤ$
3		eldifsni	$⊢ a \in (ℤ ∖ \{0\}) \to a \neq 0$
4	2 3	jca	$⊢ a \in (ℤ ∖ \{0\}) \to (a \in ℤ \land a \neq 0)$
5		nnabscl	$⊢ (a \in ℤ \land a \neq 0) \to \|a\| \in ℕ$
6	1 4 5	3syl	$⊢ ((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \to \|a\| \in ℕ$
7		simp-6r	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land 0 < b) \to a \in (ℤ ∖ \{0\})$
8	7	eldifad	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land 0 < b) \to a \in ℤ$
9		simplr	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land 0 < b) \to 0 < a$
10		elnnz	$⊢ a \in ℕ \leftrightarrow (a \in ℤ \land 0 < a)$
11	8 9 10	sylanbrc	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land 0 < b) \to a \in ℕ$
12		eldifsni	$⊢ b \in (ℤ ∖ \{0\}) \to b \neq 0$
13	12	ad6antlr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to b \neq 0$
14		simplr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to \neg 0 < b$
15		eldifi	$⊢ b \in (ℤ ∖ \{0\}) \to b \in ℤ$
16	15	ad6antlr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to b \in ℤ$
17	13 14 16	negn0nposznnd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to - b \in ℕ$
18		simp-7r	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a \in (ℤ ∖ \{0\})$
19	18	eldifad	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a \in ℤ$
20		simpllr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to 0 < a$
21	19 20 10	sylanbrc	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a \in ℕ$
22	17 21	ifclda	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \to if (0 < c, - b, a) \in ℕ$
23	11 22	ifclda	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \to if (0 < b, a, if (0 < c, - b, a)) \in ℕ$
24	3	ad7antlr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to a \neq 0$
25		simpllr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to \neg 0 < a$
26	2	ad7antlr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to a \in ℤ$
27	24 25 26	negn0nposznnd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to - a \in ℕ$
28		simp-6r	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to b \in (ℤ ∖ \{0\})$
29	28	eldifad	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to b \in ℤ$
30		simplr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to 0 < b$
31		elnnz	$⊢ b \in ℕ \leftrightarrow (b \in ℤ \land 0 < b)$
32	29 30 31	sylanbrc	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to b \in ℕ$
33	27 32	ifclda	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \to if (0 < c, - a, b) \in ℕ$
34	3	ad6antlr	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land \neg 0 < b) \to a \neq 0$
35		simplr	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land \neg 0 < b) \to \neg 0 < a$
36	2	ad6antlr	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land \neg 0 < b) \to a \in ℤ$
37	34 35 36	negn0nposznnd	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land \neg 0 < b) \to - a \in ℕ$
38	33 37	ifclda	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \to if (0 < b, if (0 < c, - a, b), - a) \in ℕ$
39	23 38	ifclda	$⊢ ((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \to if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)) \in ℕ$
40	6 39	ifcld	$⊢ ((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \to if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))) \in ℕ$
41		simpllr	$⊢ ((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \to b \in (ℤ ∖ \{0\})$
42	15 12	jca	$⊢ b \in (ℤ ∖ \{0\}) \to (b \in ℤ \land b \neq 0)$
43		nnabscl	$⊢ (b \in ℤ \land b \neq 0) \to \|b\| \in ℕ$
44	41 42 43	3syl	$⊢ ((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \to \|b\| \in ℕ$
45		simp-5r	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land 0 < b) \to b \in (ℤ ∖ \{0\})$
46	45	eldifad	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land 0 < b) \to b \in ℤ$
47		simpr	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land 0 < b) \to 0 < b$
48	46 47 31	sylanbrc	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land 0 < b) \to b \in ℕ$
49		simp-5r	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to c \in (ℤ ∖ \{0\})$
50	49	eldifad	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to c \in ℤ$
51		simpr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to 0 < c$
52		elnnz	$⊢ c \in ℕ \leftrightarrow (c \in ℤ \land 0 < c)$
53	50 51 52	sylanbrc	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to c \in ℕ$
54		eldifsni	$⊢ c \in (ℤ ∖ \{0\}) \to c \neq 0$
55	54	ad5antlr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to c \neq 0$
56		simpr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to \neg 0 < c$
57		eldifi	$⊢ c \in (ℤ ∖ \{0\}) \to c \in ℤ$
58	57	ad5antlr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to c \in ℤ$
59	55 56 58	negn0nposznnd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to - c \in ℕ$
60	53 59	ifclda	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \land \neg 0 < b) \to if (0 < c, c, - c) \in ℕ$
61	48 60	ifclda	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land 0 < a) \to if (0 < b, b, if (0 < c, c, - c)) \in ℕ$
62		simp-5r	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to c \in (ℤ ∖ \{0\})$
63	62	eldifad	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to c \in ℤ$
64		simpr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to 0 < c$
65	63 64 52	sylanbrc	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to c \in ℕ$
66	54	ad5antlr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to c \neq 0$
67		simpr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to \neg 0 < c$
68	57	ad5antlr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to c \in ℤ$
69	66 67 68	negn0nposznnd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to - c \in ℕ$
70	65 69	ifclda	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land 0 < b) \to if (0 < c, c, - c) \in ℕ$
71	12	ad5antlr	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land \neg 0 < b) \to b \neq 0$
72		simpr	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land \neg 0 < b) \to \neg 0 < b$
73	15	ad5antlr	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land \neg 0 < b) \to b \in ℤ$
74	71 72 73	negn0nposznnd	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \land \neg 0 < b) \to - b \in ℕ$
75	70 74	ifclda	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg 0 < a) \to if (0 < b, if (0 < c, c, - c), - b) \in ℕ$
76	61 75	ifclda	$⊢ ((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \to if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)) \in ℕ$
77	44 76	ifcld	$⊢ ((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \to if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))) \in ℕ$
78		simpllr	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to c \in (ℤ ∖ \{0\})$
79	78	eldifad	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to c \in ℤ$
80	78 54	syl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to c \neq 0$
81		nnabscl	$⊢ (c \in ℤ \land c \neq 0) \to \|c\| \in ℕ$
82	79 80 81	syl2anc	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to \|c\| \in ℕ$
83		simp-5r	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to c \in (ℤ ∖ \{0\})$
84	83	eldifad	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to c \in ℤ$
85		simp-7r	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to a \in (ℤ ∖ \{0\})$
86	85	eldifad	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to a \in ℤ$
87	86	zred	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to a \in ℝ$
88		eluzge3nn	$⊢ n \in ℤ_{\geq 3} \to n \in ℕ$
89	88	ad7antr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to n \in ℕ$
90	89	nnnn0d	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to n \in ℕ_{0}$
91	87 90	reexpcld	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to a^{n} \in ℝ$
92		simp-6r	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to b \in (ℤ ∖ \{0\})$
93	92	eldifad	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to b \in ℤ$
94	93	zred	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to b \in ℝ$
95	94 90	reexpcld	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to b^{n} \in ℝ$
96		simplr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to 0 < a$
97		simpllr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to \neg \frac{n}{2} \in ℕ$
98	87 89 97	oexpreposd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to (0 < a \leftrightarrow 0 < a^{n})$
99	96 98	mpbid	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to 0 < a^{n}$
100		simpr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to 0 < b$
101	94 89 97	oexpreposd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to (0 < b \leftrightarrow 0 < b^{n})$
102	100 101	mpbid	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to 0 < b^{n}$
103	91 95 99 102	addgt0d	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to 0 < a^{n} + b^{n}$
104		simp-4r	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to a^{n} + b^{n} = c^{n}$
105	103 104	breqtrd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to 0 < c^{n}$
106	84	zred	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to c \in ℝ$
107	106 89 97	oexpreposd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to (0 < c \leftrightarrow 0 < c^{n})$
108	105 107	mpbird	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to 0 < c$
109	84 108 52	sylanbrc	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to c \in ℕ$
110		simp-8r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to a \in (ℤ ∖ \{0\})$
111	110	eldifad	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to a \in ℤ$
112		simpllr	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to 0 < a$
113	111 112 10	sylanbrc	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to a \in ℕ$
114		simp-7r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to b \in (ℤ ∖ \{0\})$
115	114 12	syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to b \neq 0$
116		simplr	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to \neg 0 < b$
117	114	eldifad	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to b \in ℤ$
118	115 116 117	negn0nposznnd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to - b \in ℕ$
119	113 118	ifclda	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \to if (0 < c, a, - b) \in ℕ$
120	109 119	ifclda	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \to if (0 < b, c, if (0 < c, a, - b)) \in ℕ$
121		simp-7r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to b \in (ℤ ∖ \{0\})$
122	121	eldifad	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to b \in ℤ$
123		simplr	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to 0 < b$
124	122 123 31	sylanbrc	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to b \in ℕ$
125		simp-8r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to a \in (ℤ ∖ \{0\})$
126	125 3	syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to a \neq 0$
127		simpllr	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to \neg 0 < a$
128	125	eldifad	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to a \in ℤ$
129	126 127 128	negn0nposznnd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to - a \in ℕ$
130	124 129	ifclda	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \to if (0 < c, b, - a) \in ℕ$
131		simp-5r	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to c \in (ℤ ∖ \{0\})$
132	131 54	syl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to c \neq 0$
133		simp-7r	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to a \in (ℤ ∖ \{0\})$
134	133	eldifad	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to a \in ℤ$
135	134	zred	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to a \in ℝ$
136	88	ad7antr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to n \in ℕ$
137	136	nnnn0d	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to n \in ℕ_{0}$
138	135 137	reexpcld	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to a^{n} \in ℝ$
139		simp-6r	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to b \in (ℤ ∖ \{0\})$
140	139	eldifad	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to b \in ℤ$
141	140	zred	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to b \in ℝ$
142	141 137	reexpcld	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to b^{n} \in ℝ$
143	138 142	readdcld	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to a^{n} + b^{n} \in ℝ$
144		0red	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to 0 \in ℝ$
145	3	neneqd	$⊢ a \in (ℤ ∖ \{0\}) \to \neg a = 0$
146	133 145	syl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg a = 0$
147		zcn	$⊢ a \in ℤ \to a \in ℂ$
148	133 2 147	3syl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to a \in ℂ$
149		expeq0	$⊢ (a \in ℂ \land n \in ℕ) \to (a^{n} = 0 \leftrightarrow a = 0)$
150	148 136 149	syl2anc	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to (a^{n} = 0 \leftrightarrow a = 0)$
151	146 150	mtbird	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg a^{n} = 0$
152		simplr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg 0 < a$
153		simpllr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg \frac{n}{2} \in ℕ$
154	135 136 153	oexpreposd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to (0 < a \leftrightarrow 0 < a^{n})$
155	152 154	mtbid	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg 0 < a^{n}$
156		ioran	$⊢ \neg (a^{n} = 0 \lor 0 < a^{n}) \leftrightarrow (\neg a^{n} = 0 \land \neg 0 < a^{n})$
157	151 155 156	sylanbrc	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg (a^{n} = 0 \lor 0 < a^{n})$
158	138 144	lttrid	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to (a^{n} < 0 \leftrightarrow \neg (a^{n} = 0 \lor 0 < a^{n}))$
159	157 158	mpbird	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to a^{n} < 0$
160		zcn	$⊢ b \in ℤ \to b \in ℂ$
161	139 15 160	3syl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to b \in ℂ$
162	139 12	syl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to b \neq 0$
163		eluzelz	$⊢ n \in ℤ_{\geq 3} \to n \in ℤ$
164	163	ad7antr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to n \in ℤ$
165	161 162 164	expne0d	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to b^{n} \neq 0$
166	165	neneqd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg b^{n} = 0$
167		simpr	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg 0 < b$
168	141 136 153	oexpreposd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to (0 < b \leftrightarrow 0 < b^{n})$
169	167 168	mtbid	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg 0 < b^{n}$
170		ioran	$⊢ \neg (b^{n} = 0 \lor 0 < b^{n}) \leftrightarrow (\neg b^{n} = 0 \land \neg 0 < b^{n})$
171	166 169 170	sylanbrc	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg (b^{n} = 0 \lor 0 < b^{n})$
172	142 144	lttrid	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to (b^{n} < 0 \leftrightarrow \neg (b^{n} = 0 \lor 0 < b^{n}))$
173	171 172	mpbird	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to b^{n} < 0$
174	138 142 144 144 159 173	lt2addd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to a^{n} + b^{n} < 0 + 0$
175		00id	$⊢ 0 + 0 = 0$
176	174 175	breqtrdi	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to a^{n} + b^{n} < 0$
177	143 144 176	ltnsymd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg 0 < a^{n} + b^{n}$
178		simp-4r	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to a^{n} + b^{n} = c^{n}$
179	178	eqcomd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to c^{n} = a^{n} + b^{n}$
180	179	breq2d	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to (0 < c^{n} \leftrightarrow 0 < a^{n} + b^{n})$
181	177 180	mtbird	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg 0 < c^{n}$
182	131	eldifad	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to c \in ℤ$
183	182	zred	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to c \in ℝ$
184	183 136 153	oexpreposd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to (0 < c \leftrightarrow 0 < c^{n})$
185	181 184	mtbird	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg 0 < c$
186	132 185 182	negn0nposznnd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to - c \in ℕ$
187	130 186	ifclda	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \to if (0 < b, if (0 < c, b, - a), - c) \in ℕ$
188	120 187	ifclda	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \to if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)) \in ℕ$
189	82 188	ifclda	$⊢ ((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \to if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))) \in ℕ$
190		oveq1	$⊢ x = if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))) \to x^{n} = {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n}$
191	190	oveq1d	$⊢ x = if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))) \to x^{n} + y^{n} = {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + y^{n}$
192	191	eqeq1d	$⊢ x = if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))) \to (x^{n} + y^{n} = z^{n} \leftrightarrow {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + y^{n} = z^{n})$
193	192	adantl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land x = if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))) \to (x^{n} + y^{n} = z^{n} \leftrightarrow {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + y^{n} = z^{n})$
194		oveq1	$⊢ y = if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))) \to y^{n} = {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n}$
195	194	oveq2d	$⊢ y = if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))) \to {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + y^{n} = {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n}$
196	195	eqeq1d	$⊢ y = if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))) \to ({if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + y^{n} = z^{n} \leftrightarrow {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = z^{n})$
197	196	adantl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land y = if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))) \to ({if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + y^{n} = z^{n} \leftrightarrow {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = z^{n})$
198		oveq1	$⊢ z = if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))) \to z^{n} = {if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)))}^{n}$
199	198	eqeq2d	$⊢ z = if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))) \to ({if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = z^{n} \leftrightarrow {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = {if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)))}^{n})$
200	199	adantl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land z = if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)))) \to ({if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = z^{n} \leftrightarrow {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = {if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)))}^{n})$
201		simplr	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to a^{n} + b^{n} = c^{n}$
202		simp-5r	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to a \in (ℤ ∖ \{0\})$
203	202	eldifad	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to a \in ℤ$
204	203	zred	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to a \in ℝ$
205		absresq	$⊢ a \in ℝ \to {\|a\|}^{2} = a^{2}$
206	204 205	syl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|a\|}^{2} = a^{2}$
207	206	oveq1d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {({\|a\|}^{2})}^{\frac{n}{2}} = {(a^{2})}^{\frac{n}{2}}$
208	202 2 147	3syl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to a \in ℂ$
209	208	abscld	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to \|a\| \in ℝ$
210	209	recnd	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to \|a\| \in ℂ$
211		simpr	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to \frac{n}{2} \in ℕ$
212	211	nnnn0d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to \frac{n}{2} \in ℕ_{0}$
213		2nn0	$⊢ 2 \in ℕ_{0}$
214	213	a1i	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to 2 \in ℕ_{0}$
215	210 212 214	expmuld	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|a\|}^{2 (\frac{n}{2})} = {({\|a\|}^{2})}^{\frac{n}{2}}$
216	208 212 214	expmuld	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to a^{2 (\frac{n}{2})} = {(a^{2})}^{\frac{n}{2}}$
217	207 215 216	3eqtr4d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|a\|}^{2 (\frac{n}{2})} = a^{2 (\frac{n}{2})}$
218		simp-5l	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to n \in ℤ_{\geq 3}$
219		nncn	$⊢ n \in ℕ \to n \in ℂ$
220	218 88 219	3syl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to n \in ℂ$
221		2cnd	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to 2 \in ℂ$
222		2ne0	$⊢ 2 \neq 0$
223	222	a1i	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to 2 \neq 0$
224	220 221 223	divcan2d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to 2 (\frac{n}{2}) = n$
225	224	eqcomd	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to n = 2 (\frac{n}{2})$
226	225	oveq2d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|a\|}^{n} = {\|a\|}^{2 (\frac{n}{2})}$
227	225	oveq2d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to a^{n} = a^{2 (\frac{n}{2})}$
228	217 226 227	3eqtr4d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|a\|}^{n} = a^{n}$
229		simp-4r	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to b \in (ℤ ∖ \{0\})$
230	229	eldifad	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to b \in ℤ$
231	230	zred	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to b \in ℝ$
232		absresq	$⊢ b \in ℝ \to {\|b\|}^{2} = b^{2}$
233	231 232	syl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|b\|}^{2} = b^{2}$
234	233	oveq1d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {({\|b\|}^{2})}^{\frac{n}{2}} = {(b^{2})}^{\frac{n}{2}}$
235	229 15 160	3syl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to b \in ℂ$
236	235	abscld	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to \|b\| \in ℝ$
237	236	recnd	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to \|b\| \in ℂ$
238	237 212 214	expmuld	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|b\|}^{2 (\frac{n}{2})} = {({\|b\|}^{2})}^{\frac{n}{2}}$
239	235 212 214	expmuld	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to b^{2 (\frac{n}{2})} = {(b^{2})}^{\frac{n}{2}}$
240	234 238 239	3eqtr4d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|b\|}^{2 (\frac{n}{2})} = b^{2 (\frac{n}{2})}$
241	225	oveq2d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|b\|}^{n} = {\|b\|}^{2 (\frac{n}{2})}$
242	225	oveq2d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to b^{n} = b^{2 (\frac{n}{2})}$
243	240 241 242	3eqtr4d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|b\|}^{n} = b^{n}$
244	228 243	oveq12d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|a\|}^{n} + {\|b\|}^{n} = a^{n} + b^{n}$
245	79	zred	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to c \in ℝ$
246		absresq	$⊢ c \in ℝ \to {\|c\|}^{2} = c^{2}$
247	245 246	syl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|c\|}^{2} = c^{2}$
248	247	oveq1d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {({\|c\|}^{2})}^{\frac{n}{2}} = {(c^{2})}^{\frac{n}{2}}$
249		zcn	$⊢ c \in ℤ \to c \in ℂ$
250	78 57 249	3syl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to c \in ℂ$
251	250	abscld	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to \|c\| \in ℝ$
252	251	recnd	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to \|c\| \in ℂ$
253	252 212 214	expmuld	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|c\|}^{2 (\frac{n}{2})} = {({\|c\|}^{2})}^{\frac{n}{2}}$
254	250 212 214	expmuld	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to c^{2 (\frac{n}{2})} = {(c^{2})}^{\frac{n}{2}}$
255	248 253 254	3eqtr4d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|c\|}^{2 (\frac{n}{2})} = c^{2 (\frac{n}{2})}$
256	225	oveq2d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|c\|}^{n} = {\|c\|}^{2 (\frac{n}{2})}$
257	225	oveq2d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to c^{n} = c^{2 (\frac{n}{2})}$
258	255 256 257	3eqtr4d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|c\|}^{n} = c^{n}$
259	201 244 258	3eqtr4d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {\|a\|}^{n} + {\|b\|}^{n} = {\|c\|}^{n}$
260		iftrue	$⊢ \frac{n}{2} \in ℕ \to if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))) = \|a\|$
261	260	oveq1d	$⊢ \frac{n}{2} \in ℕ \to {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} = {\|a\|}^{n}$
262		iftrue	$⊢ \frac{n}{2} \in ℕ \to if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))) = \|b\|$
263	262	oveq1d	$⊢ \frac{n}{2} \in ℕ \to {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = {\|b\|}^{n}$
264	261 263	oveq12d	$⊢ \frac{n}{2} \in ℕ \to {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = {\|a\|}^{n} + {\|b\|}^{n}$
265	264	adantl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = {\|a\|}^{n} + {\|b\|}^{n}$
266		iftrue	$⊢ \frac{n}{2} \in ℕ \to if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))) = \|c\|$
267	266	oveq1d	$⊢ \frac{n}{2} \in ℕ \to {if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)))}^{n} = {\|c\|}^{n}$
268	267	adantl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)))}^{n} = {\|c\|}^{n}$
269	259 265 268	3eqtr4d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \frac{n}{2} \in ℕ) \to {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = {if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)))}^{n}$
270		iftrue	$⊢ 0 < b \to if (0 < b, a, if (0 < c, - b, a)) = a$
271	270	oveq1d	$⊢ 0 < b \to {if (0 < b, a, if (0 < c, - b, a))}^{n} = a^{n}$
272		iftrue	$⊢ 0 < b \to if (0 < b, b, if (0 < c, c, - c)) = b$
273	272	oveq1d	$⊢ 0 < b \to {if (0 < b, b, if (0 < c, c, - c))}^{n} = b^{n}$
274	271 273	oveq12d	$⊢ 0 < b \to {if (0 < b, a, if (0 < c, - b, a))}^{n} + {if (0 < b, b, if (0 < c, c, - c))}^{n} = a^{n} + b^{n}$
275	274	adantl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to {if (0 < b, a, if (0 < c, - b, a))}^{n} + {if (0 < b, b, if (0 < c, c, - c))}^{n} = a^{n} + b^{n}$
276		iftrue	$⊢ 0 < b \to if (0 < b, c, if (0 < c, a, - b)) = c$
277	276	oveq1d	$⊢ 0 < b \to {if (0 < b, c, if (0 < c, a, - b))}^{n} = c^{n}$
278	277	adantl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to {if (0 < b, c, if (0 < c, a, - b))}^{n} = c^{n}$
279	104 275 278	3eqtr4d	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land 0 < b) \to {if (0 < b, a, if (0 < c, - b, a))}^{n} + {if (0 < b, b, if (0 < c, c, - c))}^{n} = {if (0 < b, c, if (0 < c, a, - b))}^{n}$
280		simp-7r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to b \in (ℤ ∖ \{0\})$
281	280 15 160	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to b \in ℂ$
282		simp-8l	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to n \in ℤ_{\geq 3}$
283	282 88	syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to n \in ℕ$
284		simp-4r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to \neg \frac{n}{2} \in ℕ$
285		2nn	$⊢ 2 \in ℕ$
286		nndivdvds	$⊢ (n \in ℕ \land 2 \in ℕ) \to (2 ∥ n \leftrightarrow \frac{n}{2} \in ℕ)$
287	283 285 286	sylancl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to (2 ∥ n \leftrightarrow \frac{n}{2} \in ℕ)$
288	284 287	mtbird	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to \neg 2 ∥ n$
289		oexpneg	$⊢ (b \in ℂ \land n \in ℕ \land \neg 2 ∥ n) \to {(- b)}^{n} = - b^{n}$
290	281 283 288 289	syl3anc	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to {(- b)}^{n} = - b^{n}$
291	290	oveq1d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to {(- b)}^{n} + c^{n} = - b^{n} + c^{n}$
292		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
293	282 88 292	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to n \in ℕ_{0}$
294	281 293	expcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to b^{n} \in ℂ$
295	294	negcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to - b^{n} \in ℂ$
296		simp-6r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to c \in (ℤ ∖ \{0\})$
297	296 57 249	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to c \in ℂ$
298	297 293	expcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to c^{n} \in ℂ$
299	295 298	addcomd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to - b^{n} + c^{n} = c^{n} + (- b^{n})$
300	298 294	negsubd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to c^{n} + (- b^{n}) = c^{n} - b^{n}$
301	299 300	eqtrd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to - b^{n} + c^{n} = c^{n} - b^{n}$
302	110 2 147	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to a \in ℂ$
303	302 293	expcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to a^{n} \in ℂ$
304		simp-5r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to a^{n} + b^{n} = c^{n}$
305	304	eqcomd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to c^{n} = a^{n} + b^{n}$
306	303 294 305	mvrraddd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to c^{n} - b^{n} = a^{n}$
307	291 301 306	3eqtrd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to {(- b)}^{n} + c^{n} = a^{n}$
308		iftrue	$⊢ 0 < c \to if (0 < c, - b, a) = - b$
309	308	oveq1d	$⊢ 0 < c \to {if (0 < c, - b, a)}^{n} = {(- b)}^{n}$
310		iftrue	$⊢ 0 < c \to if (0 < c, c, - c) = c$
311	310	oveq1d	$⊢ 0 < c \to {if (0 < c, c, - c)}^{n} = c^{n}$
312	309 311	oveq12d	$⊢ 0 < c \to {if (0 < c, - b, a)}^{n} + {if (0 < c, c, - c)}^{n} = {(- b)}^{n} + c^{n}$
313	312	adantl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to {if (0 < c, - b, a)}^{n} + {if (0 < c, c, - c)}^{n} = {(- b)}^{n} + c^{n}$
314		iftrue	$⊢ 0 < c \to if (0 < c, a, - b) = a$
315	314	oveq1d	$⊢ 0 < c \to {if (0 < c, a, - b)}^{n} = a^{n}$
316	315	adantl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to {if (0 < c, a, - b)}^{n} = a^{n}$
317	307 313 316	3eqtr4d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land 0 < c) \to {if (0 < c, - b, a)}^{n} + {if (0 < c, c, - c)}^{n} = {if (0 < c, a, - b)}^{n}$
318		simp-8r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a \in (ℤ ∖ \{0\})$
319	318 2 147	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a \in ℂ$
320	88	ad8antr	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to n \in ℕ$
321	320	nnnn0d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to n \in ℕ_{0}$
322	319 321	expcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a^{n} \in ℂ$
323		simp-6r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to c \in (ℤ ∖ \{0\})$
324	323 57 249	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to c \in ℂ$
325	324 321	expcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to c^{n} \in ℂ$
326	322 325	negsubd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a^{n} + (- c^{n}) = a^{n} - c^{n}$
327	322 325	subcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a^{n} - c^{n} \in ℂ$
328	114 15 160	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to b \in ℂ$
329	328 321	expcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to b^{n} \in ℂ$
330	329	negcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to - b^{n} \in ℂ$
331		simp-5r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a^{n} + b^{n} = c^{n}$
332	322 329 331	mvlraddd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a^{n} = c^{n} - b^{n}$
333	325 322	pncan3d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to c^{n} + a^{n} - c^{n} = a^{n}$
334	325 329	negsubd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to c^{n} + (- b^{n}) = c^{n} - b^{n}$
335	332 333 334	3eqtr4d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to c^{n} + a^{n} - c^{n} = c^{n} + (- b^{n})$
336	325 327 330 335	addcanad	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a^{n} - c^{n} = - b^{n}$
337	326 336	eqtrd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a^{n} + (- c^{n}) = - b^{n}$
338		simp-4r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to \neg \frac{n}{2} \in ℕ$
339	320 285 286	sylancl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to (2 ∥ n \leftrightarrow \frac{n}{2} \in ℕ)$
340	338 339	mtbird	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to \neg 2 ∥ n$
341		oexpneg	$⊢ (c \in ℂ \land n \in ℕ \land \neg 2 ∥ n) \to {(- c)}^{n} = - c^{n}$
342	324 320 340 341	syl3anc	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to {(- c)}^{n} = - c^{n}$
343	342	oveq2d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a^{n} + {(- c)}^{n} = a^{n} + (- c^{n})$
344	328 320 340 289	syl3anc	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to {(- b)}^{n} = - b^{n}$
345	337 343 344	3eqtr4d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to a^{n} + {(- c)}^{n} = {(- b)}^{n}$
346		iffalse	$⊢ \neg 0 < c \to if (0 < c, - b, a) = a$
347	346	oveq1d	$⊢ \neg 0 < c \to {if (0 < c, - b, a)}^{n} = a^{n}$
348		iffalse	$⊢ \neg 0 < c \to if (0 < c, c, - c) = - c$
349	348	oveq1d	$⊢ \neg 0 < c \to {if (0 < c, c, - c)}^{n} = {(- c)}^{n}$
350	347 349	oveq12d	$⊢ \neg 0 < c \to {if (0 < c, - b, a)}^{n} + {if (0 < c, c, - c)}^{n} = a^{n} + {(- c)}^{n}$
351	350	adantl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to {if (0 < c, - b, a)}^{n} + {if (0 < c, c, - c)}^{n} = a^{n} + {(- c)}^{n}$
352		iffalse	$⊢ \neg 0 < c \to if (0 < c, a, - b) = - b$
353	352	oveq1d	$⊢ \neg 0 < c \to {if (0 < c, a, - b)}^{n} = {(- b)}^{n}$
354	353	adantl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to {if (0 < c, a, - b)}^{n} = {(- b)}^{n}$
355	345 351 354	3eqtr4d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \land \neg 0 < c) \to {if (0 < c, - b, a)}^{n} + {if (0 < c, c, - c)}^{n} = {if (0 < c, a, - b)}^{n}$
356	317 355	pm2.61dan	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \to {if (0 < c, - b, a)}^{n} + {if (0 < c, c, - c)}^{n} = {if (0 < c, a, - b)}^{n}$
357		iffalse	$⊢ \neg 0 < b \to if (0 < b, a, if (0 < c, - b, a)) = if (0 < c, - b, a)$
358	357	oveq1d	$⊢ \neg 0 < b \to {if (0 < b, a, if (0 < c, - b, a))}^{n} = {if (0 < c, - b, a)}^{n}$
359		iffalse	$⊢ \neg 0 < b \to if (0 < b, b, if (0 < c, c, - c)) = if (0 < c, c, - c)$
360	359	oveq1d	$⊢ \neg 0 < b \to {if (0 < b, b, if (0 < c, c, - c))}^{n} = {if (0 < c, c, - c)}^{n}$
361	358 360	oveq12d	$⊢ \neg 0 < b \to {if (0 < b, a, if (0 < c, - b, a))}^{n} + {if (0 < b, b, if (0 < c, c, - c))}^{n} = {if (0 < c, - b, a)}^{n} + {if (0 < c, c, - c)}^{n}$
362	361	adantl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \to {if (0 < b, a, if (0 < c, - b, a))}^{n} + {if (0 < b, b, if (0 < c, c, - c))}^{n} = {if (0 < c, - b, a)}^{n} + {if (0 < c, c, - c)}^{n}$
363		iffalse	$⊢ \neg 0 < b \to if (0 < b, c, if (0 < c, a, - b)) = if (0 < c, a, - b)$
364	363	oveq1d	$⊢ \neg 0 < b \to {if (0 < b, c, if (0 < c, a, - b))}^{n} = {if (0 < c, a, - b)}^{n}$
365	364	adantl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \to {if (0 < b, c, if (0 < c, a, - b))}^{n} = {if (0 < c, a, - b)}^{n}$
366	356 362 365	3eqtr4d	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \land \neg 0 < b) \to {if (0 < b, a, if (0 < c, - b, a))}^{n} + {if (0 < b, b, if (0 < c, c, - c))}^{n} = {if (0 < b, c, if (0 < c, a, - b))}^{n}$
367	279 366	pm2.61dan	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \to {if (0 < b, a, if (0 < c, - b, a))}^{n} + {if (0 < b, b, if (0 < c, c, - c))}^{n} = {if (0 < b, c, if (0 < c, a, - b))}^{n}$
368		iftrue	$⊢ 0 < a \to if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)) = if (0 < b, a, if (0 < c, - b, a))$
369	368	oveq1d	$⊢ 0 < a \to {if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))}^{n} = {if (0 < b, a, if (0 < c, - b, a))}^{n}$
370		iftrue	$⊢ 0 < a \to if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)) = if (0 < b, b, if (0 < c, c, - c))$
371	370	oveq1d	$⊢ 0 < a \to {if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))}^{n} = {if (0 < b, b, if (0 < c, c, - c))}^{n}$
372	369 371	oveq12d	$⊢ 0 < a \to {if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))}^{n} + {if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))}^{n} = {if (0 < b, a, if (0 < c, - b, a))}^{n} + {if (0 < b, b, if (0 < c, c, - c))}^{n}$
373	372	adantl	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \to {if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))}^{n} + {if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))}^{n} = {if (0 < b, a, if (0 < c, - b, a))}^{n} + {if (0 < b, b, if (0 < c, c, - c))}^{n}$
374		iftrue	$⊢ 0 < a \to if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)) = if (0 < b, c, if (0 < c, a, - b))$
375	374	oveq1d	$⊢ 0 < a \to {if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))}^{n} = {if (0 < b, c, if (0 < c, a, - b))}^{n}$
376	375	adantl	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \to {if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))}^{n} = {if (0 < b, c, if (0 < c, a, - b))}^{n}$
377	367 373 376	3eqtr4d	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land 0 < a) \to {if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))}^{n} + {if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))}^{n} = {if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))}^{n}$
378		simp-8r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to a \in (ℤ ∖ \{0\})$
379	378 2 147	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to a \in ℂ$
380	88	ad8antr	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to n \in ℕ$
381		simp-4r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to \neg \frac{n}{2} \in ℕ$
382	380 285 286	sylancl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to (2 ∥ n \leftrightarrow \frac{n}{2} \in ℕ)$
383	381 382	mtbird	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to \neg 2 ∥ n$
384		oexpneg	$⊢ (a \in ℂ \land n \in ℕ \land \neg 2 ∥ n) \to {(- a)}^{n} = - a^{n}$
385	379 380 383 384	syl3anc	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to {(- a)}^{n} = - a^{n}$
386	385	oveq1d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to {(- a)}^{n} + c^{n} = - a^{n} + c^{n}$
387	380	nnnn0d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to n \in ℕ_{0}$
388	379 387	expcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to a^{n} \in ℂ$
389	388	negcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to - a^{n} \in ℂ$
390		simp-6r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to c \in (ℤ ∖ \{0\})$
391	390 57 249	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to c \in ℂ$
392	391 387	expcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to c^{n} \in ℂ$
393	389 392	addcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to - a^{n} + c^{n} \in ℂ$
394	121 15 160	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to b \in ℂ$
395	394 387	expcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to b^{n} \in ℂ$
396	388	negidd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to a^{n} + (- a^{n}) = 0$
397	396	oveq1d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to a^{n} + (- a^{n}) + c^{n} = 0 + c^{n}$
398	388 389 392	addassd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to a^{n} + (- a^{n}) + c^{n} = a^{n} + (- a^{n}) + c^{n}$
399	392	addid2d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to 0 + c^{n} = c^{n}$
400	397 398 399	3eqtr3d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to a^{n} + (- a^{n}) + c^{n} = c^{n}$
401		simp-5r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to a^{n} + b^{n} = c^{n}$
402	400 401	eqtr4d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to a^{n} + (- a^{n}) + c^{n} = a^{n} + b^{n}$
403	388 393 395 402	addcanad	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to - a^{n} + c^{n} = b^{n}$
404	386 403	eqtrd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to {(- a)}^{n} + c^{n} = b^{n}$
405		iftrue	$⊢ 0 < c \to if (0 < c, - a, b) = - a$
406	405	oveq1d	$⊢ 0 < c \to {if (0 < c, - a, b)}^{n} = {(- a)}^{n}$
407	406 311	oveq12d	$⊢ 0 < c \to {if (0 < c, - a, b)}^{n} + {if (0 < c, c, - c)}^{n} = {(- a)}^{n} + c^{n}$
408	407	adantl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to {if (0 < c, - a, b)}^{n} + {if (0 < c, c, - c)}^{n} = {(- a)}^{n} + c^{n}$
409		iftrue	$⊢ 0 < c \to if (0 < c, b, - a) = b$
410	409	oveq1d	$⊢ 0 < c \to {if (0 < c, b, - a)}^{n} = b^{n}$
411	410	adantl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to {if (0 < c, b, - a)}^{n} = b^{n}$
412	404 408 411	3eqtr4d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land 0 < c) \to {if (0 < c, - a, b)}^{n} + {if (0 < c, c, - c)}^{n} = {if (0 < c, b, - a)}^{n}$
413		simp-7r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to b \in (ℤ ∖ \{0\})$
414	413 15 160	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to b \in ℂ$
415		simp-8l	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to n \in ℤ_{\geq 3}$
416	415 88 292	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to n \in ℕ_{0}$
417	414 416	expcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to b^{n} \in ℂ$
418	417	negcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to - b^{n} \in ℂ$
419		simp-6r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to c \in (ℤ ∖ \{0\})$
420	419 57 249	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to c \in ℂ$
421	420 416	expcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to c^{n} \in ℂ$
422	418 421	addcomd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to - b^{n} + c^{n} = c^{n} + (- b^{n})$
423	421 417	negsubd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to c^{n} + (- b^{n}) = c^{n} - b^{n}$
424		simp-5r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to a^{n} + b^{n} = c^{n}$
425	424	oveq1d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to a^{n} + b^{n} - b^{n} = c^{n} - b^{n}$
426	125 2 147	3syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to a \in ℂ$
427	426 416	expcld	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to a^{n} \in ℂ$
428	427 417	pncand	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to a^{n} + b^{n} - b^{n} = a^{n}$
429	425 428	eqtr3d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to c^{n} - b^{n} = a^{n}$
430	422 423 429	3eqtrd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to - b^{n} + c^{n} = a^{n}$
431	430	negeqd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to - (- b^{n} + c^{n}) = - a^{n}$
432	417	negnegd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to - (- b^{n}) = b^{n}$
433	432	eqcomd	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to b^{n} = - (- b^{n})$
434	433	oveq1d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to b^{n} + (- c^{n}) = - (- b^{n}) + (- c^{n})$
435	415 88	syl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to n \in ℕ$
436		simp-4r	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to \neg \frac{n}{2} \in ℕ$
437	435 285 286	sylancl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to (2 ∥ n \leftrightarrow \frac{n}{2} \in ℕ)$
438	436 437	mtbird	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to \neg 2 ∥ n$
439	420 435 438 341	syl3anc	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to {(- c)}^{n} = - c^{n}$
440	439	oveq2d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to b^{n} + {(- c)}^{n} = b^{n} + (- c^{n})$
441	418 421	negdid	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to - (- b^{n} + c^{n}) = - (- b^{n}) + (- c^{n})$
442	434 440 441	3eqtr4d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to b^{n} + {(- c)}^{n} = - (- b^{n} + c^{n})$
443	426 435 438 384	syl3anc	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to {(- a)}^{n} = - a^{n}$
444	431 442 443	3eqtr4d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to b^{n} + {(- c)}^{n} = {(- a)}^{n}$
445		iffalse	$⊢ \neg 0 < c \to if (0 < c, - a, b) = b$
446	445	oveq1d	$⊢ \neg 0 < c \to {if (0 < c, - a, b)}^{n} = b^{n}$
447	446 349	oveq12d	$⊢ \neg 0 < c \to {if (0 < c, - a, b)}^{n} + {if (0 < c, c, - c)}^{n} = b^{n} + {(- c)}^{n}$
448	447	adantl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to {if (0 < c, - a, b)}^{n} + {if (0 < c, c, - c)}^{n} = b^{n} + {(- c)}^{n}$
449		iffalse	$⊢ \neg 0 < c \to if (0 < c, b, - a) = - a$
450	449	oveq1d	$⊢ \neg 0 < c \to {if (0 < c, b, - a)}^{n} = {(- a)}^{n}$
451	450	adantl	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to {if (0 < c, b, - a)}^{n} = {(- a)}^{n}$
452	444 448 451	3eqtr4d	$⊢ ((((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \land \neg 0 < c) \to {if (0 < c, - a, b)}^{n} + {if (0 < c, c, - c)}^{n} = {if (0 < c, b, - a)}^{n}$
453	412 452	pm2.61dan	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \to {if (0 < c, - a, b)}^{n} + {if (0 < c, c, - c)}^{n} = {if (0 < c, b, - a)}^{n}$
454		iftrue	$⊢ 0 < b \to if (0 < b, if (0 < c, - a, b), - a) = if (0 < c, - a, b)$
455	454	oveq1d	$⊢ 0 < b \to {if (0 < b, if (0 < c, - a, b), - a)}^{n} = {if (0 < c, - a, b)}^{n}$
456		iftrue	$⊢ 0 < b \to if (0 < b, if (0 < c, c, - c), - b) = if (0 < c, c, - c)$
457	456	oveq1d	$⊢ 0 < b \to {if (0 < b, if (0 < c, c, - c), - b)}^{n} = {if (0 < c, c, - c)}^{n}$
458	455 457	oveq12d	$⊢ 0 < b \to {if (0 < b, if (0 < c, - a, b), - a)}^{n} + {if (0 < b, if (0 < c, c, - c), - b)}^{n} = {if (0 < c, - a, b)}^{n} + {if (0 < c, c, - c)}^{n}$
459	458	adantl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \to {if (0 < b, if (0 < c, - a, b), - a)}^{n} + {if (0 < b, if (0 < c, c, - c), - b)}^{n} = {if (0 < c, - a, b)}^{n} + {if (0 < c, c, - c)}^{n}$
460		iftrue	$⊢ 0 < b \to if (0 < b, if (0 < c, b, - a), - c) = if (0 < c, b, - a)$
461	460	oveq1d	$⊢ 0 < b \to {if (0 < b, if (0 < c, b, - a), - c)}^{n} = {if (0 < c, b, - a)}^{n}$
462	461	adantl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \to {if (0 < b, if (0 < c, b, - a), - c)}^{n} = {if (0 < c, b, - a)}^{n}$
463	453 459 462	3eqtr4d	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land 0 < b) \to {if (0 < b, if (0 < c, - a, b), - a)}^{n} + {if (0 < b, if (0 < c, c, - c), - b)}^{n} = {if (0 < b, if (0 < c, b, - a), - c)}^{n}$
464	178	negeqd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to - (a^{n} + b^{n}) = - c^{n}$
465	136 285 286	sylancl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to (2 ∥ n \leftrightarrow \frac{n}{2} \in ℕ)$
466	153 465	mtbird	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to \neg 2 ∥ n$
467	148 136 466 384	syl3anc	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to {(- a)}^{n} = - a^{n}$
468	161 136 466 289	syl3anc	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to {(- b)}^{n} = - b^{n}$
469	467 468	oveq12d	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to {(- a)}^{n} + {(- b)}^{n} = - a^{n} + (- b^{n})$
470	133 3	syl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to a \neq 0$
471	148 470 164	expclzd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to a^{n} \in ℂ$
472	161 162 164	expclzd	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to b^{n} \in ℂ$
473	471 472	negdid	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to - (a^{n} + b^{n}) = - a^{n} + (- b^{n})$
474	469 473	eqtr4d	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to {(- a)}^{n} + {(- b)}^{n} = - (a^{n} + b^{n})$
475	131 57 249	3syl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to c \in ℂ$
476	475 136 466 341	syl3anc	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to {(- c)}^{n} = - c^{n}$
477	464 474 476	3eqtr4d	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to {(- a)}^{n} + {(- b)}^{n} = {(- c)}^{n}$
478		iffalse	$⊢ \neg 0 < b \to if (0 < b, if (0 < c, - a, b), - a) = - a$
479	478	oveq1d	$⊢ \neg 0 < b \to {if (0 < b, if (0 < c, - a, b), - a)}^{n} = {(- a)}^{n}$
480		iffalse	$⊢ \neg 0 < b \to if (0 < b, if (0 < c, c, - c), - b) = - b$
481	480	oveq1d	$⊢ \neg 0 < b \to {if (0 < b, if (0 < c, c, - c), - b)}^{n} = {(- b)}^{n}$
482	479 481	oveq12d	$⊢ \neg 0 < b \to {if (0 < b, if (0 < c, - a, b), - a)}^{n} + {if (0 < b, if (0 < c, c, - c), - b)}^{n} = {(- a)}^{n} + {(- b)}^{n}$
483	482	adantl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to {if (0 < b, if (0 < c, - a, b), - a)}^{n} + {if (0 < b, if (0 < c, c, - c), - b)}^{n} = {(- a)}^{n} + {(- b)}^{n}$
484		iffalse	$⊢ \neg 0 < b \to if (0 < b, if (0 < c, b, - a), - c) = - c$
485	484	oveq1d	$⊢ \neg 0 < b \to {if (0 < b, if (0 < c, b, - a), - c)}^{n} = {(- c)}^{n}$
486	485	adantl	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to {if (0 < b, if (0 < c, b, - a), - c)}^{n} = {(- c)}^{n}$
487	477 483 486	3eqtr4d	$⊢ (((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \land \neg 0 < b) \to {if (0 < b, if (0 < c, - a, b), - a)}^{n} + {if (0 < b, if (0 < c, c, - c), - b)}^{n} = {if (0 < b, if (0 < c, b, - a), - c)}^{n}$
488	463 487	pm2.61dan	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \to {if (0 < b, if (0 < c, - a, b), - a)}^{n} + {if (0 < b, if (0 < c, c, - c), - b)}^{n} = {if (0 < b, if (0 < c, b, - a), - c)}^{n}$
489		iffalse	$⊢ \neg 0 < a \to if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)) = if (0 < b, if (0 < c, - a, b), - a)$
490	489	oveq1d	$⊢ \neg 0 < a \to {if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))}^{n} = {if (0 < b, if (0 < c, - a, b), - a)}^{n}$
491		iffalse	$⊢ \neg 0 < a \to if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)) = if (0 < b, if (0 < c, c, - c), - b)$
492	491	oveq1d	$⊢ \neg 0 < a \to {if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))}^{n} = {if (0 < b, if (0 < c, c, - c), - b)}^{n}$
493	490 492	oveq12d	$⊢ \neg 0 < a \to {if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))}^{n} + {if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))}^{n} = {if (0 < b, if (0 < c, - a, b), - a)}^{n} + {if (0 < b, if (0 < c, c, - c), - b)}^{n}$
494	493	adantl	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \to {if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))}^{n} + {if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))}^{n} = {if (0 < b, if (0 < c, - a, b), - a)}^{n} + {if (0 < b, if (0 < c, c, - c), - b)}^{n}$
495		iffalse	$⊢ \neg 0 < a \to if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)) = if (0 < b, if (0 < c, b, - a), - c)$
496	495	oveq1d	$⊢ \neg 0 < a \to {if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))}^{n} = {if (0 < b, if (0 < c, b, - a), - c)}^{n}$
497	496	adantl	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \to {if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))}^{n} = {if (0 < b, if (0 < c, b, - a), - c)}^{n}$
498	488 494 497	3eqtr4d	$⊢ ((((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \land \neg 0 < a) \to {if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))}^{n} + {if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))}^{n} = {if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))}^{n}$
499	377 498	pm2.61dan	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \to {if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))}^{n} + {if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))}^{n} = {if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))}^{n}$
500		iffalse	$⊢ \neg \frac{n}{2} \in ℕ \to if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))) = if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))$
501	500	oveq1d	$⊢ \neg \frac{n}{2} \in ℕ \to {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} = {if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))}^{n}$
502		iffalse	$⊢ \neg \frac{n}{2} \in ℕ \to if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))) = if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))$
503	502	oveq1d	$⊢ \neg \frac{n}{2} \in ℕ \to {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = {if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))}^{n}$
504	501 503	oveq12d	$⊢ \neg \frac{n}{2} \in ℕ \to {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = {if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))}^{n} + {if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))}^{n}$
505	504	adantl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \to {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = {if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a))}^{n} + {if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b))}^{n}$
506		iffalse	$⊢ \neg \frac{n}{2} \in ℕ \to if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))) = if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))$
507	506	oveq1d	$⊢ \neg \frac{n}{2} \in ℕ \to {if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)))}^{n} = {if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))}^{n}$
508	507	adantl	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \to {if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)))}^{n} = {if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c))}^{n}$
509	499 505 508	3eqtr4d	$⊢ (((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \land \neg \frac{n}{2} \in ℕ) \to {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = {if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)))}^{n}$
510	269 509	pm2.61dan	$⊢ ((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \to {if (\frac{n}{2} \in ℕ, \|a\|, if (0 < a, if (0 < b, a, if (0 < c, - b, a)), if (0 < b, if (0 < c, - a, b), - a)))}^{n} + {if (\frac{n}{2} \in ℕ, \|b\|, if (0 < a, if (0 < b, b, if (0 < c, c, - c)), if (0 < b, if (0 < c, c, - c), - b)))}^{n} = {if (\frac{n}{2} \in ℕ, \|c\|, if (0 < a, if (0 < b, c, if (0 < c, a, - b)), if (0 < b, if (0 < c, b, - a), - c)))}^{n}$
511	40 77 189 193 197 200 510	3rspcedvd	$⊢ ((((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \land c \in (ℤ ∖ \{0\})) \land a^{n} + b^{n} = c^{n}) \to \exists x \in ℕ \exists y \in ℕ \exists z \in ℕ x^{n} + y^{n} = z^{n}$
512	511	rexlimdva2	$⊢ ((n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \land b \in (ℤ ∖ \{0\})) \to (\exists c \in (ℤ ∖ \{0\}) a^{n} + b^{n} = c^{n} \to \exists x \in ℕ \exists y \in ℕ \exists z \in ℕ x^{n} + y^{n} = z^{n})$
513	512	rexlimdva	$⊢ (n \in ℤ_{\geq 3} \land a \in (ℤ ∖ \{0\})) \to (\exists b \in (ℤ ∖ \{0\}) \exists c \in (ℤ ∖ \{0\}) a^{n} + b^{n} = c^{n} \to \exists x \in ℕ \exists y \in ℕ \exists z \in ℕ x^{n} + y^{n} = z^{n})$
514	513	rexlimdva	$⊢ n \in ℤ_{\geq 3} \to (\exists a \in (ℤ ∖ \{0\}) \exists b \in (ℤ ∖ \{0\}) \exists c \in (ℤ ∖ \{0\}) a^{n} + b^{n} = c^{n} \to \exists x \in ℕ \exists y \in ℕ \exists z \in ℕ x^{n} + y^{n} = z^{n})$
515	514	reximia	$⊢ \exists n \in ℤ_{\geq 3} \exists a \in (ℤ ∖ \{0\}) \exists b \in (ℤ ∖ \{0\}) \exists c \in (ℤ ∖ \{0\}) a^{n} + b^{n} = c^{n} \to \exists n \in ℤ_{\geq 3} \exists x \in ℕ \exists y \in ℕ \exists z \in ℕ x^{n} + y^{n} = z^{n}$
516		nne	$⊢ \neg a^{n} + b^{n} \neq c^{n} \leftrightarrow a^{n} + b^{n} = c^{n}$
517	516	bicomi	$⊢ a^{n} + b^{n} = c^{n} \leftrightarrow \neg a^{n} + b^{n} \neq c^{n}$
518	517	rexbii	$⊢ \exists c \in (ℤ ∖ \{0\}) a^{n} + b^{n} = c^{n} \leftrightarrow \exists c \in (ℤ ∖ \{0\}) \neg a^{n} + b^{n} \neq c^{n}$
519		rexnal	$⊢ \exists c \in (ℤ ∖ \{0\}) \neg a^{n} + b^{n} \neq c^{n} \leftrightarrow \neg \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$
520	518 519	bitri	$⊢ \exists c \in (ℤ ∖ \{0\}) a^{n} + b^{n} = c^{n} \leftrightarrow \neg \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$
521	520	rexbii	$⊢ \exists b \in (ℤ ∖ \{0\}) \exists c \in (ℤ ∖ \{0\}) a^{n} + b^{n} = c^{n} \leftrightarrow \exists b \in (ℤ ∖ \{0\}) \neg \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$
522		rexnal	$⊢ \exists b \in (ℤ ∖ \{0\}) \neg \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n} \leftrightarrow \neg \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$
523	521 522	bitri	$⊢ \exists b \in (ℤ ∖ \{0\}) \exists c \in (ℤ ∖ \{0\}) a^{n} + b^{n} = c^{n} \leftrightarrow \neg \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$
524	523	rexbii	$⊢ \exists a \in (ℤ ∖ \{0\}) \exists b \in (ℤ ∖ \{0\}) \exists c \in (ℤ ∖ \{0\}) a^{n} + b^{n} = c^{n} \leftrightarrow \exists a \in (ℤ ∖ \{0\}) \neg \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$
525		rexnal	$⊢ \exists a \in (ℤ ∖ \{0\}) \neg \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n} \leftrightarrow \neg \forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$
526	524 525	bitri	$⊢ \exists a \in (ℤ ∖ \{0\}) \exists b \in (ℤ ∖ \{0\}) \exists c \in (ℤ ∖ \{0\}) a^{n} + b^{n} = c^{n} \leftrightarrow \neg \forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$
527	526	rexbii	$⊢ \exists n \in ℤ_{\geq 3} \exists a \in (ℤ ∖ \{0\}) \exists b \in (ℤ ∖ \{0\}) \exists c \in (ℤ ∖ \{0\}) a^{n} + b^{n} = c^{n} \leftrightarrow \exists n \in ℤ_{\geq 3} \neg \forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$
528		rexnal	$⊢ \exists n \in ℤ_{\geq 3} \neg \forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n} \leftrightarrow \neg \forall n \in ℤ_{\geq 3} \forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$
529	527 528	bitri	$⊢ \exists n \in ℤ_{\geq 3} \exists a \in (ℤ ∖ \{0\}) \exists b \in (ℤ ∖ \{0\}) \exists c \in (ℤ ∖ \{0\}) a^{n} + b^{n} = c^{n} \leftrightarrow \neg \forall n \in ℤ_{\geq 3} \forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$
530		nne	$⊢ \neg x^{n} + y^{n} \neq z^{n} \leftrightarrow x^{n} + y^{n} = z^{n}$
531	530	bicomi	$⊢ x^{n} + y^{n} = z^{n} \leftrightarrow \neg x^{n} + y^{n} \neq z^{n}$
532	531	rexbii	$⊢ \exists z \in ℕ x^{n} + y^{n} = z^{n} \leftrightarrow \exists z \in ℕ \neg x^{n} + y^{n} \neq z^{n}$
533		rexnal	$⊢ \exists z \in ℕ \neg x^{n} + y^{n} \neq z^{n} \leftrightarrow \neg \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
534	532 533	bitri	$⊢ \exists z \in ℕ x^{n} + y^{n} = z^{n} \leftrightarrow \neg \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
535	534	rexbii	$⊢ \exists y \in ℕ \exists z \in ℕ x^{n} + y^{n} = z^{n} \leftrightarrow \exists y \in ℕ \neg \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
536		rexnal	$⊢ \exists y \in ℕ \neg \forall z \in ℕ x^{n} + y^{n} \neq z^{n} \leftrightarrow \neg \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
537	535 536	bitri	$⊢ \exists y \in ℕ \exists z \in ℕ x^{n} + y^{n} = z^{n} \leftrightarrow \neg \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
538	537	rexbii	$⊢ \exists x \in ℕ \exists y \in ℕ \exists z \in ℕ x^{n} + y^{n} = z^{n} \leftrightarrow \exists x \in ℕ \neg \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
539		rexnal	$⊢ \exists x \in ℕ \neg \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n} \leftrightarrow \neg \forall x \in ℕ \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
540	538 539	bitri	$⊢ \exists x \in ℕ \exists y \in ℕ \exists z \in ℕ x^{n} + y^{n} = z^{n} \leftrightarrow \neg \forall x \in ℕ \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
541	540	rexbii	$⊢ \exists n \in ℤ_{\geq 3} \exists x \in ℕ \exists y \in ℕ \exists z \in ℕ x^{n} + y^{n} = z^{n} \leftrightarrow \exists n \in ℤ_{\geq 3} \neg \forall x \in ℕ \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
542		rexnal	$⊢ \exists n \in ℤ_{\geq 3} \neg \forall x \in ℕ \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n} \leftrightarrow \neg \forall n \in ℤ_{\geq 3} \forall x \in ℕ \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
543	541 542	bitri	$⊢ \exists n \in ℤ_{\geq 3} \exists x \in ℕ \exists y \in ℕ \exists z \in ℕ x^{n} + y^{n} = z^{n} \leftrightarrow \neg \forall n \in ℤ_{\geq 3} \forall x \in ℕ \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
544	515 529 543	3imtr3i	$⊢ \neg \forall n \in ℤ_{\geq 3} \forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n} \to \neg \forall n \in ℤ_{\geq 3} \forall x \in ℕ \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
545	544	con4i	$⊢ \forall n \in ℤ_{\geq 3} \forall x \in ℕ \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n} \to \forall n \in ℤ_{\geq 3} \forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$
546		dfn2	$⊢ ℕ = ℕ_{0} ∖ \{0\}$
547		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
548		ssdif	$⊢ ℕ_{0} \subseteq ℤ \to ℕ_{0} ∖ \{0\} \subseteq ℤ ∖ \{0\}$
549	547 548	ax-mp	$⊢ ℕ_{0} ∖ \{0\} \subseteq ℤ ∖ \{0\}$
550	546 549	eqsstri	$⊢ ℕ \subseteq ℤ ∖ \{0\}$
551		ssel	$⊢ ℕ \subseteq ℤ ∖ \{0\} \to (a \in ℕ \to a \in (ℤ ∖ \{0\}))$
552		ss2ralv	$⊢ ℕ \subseteq ℤ ∖ \{0\} \to (\forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n} \to \forall b \in ℕ \forall c \in ℕ a^{n} + b^{n} \neq c^{n})$
553	551 552	imim12d	$⊢ ℕ \subseteq ℤ ∖ \{0\} \to ((a \in (ℤ ∖ \{0\}) \to \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}) \to (a \in ℕ \to \forall b \in ℕ \forall c \in ℕ a^{n} + b^{n} \neq c^{n}))$
554	553	ralimdv2	$⊢ ℕ \subseteq ℤ ∖ \{0\} \to (\forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n} \to \forall a \in ℕ \forall b \in ℕ \forall c \in ℕ a^{n} + b^{n} \neq c^{n})$
555	550 554	ax-mp	$⊢ \forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n} \to \forall a \in ℕ \forall b \in ℕ \forall c \in ℕ a^{n} + b^{n} \neq c^{n}$
556		oveq1	$⊢ a = x \to a^{n} = x^{n}$
557	556	oveq1d	$⊢ a = x \to a^{n} + b^{n} = x^{n} + b^{n}$
558	557	neeq1d	$⊢ a = x \to (a^{n} + b^{n} \neq c^{n} \leftrightarrow x^{n} + b^{n} \neq c^{n})$
559		oveq1	$⊢ b = y \to b^{n} = y^{n}$
560	559	oveq2d	$⊢ b = y \to x^{n} + b^{n} = x^{n} + y^{n}$
561	560	neeq1d	$⊢ b = y \to (x^{n} + b^{n} \neq c^{n} \leftrightarrow x^{n} + y^{n} \neq c^{n})$
562		oveq1	$⊢ c = z \to c^{n} = z^{n}$
563	562	neeq2d	$⊢ c = z \to (x^{n} + y^{n} \neq c^{n} \leftrightarrow x^{n} + y^{n} \neq z^{n})$
564	558 561 563	cbvral3vw	$⊢ \forall a \in ℕ \forall b \in ℕ \forall c \in ℕ a^{n} + b^{n} \neq c^{n} \leftrightarrow \forall x \in ℕ \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
565	555 564	sylib	$⊢ \forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n} \to \forall x \in ℕ \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
566	565	ralimi	$⊢ \forall n \in ℤ_{\geq 3} \forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n} \to \forall n \in ℤ_{\geq 3} \forall x \in ℕ \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n}$
567	545 566	impbii	$⊢ \forall n \in ℤ_{\geq 3} \forall x \in ℕ \forall y \in ℕ \forall z \in ℕ x^{n} + y^{n} \neq z^{n} \leftrightarrow \forall n \in ℤ_{\geq 3} \forall a \in (ℤ ∖ \{0\}) \forall b \in (ℤ ∖ \{0\}) \forall c \in (ℤ ∖ \{0\}) a^{n} + b^{n} \neq c^{n}$

Metamath Proof Explorer

Theorem dffltz

Proof