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:3;
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:25; :: 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:52;
j >= 1 + 0 by A6;
then A10: j - 1 >= 0 by XREAL_1:19;
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 3
.= ((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 10 ; :: 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 10 ; :: 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 3
.= (1. L) * (pow (x,(- j))) by A1, VECTSP_1:def 10
.= pow (x,0) by A15, VECTSP_1:def 8
.= 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:3;
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:25; :: 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:3;
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:25; :: 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 10 ;
then x * (pow (x,(- j))) = pow (x,(1 - j)) by A5, A19, VECTSP_1:5;
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