let n be Nat; :: thesis: ( 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; :: thesis: ( 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)) ; :: thesis: (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 ; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: (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 ; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: (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 ; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: (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 ; :: thesis: 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; :: thesis: ( 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))) ; :: thesis: ex x being Element of INT st S1[k,x]
take ((SubXFinS (p,EvenNAT)) . k) - ((SubXFinS ((digits (n,10)),EvenNAT)) . k) ; :: thesis: ( ((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; :: thesis: 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 :: thesis: for i being Nat st i in dom pede holds
11 divides pede . i
let i be Nat; :: thesis: ( 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 ; :: thesis: 11 divides pede . i
then 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; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: (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 ; :: thesis: 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 :: thesis: for i being Nat st i in dom podo holds
11 divides podo . i
let i be Nat; :: thesis: ( 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 ; :: thesis: 11 divides podo . i
then 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; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: (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 ; :: thesis: 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))) ) :: thesis: ( 11 divides (Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT))) implies 11 divides n )
proof
assume 11 divides n ; :: thesis: 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; :: thesis: verum
end;
thus ( 11 divides (Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT))) implies 11 divides n ) :: thesis: verum
proof
assume 11 divides (Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT))) ; :: thesis: 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; :: thesis: verum
end;