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: now

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

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

then j >= 1 + 0 ;
then A4: j - 1 >= 0 by XREAL_1:21;
A5: pow x,(abs (- j)) <> 0. L

proof

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

end;

A6: ( - 1 >= - j & 0 >= - 1 ) by A3, XREAL_1:26;
A7: (abs (j - 1)) + 1 = (j - 1) + 1 by A4, ABSVALUE:def 1
.= j ;
A8: ( abs j = j & abs j = abs (- j) ) by A3, ABSVALUE:def 1, COMPLEX1:138;
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 A4, 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 A5, A7, A8, VECTSP_1:def 22 ; :: thesis: verum

end;

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

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

proof

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

end;

A12: j + (- 1) < 0 by A9;
then A13: - (j - 1) > - 0 by XREAL_1:26;
A14: - j >= - 0 by A9;
1 - j = - (j - 1) ;
then A15: abs (1 - j) = abs (j - 1) by COMPLEX1:138;
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 A14, 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 A14, ABSVALUE:def 1
.= ((pow x,(abs (j - 1))) " ) * (pow x,(abs (j - 1))) by A13, A15, ABSVALUE:def 1
.= 1. L by A11, VECTSP_1:def 22 ; :: thesis: verum

end;

suppose A16: 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 A16, VECTSP_1:def 19
.= 1. L by Th13 ;
:: thesis: verum

end;

end;

end;

A17: 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 j - 1 < 0 ; :: thesis: pow x,(j - 1) <> 0. L

then A18: pow x,(j - 1) = (x |^ (abs (j - 1))) " by Def3;
x |^ (abs (j - 1)) <> 0. L by A1, Th1;
hence pow x,(j - 1) <> 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 j - 1 < 0 ; :: thesis: pow x,(j - 1) <> 0. L

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

end;

end;

end;

A21: 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 - j < 0 ; :: thesis: pow x,(- j) <> 0. L

then A22: pow x,(- j) = (x |^ (abs (- j))) " by Def3;
x |^ (abs (- j)) <> 0. L by A1, Th1;
hence pow x,(- j) <> 0. L by A22, 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 A17, VECTSP_1:def 22 ;
then x * (pow x,(- j)) = pow x,(1 - j) by A2, A19, VECTSP_1:33;
then (pow x,(1 - j)) " = ((pow x,(- j)) " ) * (x " ) by A1, A21, 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