set M = { a where a is Element of R : ex n being Element of NAT st a |^ n in I } ;
{ a where a is Element of R : ex n being Element of NAT st a |^ n in I } = sqrt I
;
then reconsider M = { a where a is Element of R : ex n being Element of NAT st a |^ n in I } as non empty Subset of R ;
for x, y being Element of R st x in M & y in M holds
x + y in M
proof
let x,
y be
Element of
R;
( x in M & y in M implies x + y in M )
assume that A1:
x in M
and A2:
y in M
;
x + y in M
consider a being
Element of
R such that A3:
x = a
and A4:
ex
n being
Element of
NAT st
a |^ n in I
by A1;
consider n being
Element of
NAT such that A5:
a |^ n in I
by A4;
consider b being
Element of
R such that A6:
y = b
and A7:
ex
m being
Element of
NAT st
b |^ m in I
by A2;
consider m being
Element of
NAT such that A8:
b |^ m in I
by A7;
set p = (
a,
b)
In_Power (n + m);
consider f being
sequence of the
carrier of
R such that A9:
Sum ((a,b) In_Power (n + m)) = f . (len ((a,b) In_Power (n + m)))
and A10:
f . 0 = 0. R
and A11:
for
j being
Nat for
v being
Element of
R st
j < len ((a,b) In_Power (n + m)) &
v = ((a,b) In_Power (n + m)) . (j + 1) holds
f . (j + 1) = (f . j) + v
by RLVECT_1:def 12;
defpred S1[
Element of
NAT ]
means f . R in I;
A12:
for
i being
Element of
NAT st 1
<= i &
i <= len ((a,b) In_Power (n + m)) holds
((a,b) In_Power (n + m)) . i in I
proof
let i be
Element of
NAT ;
( 1 <= i & i <= len ((a,b) In_Power (n + m)) implies ((a,b) In_Power (n + m)) . i in I )
assume that A13:
1
<= i
and A14:
i <= len ((a,b) In_Power (n + m))
;
((a,b) In_Power (n + m)) . i in I
set r =
i - 1;
set l =
(n + m) - (i - 1);
1
- 1
<= i - 1
by A13, XREAL_1:9;
then reconsider r =
i - 1 as
Element of
NAT by INT_1:3;
i <= (n + m) + 1
by A14, BINOM:def 7;
then
r <= ((n + m) + 1) - 1
by XREAL_1:9;
then
r - r <= (n + m) - r
by XREAL_1:9;
then reconsider l =
(n + m) - (i - 1) as
Element of
NAT by INT_1:3;
i in Seg (len ((a,b) In_Power (n + m)))
by A13, A14, FINSEQ_1:1;
then A15:
i in dom ((a,b) In_Power (n + m))
by FINSEQ_1:def 3;
then A16:
((a,b) In_Power (n + m)) . i =
((a,b) In_Power (n + m)) /. i
by PARTFUN1:def 6
.=
(((n + m) choose r) * (a |^ l)) * (b |^ r)
by A15, BINOM:def 7
;
end;
A19:
now for j being Element of NAT st 0 <= j & j < len ((a,b) In_Power (n + m)) & S1[j] holds
S1[j + 1]let j be
Element of
NAT ;
( 0 <= j & j < len ((a,b) In_Power (n + m)) & S1[j] implies S1[j + 1] )assume that
0 <= j
and A20:
j < len ((a,b) In_Power (n + m))
;
( S1[j] implies S1[j + 1] )thus
(
S1[
j] implies
S1[
j + 1] )
verumproof
assume A21:
f . j in I
;
S1[j + 1]
A22:
j + 1
<= len ((a,b) In_Power (n + m))
by A20, NAT_1:13;
1
<= j + 1
by NAT_1:11;
then
j + 1
in Seg (len ((a,b) In_Power (n + m)))
by A22, FINSEQ_1:1;
then
j + 1
in dom ((a,b) In_Power (n + m))
by FINSEQ_1:def 3;
then A23:
((a,b) In_Power (n + m)) /. (j + 1) = ((a,b) In_Power (n + m)) . (j + 1)
by PARTFUN1:def 6;
then A24:
((a,b) In_Power (n + m)) /. (j + 1) in I
by A12, A22, NAT_1:11;
f . (j + 1) = (f . j) + (((a,b) In_Power (n + m)) /. (j + 1))
by A11, A20, A23;
hence
S1[
j + 1]
by A21, A24, Def1;
verum
end; end;
A25:
(a + b) |^ (n + m) = Sum ((a,b) In_Power (n + m))
by BINOM:25;
A26:
S1[
0 ]
by A10, Th2;
for
i being
Element of
NAT st
0 <= i &
i <= len ((a,b) In_Power (n + m)) holds
S1[
i]
from INT_1:sch 7(A26, A19);
then
(a + b) |^ (n + m) in I
by A25, A9;
hence
x + y in M
by A3, A6;
verum
end;
hence
sqrt I is add-closed
; verum