let L be Field; :: thesis: for j being Integer
for x being Element of L st x <> 0. L holds
pow x,(j - 1) = (pow x,j) * (pow x,(- 1))
let j be Integer; :: thesis: for x being Element of L st x <> 0. L holds
pow x,(j - 1) = (pow x,j) * (pow x,(- 1))
let x be Element of L; :: thesis: ( x <> 0. L implies pow x,(j - 1) = (pow x,j) * (pow x,(- 1)) )
assume A1: x <> 0. L ; :: thesis: pow x,(j - 1) = (pow x,j) * (pow x,(- 1))
A2: pow x,(j - 1) <> 0. L

proof

per cases ( 0 <= j - 1 or j - 1 < 0 ) ;

suppose 0 <= j - 1 ; :: thesis: pow x,(j - 1) <> 0. L

then reconsider k = j - 1 as Element of NAT by INT_1:16;
pow x,(j - 1) = x |^ k by Def3;
hence pow x,(j - 1) <> 0. L by A1, Th1; :: thesis: verum

end;

suppose A3: j - 1 < 0 ; :: thesis: pow x,(j - 1) <> 0. L

A4: x |^ (abs (j - 1)) <> 0. L by A1, Th1;
pow x,(j - 1) = (x |^ (abs (j - 1))) " by A3, Def3;
hence pow x,(j - 1) <> 0. L by A4, VECTSP_1:74; :: thesis: verum

end;

end;

end;

A5: now

per cases ( j >= 1 or j < 0 or j = 0 ) by Lm2;

suppose A6: j >= 1 ; :: thesis: (pow x,(j - 1)) * (x * (pow x,(- j))) = 1. L

then A7: abs j = j by ABSVALUE:def 1;
pow x,(abs (- j)) = x |^ (abs (- j)) by Def3;
then A8: pow x,(abs (- j)) <> 0. L by A1, Th1;
A9: abs j = abs (- j) by COMPLEX1:138;
j >= 1 + 0 by A6;
then A10: j - 1 >= 0 by XREAL_1:21;
then A11: (abs (j - 1)) + 1 = (j - 1) + 1 by ABSVALUE:def 1
.= j ;
thus (pow x,(j - 1)) * (x * (pow x,(- j))) = ((pow x,(j - 1)) * x) * (pow x,(- j)) by GROUP_1:def 4
.= ((pow x,(abs (j - 1))) * x) * (pow x,(- j)) by A10, ABSVALUE:def 1
.= ((pow x,(abs (j - 1))) * x) * ((pow x,(abs (- j))) " ) by A6, Lm4
.= (pow x,((abs (j - 1)) + 1)) * ((pow x,(abs (- j))) " ) by Th17
.= 1. L by A8, A11, A7, A9, VECTSP_1:def 22 ; :: thesis: verum

end;

suppose A12: j < 0 ; :: thesis: (pow x,(j - 1)) * (x * (pow x,(- j))) = 1. L

pow x,(abs (j - 1)) = x |^ (abs (j - 1)) by Def3;
then A13: pow x,(abs (j - 1)) <> 0. L by A1, Th1;
A14: 1 - j = - (j - 1) ;
thus (pow x,(j - 1)) * (x * (pow x,(- j))) = ((pow x,(abs (j - 1))) " ) * (x * (pow x,(- j))) by A12, Lm3
.= ((pow x,(abs (j - 1))) " ) * (x * (pow x,(abs (- j)))) by A12, ABSVALUE:def 1
.= ((pow x,(abs (j - 1))) " ) * (pow x,(1 + (abs (- j)))) by Th17
.= ((pow x,(abs (j - 1))) " ) * (pow x,(1 + (- j))) by A12, ABSVALUE:def 1
.= ((pow x,(abs (j - 1))) " ) * (pow x,(abs (j - 1))) by A12, A14, ABSVALUE:def 1
.= 1. L by A13, VECTSP_1:def 22 ; :: thesis: verum

end;

suppose A15: j = 0 ; :: thesis: (pow x,(j - 1)) * (x * (pow x,(- j))) = 1. L

hence (pow x,(j - 1)) * (x * (pow x,(- j))) = (x " ) * (x * (pow x,(- j))) by Th15
.= ((x " ) * x) * (pow x,(- j)) by GROUP_1:def 4
.= (1. L) * (pow x,(- j)) by A1, VECTSP_1:def 22
.= pow x,0 by A15, VECTSP_1:def 19
.= 1. L by Th13 ;
:: thesis: verum

end;

end;

end;

A16: pow x,(- j) <> 0. L

proof

per cases ( 0 <= - j or - j < 0 ) ;

suppose 0 <= - j ; :: thesis: pow x,(- j) <> 0. L

then reconsider k = - j as Element of NAT by INT_1:16;
pow x,(- j) = x |^ k by Def3;
hence pow x,(- j) <> 0. L by A1, Th1; :: thesis: verum

end;

suppose A17: - j < 0 ; :: thesis: pow x,(- j) <> 0. L

A18: x |^ (abs (- j)) <> 0. L by A1, Th1;
pow x,(- j) = (x |^ (abs (- j))) " by A17, Def3;
hence pow x,(- j) <> 0. L by A18, VECTSP_1:74; :: thesis: verum

end;

end;

end;

A19: pow x,(j - 1) <> 0. L

proof

per cases ( 0 <= j - 1 or j - 1 < 0 ) ;

suppose 0 <= j - 1 ; :: thesis: pow x,(j - 1) <> 0. L

then reconsider k = j - 1 as Element of NAT by INT_1:16;
pow x,(j - 1) = x |^ k by Def3;
hence pow x,(j - 1) <> 0. L by A1, Th1; :: thesis: verum

end;

suppose A20: j - 1 < 0 ; :: thesis: pow x,(j - 1) <> 0. L

A21: x |^ (abs (j - 1)) <> 0. L by A1, Th1;
pow x,(j - 1) = (x |^ (abs (j - 1))) " by A20, Def3;
hence pow x,(j - 1) <> 0. L by A21, VECTSP_1:74; :: thesis: verum

end;

end;

end;

(pow x,(j - 1)) * (pow x,(1 - j)) = (pow x,(j - 1)) * (pow x,(- (j - 1)))
.= (pow x,(j - 1)) * ((pow x,(j - 1)) " ) by A1, Th18
.= 1. L by A2, VECTSP_1:def 22 ;
then x * (pow x,(- j)) = pow x,(1 - j) by A5, A19, VECTSP_1:33;
then (pow x,(1 - j)) " = ((pow x,(- j)) " ) * (x " ) by A1, A16, Th2
.= (pow x,(- (- j))) * (x " ) by A1, Th18
.= (pow x,j) * (pow x,(- 1)) by Th15 ;
then (pow x,j) * (pow x,(- 1)) = pow x,(- (1 - j)) by A1, Th18;
hence pow x,(j - 1) = (pow x,j) * (pow x,(- 1)) ; :: thesis: verum