begin
definition
let x,
y,
w,
z,
a,
b,
c,
d be
set ;
func (
x,
y,
w,
z)
--> (
a,
b,
c,
d)
-> set equals
((x,y) --> (a,b)) +* ((w,z) --> (c,d));
coherence
((x,y) --> (a,b)) +* ((w,z) --> (c,d)) is set
;
end;
::
deftheorem defines
--> QUATERNI:def 3 :
for x, y, w, z, a, b, c, d being set holds (x,y,w,z) --> (a,b,c,d) = ((x,y) --> (a,b)) +* ((w,z) --> (c,d));
registration
let x,
y,
w,
z,
a,
b,
c,
d be
set ;
coherence
( (x,y,w,z) --> (a,b,c,d) is Function-like & (x,y,w,z) --> (a,b,c,d) is Relation-like )
;
end;
theorem Th1:
for
x,
y,
w,
z,
a,
b,
c,
d being
set holds
dom ((x,y,w,z) --> (a,b,c,d)) = {x,y,w,z}
theorem Th2:
for
x,
y,
w,
z,
a,
b,
c,
d being
set holds
rng ((x,y,w,z) --> (a,b,c,d)) c= {a,b,c,d}
Lm1:
0 ,1,2,3 are_mutually_different
by ZFMISC_1:def 6;
theorem Th3:
for
x,
y,
w,
z,
a,
b,
c,
d being
set st
x,
y,
w,
z are_mutually_different holds
(
((x,y,w,z) --> (a,b,c,d)) . x = a &
((x,y,w,z) --> (a,b,c,d)) . y = b &
((x,y,w,z) --> (a,b,c,d)) . w = c &
((x,y,w,z) --> (a,b,c,d)) . z = d )
Lm2:
for x, y, w, z, a, b, c, d being set st x,y,w,z are_mutually_different holds
{a,b,c,d} c= rng ((x,y,w,z) --> (a,b,c,d))
theorem
for
x,
y,
w,
z,
a,
b,
c,
d being
set st
x,
y,
w,
z are_mutually_different holds
rng ((x,y,w,z) --> (a,b,c,d)) = {a,b,c,d}
theorem
for
x1,
x2,
x3,
x4,
X being
set holds
(
{x1,x2,x3,x4} c= X iff (
x1 in X &
x2 in X &
x3 in X &
x4 in X ) )
definition
let A be non
empty set ;
let x,
y,
w,
z be
set ;
let a,
b,
c,
d be
Element of
A;
-->redefine func (
x,
y,
w,
z)
--> (
a,
b,
c,
d)
-> Function of
{x,y,w,z},
A;
coherence
(x,y,w,z) --> (a,b,c,d) is Function of {x,y,w,z},A
end;
definition
coherence
(0,1,2,3) --> (0,0,1,0) is set
;
coherence
(0,1,2,3) --> (0,0,0,1) is set
;
end;
Lm3:
<i> = [*0,1*]
by ARYTM_0:def 5;
definition
let x,
y,
w,
z be
real number ;
func [*x,y,w,z*] -> Element of
QUATERNION means :
Def6:
ex
x9,
y9 being
Element of
REAL st
(
x9 = x &
y9 = y &
it = [*x9,y9*] )
if (
w = 0 &
z = 0 )
otherwise it = (
0,1,2,3)
--> (
x,
y,
w,
z);
consistency
for b1 being Element of QUATERNION holds verum
;
existence
( ( w = 0 & z = 0 implies ex b1 being Element of QUATERNION ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & b1 = [*x9,y9*] ) ) & ( ( not w = 0 or not z = 0 ) implies ex b1 being Element of QUATERNION st b1 = (0,1,2,3) --> (x,y,w,z) ) )
uniqueness
for b1, b2 being Element of QUATERNION holds
( ( w = 0 & z = 0 & ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & b1 = [*x9,y9*] ) & ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & b2 = [*x9,y9*] ) implies b1 = b2 ) & ( ( not w = 0 or not z = 0 ) & b1 = (0,1,2,3) --> (x,y,w,z) & b2 = (0,1,2,3) --> (x,y,w,z) implies b1 = b2 ) )
;
end;
::
deftheorem Def6 defines
[* QUATERNI:def 6 :
for x, y, w, z being real number
for b5 being Element of QUATERNION holds
( ( w = 0 & z = 0 implies ( b5 = [*x,y,w,z*] iff ex x9, y9 being Element of REAL st
( x9 = x & y9 = y & b5 = [*x9,y9*] ) ) ) & ( ( not w = 0 or not z = 0 ) implies ( b5 = [*x,y,w,z*] iff b5 = (0,1,2,3) --> (x,y,w,z) ) ) );
Lm4:
for x, y being Element of REAL holds [*x,y,0,0*] = [*x,y*]
theorem Th6:
for
a,
b,
c,
d,
e,
i,
j,
k being
set for
g being
Function st
a <> b &
c <> d &
dom g = {a,b,c,d} &
g . a = e &
g . b = i &
g . c = j &
g . d = k holds
g = (
a,
b,
c,
d)
--> (
e,
i,
j,
k)
theorem Th8:
for
a,
c,
x,
w,
b,
d,
y,
z being
set st
a,
c,
x,
w are_mutually_different holds
(
a,
c,
x,
w)
--> (
b,
d,
y,
z)
= {[a,b],[c,d],[x,y],[w,z]}
Lm5:
for x, y, z being set st [x,y] = {z} holds
( z = {x} & x = y )
Lm6:
for a, b, c, d being Element of REAL holds not (0,1,2,3) --> (a,b,c,d) in REAL
theorem Th11:
for
a,
b,
c,
d,
x,
y,
z,
w,
x9,
y9,
z9,
w9 being
set st
a,
b,
c,
d are_mutually_different & (
a,
b,
c,
d)
--> (
x,
y,
z,
w)
= (
a,
b,
c,
d)
--> (
x9,
y9,
z9,
w9) holds
(
x = x9 &
y = y9 &
z = z9 &
w = w9 )
theorem Th12:
for
x1,
x2,
x3,
x4,
y1,
y2,
y3,
y4 being
Element of
REAL st
[*x1,x2,x3,x4*] = [*y1,y2,y3,y4*] holds
(
x1 = y1 &
x2 = y2 &
x3 = y3 &
x4 = y4 )
definition
let x,
y be
quaternion number ;
consider x1,
x2,
x3,
x4 being
Element of
REAL such that A1:
x = [*x1,x2,x3,x4*]
by Th7;
consider y1,
y2,
y3,
y4 being
Element of
REAL such that A2:
y = [*y1,y2,y3,y4*]
by Th7;
func x + y -> set means :
Def7:
ex
x1,
x2,
x3,
x4,
y1,
y2,
y3,
y4 being
Element of
REAL st
(
x = [*x1,x2,x3,x4*] &
y = [*y1,y2,y3,y4*] &
it = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] );
existence
ex b1 being set ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] )
uniqueness
for b1, b2 being set st ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) & ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b2 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) holds
b1 = b2
commutativity
for b1 being set
for x, y being quaternion number st ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) holds
ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( y = [*x1,x2,x3,x4*] & x = [*y1,y2,y3,y4*] & b1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] )
;
end;
::
deftheorem Def7 defines
+ QUATERNI:def 7 :
for x, y being quaternion number
for b3 being set holds
( b3 = x + y iff ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b3 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) );
Lm7:
0 = [*0,0,0,0*]
definition
let x,
y be
quaternion number ;
consider x1,
x2,
x3,
x4 being
Element of
REAL such that A1:
x = [*x1,x2,x3,x4*]
by Th7;
consider y1,
y2,
y3,
y4 being
Element of
REAL such that A2:
y = [*y1,y2,y3,y4*]
by Th7;
func x * y -> set means :
Def10:
ex
x1,
x2,
x3,
x4,
y1,
y2,
y3,
y4 being
Element of
REAL st
(
x = [*x1,x2,x3,x4*] &
y = [*y1,y2,y3,y4*] &
it = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)),((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)),((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)),((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] );
existence
ex b1 being set ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)),((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)),((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)),((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] )
uniqueness
for b1, b2 being set st ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b1 = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)),((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)),((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)),((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] ) & ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b2 = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)),((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)),((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)),((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] ) holds
b1 = b2
end;
::
deftheorem Def10 defines
* QUATERNI:def 10 :
for x, y being quaternion number
for b3 being set holds
( b3 = x * y iff ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & b3 = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)),((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)),((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)),((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] ) );
definition
let z be
quaternion number ;
existence
( ( z in COMPLEX implies ex b1 being set ex z9 being complex number st
( z = z9 & b1 = Re z9 ) ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 0 ) ) )
uniqueness
for b1, b2 being set holds
( ( z in COMPLEX & ex z9 being complex number st
( z = z9 & b1 = Re z9 ) & ex z9 being complex number st
( z = z9 & b2 = Re z9 ) implies b1 = b2 ) & ( not z in COMPLEX & ex f being Function of 4,REAL st
( z = f & b1 = f . 0 ) & ex f being Function of 4,REAL st
( z = f & b2 = f . 0 ) implies b1 = b2 ) )
;
consistency
for b1 being set holds verum
;
existence
( ( z in COMPLEX implies ex b1 being set ex z9 being complex number st
( z = z9 & b1 = Im z9 ) ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 1 ) ) )
uniqueness
for b1, b2 being set holds
( ( z in COMPLEX & ex z9 being complex number st
( z = z9 & b1 = Im z9 ) & ex z9 being complex number st
( z = z9 & b2 = Im z9 ) implies b1 = b2 ) & ( not z in COMPLEX & ex f being Function of 4,REAL st
( z = f & b1 = f . 1 ) & ex f being Function of 4,REAL st
( z = f & b2 = f . 1 ) implies b1 = b2 ) )
;
consistency
for b1 being set holds verum
;
existence
( ( z in COMPLEX implies ex b1 being set st b1 = 0 ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 2 ) ) )
uniqueness
for b1, b2 being set holds
( ( z in COMPLEX & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not z in COMPLEX & ex f being Function of 4,REAL st
( z = f & b1 = f . 2 ) & ex f being Function of 4,REAL st
( z = f & b2 = f . 2 ) implies b1 = b2 ) )
;
consistency
for b1 being set holds verum
;
existence
( ( z in COMPLEX implies ex b1 being set st b1 = 0 ) & ( not z in COMPLEX implies ex b1 being set ex f being Function of 4,REAL st
( z = f & b1 = f . 3 ) ) )
uniqueness
for b1, b2 being set holds
( ( z in COMPLEX & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not z in COMPLEX & ex f being Function of 4,REAL st
( z = f & b1 = f . 3 ) & ex f being Function of 4,REAL st
( z = f & b2 = f . 3 ) implies b1 = b2 ) )
;
consistency
for b1 being set holds verum
;
end;
theorem Th22:
for
f being
Function of 4,
REAL ex
a,
b,
c,
d being
Element of
REAL st
f = (
0,1,2,3)
--> (
a,
b,
c,
d)
Lm8:
for a, b being Element of REAL holds
( Re [*a,b*] = a & Im [*a,b*] = b )
Lm9:
for z being complex number holds [*(Re z),(Im z)*] = z
theorem Th23:
for
a,
b,
c,
d being
Element of
REAL holds
(
Rea [*a,b,c,d*] = a &
Im1 [*a,b,c,d*] = b &
Im2 [*a,b,c,d*] = c &
Im3 [*a,b,c,d*] = d )
Lm10:
for a, b, c, d being real number st (((a ^2) + (b ^2)) + (c ^2)) + (d ^2) = 0 holds
( a = 0 & b = 0 & c = 0 & d = 0 )
Lm11:
[*1,0,0,0*] = 1
Lm12:
for m, n, x, y, z being quaternion number st z = ((m + n) + x) + y holds
( Rea z = (((Rea m) + (Rea n)) + (Rea x)) + (Rea y) & Im1 z = (((Im1 m) + (Im1 n)) + (Im1 x)) + (Im1 y) & Im2 z = (((Im2 m) + (Im2 n)) + (Im2 x)) + (Im2 y) & Im3 z = (((Im3 m) + (Im3 n)) + (Im3 x)) + (Im3 y) )
Lm13:
for x, y, z being quaternion number st z = x + y holds
( Rea z = (Rea x) + (Rea y) & Im1 z = (Im1 x) + (Im1 y) & Im2 z = (Im2 x) + (Im2 y) & Im3 z = (Im3 x) + (Im3 y) )
Lm14:
for z1, z2 being quaternion number holds z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*]
Lm15:
for x, y, z being quaternion number st z = x * y holds
( Rea z = ((((Rea x) * (Rea y)) - ((Im1 x) * (Im1 y))) - ((Im2 x) * (Im2 y))) - ((Im3 x) * (Im3 y)) & Im1 z = ((((Rea x) * (Im1 y)) + ((Im1 x) * (Rea y))) + ((Im2 x) * (Im3 y))) - ((Im3 x) * (Im2 y)) & Im2 z = ((((Rea x) * (Im2 y)) + ((Im2 x) * (Rea y))) + ((Im3 x) * (Im1 y))) - ((Im1 x) * (Im3 y)) & Im3 z = ((((Rea x) * (Im3 y)) + ((Im3 x) * (Rea y))) + ((Im1 x) * (Im2 y))) - ((Im2 x) * (Im1 y)) )
Lm16:
for z1, z2, z3, z4 being quaternion number holds ((z1 + z2) + z3) + z4 = [*((((Rea z1) + (Rea z2)) + (Rea z3)) + (Rea z4)),((((Im1 z1) + (Im1 z2)) + (Im1 z3)) + (Im1 z4)),((((Im2 z1) + (Im2 z2)) + (Im2 z3)) + (Im2 z4)),((((Im3 z1) + (Im3 z2)) + (Im3 z3)) + (Im3 z4))*]
Lm17:
for z1, z2 being quaternion number holds z1 * z2 = [*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),(((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))),(((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))),(((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)))*]
Lm18:
for z1, z2 being quaternion number holds
( Rea (z1 * z2) = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) & Im1 (z1 * z2) = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) & Im2 (z1 * z2) = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)) )
Lm19:
for z being quaternion number
for x being Real st z = x holds
( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )
definition
let x be
Real;
let y be
quaternion number ;
consider y1,
y2,
y3,
y4 being
Element of
REAL such that A1:
y = [*y1,y2,y3,y4*]
by Th7;
existence
ex b1 being set ex y1, y2, y3, y4 being Element of REAL st
( y = [*y1,y2,y3,y4*] & b1 = [*(x + y1),y2,y3,y4*] )
uniqueness
for b1, b2 being set st ex y1, y2, y3, y4 being Element of REAL st
( y = [*y1,y2,y3,y4*] & b1 = [*(x + y1),y2,y3,y4*] ) & ex y1, y2, y3, y4 being Element of REAL st
( y = [*y1,y2,y3,y4*] & b2 = [*(x + y1),y2,y3,y4*] ) holds
b1 = b2
end;
definition
let x be
Real;
let y be
quaternion number ;
consider y1,
y2,
y3,
y4 being
Element of
REAL such that A1:
y = [*y1,y2,y3,y4*]
by Th7;
existence
ex b1 being set ex y1, y2, y3, y4 being Element of REAL st
( y = [*y1,y2,y3,y4*] & b1 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] )
uniqueness
for b1, b2 being set st ex y1, y2, y3, y4 being Element of REAL st
( y = [*y1,y2,y3,y4*] & b1 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) & ex y1, y2, y3, y4 being Element of REAL st
( y = [*y1,y2,y3,y4*] & b2 = [*(x * y1),(x * y2),(x * y3),(x * y4)*] ) holds
b1 = b2
end;
Lm20:
for x, y, z, w being Real holds [*x,y,z,w*] = ((x + (y * <i>)) + (z * <j>)) + (w * <k>)
Lm21:
for z1, z2 being quaternion number holds z1 + z2 = ((((Rea z1) + (Rea z2)) + (((Im1 z1) + (Im1 z2)) * <i>)) + (((Im2 z1) + (Im2 z2)) * <j>)) + (((Im3 z1) + (Im3 z2)) * <k>)
Lm22:
for z1, z2 being quaternion number holds z1 * z2 = (((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) * <i>)) + ((((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))) * <j>)) + ((((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))) * <k>)
Lm23:
for c being quaternion number holds c + 0q = c
Lm24:
( 0 * <i> = 0 & 0 * <j> = 0 & 0 * <k> = 0 )
Lm25:
for z being quaternion number holds - z = (((- (Rea z)) + ((- (Im1 z)) * <i>)) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>)
Lm26:
for z1, z2 being quaternion number holds z1 - z2 = ((((Rea z1) - (Rea z2)) + (((Im1 z1) - (Im1 z2)) * <i>)) + (((Im2 z1) - (Im2 z2)) * <j>)) + (((Im3 z1) - (Im3 z2)) * <k>)
Lm27:
for a, b, c, d being Element of REAL holds a ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2)
Lm28:
for a, b, c, d being real number holds c ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2)
Lm29:
for d, a, b, c being Element of REAL holds d ^2 <= (((a ^2) + (b ^2)) + (c ^2)) + (d ^2)
Lm30:
for a, b being Element of REAL st a >= b ^2 holds
sqrt a >= b
Lm31:
for a1, a2, a3, a4, a5, a6, b1, b2, b3, b4, b5, b6 being real number st a1 >= b1 & a2 >= b2 & a3 >= b3 & a4 >= b4 & a5 >= b5 & a6 >= b6 holds
((((a1 + a2) + a3) + a4) + a5) + a6 >= ((((b1 + b2) + b3) + b4) + b5) + b6
Lm32:
for a, b being Element of REAL st a >= 0 & b >= 0 & a ^2 >= b ^2 holds
a >= b
Lm33:
for m1, m2, m4, m3, n1, n2, n3, n4 being real number holds ((sqrt ((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2))) + (sqrt ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)))) ^2 = ((((((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) + (n1 ^2)) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)) + (2 * (sqrt (((((m1 ^2) + (m2 ^2)) + (m3 ^2)) + (m4 ^2)) * ((((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2)))))
Lm34:
for m1, m2, m3, m4, n1, n2, n3, n4 being real number holds (sqrt (((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2))) ^2 = ((((m1 + n1) ^2) + ((m2 + n2) ^2)) + ((m3 + n3) ^2)) + ((m4 + n4) ^2)
Lm35:
for z1, z2 being quaternion number holds z1 = (z1 + z2) - z2
Lm36:
for z1, z2 being quaternion number holds z1 = (z1 - z2) + z2
Lm37:
for z1, z2 being quaternion number holds z1 - z2 = [*((Rea z1) - (Rea z2)),((Im1 z1) - (Im1 z2)),((Im2 z1) - (Im2 z2)),((Im3 z1) - (Im3 z2))*]
Lm38:
for z1, z2 being quaternion number holds z1 - z2 = - (z2 - z1)
Lm39:
for z1, z2 being quaternion number st z1 - z2 = 0 holds
z1 = z2
Lm40:
for z, z1, z2 being quaternion number holds z1 - z2 = (z1 - z) + (z - z2)