defpred S1[ Nat] means for k being Nat st k >= 2 holds
SDDec (Fmin ($1,$1,k)) > 0 ;
A1:
for m being Nat st m >= 1 & S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( m >= 1 & S1[m] implies S1[m + 1] )
assume that A2:
m >= 1
and
S1[
m]
;
S1[m + 1]
let k be
Nat;
( k >= 2 implies SDDec (Fmin ((m + 1),(m + 1),k)) > 0 )
assume A3:
k >= 2
;
SDDec (Fmin ((m + 1),(m + 1),k)) > 0
then
Radix k > 2
by RADIX_4:1;
then A4:
Radix k > 1
by XXREAL_0:2;
m + 1
in Seg (m + 1)
by FINSEQ_1:4;
then A5:
DigA (
(Fmin ((m + 1),(m + 1),k)),
(m + 1)) =
FminDigit (
(m + 1),
k,
(m + 1))
by RADIX_5:def 6
.=
1
by A3, RADIX_5:def 5
;
for
i being
Nat st
i in Seg m holds
(Fmin ((m + 1),(m + 1),k)) . i = (DecSD (0,m,k)) . i
proof
let i be
Nat;
( i in Seg m implies (Fmin ((m + 1),(m + 1),k)) . i = (DecSD (0,m,k)) . i )
assume A6:
i in Seg m
;
(Fmin ((m + 1),(m + 1),k)) . i = (DecSD (0,m,k)) . i
then
i <= m
by FINSEQ_1:1;
then A7:
i < m + 1
by NAT_1:13;
A8:
i in Seg (m + 1)
by A6, FINSEQ_2:8;
then (Fmin ((m + 1),(m + 1),k)) . i =
DigA (
(Fmin ((m + 1),(m + 1),k)),
i)
by RADIX_1:def 3
.=
FminDigit (
(m + 1),
k,
i)
by A8, RADIX_5:def 6
.=
0
by A3, A7, RADIX_5:def 5
.=
DigA (
(DecSD (0,m,k)),
i)
by A6, RADIX_5:5
;
hence
(Fmin ((m + 1),(m + 1),k)) . i = (DecSD (0,m,k)) . i
by A6, RADIX_1:def 3;
verum
end;
then SDDec (Fmin ((m + 1),(m + 1),k)) =
(SDDec (DecSD (0,m,k))) + (((Radix k) |^ m) * (DigA ((Fmin ((m + 1),(m + 1),k)),(m + 1))))
by RADIX_2:10
.=
0 + ((Radix k) |^ m)
by A2, A5, RADIX_5:6
;
hence
SDDec (Fmin ((m + 1),(m + 1),k)) > 0
by A4, PREPOWER:11;
verum
end;
A9:
S1[1]
proof
let k be
Nat;
( k >= 2 implies SDDec (Fmin (1,1,k)) > 0 )
assume A10:
k >= 2
;
SDDec (Fmin (1,1,k)) > 0
A11:
1
in Seg 1
by FINSEQ_1:1;
then (DigitSD (Fmin (1,1,k))) /. 1 =
SubDigit (
(Fmin (1,1,k)),1,
k)
by RADIX_1:def 6
.=
((Radix k) |^ (1 -' 1)) * (DigB ((Fmin (1,1,k)),1))
by RADIX_1:def 5
.=
((Radix k) |^ (1 -' 1)) * (DigA ((Fmin (1,1,k)),1))
by RADIX_1:def 4
.=
((Radix k) |^ 0) * (DigA ((Fmin (1,1,k)),1))
by XREAL_1:232
.=
1
* (DigA ((Fmin (1,1,k)),1))
by NEWTON:4
.=
FminDigit (1,
k,1)
by A11, RADIX_5:def 6
.=
1
by A10, RADIX_5:def 5
;
then A12:
DigitSD (Fmin (1,1,k)) = <*1*>
by RADIX_1:17;
SDDec (Fmin (1,1,k)) =
Sum (DigitSD (Fmin (1,1,k)))
by RADIX_1:def 7
.=
1
by A12, RVSUM_1:73
;
hence
SDDec (Fmin (1,1,k)) > 0
;
verum
end;
for m being Nat st m >= 1 holds
S1[m]
from NAT_1:sch 8(A9, A1);
hence
for m, k being Nat st m >= 1 & k >= 2 holds
SDDec (Fmin (m,m,k)) > 0
; verum