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 
|- ( A. n e. ( ZZ>= ` 3 ) A. x e. NN A. y e. NN A. z e. NN ( ( x ^ n ) + ( y ^ n ) ) =/= ( z ^ n ) <-> A. n e. ( ZZ>= ` 3 ) A. a e. ( ZZ \ { 0 } ) A. b e. ( ZZ \ { 0 } ) A. c e. ( ZZ \ { 0 } ) ( ( a ^ n ) + ( b ^ n ) ) =/= ( c ^ n ) )

Proof

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