Metamath Proof Explorer

Theorem 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 ⊢∀n∈ℤ≥3∀x∈ℕ∀y∈ℕ∀z∈ℕxn+yn≠zn↔∀n∈ℤ≥3∀a∈ℤ∖0∀b∈ℤ∖0∀c∈ℤ∖0an+bn≠cn

Proof

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