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		eluzge3nn	|- ( 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 ) )