let L be Field; 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; 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; ( x <> 0. L implies pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1)) )
A1:
pow (x,(- 1)) = (x |^ |.(- 1).|) "
by Def2;
assume A2:
x <> 0. L
; pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1))
then
x |^ |.(- 1).| <> 0. L
by Th1;
then A3:
pow (x,(- 1)) <> 0. L
by A1, VECTSP_1:25;
A4:
pow (x,(- j)) <> 0. L
A7:
pow (x,(j + 1)) <> 0. L
A10:
now (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = 1. Lper cases
( j >= 0 or j < - 1 or j = - 1 )
by Lm1;
suppose A11:
j >= 0
;
(pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = 1. Lthen reconsider n =
j as
Element of
NAT by INT_1:3;
A12:
n + 1
= |.(j + 1).|
by ABSVALUE:def 1;
pow (
x,
|.j.|)
= x |^ |.j.|
by Def2;
then A13:
pow (
x,
|.j.|)
<> 0. L
by A2, Th1;
pow (
x,
|.(j + 1).|)
= x |^ |.(j + 1).|
by Def2;
then A14:
pow (
x,
|.(j + 1).|)
<> 0. L
by A2, Th1;
n + 1
>= 0
;
hence (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) =
(pow (x,|.(j + 1).|)) * ((pow (x,(- 1))) * (pow (x,(- j))))
by ABSVALUE:def 1
.=
(pow (x,|.(j + 1).|)) * ((x ") * (pow (x,(- j))))
by Th15
.=
(pow (x,|.(j + 1).|)) * ((x ") * ((pow (x,j)) "))
by A2, Th18
.=
(pow (x,|.(j + 1).|)) * ((x ") * ((pow (x,|.j.|)) "))
by A11, ABSVALUE:def 1
.=
(pow (x,|.(j + 1).|)) * ((x * (pow (x,|.j.|))) ")
by A2, A13, Th2
.=
(pow (x,|.(j + 1).|)) * ((pow (x,(|.j.| + 1))) ")
by Th17
.=
(pow (x,|.(j + 1).|)) * ((pow (x,|.(j + 1).|)) ")
by A12, ABSVALUE:def 1
.=
1. L
by A14, VECTSP_1:def 10
;
verum end; suppose A15:
j < - 1
;
(pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = 1. LA16:
pow (
x,
(- j))
<> 0. L
pow (
x,
|.(j + 1).|)
= x |^ |.(j + 1).|
by Def2;
then A17:
pow (
x,
|.(j + 1).|)
<> 0. L
by A2, Th1;
A18:
j + 1
< (- 1) + 1
by A15, XREAL_1:6;
hence (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) =
((pow (x,|.(j + 1).|)) ") * ((pow (x,(- 1))) * (pow (x,(- j))))
by Lm3
.=
((pow (x,|.(j + 1).|)) ") * ((x ") * (pow (x,(- j))))
by Th15
.=
(((pow (x,|.(j + 1).|)) ") * (x ")) * (pow (x,(- j)))
by GROUP_1:def 3
.=
(((pow (x,|.(j + 1).|)) * x) ") * (pow (x,(- j)))
by A2, A17, Th2
.=
((pow (x,(|.(j + 1).| + 1))) ") * (pow (x,(- j)))
by Th17
.=
((pow (x,((- (j + 1)) + 1))) ") * (pow (x,(- j)))
by A18, ABSVALUE:def 1
.=
1. L
by A16, VECTSP_1:def 10
;
verum end; suppose A19:
j = - 1
;
(pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = 1. LA20:
x " <> 0. L
by A2, VECTSP_1:25;
thus (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) =
(1. L) * ((pow (x,(- 1))) * (pow (x,(- j))))
by A19, Th13
.=
(pow (x,(- 1))) * (pow (x,(- j)))
.=
(x ") * (pow (x,(- j)))
by Th15
.=
(x ") * ((pow (x,j)) ")
by A2, Th18
.=
(x ") * ((x ") ")
by A19, Th15
.=
1. L
by A20, VECTSP_1:def 10
;
verum end; end; end;
A21:
pow (x,(j + 1)) <> 0. L
(pow (x,(j + 1))) * (pow (x,(- (j + 1)))) =
(pow (x,(j + 1))) * ((pow (x,(j + 1))) ")
by A2, Th18
.=
1. L
by A7, VECTSP_1:def 10
;
then A24:
pow (x,(- (j + 1))) = (pow (x,(- 1))) * (pow (x,(- j)))
by A10, A21, VECTSP_1:5;
thus pow (x,(j + 1)) =
pow (x,(- (- (j + 1))))
.=
((pow (x,(- 1))) * (pow (x,(- j)))) "
by A2, A24, Th18
.=
((pow (x,(- j))) ") * ((pow (x,(- 1))) ")
by A4, A3, Th2
.=
(pow (x,(- (- j)))) * ((pow (x,(- 1))) ")
by A2, Th18
.=
(pow (x,j)) * (pow (x,(- (- 1))))
by A2, Th18
.=
(pow (x,j)) * (pow (x,1))
; verum