let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for i, j being Integer holds (a |^ i) \ (a |^ j) = a |^ (i - j)
let a be Element of AtomSet X; :: thesis: for i, j being Integer holds (a |^ i) \ (a |^ j) = a |^ (i - j)
let i, j be Integer; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
per cases ( i > 0 or i = 0 or i < 0 ) ;
suppose A1: i > 0 ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
per cases ( j > 0 or j = 0 or j < 0 ) ;
suppose j > 0 ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A1, Lm3; :: thesis: verum
end;
suppose A2: j = 0 ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
a |^ (i - 0) = (a |^ i) \ (0. X) by BCIALG_1:2
.= (a |^ i) \ (a |^ 0) by Def1 ;
hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A2; :: thesis: verum
end;
suppose A3: j < 0 ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
set m = - j;
reconsider i = i, m = - j as Element of NAT by A1, A3, INT_1:3;
a |^ j = (BCI-power X) . ((a `),|.j.|) by A3, Def2
.= (a `) |^ m by A3, ABSVALUE:def 1
.= (a |^ m) ` by Th17 ;
then (a |^ i) \ (a |^ j) = a |^ (i + m) by Lm1;
hence (a |^ i) \ (a |^ j) = a |^ (i - j) ; :: thesis: verum
end;
end;
end;
suppose A4: i = 0 ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
per cases ( j >= 0 or j < 0 ) ;
suppose j >= 0 ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
then reconsider j = j as Element of NAT by INT_1:3;
(a |^ 0) \ (a |^ j) = (a |^ j) ` by Def1
.= (a `) |^ j by Th17
.= a |^ (- j) by Th10 ;
hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A4; :: thesis: verum
end;
suppose A5: j < 0 ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
set m = - j;
reconsider m = - j as Element of NAT by A5, INT_1:3;
a |^ j = (BCI-power X) . ((a `),|.j.|) by A5, Def2
.= (a `) |^ m by A5, ABSVALUE:def 1
.= (a |^ m) ` by Th17 ;
then (a |^ 0) \ (a |^ j) = a |^ (0 + m) by Lm1;
hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A4; :: thesis: verum
end;
end;
end;
suppose A6: i < 0 ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
then reconsider m = - i as Element of NAT by INT_1:3;
A7: - i > 0 by A6;
per cases ( j >= 0 or j < 0 ) ;
suppose A8: j >= 0 ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
set n = - (i - j);
reconsider n = - (i - j), j = j as Element of NAT by A6, A8, INT_1:3;
reconsider b = a ` as Element of AtomSet X by BCIALG_1:34;
A9: ((a `) |^ j) ` = (b `) |^ j by Th17
.= a |^ j by BCIALG_1:29 ;
A10: a |^ i = (BCI-power X) . ((a `),|.i.|) by A6, Def2
.= (a `) |^ m by A6, ABSVALUE:def 1 ;
a |^ (i - j) = (BCI-power X) . ((a `),|.(i - j).|) by A6, Def2
.= (a `) |^ n by A6, ABSVALUE:def 1
.= b |^ (j + m)
.= ((a `) |^ m) \ (((a `) |^ j) `) by Lm1 ;
hence (a |^ i) \ (a |^ j) = a |^ (i - j) by A10, A9; :: thesis: verum
end;
suppose A11: j < 0 ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
reconsider b = a ` as Element of AtomSet X by BCIALG_1:34;
A12: - j > 0 by A11;
reconsider n = - j as Element of NAT by A11, INT_1:3;
A13: a |^ j = (BCI-power X) . ((a `),|.j.|) by A11, Def2
.= (a `) |^ n by A11, ABSVALUE:def 1 ;
a |^ i = (BCI-power X) . ((a `),|.i.|) by A6, Def2
.= (a `) |^ m by A6, ABSVALUE:def 1 ;
then A14: (a |^ i) \ (a |^ j) = b |^ (m - n) by A7, A12, A13, Lm3;
per cases ( m >= n or m < n ) ;
suppose m >= n ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
then reconsider q = m - n as Element of NAT by INT_1:3, XREAL_1:48;
(a |^ i) \ (a |^ j) = a |^ (- q) by A14, Th10;
hence (a |^ i) \ (a |^ j) = a |^ (i - j) ; :: thesis: verum
end;
suppose A15: m < n ; :: thesis: (a |^ i) \ (a |^ j) = a |^ (i - j)
then n - m > 0 by XREAL_1:50;
then reconsider p = n - m as Element of NAT by INT_1:3;
A16: m - n < 0 by A15, XREAL_1:49;
then (a |^ i) \ (a |^ j) = (BCI-power X) . ((b `),|.(m - n).|) by A14, Def2
.= (BCI-power X) . ((b `),(- (m - n))) by A16, ABSVALUE:def 1
.= a |^ p by BCIALG_1:29 ;
hence (a |^ i) \ (a |^ j) = a |^ (i - j) ; :: thesis: verum
end;
end;
end;
end;
end;
end;