let n be Element of NAT ; for q being Element of REAL n
for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n & q = p holds
( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
let q be Element of REAL n; for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n & q = p holds
( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
let p be Point of (TOP-REAL n); for i being Element of NAT st i in Seg n & q = p holds
( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
let i be Element of NAT ; ( i in Seg n & q = p implies ( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 ) )
assume that
A1:
i in Seg n
and
A2:
q = p
; ( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
reconsider pd = (p /. i) ^2 as Element of REAL by XREAL_0:def 1;
A3:
Sum ((0* n) +* (i,pd)) = pd
by A1, Th10;
len (0* n) = n
by CARD_1:def 7;
then
len ((0* n) +* (i,pd)) = n
by FUNCT_7:97;
then reconsider w1 = (0* n) +* (i,pd) as Element of n -tuples_on REAL by FINSEQ_2:92;
A4:
len w1 = n
by CARD_1:def 7;
reconsider w2 = sqr q as Element of n -tuples_on REAL ;
A5:
Sum (sqr q) >= 0
by RVSUM_1:86;
A6:
len q = n
by CARD_1:def 7;
A7:
for j being Nat st j in Seg n holds
w1 . j <= w2 . j
proof
let j be
Nat;
( j in Seg n implies w1 . j <= w2 . j )
assume A8:
j in Seg n
;
w1 . j <= w2 . j
set r1 =
w1 . j;
set r2 =
w2 . j;
per cases
( j = i or j <> i )
;
suppose A9:
j = i
;
w1 . j <= w2 . jthen
j in dom q
by A1, A6, FINSEQ_1:def 3;
then A10:
q /. j = q . j
by PARTFUN1:def 6;
A11:
dom (0* n) =
Seg (len (0* n))
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
i in dom w1
by A1, A4, FINSEQ_1:def 3;
then w1 . j =
w1 /. i
by A9, PARTFUN1:def 6
.=
(q /. i) ^2
by A2, A1, A11, FUNCT_7:36
;
hence
w1 . j <= w2 . j
by A9, A10, VALUED_1:11;
verum end; suppose A12:
j <> i
;
w1 . j <= w2 . jA13:
dom (0* n) =
Seg (len (0* n))
by FINSEQ_1:def 3
.=
Seg n
by CARD_1:def 7
;
dom q = Seg n
by A6, FINSEQ_1:def 3;
then
q /. j = q . j
by A8, PARTFUN1:def 6;
then A14:
w2 . j = (q /. j) ^2
by VALUED_1:11;
j in dom w1
by A4, A8, FINSEQ_1:def 3;
then w1 . j =
w1 /. j
by PARTFUN1:def 6
.=
(0* n) /. j
by A8, A12, A13, FUNCT_7:37
.=
(n |-> 0) . j
by A8, A13, PARTFUN1:def 6
.=
0
by A8, FUNCOP_1:7
;
hence
w1 . j <= w2 . j
by A14, XREAL_1:63;
verum end;
end;
then
Sum w1 <= Sum w2
by RVSUM_1:82;
then
( 0 <= (p /. i) ^2 & (p /. i) ^2 <= (sqrt (Sum (sqr q))) ^2 )
by A5, A3, SQUARE_1:def 2, XREAL_1:63;
then
sqrt ((p /. i) ^2) <= sqrt ((sqrt (Sum (sqr q))) ^2)
by SQUARE_1:26;
then
|.|.(p /. i).|.| <= sqrt ((sqrt (Sum (sqr q))) ^2)
by COMPLEX1:72;
then
( 0 <= |.q.| & |.(p /. i).| <= |.(sqrt (Sum (sqr q))).| )
by COMPLEX1:72;
then A15:
|.(p /. i).| <= sqrt (Sum (sqr q))
by ABSVALUE:def 1;
A16:
p /. i <= |.(p /. i).|
by ABSVALUE:4;
|.q.| ^2 = Sum (sqr q)
by A5, SQUARE_1:def 2;
hence
( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
by A7, A3, A15, A16, RVSUM_1:82, XXREAL_0:2; verum