This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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