let n be Nat; ( 11 divides n iff 11 divides (Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT))) )
set d = digits (n,10);
consider p being XFinSequence of NAT such that
A1:
dom p = dom (digits (n,10))
and
A2:
for i being Nat st i in dom p holds
p . i = ((digits (n,10)) . i) * (10 |^ i)
and
A3:
value ((digits (n,10)),10) = Sum p
by NUMERAL1:def 1;
set pe = SubXFinS (p,EvenNAT);
set po = SubXFinS (p,OddNAT);
A4: (Sum (SubXFinS (p,EvenNAT))) + (Sum (SubXFinS (p,OddNAT))) =
Sum (SubXFinS (p,NAT))
by Th10, Th7, Th8
.=
Sum p
by Th11
;
set de = SubXFinS ((digits (n,10)),EvenNAT);
set dod = SubXFinS ((digits (n,10)),OddNAT);
A5: dom (SubXFinS (p,EvenNAT)) =
dom (Sgm0 (EvenNAT /\ (len (digits (n,10)))))
by Th6, A1
.=
dom (SubXFinS ((digits (n,10)),EvenNAT))
by Th6
;
A6: dom (SubXFinS (p,OddNAT)) =
dom (Sgm0 (OddNAT /\ (len (digits (n,10)))))
by Th6, A1
.=
dom (SubXFinS ((digits (n,10)),OddNAT))
by Th6
;
A7:
for i being Nat st i in dom (SubXFinS ((digits (n,10)),EvenNAT)) holds
(SubXFinS ((digits (n,10)),EvenNAT)) . i = (digits (n,10)) . (2 * i)
proof
set se =
Sgm0 (EvenNAT /\ (len (digits (n,10))));
let i be
Nat;
( i in dom (SubXFinS ((digits (n,10)),EvenNAT)) implies (SubXFinS ((digits (n,10)),EvenNAT)) . i = (digits (n,10)) . (2 * i) )
assume A8:
i in dom (SubXFinS ((digits (n,10)),EvenNAT))
;
(SubXFinS ((digits (n,10)),EvenNAT)) . i = (digits (n,10)) . (2 * i)
then A9:
(
i in dom (Sgm0 (EvenNAT /\ (len (digits (n,10))))) &
(Sgm0 (EvenNAT /\ (len (digits (n,10))))) . i in dom (digits (n,10)) )
by FUNCT_1:11;
thus (SubXFinS ((digits (n,10)),EvenNAT)) . i =
(digits (n,10)) . ((Sgm0 (EvenNAT /\ (len (digits (n,10))))) . i)
by A8, FUNCT_1:12
.=
(digits (n,10)) . (2 * i)
by A9, Th12
;
verum
end;
A10:
for i being Nat st i in dom (SubXFinS (p,EvenNAT)) holds
(SubXFinS (p,EvenNAT)) . i = ((SubXFinS ((digits (n,10)),EvenNAT)) . i) * (10 |^ (2 * i))
proof
set se =
Sgm0 (EvenNAT /\ (len p));
let i be
Nat;
( i in dom (SubXFinS (p,EvenNAT)) implies (SubXFinS (p,EvenNAT)) . i = ((SubXFinS ((digits (n,10)),EvenNAT)) . i) * (10 |^ (2 * i)) )
assume A11:
i in dom (SubXFinS (p,EvenNAT))
;
(SubXFinS (p,EvenNAT)) . i = ((SubXFinS ((digits (n,10)),EvenNAT)) . i) * (10 |^ (2 * i))
then A12:
(
i in dom (Sgm0 (EvenNAT /\ (len p))) &
(Sgm0 (EvenNAT /\ (len p))) . i in dom p )
by FUNCT_1:11;
then A13:
(Sgm0 (EvenNAT /\ (len p))) . i = 2
* i
by Th12;
thus (SubXFinS (p,EvenNAT)) . i =
p . ((Sgm0 (EvenNAT /\ (len p))) . i)
by A11, FUNCT_1:12
.=
((digits (n,10)) . (2 * i)) * (10 |^ (2 * i))
by A12, A13, A2
.=
((SubXFinS ((digits (n,10)),EvenNAT)) . i) * (10 |^ (2 * i))
by A12, A1, FUNCT_1:11, A7
;
verum
end;
A14:
for i being Nat st i in dom (SubXFinS ((digits (n,10)),OddNAT)) holds
(SubXFinS ((digits (n,10)),OddNAT)) . i = (digits (n,10)) . ((2 * i) + 1)
proof
set so =
Sgm0 (OddNAT /\ (len (digits (n,10))));
let i be
Nat;
( i in dom (SubXFinS ((digits (n,10)),OddNAT)) implies (SubXFinS ((digits (n,10)),OddNAT)) . i = (digits (n,10)) . ((2 * i) + 1) )
assume A15:
i in dom (SubXFinS ((digits (n,10)),OddNAT))
;
(SubXFinS ((digits (n,10)),OddNAT)) . i = (digits (n,10)) . ((2 * i) + 1)
then A16:
(
i in dom (Sgm0 (OddNAT /\ (len (digits (n,10))))) &
(Sgm0 (OddNAT /\ (len (digits (n,10))))) . i in dom (digits (n,10)) )
by FUNCT_1:11;
thus (SubXFinS ((digits (n,10)),OddNAT)) . i =
(digits (n,10)) . ((Sgm0 (OddNAT /\ (len (digits (n,10))))) . i)
by A15, FUNCT_1:12
.=
(digits (n,10)) . ((2 * i) + 1)
by A16, Th13
;
verum
end;
A17:
for i being Nat st i in dom (SubXFinS (p,OddNAT)) holds
(SubXFinS (p,OddNAT)) . i = ((SubXFinS ((digits (n,10)),OddNAT)) . i) * (10 |^ ((2 * i) + 1))
proof
set so =
Sgm0 (OddNAT /\ (len p));
let i be
Nat;
( i in dom (SubXFinS (p,OddNAT)) implies (SubXFinS (p,OddNAT)) . i = ((SubXFinS ((digits (n,10)),OddNAT)) . i) * (10 |^ ((2 * i) + 1)) )
assume A18:
i in dom (SubXFinS (p,OddNAT))
;
(SubXFinS (p,OddNAT)) . i = ((SubXFinS ((digits (n,10)),OddNAT)) . i) * (10 |^ ((2 * i) + 1))
then A19:
(
i in dom (Sgm0 (OddNAT /\ (len p))) &
(Sgm0 (OddNAT /\ (len p))) . i in dom p )
by FUNCT_1:11;
then A20:
(Sgm0 (OddNAT /\ (len p))) . i = (2 * i) + 1
by Th13;
thus (SubXFinS (p,OddNAT)) . i =
p . ((Sgm0 (OddNAT /\ (len p))) . i)
by A18, FUNCT_1:12
.=
((digits (n,10)) . ((2 * i) + 1)) * (10 |^ ((2 * i) + 1))
by A19, A20, A2
.=
((SubXFinS ((digits (n,10)),OddNAT)) . i) * (10 |^ ((2 * i) + 1))
by A19, A1, FUNCT_1:11, A14
;
verum
end;
defpred S1[ set , set ] means $2 = ((SubXFinS (p,EvenNAT)) . $1) - ((SubXFinS ((digits (n,10)),EvenNAT)) . $1);
A21:
for k being Nat st k in Segm (dom (SubXFinS (p,EvenNAT))) holds
ex x being Element of INT st S1[k,x]
proof
let k be
Nat;
( k in Segm (dom (SubXFinS (p,EvenNAT))) implies ex x being Element of INT st S1[k,x] )
assume
k in Segm (dom (SubXFinS (p,EvenNAT)))
;
ex x being Element of INT st S1[k,x]
take
((SubXFinS (p,EvenNAT)) . k) - ((SubXFinS ((digits (n,10)),EvenNAT)) . k)
;
( ((SubXFinS (p,EvenNAT)) . k) - ((SubXFinS ((digits (n,10)),EvenNAT)) . k) is Element of INT & S1[k,((SubXFinS (p,EvenNAT)) . k) - ((SubXFinS ((digits (n,10)),EvenNAT)) . k)] )
thus
(
((SubXFinS (p,EvenNAT)) . k) - ((SubXFinS ((digits (n,10)),EvenNAT)) . k) is
Element of
INT &
S1[
k,
((SubXFinS (p,EvenNAT)) . k) - ((SubXFinS ((digits (n,10)),EvenNAT)) . k)] )
by INT_1:def 2;
verum
end;
consider pede being XFinSequence of INT such that
A22:
( dom pede = Segm (dom (SubXFinS (p,EvenNAT))) & ( for k being Nat st k in Segm (dom (SubXFinS (p,EvenNAT))) holds
S1[k,pede . k] ) )
from STIRL2_1:sch 5(A21);
now for i being Nat st i in dom pede holds
11 divides pede . ilet i be
Nat;
( i in dom pede implies 11 divides pede . i )reconsider dz =
(10 |^ (2 * i)) - 1 as
Nat by NAT_1:20, NEWTON:83;
assume A23:
i in dom pede
;
11 divides pede . ithen pede . i =
((SubXFinS (p,EvenNAT)) . i) - ((SubXFinS ((digits (n,10)),EvenNAT)) . i)
by A22
.=
(((SubXFinS ((digits (n,10)),EvenNAT)) . i) * (10 |^ (2 * i))) - ((SubXFinS ((digits (n,10)),EvenNAT)) . i)
by A10, A23, A22
.=
((SubXFinS ((digits (n,10)),EvenNAT)) . i) * dz
;
hence
11
divides pede . i
by Th20, NAT_D:9;
verum end;
then
11 divides Sum pede
by Th16;
then A24:
(Sum pede) mod 11 = 0
by INT_1:62;
A25:
len pede = len (SubXFinS ((digits (n,10)),EvenNAT))
by A22, A5;
A26:
len pede = len (SubXFinS (p,EvenNAT))
by A22;
A27:
for i being Nat st i in dom (SubXFinS (p,EvenNAT)) holds
(SubXFinS (p,EvenNAT)) . i = addint . ((pede . i),((SubXFinS ((digits (n,10)),EvenNAT)) . i))
proof
let i be
Nat;
( i in dom (SubXFinS (p,EvenNAT)) implies (SubXFinS (p,EvenNAT)) . i = addint . ((pede . i),((SubXFinS ((digits (n,10)),EvenNAT)) . i)) )
assume A28:
i in dom (SubXFinS (p,EvenNAT))
;
(SubXFinS (p,EvenNAT)) . i = addint . ((pede . i),((SubXFinS ((digits (n,10)),EvenNAT)) . i))
thus addint . (
(pede . i),
((SubXFinS ((digits (n,10)),EvenNAT)) . i)) =
(pede . i) + ((SubXFinS ((digits (n,10)),EvenNAT)) . i)
by BINOP_2:def 20
.=
(((SubXFinS (p,EvenNAT)) . i) - ((SubXFinS ((digits (n,10)),EvenNAT)) . i)) + ((SubXFinS ((digits (n,10)),EvenNAT)) . i)
by A28, A22
.=
(SubXFinS (p,EvenNAT)) . i
;
verum
end;
A29: Sum (SubXFinS (p,EvenNAT)) =
addint "**" (SubXFinS (p,EvenNAT))
by AFINSQ_2:50
.=
addint "**" (pede ^ (SubXFinS ((digits (n,10)),EvenNAT)))
by A25, A26, A27, AFINSQ_2:46
.=
Sum (pede ^ (SubXFinS ((digits (n,10)),EvenNAT)))
by AFINSQ_2:50
.=
(Sum pede) + (Sum (SubXFinS ((digits (n,10)),EvenNAT)))
by AFINSQ_2:55
;
defpred S2[ set , set ] means $2 = ((SubXFinS (p,OddNAT)) . $1) + ((SubXFinS ((digits (n,10)),OddNAT)) . $1);
A30:
for k being Nat st k in Segm (dom (SubXFinS (p,OddNAT))) holds
ex x being Element of NAT st S2[k,x]
;
consider podo being XFinSequence of NAT such that
A31:
( dom podo = Segm (dom (SubXFinS (p,OddNAT))) & ( for k being Nat st k in Segm (dom (SubXFinS (p,OddNAT))) holds
S2[k,podo . k] ) )
from STIRL2_1:sch 5(A30);
now for i being Nat st i in dom podo holds
11 divides podo . ilet i be
Nat;
( i in dom podo implies 11 divides podo . i )reconsider dz =
(10 |^ (2 * i)) - 1 as
Nat by NAT_1:20, NEWTON:83;
assume A32:
i in dom podo
;
11 divides podo . ithen podo . i =
((SubXFinS (p,OddNAT)) . i) + ((SubXFinS ((digits (n,10)),OddNAT)) . i)
by A31
.=
(((SubXFinS ((digits (n,10)),OddNAT)) . i) * (10 |^ ((2 * i) + 1))) + ((SubXFinS ((digits (n,10)),OddNAT)) . i)
by A17, A32, A31
.=
((SubXFinS ((digits (n,10)),OddNAT)) . i) * ((10 |^ ((2 * i) + 1)) + 1)
;
hence
11
divides podo . i
by Th21, NAT_D:9;
verum end;
then
11 divides Sum podo
by Th16;
then A33:
(Sum podo) mod 11 = 0
by INT_1:62;
set mdo = (- 1) (#) (SubXFinS ((digits (n,10)),OddNAT));
A34:
len podo = len ((- 1) (#) (SubXFinS ((digits (n,10)),OddNAT)))
by A31, A6, VALUED_1:def 5;
A35:
len podo = len (SubXFinS (p,OddNAT))
by A31;
A36:
for i being Nat st i in dom (SubXFinS (p,OddNAT)) holds
(SubXFinS (p,OddNAT)) . i = addint . ((podo . i),(((- 1) (#) (SubXFinS ((digits (n,10)),OddNAT))) . i))
proof
let i be
Nat;
( i in dom (SubXFinS (p,OddNAT)) implies (SubXFinS (p,OddNAT)) . i = addint . ((podo . i),(((- 1) (#) (SubXFinS ((digits (n,10)),OddNAT))) . i)) )
assume A37:
i in dom (SubXFinS (p,OddNAT))
;
(SubXFinS (p,OddNAT)) . i = addint . ((podo . i),(((- 1) (#) (SubXFinS ((digits (n,10)),OddNAT))) . i))
then A38:
i in dom ((- 1) (#) (SubXFinS ((digits (n,10)),OddNAT)))
by A6, VALUED_1:def 5;
thus addint . (
(podo . i),
(((- 1) (#) (SubXFinS ((digits (n,10)),OddNAT))) . i)) =
(podo . i) + (((- 1) (#) (SubXFinS ((digits (n,10)),OddNAT))) . i)
by BINOP_2:def 20
.=
(podo . i) + ((- 1) * ((SubXFinS ((digits (n,10)),OddNAT)) . i))
by A38, VALUED_1:def 5
.=
(((SubXFinS (p,OddNAT)) . i) + ((SubXFinS ((digits (n,10)),OddNAT)) . i)) - ((SubXFinS ((digits (n,10)),OddNAT)) . i)
by A37, A31
.=
(SubXFinS (p,OddNAT)) . i
;
verum
end;
A39: Sum (SubXFinS (p,OddNAT)) =
addint "**" (SubXFinS (p,OddNAT))
by AFINSQ_2:50
.=
addint "**" (podo ^ ((- 1) (#) (SubXFinS ((digits (n,10)),OddNAT))))
by A34, A35, A36, AFINSQ_2:46
.=
Sum (podo ^ ((- 1) (#) (SubXFinS ((digits (n,10)),OddNAT))))
by AFINSQ_2:50
.=
(Sum podo) + (Sum ((- 1) (#) (SubXFinS ((digits (n,10)),OddNAT))))
by AFINSQ_2:55
.=
(Sum podo) + ((- 1) * (Sum (SubXFinS ((digits (n,10)),OddNAT))))
by AFINSQ_2:64
.=
(Sum podo) - (Sum (SubXFinS ((digits (n,10)),OddNAT)))
;
thus
( 11 divides n implies 11 divides (Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT))) )
( 11 divides (Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT))) implies 11 divides n )proof
assume
11
divides n
;
11 divides (Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT)))
then
11
divides Sum p
by A3, NUMERAL1:5;
then 0 =
(((Sum pede) + (Sum podo)) + ((Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT))))) mod 11
by INT_1:62, A4, A29, A39
.=
((((Sum pede) + (Sum podo)) mod 11) + (((Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT)))) mod 11)) mod 11
by NAT_D:66
.=
(((((Sum pede) mod 11) + ((Sum podo) mod 11)) mod 11) + (((Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT)))) mod 11)) mod 11
by NAT_D:66
.=
(0 + (((Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT)))) mod 11)) mod 11
by A24, A33, NAT_D:26
.=
((Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT)))) mod 11
by Th14
;
hence
11
divides (Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT)))
by INT_1:62;
verum
end;
thus
( 11 divides (Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT))) implies 11 divides n )
verumproof
assume
11
divides (Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT)))
;
11 divides n
then 0 =
((Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT)))) mod 11
by INT_1:62
.=
(0 + (((Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT)))) mod 11)) mod 11
by Th14
.=
(((((Sum pede) mod 11) + ((Sum podo) mod 11)) mod 11) + (((Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT)))) mod 11)) mod 11
by A24, A33, NAT_D:26
.=
((((Sum pede) + (Sum podo)) mod 11) + (((Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT)))) mod 11)) mod 11
by NAT_D:66
.=
(((Sum pede) + (Sum podo)) + ((Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT))))) mod 11
by NAT_D:66
.=
n mod 11
by A4, A29, A39, A3, NUMERAL1:5
;
hence
11
divides n
by INT_1:62;
verum
end;