:: NUMERAL1 semantic presentation begin theorem Th1: :: NUMERAL1:1 for k, l, m being Nat holds (k (#) (l GeoSeq)) | m is XFinSequence of NAT proof let k, l, m be Nat; ::_thesis: (k (#) (l GeoSeq)) | m is XFinSequence of NAT set g = (k (#) (l GeoSeq)) | m; A1: dom (k (#) (l GeoSeq)) = NAT by FUNCT_2:def_1; then m in dom (k (#) (l GeoSeq)) by ORDINAL1:def_12; then m c= dom (k (#) (l GeoSeq)) by A1, ORDINAL1:def_2; then dom ((k (#) (l GeoSeq)) | m) = m by RELAT_1:62; then reconsider g9 = (k (#) (l GeoSeq)) | m as XFinSequence by ORDINAL1:def_7; rng g9 c= NAT proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng g9 or a in NAT ) assume a in rng g9 ; ::_thesis: a in NAT then consider o being set such that A2: o in dom ((k (#) (l GeoSeq)) | m) and A3: a = ((k (#) (l GeoSeq)) | m) . o by FUNCT_1:def_3; o in dom (k (#) (l GeoSeq)) by A2, RELAT_1:57; then reconsider o = o as Element of NAT ; ((k (#) (l GeoSeq)) | m) . o = (k (#) (l GeoSeq)) . o by A2, FUNCT_1:47 .= k * ((l GeoSeq) . o) by SEQ_1:9 .= k * (l |^ o) by PREPOWER:def_1 ; hence a in NAT by A3; ::_thesis: verum end; hence (k (#) (l GeoSeq)) | m is XFinSequence of NAT by RELAT_1:def_19; ::_thesis: verum end; theorem Th2: :: NUMERAL1:2 for d being XFinSequence of NAT for n being Nat st ( for i being Nat st i in dom d holds n divides d . i ) holds n divides Sum d proof let d be XFinSequence of NAT ; ::_thesis: for n being Nat st ( for i being Nat st i in dom d holds n divides d . i ) holds n divides Sum d let n be Nat; ::_thesis: ( ( for i being Nat st i in dom d holds n divides d . i ) implies n divides Sum d ) assume A1: for i being Nat st i in dom d holds n divides d . i ; ::_thesis: n divides Sum d percases ( len d = 0 or len d > 0 ) ; suppose len d = 0 ; ::_thesis: n divides Sum d then d = {} ; then Sum d = 0 ; hence n divides Sum d by NAT_D:6; ::_thesis: verum end; supposeA2: len d > 0 ; ::_thesis: n divides Sum d then consider f being Function of NAT,NAT such that A3: f . 0 = d . 0 and A4: for n being Nat st n + 1 < len d holds f . (n + 1) = addnat . ((f . n),(d . (n + 1))) and A5: addnat "**" d = f . ((len d) - 1) by AFINSQ_2:def_8; defpred S1[ Element of NAT ] means ( $1 < len d implies n divides f . $1 ); A6: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A7: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof assume A8: k + 1 < len d ; ::_thesis: n divides f . (k + 1) then k + 1 in len d by NAT_1:44; then A9: n divides d . (k + 1) by A1; f . (k + 1) = addnat . ((f . k),(d . (k + 1))) by A4, A8 .= (f . k) + (d . (k + 1)) by BINOP_2:def_23 ; hence n divides f . (k + 1) by A7, A8, A9, NAT_1:13, NAT_D:8; ::_thesis: verum end; end; reconsider ld = (len d) - 1 as Element of NAT by A2, NAT_1:20; A10: ld < len d by XREAL_1:147; 0 in len d by A2, NAT_1:44; then A11: S1[ 0 ] by A1, A3; A12: addnat "**" d = Sum d by AFINSQ_2:51; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A11, A6); hence n divides Sum d by A5, A10, A12; ::_thesis: verum end; end; end; theorem Th3: :: NUMERAL1:3 for d, e being XFinSequence of NAT for n being Nat st dom d = dom e & ( for i being Nat st i in dom d holds e . i = (d . i) mod n ) holds (Sum d) mod n = (Sum e) mod n proof let d, e be XFinSequence of NAT ; ::_thesis: for n being Nat st dom d = dom e & ( for i being Nat st i in dom d holds e . i = (d . i) mod n ) holds (Sum d) mod n = (Sum e) mod n let n be Nat; ::_thesis: ( dom d = dom e & ( for i being Nat st i in dom d holds e . i = (d . i) mod n ) implies (Sum d) mod n = (Sum e) mod n ) assume A1: ( dom d = dom e & ( for i being Nat st i in dom d holds e . i = (d . i) mod n ) ) ; ::_thesis: (Sum d) mod n = (Sum e) mod n defpred S1[ XFinSequence of NAT ] means for e being XFinSequence of NAT st dom $1 = dom e & ( for i being Nat st i in dom $1 holds e . i = ($1 . i) mod n ) holds (Sum $1) mod n = (Sum e) mod n; A2: for p being XFinSequence of NAT for l being Element of NAT st S1[p] holds S1[p ^ <%l%>] proof let p be XFinSequence of NAT ; ::_thesis: for l being Element of NAT st S1[p] holds S1[p ^ <%l%>] let l be Element of NAT ; ::_thesis: ( S1[p] implies S1[p ^ <%l%>] ) assume A3: S1[p] ; ::_thesis: S1[p ^ <%l%>] thus S1[p ^ <%l%>] ::_thesis: verum proof reconsider dop = dom p as Element of NAT by ORDINAL1:def_12; defpred S2[ set , set ] means $2 = (p . $1) mod n; let e be XFinSequence of NAT ; ::_thesis: ( dom (p ^ <%l%>) = dom e & ( for i being Nat st i in dom (p ^ <%l%>) holds e . i = ((p ^ <%l%>) . i) mod n ) implies (Sum (p ^ <%l%>)) mod n = (Sum e) mod n ) assume that A4: dom (p ^ <%l%>) = dom e and A5: for i being Nat st i in dom (p ^ <%l%>) holds e . i = ((p ^ <%l%>) . i) mod n ; ::_thesis: (Sum (p ^ <%l%>)) mod n = (Sum e) mod n A6: for k being Nat st k in dop holds ex x being Element of NAT st S2[k,x] ; consider p9 being XFinSequence of NAT such that A7: ( dom p9 = dop & ( for k being Nat st k in dop holds S2[k,p9 . k] ) ) from STIRL2_1:sch_5(A6); A8: now__::_thesis:_for_k_being_Nat_st_k_in_dom_p9_holds_ e_._k_=_p9_._k let k be Nat; ::_thesis: ( k in dom p9 implies e . k = p9 . k ) assume A9: k in dom p9 ; ::_thesis: e . k = p9 . k then k < dom p9 by NAT_1:44; then k < (len p) + 1 by A7, NAT_1:13; then k < (len p) + (len <%l%>) by AFINSQ_1:33; then k in (len p) + (len <%l%>) by NAT_1:44; then k in dom (p ^ <%l%>) by AFINSQ_1:def_3; hence e . k = ((p ^ <%l%>) . k) mod n by A5 .= (p . k) mod n by A7, A9, AFINSQ_1:def_3 .= p9 . k by A7, A9 ; ::_thesis: verum end; A10: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(l_mod_n)%>_holds_ e_._((len_p9)_+_k)_=_<%(l_mod_n)%>_._k let k be Nat; ::_thesis: ( k in dom <%(l mod n)%> implies e . ((len p9) + k) = <%(l mod n)%> . k ) assume k in dom <%(l mod n)%> ; ::_thesis: e . ((len p9) + k) = <%(l mod n)%> . k then A11: k in 1 by AFINSQ_1:33; then k < 1 by NAT_1:44; then A12: k = 0 by NAT_1:14; k in dom <%l%> by A11, AFINSQ_1:33; hence e . ((len p9) + k) = ((p ^ <%l%>) . (len p)) mod n by A5, A7, A12, AFINSQ_1:23 .= l mod n by AFINSQ_1:36 .= <%(l mod n)%> . k by A12, AFINSQ_1:34 ; ::_thesis: verum end; dom e = (len p) + (len <%l%>) by A4, AFINSQ_1:def_3 .= (dom p) + 1 by AFINSQ_1:33 .= (len p9) + (len <%(l mod n)%>) by A7, AFINSQ_1:33 ; then A13: e = p9 ^ <%(l mod n)%> by A8, A10, AFINSQ_1:def_3; thus (Sum (p ^ <%l%>)) mod n = ((Sum p) + (Sum <%l%>)) mod n by AFINSQ_2:55 .= ((Sum p) + l) mod n by AFINSQ_2:53 .= (((Sum p) mod n) + l) mod n by NAT_D:22 .= (((Sum p) mod n) + (l mod n)) mod n by NAT_D:23 .= (((Sum p9) mod n) + (l mod n)) mod n by A3, A7 .= ((Sum p9) + (l mod n)) mod n by NAT_D:22 .= ((Sum p9) + (Sum <%(l mod n)%>)) mod n by AFINSQ_2:53 .= (Sum e) mod n by A13, AFINSQ_2:55 ; ::_thesis: verum end; end; A14: S1[ <%> NAT] proof let e be XFinSequence of NAT ; ::_thesis: ( dom (<%> NAT) = dom e & ( for i being Nat st i in dom (<%> NAT) holds e . i = ((<%> NAT) . i) mod n ) implies (Sum (<%> NAT)) mod n = (Sum e) mod n ) assume that A15: dom (<%> NAT) = dom e and for i being Nat st i in dom (<%> NAT) holds e . i = ((<%> NAT) . i) mod n ; ::_thesis: (Sum (<%> NAT)) mod n = (Sum e) mod n len e = 0 by A15; hence (Sum (<%> NAT)) mod n = (Sum e) mod n by AFINSQ_1:15; ::_thesis: verum end; for p being XFinSequence of NAT holds S1[p] from AFINSQ_2:sch_2(A14, A2); hence (Sum d) mod n = (Sum e) mod n by A1; ::_thesis: verum end; begin definition let d be XFinSequence of NAT ; let b be Nat; func value (d,b) -> Nat means :Def1: :: NUMERAL1:def 1 ex d9 being XFinSequence of NAT st ( dom d9 = dom d & ( for i being Nat st i in dom d9 holds d9 . i = (d . i) * (b |^ i) ) & it = Sum d9 ); existence ex b1 being Nat ex d9 being XFinSequence of NAT st ( dom d9 = dom d & ( for i being Nat st i in dom d9 holds d9 . i = (d . i) * (b |^ i) ) & b1 = Sum d9 ) proof deffunc H1( Nat) -> Element of NAT = (d . $1) * (b |^ $1); consider d9 being XFinSequence such that A1: ( len d9 = len d & ( for i being Nat st i in len d holds d9 . i = H1(i) ) ) from AFINSQ_1:sch_2(); rng d9 c= NAT proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng d9 or a in NAT ) assume a in rng d9 ; ::_thesis: a in NAT then consider i being set such that A2: i in dom d9 and A3: d9 . i = a by FUNCT_1:def_3; reconsider i = i as Element of NAT by A2; a = H1(i) by A1, A2, A3; hence a in NAT ; ::_thesis: verum end; then reconsider d9 = d9 as XFinSequence of NAT by RELAT_1:def_19; take Sum d9 ; ::_thesis: ex d9 being XFinSequence of NAT st ( dom d9 = dom d & ( for i being Nat st i in dom d9 holds d9 . i = (d . i) * (b |^ i) ) & Sum d9 = Sum d9 ) thus ex d9 being XFinSequence of NAT st ( dom d9 = dom d & ( for i being Nat st i in dom d9 holds d9 . i = (d . i) * (b |^ i) ) & Sum d9 = Sum d9 ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Nat st ex d9 being XFinSequence of NAT st ( dom d9 = dom d & ( for i being Nat st i in dom d9 holds d9 . i = (d . i) * (b |^ i) ) & b1 = Sum d9 ) & ex d9 being XFinSequence of NAT st ( dom d9 = dom d & ( for i being Nat st i in dom d9 holds d9 . i = (d . i) * (b |^ i) ) & b2 = Sum d9 ) holds b1 = b2 proof let k, l be Nat; ::_thesis: ( ex d9 being XFinSequence of NAT st ( dom d9 = dom d & ( for i being Nat st i in dom d9 holds d9 . i = (d . i) * (b |^ i) ) & k = Sum d9 ) & ex d9 being XFinSequence of NAT st ( dom d9 = dom d & ( for i being Nat st i in dom d9 holds d9 . i = (d . i) * (b |^ i) ) & l = Sum d9 ) implies k = l ) given k9 being XFinSequence of NAT such that A4: dom k9 = dom d and A5: for i being Nat st i in dom k9 holds k9 . i = (d . i) * (b |^ i) and A6: k = Sum k9 ; ::_thesis: ( for d9 being XFinSequence of NAT holds ( not dom d9 = dom d or ex i being Nat st ( i in dom d9 & not d9 . i = (d . i) * (b |^ i) ) or not l = Sum d9 ) or k = l ) given l9 being XFinSequence of NAT such that A7: dom l9 = dom d and A8: for i being Nat st i in dom l9 holds l9 . i = (d . i) * (b |^ i) and A9: l = Sum l9 ; ::_thesis: k = l now__::_thesis:_for_i_being_Nat_st_i_in_dom_d_holds_ k9_._i_=_l9_._i let i be Nat; ::_thesis: ( i in dom d implies k9 . i = l9 . i ) assume A10: i in dom d ; ::_thesis: k9 . i = l9 . i hence k9 . i = (d . i) * (b |^ i) by A4, A5 .= l9 . i by A7, A8, A10 ; ::_thesis: verum end; hence k = l by A4, A6, A7, A9, AFINSQ_1:8; ::_thesis: verum end; end; :: deftheorem Def1 defines value NUMERAL1:def_1_:_ for d being XFinSequence of NAT for b, b3 being Nat holds ( b3 = value (d,b) iff ex d9 being XFinSequence of NAT st ( dom d9 = dom d & ( for i being Nat st i in dom d9 holds d9 . i = (d . i) * (b |^ i) ) & b3 = Sum d9 ) ); definition let n, b be Nat; assume A1: b > 1 ; func digits (n,b) -> XFinSequence of NAT means :Def2: :: NUMERAL1:def 2 ( value (it,b) = n & it . ((len it) - 1) <> 0 & ( for i being Nat st i in dom it holds ( 0 <= it . i & it . i < b ) ) ) if n <> 0 otherwise it = <%0%>; consistency for b1 being XFinSequence of NAT holds verum ; existence ( ( n <> 0 implies ex b1 being XFinSequence of NAT st ( value (b1,b) = n & b1 . ((len b1) - 1) <> 0 & ( for i being Nat st i in dom b1 holds ( 0 <= b1 . i & b1 . i < b ) ) ) ) & ( not n <> 0 implies ex b1 being XFinSequence of NAT st b1 = <%0%> ) ) proof reconsider d = <%0%> as XFinSequence of NAT ; reconsider N = n, B = b as Element of NAT by ORDINAL1:def_12; thus ( n <> 0 implies ex d being XFinSequence of NAT st ( value (d,b) = n & d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds ( 0 <= d . i & d . i < b ) ) ) ) ::_thesis: ( not n <> 0 implies ex b1 being XFinSequence of NAT st b1 = <%0%> ) proof deffunc H1( Nat, Element of NAT ) -> Element of NAT = $2 div B; consider f being Function of NAT,NAT such that A2: ( f . 0 = N & ( for i being Nat holds f . (i + 1) = H1(i,f . i) ) ) from NAT_1:sch_12(); defpred S1[ Nat] means f . $1 = 0 ; defpred S2[ Nat] means ex i being Element of NAT st f . i = $1; A3: for k being Nat st k <> 0 & S2[k] holds ex l being Nat st ( l < k & S2[l] ) proof let k be Nat; ::_thesis: ( k <> 0 & S2[k] implies ex l being Nat st ( l < k & S2[l] ) ) assume that A4: k <> 0 and A5: S2[k] ; ::_thesis: ex l being Nat st ( l < k & S2[l] ) take l = k div b; ::_thesis: ( l < k & S2[l] ) thus l < k by A1, A4, INT_1:56; ::_thesis: S2[l] consider i being Element of NAT such that A6: f . i = k by A5; take i + 1 ; ::_thesis: f . (i + 1) = l thus f . (i + 1) = l by A2, A6; ::_thesis: verum end; A7: ex k being Nat st S2[k] by A2; S2[ 0 ] from NAT_1:sch_7(A7, A3); then A8: ex l being Nat st S1[l] ; consider l being Nat such that A9: ( S1[l] & ( for i being Nat st S1[i] holds l <= i ) ) from NAT_1:sch_5(A8); assume n <> 0 ; ::_thesis: ex d being XFinSequence of NAT st ( value (d,b) = n & d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds ( 0 <= d . i & d . i < b ) ) ) then consider m being Nat such that A10: m + 1 = l by A2, A9, NAT_1:6; reconsider m = m as Element of NAT by ORDINAL1:def_12; dom f = NAT by FUNCT_2:def_1; then m + 1 c= dom f by ORDINAL1:def_2; then dom (f | (m + 1)) = m + 1 by RELAT_1:62; then reconsider g = f | (m + 1) as XFinSequence of NAT by ORDINAL1:def_7; defpred S3[ Nat, Nat] means $2 = (g . $1) mod b; A11: for i being Nat st i in m + 1 holds ex x being Element of NAT st S3[i,x] ; consider d being XFinSequence of NAT such that A12: ( dom d = m + 1 & ( for i being Nat st i in m + 1 holds S3[i,d . i] ) ) from STIRL2_1:sch_5(A11); A13: now__::_thesis:_for_i_being_Nat_st_l_<=_i_&_S1[i]_holds_ S1[i_+_1] let i be Nat; ::_thesis: ( l <= i & S1[i] implies S1[i + 1] ) assume l <= i ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume S1[i] ; ::_thesis: S1[i + 1] then f . (i + 1) = 0 div b by A2; hence S1[i + 1] by NAT_2:2; ::_thesis: verum end; A14: S1[l] by A9; A15: for i being Nat st l <= i holds S1[i] from NAT_1:sch_8(A14, A13); A16: now__::_thesis:_for_i_being_Element_of_NAT_st_m_<_i_holds_ f_._i_=_0 let i be Element of NAT ; ::_thesis: ( m < i implies f . i = 0 ) assume m < i ; ::_thesis: f . i = 0 then l <= i by A10, NAT_1:13; hence f . i = 0 by A15; ::_thesis: verum end; deffunc H2( Nat) -> Element of NAT = (d . $1) * (b |^ $1); consider d9 being XFinSequence such that A17: ( len d9 = len d & ( for i being Nat st i in len d holds d9 . i = H2(i) ) ) from AFINSQ_1:sch_2(); rng d9 c= NAT proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng d9 or a in NAT ) assume a in rng d9 ; ::_thesis: a in NAT then consider i being set such that A18: i in dom d9 and A19: d9 . i = a by FUNCT_1:def_3; reconsider i = i as Element of NAT by A18; a = H2(i) by A17, A18, A19; hence a in NAT ; ::_thesis: verum end; then reconsider d9 = d9 as XFinSequence of NAT by RELAT_1:def_19; consider s being Function of NAT,NAT such that A20: s . 0 = d9 . 0 and A21: for i being Nat st i + 1 < len d9 holds s . (i + 1) = addnat . ((s . i),(d9 . (i + 1))) and A22: addnat "**" d9 = s . ((len d9) - 1) by A12, A17, AFINSQ_2:def_8; defpred S4[ Element of NAT ] means ( $1 < len d9 implies s . $1 = n - ((f . ($1 + 1)) * (b |^ ($1 + 1))) ); A23: now__::_thesis:_for_i_being_Element_of_NAT_st_S4[i]_holds_ S4[i_+_1] let i be Element of NAT ; ::_thesis: ( S4[i] implies S4[i + 1] ) assume A24: S4[i] ; ::_thesis: S4[i + 1] now__::_thesis:_(_i_+_1_<_len_d9_implies_s_._(i_+_1)_=_n_-_((f_._((i_+_1)_+_1))_*_(b_|^_((i_+_1)_+_1)))_) assume A25: i + 1 < len d9 ; ::_thesis: s . (i + 1) = n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1))) then A26: i + 1 in dom d9 by NAT_1:44; thus s . (i + 1) = addnat . ((s . i),(d9 . (i + 1))) by A21, A25 .= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (d9 . (i + 1)) by A24, A25, BINOP_2:def_23, NAT_1:13 .= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + ((d . (i + 1)) * (b |^ (i + 1))) by A17, A26 .= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((g . (i + 1)) mod b) * (b |^ (i + 1))) by A12, A17, A26 .= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) mod b) * (b |^ (i + 1))) by A12, A17, A26, FUNCT_1:49 .= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * ((f . (i + 1)) div B))) * (b |^ (i + 1))) by A1, NEWTON:63 .= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * (f . ((i + 1) + 1)))) * (b |^ (i + 1))) by A2 .= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) * (b |^ (i + 1))) - ((f . ((i + 1) + 1)) * (b * (b |^ (i + 1))))) .= (n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) * (b |^ (i + 1))) - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1)))) by NEWTON:6 .= n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1))) ; ::_thesis: verum end; hence S4[i + 1] ; ::_thesis: verum end; reconsider ld = (len d9) - 1 as Element of NAT by A12, A17; A27: 0 in m + 1 by NAT_1:44; then d9 . 0 = (d . 0) * (b |^ 0) by A12, A17 .= ((g . 0) mod b) * (b |^ 0) by A12, A27 .= ((f . 0) mod b) * (b |^ 0) by A27, FUNCT_1:49 .= (n mod b) * 1 by A2, NEWTON:4 .= N - (B * (N div B)) by A1, NEWTON:63 .= n - ((n div b) * (b |^ 1)) by NEWTON:5 .= n - ((f . (0 + 1)) * (b |^ (0 + 1))) by A2 ; then A28: S4[ 0 ] by A20; for i being Element of NAT holds S4[i] from NAT_1:sch_1(A28, A23); then s . ld = n - ((f . (m + 1)) * (b |^ (m + 1))) by A12, A17, XREAL_1:44 .= n by A9, A10 ; then A29: n = Sum d9 by A22, AFINSQ_2:51; m < l by A10, NAT_1:13; then A30: f . m <> 0 by A9; take d ; ::_thesis: ( value (d,b) = n & d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds ( 0 <= d . i & d . i < b ) ) ) thus value (d,b) = n by A17, A29, Def1; ::_thesis: ( d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds ( 0 <= d . i & d . i < b ) ) ) g . m = f . m by FUNCT_1:49, NAT_1:45; then ( m < m + 1 & f . (m + 1) = (g . m) div b ) by A2, NAT_1:13; then A31: (g . m) div b = 0 by A16; d . ((len d) - 1) = (g . m) mod b by A12, NAT_1:45 .= g . m by A1, A31, NAT_2:12, NAT_D:24 ; hence d . ((len d) - 1) <> 0 by A30, FUNCT_1:49, NAT_1:45; ::_thesis: for i being Nat st i in dom d holds ( 0 <= d . i & d . i < b ) let i be Nat; ::_thesis: ( i in dom d implies ( 0 <= d . i & d . i < b ) ) assume i in dom d ; ::_thesis: ( 0 <= d . i & d . i < b ) then d . i = (g . i) mod b by A12; hence ( 0 <= d . i & d . i < b ) by A1, NAT_D:1; ::_thesis: verum end; assume n = 0 ; ::_thesis: ex b1 being XFinSequence of NAT st b1 = <%0%> take d ; ::_thesis: d = <%0%> thus d = <%0%> ; ::_thesis: verum end; uniqueness for b1, b2 being XFinSequence of NAT holds ( ( n <> 0 & value (b1,b) = n & b1 . ((len b1) - 1) <> 0 & ( for i being Nat st i in dom b1 holds ( 0 <= b1 . i & b1 . i < b ) ) & value (b2,b) = n & b2 . ((len b2) - 1) <> 0 & ( for i being Nat st i in dom b2 holds ( 0 <= b2 . i & b2 . i < b ) ) implies b1 = b2 ) & ( not n <> 0 & b1 = <%0%> & b2 = <%0%> implies b1 = b2 ) ) proof reconsider b1 = b - 1 as Element of NAT by A1, NAT_1:20; let d, e be XFinSequence of NAT ; ::_thesis: ( ( n <> 0 & value (d,b) = n & d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds ( 0 <= d . i & d . i < b ) ) & value (e,b) = n & e . ((len e) - 1) <> 0 & ( for i being Nat st i in dom e holds ( 0 <= e . i & e . i < b ) ) implies d = e ) & ( not n <> 0 & d = <%0%> & e = <%0%> implies d = e ) ) thus ( n <> 0 & value (d,b) = n & d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds ( 0 <= d . i & d . i < b ) ) & value (e,b) = n & e . ((len e) - 1) <> 0 & ( for i being Nat st i in dom e holds ( 0 <= e . i & e . i < b ) ) implies d = e ) ::_thesis: ( not n <> 0 & d = <%0%> & e = <%0%> implies d = e ) proof log (2,b) > log (2,1) by A1, POWER:57; then A32: log (2,b) > 0 by POWER:51; log (2,b) > log (2,1) by A1, POWER:57; then A33: log (2,b) > 0 by POWER:51; A34: 1 - b <> 0 by A1; A35: 1 - b <> 0 by A1; reconsider g = (b1 (#) (b GeoSeq)) | (len d) as XFinSequence of NAT by Th1; assume A36: n <> 0 ; ::_thesis: ( not value (d,b) = n or not d . ((len d) - 1) <> 0 or ex i being Nat st ( i in dom d & not ( 0 <= d . i & d . i < b ) ) or not value (e,b) = n or not e . ((len e) - 1) <> 0 or ex i being Nat st ( i in dom e & not ( 0 <= e . i & e . i < b ) ) or d = e ) assume that A37: value (d,b) = n and A38: d . ((len d) - 1) <> 0 and A39: for i being Nat st i in dom d holds ( 0 <= d . i & d . i < b ) ; ::_thesis: ( not value (e,b) = n or not e . ((len e) - 1) <> 0 or ex i being Nat st ( i in dom e & not ( 0 <= e . i & e . i < b ) ) or d = e ) consider D being XFinSequence of NAT such that A40: dom D = dom d and A41: for i being Nat st i in dom D holds D . i = (d . i) * (b |^ i) and A42: n = Sum D by A37, Def1; A43: len D > 0 by A38, A40, FUNCT_1:def_2; A44: (len d) - 1 in dom d by A38, FUNCT_1:def_2; then reconsider k = (len d) - 1 as Element of NAT ; A45: 1 * (b |^ k) <= (d . k) * (b |^ k) by A38, NAT_1:4, NAT_1:14; A46: b |^ k > 0 by A1, PREPOWER:6; D . k = (d . k) * (b |^ k) by A40, A41, A44; then (d . k) * (b |^ k) <= n by A40, A42, A44, A43, AFINSQ_2:61; then b |^ k <= n by A45, XXREAL_0:2; then log (2,(b to_power k)) <= log (2,n) by A46, PRE_FF:10; then k * (log (2,b)) <= log (2,n) by A1, POWER:55; then (k * (log (2,b))) / (log (2,b)) <= (log (2,n)) / (log (2,b)) by A33, XREAL_1:72; then A47: k <= (log (2,n)) / (log (2,b)) by A33, XCMPLX_1:89; g = ((b - 1) (#) (b GeoSeq)) | (k + 1) ; then A48: Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . k by AFINSQ_2:56 .= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . k by SERIES_1:9 .= (b - 1) * ((Partial_Sums (b GeoSeq)) . k) by SEQ_1:9 .= (b - 1) * ((1 - (b to_power (k + 1))) / (1 - b)) by A1, SERIES_1:22 .= - ((1 - b) * ((1 - (b |^ (k + 1))) / (1 - b))) .= - (1 - (b |^ (k + 1))) by A35, XCMPLX_1:87 .= (b |^ (k + 1)) - 1 ; A49: dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1; then A50: len D = len g by A40, RELAT_1:62; len d c= dom ((b - 1) (#) (b GeoSeq)) by A49, ORDINAL1:def_2; then A51: dom g = len d by RELAT_1:62; A52: for i being Nat st i in dom D holds D . i <= g . i proof let i be Nat; ::_thesis: ( i in dom D implies D . i <= g . i ) reconsider I = i as Element of NAT by ORDINAL1:def_12; assume A53: i in dom D ; ::_thesis: D . i <= g . i then A54: D . i = (d . i) * (b |^ i) by A41; d . i < b1 + 1 by A39, A40, A53; then A55: d . i <= b1 by NAT_1:13; g . I = ((b - 1) (#) (b GeoSeq)) . I by A40, A51, A53, FUNCT_1:47 .= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9 .= b1 * (b |^ I) by PREPOWER:def_1 ; hence D . i <= g . i by A55, A54, XREAL_1:64; ::_thesis: verum end; assume that A56: value (e,b) = n and A57: e . ((len e) - 1) <> 0 and A58: for i being Nat st i in dom e holds ( 0 <= e . i & e . i < b ) ; ::_thesis: d = e consider E being XFinSequence of NAT such that A59: dom E = dom e and A60: for i being Nat st i in dom E holds E . i = (e . i) * (b |^ i) and A61: n = Sum E by A56, Def1; A62: (len e) - 1 in dom e by A57, FUNCT_1:def_2; then reconsider l = (len e) - 1 as Element of NAT ; A63: 1 * (b |^ l) <= (e . l) * (b |^ l) by A57, NAT_1:4, NAT_1:14; reconsider g = (b1 (#) (b GeoSeq)) | (len e) as XFinSequence of NAT by Th1; g = ((b - 1) (#) (b GeoSeq)) | (l + 1) ; then A64: Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . l by AFINSQ_2:56 .= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . l by SERIES_1:9 .= (b - 1) * ((Partial_Sums (b GeoSeq)) . l) by SEQ_1:9 .= (b - 1) * ((1 - (b to_power (l + 1))) / (1 - b)) by A1, SERIES_1:22 .= - ((1 - b) * ((1 - (b |^ (l + 1))) / (1 - b))) .= - (1 - (b |^ (l + 1))) by A34, XCMPLX_1:87 .= (b |^ (l + 1)) - 1 ; A65: dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1; then len e c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2; then A66: dom g = len e by RELAT_1:62; A67: for i being Nat st i in dom E holds E . i <= g . i proof let i be Nat; ::_thesis: ( i in dom E implies E . i <= g . i ) reconsider I = i as Element of NAT by ORDINAL1:def_12; assume A68: i in dom E ; ::_thesis: E . i <= g . i then A69: E . i = (e . i) * (b |^ i) by A60; e . i < b1 + 1 by A58, A59, A68; then A70: e . i <= b1 by NAT_1:13; g . I = ((b - 1) (#) (b GeoSeq)) . I by A59, A66, A68, FUNCT_1:47 .= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9 .= b1 * (b |^ I) by PREPOWER:def_1 ; hence E . i <= g . i by A70, A69, XREAL_1:64; ::_thesis: verum end; A71: len E > 0 by A57, A59, FUNCT_1:def_2; A72: b |^ l > 0 by A1, PREPOWER:6; E . l = (e . l) * (b |^ l) by A59, A60, A62; then (e . l) * (b |^ l) <= n by A59, A61, A62, A71, AFINSQ_2:61; then b |^ l <= n by A63, XXREAL_0:2; then log (2,(b to_power l)) <= log (2,n) by A72, PRE_FF:10; then l * (log (2,b)) <= log (2,n) by A1, POWER:55; then (l * (log (2,b))) / (log (2,b)) <= (log (2,n)) / (log (2,b)) by A32, XREAL_1:72; then A73: l <= (log (2,n)) / (log (2,b)) by A32, XCMPLX_1:89; len E = len g by A59, A65, RELAT_1:62; then n < ((b |^ (l + 1)) - 1) + 1 by A61, A64, A67, AFINSQ_2:57, XREAL_1:39; then log (2,n) < log (2,(b to_power (l + 1))) by A36, POWER:57; then log (2,n) < (l + 1) * (log (2,b)) by A1, POWER:55; then (log (2,n)) / (log (2,b)) < ((l + 1) * (log (2,b))) / (log (2,b)) by A32, XREAL_1:74; then (log (2,n)) / (log (2,b)) < l + 1 by A32, XCMPLX_1:89; then k < l + 1 by A47, XXREAL_0:2; then A74: k <= l by NAT_1:13; n < ((b |^ (k + 1)) - 1) + 1 by A42, A48, A50, A52, AFINSQ_2:57, XREAL_1:39; then log (2,n) < log (2,(b to_power (k + 1))) by A36, POWER:57; then log (2,n) < (k + 1) * (log (2,b)) by A1, POWER:55; then (log (2,n)) / (log (2,b)) < ((k + 1) * (log (2,b))) / (log (2,b)) by A33, XREAL_1:74; then (log (2,n)) / (log (2,b)) < k + 1 by A33, XCMPLX_1:89; then l < k + 1 by A73, XXREAL_0:2; then l <= k by NAT_1:13; then A75: k = l by A74, XXREAL_0:1; now__::_thesis:_for_a_being_set_st_a_in_dom_d_holds_ d_._a_=_e_._a let a be set ; ::_thesis: ( a in dom d implies d . b1 = e . b1 ) assume A76: a in dom d ; ::_thesis: d . b1 = e . b1 then reconsider o = a as Element of NAT ; o < k + 1 by A76, NAT_1:44; then A77: o <= k by NAT_1:13; A78: o < len d by A76, NAT_1:44; then reconsider oo = (len d) - o as Element of NAT by NAT_1:21; percases ( ( o = 0 & o = k ) or ( o = 0 & o < k ) or ( o > 0 & o = k ) or ( o > 0 & o < k ) ) by A77, XXREAL_0:1; supposeA79: ( o = 0 & o = k ) ; ::_thesis: d . b1 = e . b1 then len E = 1 by A59, A75; then A80: E = <%(E . 0)%> by AFINSQ_1:34 .= <%((e . 0) * (b |^ 0))%> by A59, A60, A75, A76, A79 .= <%((e . 0) * 1)%> by NEWTON:4 ; len D = 1 by A40, A79; then D = <%(D . 0)%> by AFINSQ_1:34 .= <%((d . 0) * (b |^ 0))%> by A40, A41, A76, A79 .= <%((d . 0) * 1)%> by NEWTON:4 ; hence d . a = n by A42, A79, AFINSQ_2:53 .= e . a by A61, A79, A80, AFINSQ_2:53 ; ::_thesis: verum end; supposeA81: ( o = 0 & o < k ) ; ::_thesis: d . b1 = e . b1 reconsider do = <%> NAT as XFinSequence of NAT ; A82: len do = o by A81; Sum do = 0 ; then A83: (Sum do) div (b |^ o) = 0 by NAT_2:2; set d9 = D; A84: for x being Nat st x in dom do holds D . x = do . x ; ( dom D = (len do) + (len D) & ( for x being Nat st x in dom D holds D . ((len do) + x) = D . x ) ) by A81, A82; then D = do ^ D by A84, AFINSQ_1:def_3; then A85: n = (Sum do) + (Sum D) by A42, AFINSQ_2:55; reconsider bo = b |^ o as Element of NAT by ORDINAL1:def_12; A86: bo <> 0 by A1, PREPOWER:5; A87: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(D_._o)%>_holds_ D_._k_=_<%(D_._o)%>_._k let k be Nat; ::_thesis: ( k in dom <%(D . o)%> implies D . k = <%(D . o)%> . k ) assume k in dom <%(D . o)%> ; ::_thesis: D . k = <%(D . o)%> . k then k in 1 by AFINSQ_1:33; then k < 1 by NAT_1:44; then k = 0 by NAT_1:14; hence D . k = <%(D . o)%> . k by A81, AFINSQ_1:def_4; ::_thesis: verum end; reconsider o1 = o + 1 as Element of NAT ; o1 <= k by A81, NAT_1:13; then A88: o1 < len d by XREAL_1:147; reconsider oo1 = (len d) - o1 as Element of NAT by A81; defpred S1[ Nat, set ] means $2 = D . ($1 + o1); reconsider do1 = D | o1 as XFinSequence of NAT ; A89: for u being Nat st u in oo1 holds ex x being Element of NAT st S1[u,x] ; consider d91 being XFinSequence of NAT such that A90: ( dom d91 = oo1 & ( for x being Nat st x in oo1 holds S1[x,d91 . x] ) ) from STIRL2_1:sch_5(A89); A91: len d = len D by A40; then A92: len do1 = o1 by A88, AFINSQ_1:11; then A93: dom D = (len do1) + (len d91) by A40, A90; now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_ b_|^_o1_divides_d91_._k let k be Nat; ::_thesis: ( k in dom d91 implies b |^ o1 divides d91 . k ) reconsider K = k as Element of NAT by ORDINAL1:def_12; assume A94: k in dom d91 ; ::_thesis: b |^ o1 divides d91 . k then k < len d91 by NAT_1:44; then o1 + k < dom D by A92, A93, XREAL_1:8; then o1 + k in dom D by NAT_1:44; then D . (o1 + k) = (d . (o1 + k)) * (b |^ (o1 + k)) by A41; then d91 . K = (d . (o1 + k)) * (b |^ (o1 + k)) by A90, A94 .= (d . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8 .= ((d . (o1 + k)) * (b |^ k)) * (b |^ o1) ; hence b |^ o1 divides d91 . k by NAT_D:def_3; ::_thesis: verum end; then A95: b |^ o1 divides Sum d91 by Th2; A96: now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_ D_._((len_<%(D_._o)%>)_+_k)_=_d91_._k let k be Nat; ::_thesis: ( k in dom d91 implies D . ((len <%(D . o)%>) + k) = d91 . k ) assume A97: k in dom d91 ; ::_thesis: D . ((len <%(D . o)%>) + k) = d91 . k thus D . ((len <%(D . o)%>) + k) = D . ((len do1) + k) by A81, A92, AFINSQ_1:33 .= d91 . k by A90, A92, A97 ; ::_thesis: verum end; dom D = 1 + (dom d91) by A40, A81, A90 .= (len <%(D . o)%>) + (len d91) by AFINSQ_1:34 ; then D = <%(D . o)%> ^ d91 by A87, A96, AFINSQ_1:def_3; then A98: Sum D = (Sum <%(D . o)%>) + (Sum d91) by AFINSQ_2:55; ( ( for x being Nat st x in dom do1 holds D . x = do1 . x ) & ( for x being Nat st x in dom d91 holds D . ((len do1) + x) = d91 . x ) ) by A90, A92, FUNCT_1:47; then D = do1 ^ d91 by A93, AFINSQ_1:def_3; then A99: n = (Sum do1) + (Sum d91) by A42, AFINSQ_2:55; reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def_12; consider ok1 being Nat such that A100: ok1 + 1 = o1 ; now__::_thesis:_for_k_being_Nat_st_k_in_dom_D_holds_ b_|^_o_divides_D_._k let k be Nat; ::_thesis: ( k in dom D implies b |^ o divides D . k ) reconsider K = k as Element of NAT by ORDINAL1:def_12; assume k in dom D ; ::_thesis: b |^ o divides D . k then D . K = (d . (o + k)) * (b |^ (o + k)) by A41, A81 .= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8 .= ((d . (o + k)) * (b |^ k)) * (b |^ o) ; hence b |^ o divides D . k by NAT_D:def_3; ::_thesis: verum end; then A101: b |^ o divides Sum D by Th2; then (Sum D) mod (b |^ o) = 0 by A86, PEPIN:6; then n div (b |^ o) = ((Sum D) div (b |^ o)) + ((Sum do) div (b |^ o)) by A85, NAT_D:19; then A102: (n div (b |^ o)) * (b |^ o) = Sum D by A83, A101, NAT_D:3; reconsider do = <%> NAT as XFinSequence of NAT ; A103: len do = o by A81; Sum do = 0 ; then A104: (Sum do) div (b |^ o) = 0 by NAT_2:2; set d9 = E; A105: for x being Nat st x in dom do holds E . x = do . x ; ( dom E = (len do) + (len E) & ( for x being Nat st x in dom E holds E . ((len do) + x) = E . x ) ) by A81, A103; then E = do ^ E by A105, AFINSQ_1:def_3; then A106: n = (Sum do) + (Sum E) by A61, AFINSQ_2:55; reconsider bo = b |^ o as Element of NAT by ORDINAL1:def_12; A107: bo <> 0 by A1, PREPOWER:5; reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def_12; reconsider g1 = (b1 (#) (b GeoSeq)) | (ok1 + 1) as XFinSequence of NAT by Th1; A108: 1 - b <> 0 by A1; dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1; then A109: o1 c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2; then A110: len do1 = len g1 by A92, A100, RELAT_1:62; A111: dom g1 = o1 by A100, A109, RELAT_1:62; A112: for i being Nat st i in dom do1 holds do1 . i <= g1 . i proof let i be Nat; ::_thesis: ( i in dom do1 implies do1 . i <= g1 . i ) reconsider I = i as Element of NAT by ORDINAL1:def_12; assume A113: i in dom do1 ; ::_thesis: do1 . i <= g1 . i then i in o1 by A88, A91, AFINSQ_1:11; then A114: g1 . I = ((b - 1) (#) (b GeoSeq)) . I by A111, FUNCT_1:47 .= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9 .= b1 * (b |^ I) by PREPOWER:def_1 ; A115: dom do1 c= dom D by RELAT_1:60; then d . i < b1 + 1 by A39, A40, A113; then A116: d . i <= b1 by NAT_1:13; do1 . i = D . i by A113, FUNCT_1:47 .= (d . i) * (b |^ i) by A41, A113, A115 ; hence do1 . i <= g1 . i by A114, A116, XREAL_1:64; ::_thesis: verum end; Sum g1 = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok1 by AFINSQ_2:56 .= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok1 by SERIES_1:9 .= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok1) by SEQ_1:9 .= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by A1, SERIES_1:22 .= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A100 .= - (1 - (b |^ o1)) by A108, XCMPLX_1:87 .= (b |^ o1) - 1 ; then Sum do1 < ((b |^ o1) - 1) + 1 by A110, A112, AFINSQ_2:57, XREAL_1:145; then A117: (Sum do1) div (b |^ o1) = 0 by NAT_D:27; bo1 <> 0 by A1, PREPOWER:5; then (Sum d91) mod (b |^ o1) = 0 by A95, PEPIN:6; then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A99, NAT_D:19; then (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A117, A95, NAT_D:3; then D . o = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A102, A98, AFINSQ_2:53; then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A40, A41, A76; then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1))) by NEWTON:8; then (d . o) * (b |^ o) = (b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))) ; then ((b |^ o) * (d . o)) / (b |^ o) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by NEWTON:5; then A118: d . o = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by A86, XCMPLX_1:89; reconsider o1 = o + 1 as Element of NAT ; reconsider do1 = E | o1 as XFinSequence of NAT ; A119: len e = len E by A59; now__::_thesis:_for_k_being_Nat_st_k_in_dom_E_holds_ b_|^_o_divides_E_._k let k be Nat; ::_thesis: ( k in dom E implies b |^ o divides E . k ) reconsider K = k as Element of NAT by ORDINAL1:def_12; assume k in dom E ; ::_thesis: b |^ o divides E . k then E . K = (e . (o + k)) * (b |^ (o + k)) by A60, A81 .= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8 .= ((e . (o + k)) * (b |^ k)) * (b |^ o) ; hence b |^ o divides E . k by NAT_D:def_3; ::_thesis: verum end; then A120: b |^ o divides Sum E by Th2; then (Sum E) mod (b |^ o) = 0 by A107, PEPIN:6; then n div (b |^ o) = ((Sum E) div (b |^ o)) + ((Sum do) div (b |^ o)) by A106, NAT_D:19; then A121: (n div (b |^ o)) * (b |^ o) = Sum E by A104, A120, NAT_D:3; A122: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(E_._o)%>_holds_ E_._k_=_<%(E_._o)%>_._k let k be Nat; ::_thesis: ( k in dom <%(E . o)%> implies E . k = <%(E . o)%> . k ) assume k in dom <%(E . o)%> ; ::_thesis: E . k = <%(E . o)%> . k then k in 1 by AFINSQ_1:33; then k < 1 by NAT_1:44; then k = 0 by NAT_1:14; hence E . k = <%(E . o)%> . k by A81, AFINSQ_1:def_4; ::_thesis: verum end; reconsider oo1 = (len d) - o1 as Element of NAT by A81; defpred S2[ Nat, set ] means $2 = E . ($1 + o1); A123: for u being Nat st u in oo1 holds ex x being Element of NAT st S2[u,x] ; consider d91 being XFinSequence of NAT such that A124: ( dom d91 = oo1 & ( for x being Nat st x in oo1 holds S2[x,d91 . x] ) ) from STIRL2_1:sch_5(A123); o1 <= k by A81, NAT_1:13; then A125: o1 < len d by XREAL_1:147; then A126: len do1 = o1 by A75, A119, AFINSQ_1:11; A127: now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_ E_._((len_<%(E_._o)%>)_+_k)_=_d91_._k let k be Nat; ::_thesis: ( k in dom d91 implies E . ((len <%(E . o)%>) + k) = d91 . k ) assume A128: k in dom d91 ; ::_thesis: E . ((len <%(E . o)%>) + k) = d91 . k thus E . ((len <%(E . o)%>) + k) = E . ((len do1) + k) by A81, A126, AFINSQ_1:33 .= d91 . k by A124, A126, A128 ; ::_thesis: verum end; reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def_12; consider ok1 being Nat such that A129: ok1 + 1 = o1 ; A130: dom E = (len do1) + (len d91) by A59, A75, A124, A126; now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_ b_|^_o1_divides_d91_._k let k be Nat; ::_thesis: ( k in dom d91 implies b |^ o1 divides d91 . k ) reconsider K = k as Element of NAT by ORDINAL1:def_12; assume A131: k in dom d91 ; ::_thesis: b |^ o1 divides d91 . k then k < len d91 by NAT_1:44; then o1 + k < dom E by A126, A130, XREAL_1:8; then o1 + k in dom E by NAT_1:44; then E . (o1 + k) = (e . (o1 + k)) * (b |^ (o1 + k)) by A60; then d91 . K = (e . (o1 + k)) * (b |^ (o1 + k)) by A124, A131 .= (e . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8 .= ((e . (o1 + k)) * (b |^ k)) * (b |^ o1) ; hence b |^ o1 divides d91 . k by NAT_D:def_3; ::_thesis: verum end; then A132: b |^ o1 divides Sum d91 by Th2; reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def_12; reconsider g1 = (b1 (#) (b GeoSeq)) | (ok1 + 1) as XFinSequence of NAT by Th1; A133: 1 - b <> 0 by A1; dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1; then A134: o1 c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2; then A135: len do1 = len g1 by A126, A129, RELAT_1:62; A136: dom g1 = o1 by A129, A134, RELAT_1:62; A137: for i being Nat st i in dom do1 holds do1 . i <= g1 . i proof let i be Nat; ::_thesis: ( i in dom do1 implies do1 . i <= g1 . i ) reconsider I = i as Element of NAT by ORDINAL1:def_12; assume A138: i in dom do1 ; ::_thesis: do1 . i <= g1 . i then i in o1 by A75, A125, A119, AFINSQ_1:11; then A139: g1 . I = ((b - 1) (#) (b GeoSeq)) . I by A136, FUNCT_1:47 .= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9 .= b1 * (b |^ I) by PREPOWER:def_1 ; A140: dom do1 c= dom E by RELAT_1:60; then e . i < b1 + 1 by A58, A59, A138; then A141: e . i <= b1 by NAT_1:13; do1 . i = E . i by A138, FUNCT_1:47 .= (e . i) * (b |^ i) by A60, A138, A140 ; hence do1 . i <= g1 . i by A139, A141, XREAL_1:64; ::_thesis: verum end; Sum g1 = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok1 by AFINSQ_2:56 .= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok1 by SERIES_1:9 .= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok1) by SEQ_1:9 .= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by A1, SERIES_1:22 .= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A129 .= - (1 - (b |^ o1)) by A133, XCMPLX_1:87 .= (b |^ o1) - 1 ; then Sum do1 < ((b |^ o1) - 1) + 1 by A135, A137, AFINSQ_2:57, XREAL_1:145; then A142: (Sum do1) div (b |^ o1) = 0 by NAT_D:27; ( ( for x being Nat st x in dom do1 holds E . x = do1 . x ) & ( for x being Nat st x in dom d91 holds E . ((len do1) + x) = d91 . x ) ) by A124, A126, FUNCT_1:47; then E = do1 ^ d91 by A130, AFINSQ_1:def_3; then A143: n = (Sum do1) + (Sum d91) by A61, AFINSQ_2:55; bo1 <> 0 by A1, PREPOWER:5; then (Sum d91) mod (b |^ o1) = 0 by A132, PEPIN:6; then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A143, NAT_D:19; then A144: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A142, A132, NAT_D:3; dom E = 1 + (dom d91) by A59, A75, A81, A124 .= (len <%(E . o)%>) + (len d91) by AFINSQ_1:34 ; then E = <%(E . o)%> ^ d91 by A122, A127, AFINSQ_1:def_3; then Sum E = (Sum <%(E . o)%>) + (Sum d91) by AFINSQ_2:55; then E . o = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A121, A144, AFINSQ_2:53; then (e . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A59, A60, A75, A76; then (e . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1))) by NEWTON:8; then (e . o) * (b |^ o) = (b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))) ; then ((b |^ o) * (e . o)) / (b |^ o) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by NEWTON:5; hence d . a = e . a by A118, A107, XCMPLX_1:89; ::_thesis: verum end; supposeA145: ( o > 0 & o = k ) ; ::_thesis: d . b1 = e . b1 set d9 = <%(D . o)%>; reconsider do = D | o as XFinSequence of NAT ; A146: len d = len D by A40; then A147: len do = o by A78, AFINSQ_1:11; A148: len <%(D . o)%> = oo by A145, AFINSQ_1:34; then A149: dom D = (len do) + (len <%(D . o)%>) by A40, A147; A150: for x being Nat st x in dom <%(D . o)%> holds D . ((len do) + x) = <%(D . o)%> . x proof let x be Nat; ::_thesis: ( x in dom <%(D . o)%> implies D . ((len do) + x) = <%(D . o)%> . x ) assume x in dom <%(D . o)%> ; ::_thesis: D . ((len do) + x) = <%(D . o)%> . x then x < 1 by A145, A148, NAT_1:44; then x = 0 by NAT_1:14; hence D . ((len do) + x) = <%(D . o)%> . x by A147, AFINSQ_1:34; ::_thesis: verum end; now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(D_._o)%>_holds_ b_|^_o_divides_<%(D_._o)%>_._k let k be Nat; ::_thesis: ( k in dom <%(D . o)%> implies b |^ o divides <%(D . o)%> . k ) reconsider K = k as Element of NAT by ORDINAL1:def_12; assume A151: k in dom <%(D . o)%> ; ::_thesis: b |^ o divides <%(D . o)%> . k then k < len <%(D . o)%> by NAT_1:44; then o + k < dom D by A147, A149, XREAL_1:8; then o + k in dom D by NAT_1:44; then D . (o + k) = (d . (o + k)) * (b |^ (o + k)) by A41; then <%(D . o)%> . K = (d . (o + k)) * (b |^ (o + k)) by A147, A150, A151 .= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8 .= ((d . (o + k)) * (b |^ k)) * (b |^ o) ; hence b |^ o divides <%(D . o)%> . k by NAT_D:def_3; ::_thesis: verum end; then A152: b |^ o divides Sum <%(D . o)%> by Th2; reconsider bo = b |^ o as Element of NAT by ORDINAL1:def_12; A153: 1 - b <> 0 by A1; consider ok being Nat such that A154: ok + 1 = o by A145, NAT_1:6; reconsider ok = ok as Element of NAT by ORDINAL1:def_12; reconsider g = (b1 (#) (b GeoSeq)) | (ok + 1) as XFinSequence of NAT by Th1; A155: Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok by AFINSQ_2:56 .= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok by SERIES_1:9 .= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok) by SEQ_1:9 .= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by A1, SERIES_1:22 .= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A154 .= - (1 - (b |^ o)) by A153, XCMPLX_1:87 .= (b |^ o) - 1 ; consider ok being Nat such that A156: ok + 1 = o by A145, NAT_1:6; dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1; then A157: o c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2; then A158: dom g = o by A154, RELAT_1:62; A159: for i being Nat st i in dom do holds do . i <= g . i proof let i be Nat; ::_thesis: ( i in dom do implies do . i <= g . i ) reconsider I = i as Element of NAT by ORDINAL1:def_12; assume A160: i in dom do ; ::_thesis: do . i <= g . i then i in o by A78, A146, AFINSQ_1:11; then A161: g . I = ((b - 1) (#) (b GeoSeq)) . I by A158, FUNCT_1:47 .= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9 .= b1 * (b |^ I) by PREPOWER:def_1 ; A162: dom do c= dom D by RELAT_1:60; then d . i < b1 + 1 by A39, A40, A160; then A163: d . i <= b1 by NAT_1:13; do . i = D . i by A160, FUNCT_1:47 .= (d . i) * (b |^ i) by A41, A160, A162 ; hence do . i <= g . i by A161, A163, XREAL_1:64; ::_thesis: verum end; len do = len g by A147, A154, A157, RELAT_1:62; then Sum do < ((b |^ o) - 1) + 1 by A155, A159, AFINSQ_2:57, XREAL_1:145; then A164: (Sum do) div (b |^ o) = 0 by NAT_D:27; for x being Nat st x in dom do holds D . x = do . x by FUNCT_1:47; then D = do ^ <%(D . o)%> by A149, A150, AFINSQ_1:def_3; then A165: n = (Sum do) + (Sum <%(D . o)%>) by A42, AFINSQ_2:55; A166: bo <> 0 by A1, PREPOWER:5; then (Sum <%(D . o)%>) mod (b |^ o) = 0 by A152, PEPIN:6; then n div (b |^ o) = ((Sum <%(D . o)%>) div (b |^ o)) + ((Sum do) div (b |^ o)) by A165, NAT_D:19; then (n div (b |^ o)) * (b |^ o) = Sum <%(D . o)%> by A164, A152, NAT_D:3; then D . o = (n div (b |^ o)) * (b |^ o) by AFINSQ_2:53; then ((d . o) * (b |^ o)) / (b |^ o) = ((n div (b |^ o)) * (b |^ o)) / (b |^ o) by A40, A41, A76; then A167: d . o = ((n div (b |^ o)) * (b |^ o)) / (b |^ o) by A166, XCMPLX_1:89; set d9 = <%(E . o)%>; reconsider do = E | o as XFinSequence of NAT ; A168: len e = len E by A59; then A169: len do = o by A75, A78, AFINSQ_1:11; A170: len <%(E . o)%> = oo by A145, AFINSQ_1:34; then A171: dom E = (len do) + (len <%(E . o)%>) by A59, A75, A169; A172: for x being Nat st x in dom <%(E . o)%> holds E . ((len do) + x) = <%(E . o)%> . x proof let x be Nat; ::_thesis: ( x in dom <%(E . o)%> implies E . ((len do) + x) = <%(E . o)%> . x ) assume x in dom <%(E . o)%> ; ::_thesis: E . ((len do) + x) = <%(E . o)%> . x then x < 1 by A145, A170, NAT_1:44; then x = 0 by NAT_1:14; hence E . ((len do) + x) = <%(E . o)%> . x by A169, AFINSQ_1:34; ::_thesis: verum end; now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(E_._o)%>_holds_ b_|^_o_divides_<%(E_._o)%>_._k let k be Nat; ::_thesis: ( k in dom <%(E . o)%> implies b |^ o divides <%(E . o)%> . k ) reconsider K = k as Element of NAT by ORDINAL1:def_12; assume A173: k in dom <%(E . o)%> ; ::_thesis: b |^ o divides <%(E . o)%> . k then k < len <%(E . o)%> by NAT_1:44; then o + k < dom E by A169, A171, XREAL_1:8; then o + k in dom E by NAT_1:44; then E . (o + k) = (e . (o + k)) * (b |^ (o + k)) by A60; then <%(E . o)%> . K = (e . (o + k)) * (b |^ (o + k)) by A169, A172, A173 .= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8 .= ((e . (o + k)) * (b |^ k)) * (b |^ o) ; hence b |^ o divides <%(E . o)%> . k by NAT_D:def_3; ::_thesis: verum end; then A174: b |^ o divides Sum <%(E . o)%> by Th2; reconsider ok = ok as Element of NAT by ORDINAL1:def_12; reconsider g = (b1 (#) (b GeoSeq)) | (ok + 1) as XFinSequence of NAT by Th1; reconsider bo = b |^ o as Element of NAT by ORDINAL1:def_12; A175: 1 - b <> 0 by A1; dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1; then A176: o c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2; then A177: len do = len g by A169, A156, RELAT_1:62; A178: dom g = o by A156, A176, RELAT_1:62; A179: for i being Nat st i in dom do holds do . i <= g . i proof let i be Nat; ::_thesis: ( i in dom do implies do . i <= g . i ) reconsider I = i as Element of NAT by ORDINAL1:def_12; assume A180: i in dom do ; ::_thesis: do . i <= g . i then i in o by A75, A78, A168, AFINSQ_1:11; then A181: g . I = ((b - 1) (#) (b GeoSeq)) . I by A178, FUNCT_1:47 .= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9 .= b1 * (b |^ I) by PREPOWER:def_1 ; A182: dom do c= dom E by RELAT_1:60; then e . i < b1 + 1 by A58, A59, A180; then A183: e . i <= b1 by NAT_1:13; do . i = E . i by A180, FUNCT_1:47 .= (e . i) * (b |^ i) by A60, A180, A182 ; hence do . i <= g . i by A181, A183, XREAL_1:64; ::_thesis: verum end; Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok by AFINSQ_2:56 .= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok by SERIES_1:9 .= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok) by SEQ_1:9 .= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by A1, SERIES_1:22 .= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A156 .= - (1 - (b |^ o)) by A175, XCMPLX_1:87 .= (b |^ o) - 1 ; then Sum do < ((b |^ o) - 1) + 1 by A177, A179, AFINSQ_2:57, XREAL_1:145; then A184: (Sum do) div (b |^ o) = 0 by NAT_D:27; for x being Nat st x in dom do holds E . x = do . x by FUNCT_1:47; then E = do ^ <%(E . o)%> by A171, A172, AFINSQ_1:def_3; then A185: n = (Sum do) + (Sum <%(E . o)%>) by A61, AFINSQ_2:55; A186: bo <> 0 by A1, PREPOWER:5; then (Sum <%(E . o)%>) mod (b |^ o) = 0 by A174, PEPIN:6; then n div (b |^ o) = ((Sum <%(E . o)%>) div (b |^ o)) + ((Sum do) div (b |^ o)) by A185, NAT_D:19; then (n div (b |^ o)) * (b |^ o) = Sum <%(E . o)%> by A184, A174, NAT_D:3; then E . o = (n div (b |^ o)) * (b |^ o) by AFINSQ_2:53; then ((e . o) * (b |^ o)) / (b |^ o) = ((n div (b |^ o)) * (b |^ o)) / (b |^ o) by A59, A60, A75, A76; hence d . a = e . a by A167, A186, XCMPLX_1:89; ::_thesis: verum end; supposeA187: ( o > 0 & o < k ) ; ::_thesis: d . b1 = e . b1 reconsider o1 = o + 1 as Element of NAT ; A188: o1 <= k by A187, NAT_1:13; then A189: o1 < len d by XREAL_1:147; reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def_12; reconsider do1 = D | o1 as XFinSequence of NAT ; reconsider bo = b |^ o as Element of NAT by ORDINAL1:def_12; defpred S1[ Nat, set ] means $2 = D . ($1 + o); consider ok1 being Nat such that A190: ok1 + 1 = o1 ; reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def_12; reconsider g1 = (b1 (#) (b GeoSeq)) | (ok1 + 1) as XFinSequence of NAT by Th1; A191: len d = len D by A40; then A192: len do1 = o1 by A189, AFINSQ_1:11; dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1; then A193: o1 c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2; then A194: len do1 = len g1 by A192, A190, RELAT_1:62; A195: dom g1 = o1 by A190, A193, RELAT_1:62; A196: for i being Nat st i in dom do1 holds do1 . i <= g1 . i proof let i be Nat; ::_thesis: ( i in dom do1 implies do1 . i <= g1 . i ) reconsider I = i as Element of NAT by ORDINAL1:def_12; assume A197: i in dom do1 ; ::_thesis: do1 . i <= g1 . i then i in o1 by A189, A191, AFINSQ_1:11; then A198: g1 . I = ((b - 1) (#) (b GeoSeq)) . I by A195, FUNCT_1:47 .= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9 .= b1 * (b |^ I) by PREPOWER:def_1 ; A199: dom do1 c= dom D by RELAT_1:60; then d . i < b1 + 1 by A39, A40, A197; then A200: d . i <= b1 by NAT_1:13; do1 . i = D . i by A197, FUNCT_1:47 .= (d . i) * (b |^ i) by A41, A197, A199 ; hence do1 . i <= g1 . i by A198, A200, XREAL_1:64; ::_thesis: verum end; k < len d by XREAL_1:147; then reconsider oo1 = (len d) - o1 as Element of NAT by A188, NAT_1:21, XXREAL_0:2; A201: for u being Nat st u in oo holds ex x being Element of NAT st S1[u,x] ; consider d9 being XFinSequence of NAT such that A202: ( dom d9 = oo & ( for x being Nat st x in oo holds S1[x,d9 . x] ) ) from STIRL2_1:sch_5(A201); A203: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(D_._o)%>_holds_ d9_._k_=_<%(D_._o)%>_._k let k be Nat; ::_thesis: ( k in dom <%(D . o)%> implies d9 . k = <%(D . o)%> . k ) assume k in dom <%(D . o)%> ; ::_thesis: d9 . k = <%(D . o)%> . k then k in 1 by AFINSQ_1:33; then k < 1 by NAT_1:44; then A204: k = 0 by NAT_1:14; oo > 0 by A78, XREAL_1:50; then k in dom d9 by A202, A204, NAT_1:44; hence d9 . k = D . (k + o) by A202 .= <%(D . o)%> . k by A204, AFINSQ_1:def_4 ; ::_thesis: verum end; defpred S2[ Nat, set ] means $2 = D . ($1 + o1); A205: for u being Nat st u in oo1 holds ex x being Element of NAT st S2[u,x] ; consider d91 being XFinSequence of NAT such that A206: ( dom d91 = oo1 & ( for x being Nat st x in oo1 holds S2[x,d91 . x] ) ) from STIRL2_1:sch_5(A205); reconsider do = D | o as XFinSequence of NAT ; A207: len d = len D by A40; then A208: len do = o by A78, AFINSQ_1:11; then A209: dom D = (len do) + (len d9) by A40, A202; now__::_thesis:_for_k_being_Nat_st_k_in_dom_d9_holds_ b_|^_o_divides_d9_._k let k be Nat; ::_thesis: ( k in dom d9 implies b |^ o divides d9 . k ) reconsider K = k as Element of NAT by ORDINAL1:def_12; assume A210: k in dom d9 ; ::_thesis: b |^ o divides d9 . k then k < len d9 by NAT_1:44; then o + k < dom D by A208, A209, XREAL_1:8; then o + k in dom D by NAT_1:44; then D . (o + k) = (d . (o + k)) * (b |^ (o + k)) by A41; then d9 . K = (d . (o + k)) * (b |^ (o + k)) by A202, A210 .= (d . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8 .= ((d . (o + k)) * (b |^ k)) * (b |^ o) ; hence b |^ o divides d9 . k by NAT_D:def_3; ::_thesis: verum end; then A211: b |^ o divides Sum d9 by Th2; ( ( for x being Nat st x in dom do holds D . x = do . x ) & ( for x being Nat st x in dom d9 holds D . ((len do) + x) = d9 . x ) ) by A202, A208, FUNCT_1:47; then D = do ^ d9 by A209, AFINSQ_1:def_3; then A212: n = (Sum do) + (Sum d9) by A42, AFINSQ_2:55; consider ok being Nat such that A213: ok + 1 = o by A187, NAT_1:6; reconsider ok = ok as Element of NAT by ORDINAL1:def_12; reconsider g = (b1 (#) (b GeoSeq)) | (ok + 1) as XFinSequence of NAT by Th1; A214: 1 - b <> 0 by A1; A215: Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok by AFINSQ_2:56 .= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok by SERIES_1:9 .= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok) by SEQ_1:9 .= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by A1, SERIES_1:22 .= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A213 .= - (1 - (b |^ o)) by A214, XCMPLX_1:87 .= (b |^ o) - 1 ; dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1; then A216: o c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2; then A217: dom g = o by A213, RELAT_1:62; A218: for i being Nat st i in dom do holds do . i <= g . i proof let i be Nat; ::_thesis: ( i in dom do implies do . i <= g . i ) reconsider I = i as Element of NAT by ORDINAL1:def_12; assume A219: i in dom do ; ::_thesis: do . i <= g . i then i in o by A78, A207, AFINSQ_1:11; then A220: g . I = ((b - 1) (#) (b GeoSeq)) . I by A217, FUNCT_1:47 .= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9 .= b1 * (b |^ I) by PREPOWER:def_1 ; A221: dom do c= dom D by RELAT_1:60; then d . i < b1 + 1 by A39, A40, A219; then A222: d . i <= b1 by NAT_1:13; do . i = D . i by A219, FUNCT_1:47 .= (d . i) * (b |^ i) by A41, A219, A221 ; hence do . i <= g . i by A220, A222, XREAL_1:64; ::_thesis: verum end; A223: now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_ d9_._((len_<%(D_._o)%>)_+_k)_=_d91_._k let k be Nat; ::_thesis: ( k in dom d91 implies d9 . ((len <%(D . o)%>) + k) = d91 . k ) assume A224: k in dom d91 ; ::_thesis: d9 . ((len <%(D . o)%>) + k) = d91 . k then k < oo1 by A206, NAT_1:44; then k + 1 < oo1 + 1 by XREAL_1:8; then A225: k + 1 in dom d9 by A202, NAT_1:44; thus d9 . ((len <%(D . o)%>) + k) = d9 . (1 + k) by AFINSQ_1:33 .= D . ((len do) + (k + 1)) by A202, A208, A225 .= D . ((len do1) + k) by A208, A192 .= d91 . k by A206, A192, A224 ; ::_thesis: verum end; dom d9 = 1 + (dom d91) by A202, A206 .= (len <%(D . o)%>) + (len d91) by AFINSQ_1:34 ; then d9 = <%(D . o)%> ^ d91 by A203, A223, AFINSQ_1:def_3; then A226: Sum d9 = (Sum <%(D . o)%>) + (Sum d91) by AFINSQ_2:55; defpred S3[ Nat, set ] means $2 = E . ($1 + o); A227: 1 - b <> 0 by A1; consider ok being Nat such that A228: ok + 1 = o by A187, NAT_1:6; A229: dom D = (len do1) + (len d91) by A40, A206, A192; now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_ b_|^_o1_divides_d91_._k let k be Nat; ::_thesis: ( k in dom d91 implies b |^ o1 divides d91 . k ) reconsider K = k as Element of NAT by ORDINAL1:def_12; assume A230: k in dom d91 ; ::_thesis: b |^ o1 divides d91 . k then k < len d91 by NAT_1:44; then o1 + k < dom D by A192, A229, XREAL_1:8; then o1 + k in dom D by NAT_1:44; then D . (o1 + k) = (d . (o1 + k)) * (b |^ (o1 + k)) by A41; then d91 . K = (d . (o1 + k)) * (b |^ (o1 + k)) by A206, A230 .= (d . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8 .= ((d . (o1 + k)) * (b |^ k)) * (b |^ o1) ; hence b |^ o1 divides d91 . k by NAT_D:def_3; ::_thesis: verum end; then A231: b |^ o1 divides Sum d91 by Th2; len do = len g by A208, A213, A216, RELAT_1:62; then Sum do < ((b |^ o) - 1) + 1 by A215, A218, AFINSQ_2:57, XREAL_1:145; then A232: (Sum do) div (b |^ o) = 0 by NAT_D:27; A233: 1 - b <> 0 by A1; Sum g1 = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok1 by AFINSQ_2:56 .= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok1 by SERIES_1:9 .= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok1) by SEQ_1:9 .= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by A1, SERIES_1:22 .= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A190 .= - (1 - (b |^ o1)) by A233, XCMPLX_1:87 .= (b |^ o1) - 1 ; then Sum do1 < ((b |^ o1) - 1) + 1 by A194, A196, AFINSQ_2:57, XREAL_1:145; then A234: (Sum do1) div (b |^ o1) = 0 by NAT_D:27; ( ( for x being Nat st x in dom do1 holds D . x = do1 . x ) & ( for x being Nat st x in dom d91 holds D . ((len do1) + x) = d91 . x ) ) by A206, A192, FUNCT_1:47; then D = do1 ^ d91 by A229, AFINSQ_1:def_3; then A235: n = (Sum do1) + (Sum d91) by A42, AFINSQ_2:55; bo1 <> 0 by A1, PREPOWER:5; then (Sum d91) mod (b |^ o1) = 0 by A231, PEPIN:6; then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A235, NAT_D:19; then A236: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A234, A231, NAT_D:3; A237: bo <> 0 by A1, PREPOWER:5; then (Sum d9) mod (b |^ o) = 0 by A211, PEPIN:6; then n div (b |^ o) = ((Sum d9) div (b |^ o)) + ((Sum do) div (b |^ o)) by A212, NAT_D:19; then ( (n div (b |^ o)) * (b |^ o) = Sum d9 & Sum <%(D . o)%> = D . o ) by A232, A211, AFINSQ_2:53, NAT_D:3; then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A40, A41, A76, A236, A226; then (d . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1))) by NEWTON:8; then (d . o) * (b |^ o) = (b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))) ; then ((b |^ o) * (d . o)) / (b |^ o) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by NEWTON:5; then A238: d . o = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by A237, XCMPLX_1:89; reconsider o1 = o + 1 as Element of NAT ; A239: o1 <= k by A187, NAT_1:13; then A240: o1 < len d by XREAL_1:147; reconsider ok = ok as Element of NAT by ORDINAL1:def_12; reconsider g = (b1 (#) (b GeoSeq)) | (ok + 1) as XFinSequence of NAT by Th1; A241: 1 - b <> 0 by A1; reconsider bo1 = b |^ o1 as Element of NAT by ORDINAL1:def_12; reconsider do1 = E | o1 as XFinSequence of NAT ; reconsider bo = b |^ o as Element of NAT by ORDINAL1:def_12; consider ok1 being Nat such that A242: ok1 + 1 = o1 ; reconsider ok1 = ok1 as Element of NAT by ORDINAL1:def_12; reconsider g1 = (b1 (#) (b GeoSeq)) | (ok1 + 1) as XFinSequence of NAT by Th1; A243: len e = len E by A59; then A244: len do1 = o1 by A75, A240, AFINSQ_1:11; dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1; then A245: o1 c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2; then A246: len do1 = len g1 by A244, A242, RELAT_1:62; A247: dom g1 = o1 by A242, A245, RELAT_1:62; A248: for i being Nat st i in dom do1 holds do1 . i <= g1 . i proof let i be Nat; ::_thesis: ( i in dom do1 implies do1 . i <= g1 . i ) reconsider I = i as Element of NAT by ORDINAL1:def_12; assume A249: i in dom do1 ; ::_thesis: do1 . i <= g1 . i then i in o1 by A75, A240, A243, AFINSQ_1:11; then A250: g1 . I = ((b - 1) (#) (b GeoSeq)) . I by A247, FUNCT_1:47 .= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9 .= b1 * (b |^ I) by PREPOWER:def_1 ; A251: dom do1 c= dom E by RELAT_1:60; then e . i < b1 + 1 by A58, A59, A249; then A252: e . i <= b1 by NAT_1:13; do1 . i = E . i by A249, FUNCT_1:47 .= (e . i) * (b |^ i) by A60, A249, A251 ; hence do1 . i <= g1 . i by A250, A252, XREAL_1:64; ::_thesis: verum end; Sum g1 = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok1 by AFINSQ_2:56 .= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok1 by SERIES_1:9 .= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok1) by SEQ_1:9 .= (b - 1) * ((1 - (b to_power (ok1 + 1))) / (1 - b)) by A1, SERIES_1:22 .= - ((1 - b) * ((1 - (b |^ o1)) / (1 - b))) by A242 .= - (1 - (b |^ o1)) by A241, XCMPLX_1:87 .= (b |^ o1) - 1 ; then Sum do1 < ((b |^ o1) - 1) + 1 by A246, A248, AFINSQ_2:57, XREAL_1:145; then A253: (Sum do1) div (b |^ o1) = 0 by NAT_D:27; k < len d by XREAL_1:147; then reconsider oo1 = (len d) - o1 as Element of NAT by A239, NAT_1:21, XXREAL_0:2; A254: for u being Nat st u in oo holds ex x being Element of NAT st S3[u,x] ; consider d9 being XFinSequence of NAT such that A255: ( dom d9 = oo & ( for x being Nat st x in oo holds S3[x,d9 . x] ) ) from STIRL2_1:sch_5(A254); A256: now__::_thesis:_for_k_being_Nat_st_k_in_dom_<%(E_._o)%>_holds_ d9_._k_=_<%(E_._o)%>_._k let k be Nat; ::_thesis: ( k in dom <%(E . o)%> implies d9 . k = <%(E . o)%> . k ) assume k in dom <%(E . o)%> ; ::_thesis: d9 . k = <%(E . o)%> . k then k in 1 by AFINSQ_1:33; then k < 1 by NAT_1:44; then A257: k = 0 by NAT_1:14; oo > 0 by A78, XREAL_1:50; then k in dom d9 by A255, A257, NAT_1:44; hence d9 . k = E . (k + o) by A255 .= <%(E . o)%> . k by A257, AFINSQ_1:def_4 ; ::_thesis: verum end; defpred S4[ Nat, set ] means $2 = E . ($1 + o1); A258: for u being Nat st u in oo1 holds ex x being Element of NAT st S4[u,x] ; consider d91 being XFinSequence of NAT such that A259: ( dom d91 = oo1 & ( for x being Nat st x in oo1 holds S4[x,d91 . x] ) ) from STIRL2_1:sch_5(A258); A260: dom E = (len do1) + (len d91) by A59, A75, A259, A244; now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_ b_|^_o1_divides_d91_._k let k be Nat; ::_thesis: ( k in dom d91 implies b |^ o1 divides d91 . k ) reconsider K = k as Element of NAT by ORDINAL1:def_12; assume A261: k in dom d91 ; ::_thesis: b |^ o1 divides d91 . k then k < len d91 by NAT_1:44; then o1 + k < dom E by A244, A260, XREAL_1:8; then o1 + k in dom E by NAT_1:44; then E . (o1 + k) = (e . (o1 + k)) * (b |^ (o1 + k)) by A60; then d91 . K = (e . (o1 + k)) * (b |^ (o1 + k)) by A259, A261 .= (e . (o1 + k)) * ((b |^ o1) * (b |^ k)) by NEWTON:8 .= ((e . (o1 + k)) * (b |^ k)) * (b |^ o1) ; hence b |^ o1 divides d91 . k by NAT_D:def_3; ::_thesis: verum end; then A262: b |^ o1 divides Sum d91 by Th2; ( ( for x being Nat st x in dom do1 holds E . x = do1 . x ) & ( for x being Nat st x in dom d91 holds E . ((len do1) + x) = d91 . x ) ) by A259, A244, FUNCT_1:47; then E = do1 ^ d91 by A260, AFINSQ_1:def_3; then A263: n = (Sum do1) + (Sum d91) by A61, AFINSQ_2:55; bo1 <> 0 by A1, PREPOWER:5; then (Sum d91) mod (b |^ o1) = 0 by A262, PEPIN:6; then n div (b |^ o1) = ((Sum d91) div (b |^ o1)) + ((Sum do1) div (b |^ o1)) by A263, NAT_D:19; then A264: (n div (b |^ o1)) * (b |^ o1) = Sum d91 by A253, A262, NAT_D:3; reconsider do = E | o as XFinSequence of NAT ; A265: len e = len E by A59; then A266: len do = o by A75, A78, AFINSQ_1:11; then A267: dom E = (len do) + (len d9) by A59, A75, A255; now__::_thesis:_for_k_being_Nat_st_k_in_dom_d9_holds_ b_|^_o_divides_d9_._k let k be Nat; ::_thesis: ( k in dom d9 implies b |^ o divides d9 . k ) reconsider K = k as Element of NAT by ORDINAL1:def_12; assume A268: k in dom d9 ; ::_thesis: b |^ o divides d9 . k then k < len d9 by NAT_1:44; then o + k < dom E by A266, A267, XREAL_1:8; then o + k in dom E by NAT_1:44; then E . (o + k) = (e . (o + k)) * (b |^ (o + k)) by A60; then d9 . K = (e . (o + k)) * (b |^ (o + k)) by A255, A268 .= (e . (o + k)) * ((b |^ o) * (b |^ k)) by NEWTON:8 .= ((e . (o + k)) * (b |^ k)) * (b |^ o) ; hence b |^ o divides d9 . k by NAT_D:def_3; ::_thesis: verum end; then A269: b |^ o divides Sum d9 by Th2; dom ((b - 1) (#) (b GeoSeq)) = NAT by FUNCT_2:def_1; then A270: o c= dom ((b - 1) (#) (b GeoSeq)) by ORDINAL1:def_2; then A271: len do = len g by A266, A228, RELAT_1:62; A272: dom g = o by A228, A270, RELAT_1:62; A273: for i being Nat st i in dom do holds do . i <= g . i proof let i be Nat; ::_thesis: ( i in dom do implies do . i <= g . i ) reconsider I = i as Element of NAT by ORDINAL1:def_12; assume A274: i in dom do ; ::_thesis: do . i <= g . i then i in o by A75, A78, A265, AFINSQ_1:11; then A275: g . I = ((b - 1) (#) (b GeoSeq)) . I by A272, FUNCT_1:47 .= (b - 1) * ((b GeoSeq) . I) by SEQ_1:9 .= b1 * (b |^ I) by PREPOWER:def_1 ; A276: dom do c= dom E by RELAT_1:60; then e . i < b1 + 1 by A58, A59, A274; then A277: e . i <= b1 by NAT_1:13; do . i = E . i by A274, FUNCT_1:47 .= (e . i) * (b |^ i) by A60, A274, A276 ; hence do . i <= g . i by A275, A277, XREAL_1:64; ::_thesis: verum end; Sum g = (Partial_Sums ((b - 1) (#) (b GeoSeq))) . ok by AFINSQ_2:56 .= ((b - 1) (#) (Partial_Sums (b GeoSeq))) . ok by SERIES_1:9 .= (b - 1) * ((Partial_Sums (b GeoSeq)) . ok) by SEQ_1:9 .= (b - 1) * ((1 - (b to_power (ok + 1))) / (1 - b)) by A1, SERIES_1:22 .= - ((1 - b) * ((1 - (b |^ o)) / (1 - b))) by A228 .= - (1 - (b |^ o)) by A227, XCMPLX_1:87 .= (b |^ o) - 1 ; then Sum do < ((b |^ o) - 1) + 1 by A271, A273, AFINSQ_2:57, XREAL_1:145; then A278: (Sum do) div (b |^ o) = 0 by NAT_D:27; A279: now__::_thesis:_for_k_being_Nat_st_k_in_dom_d91_holds_ d9_._((len_<%(E_._o)%>)_+_k)_=_d91_._k let k be Nat; ::_thesis: ( k in dom d91 implies d9 . ((len <%(E . o)%>) + k) = d91 . k ) assume A280: k in dom d91 ; ::_thesis: d9 . ((len <%(E . o)%>) + k) = d91 . k then k < oo1 by A259, NAT_1:44; then k + 1 < oo1 + 1 by XREAL_1:8; then A281: k + 1 in oo by NAT_1:44; thus d9 . ((len <%(E . o)%>) + k) = d9 . (1 + k) by AFINSQ_1:33 .= E . ((len do) + (k + 1)) by A255, A266, A281 .= E . ((len do1) + k) by A266, A244 .= d91 . k by A259, A244, A280 ; ::_thesis: verum end; dom d9 = 1 + (dom d91) by A255, A259 .= (len <%(E . o)%>) + (len d91) by AFINSQ_1:34 ; then d9 = <%(E . o)%> ^ d91 by A256, A279, AFINSQ_1:def_3; then A282: Sum d9 = (Sum <%(E . o)%>) + (Sum d91) by AFINSQ_2:55; ( ( for x being Nat st x in dom do holds E . x = do . x ) & ( for x being Nat st x in dom d9 holds E . ((len do) + x) = d9 . x ) ) by A255, A266, FUNCT_1:47; then E = do ^ d9 by A267, AFINSQ_1:def_3; then A283: n = (Sum do) + (Sum d9) by A61, AFINSQ_2:55; A284: bo <> 0 by A1, PREPOWER:5; then (Sum d9) mod (b |^ o) = 0 by A269, PEPIN:6; then n div (b |^ o) = ((Sum d9) div (b |^ o)) + ((Sum do) div (b |^ o)) by A283, NAT_D:19; then (n div (b |^ o)) * (b |^ o) = Sum d9 by A278, A269, NAT_D:3; then E . o = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A264, A282, AFINSQ_2:53; then (e . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * (b |^ o1)) by A59, A60, A75, A76; then (e . o) * (b |^ o) = ((n div (b |^ o)) * (b |^ o)) - ((n div (b |^ o1)) * ((b |^ o) * (b |^ 1))) by NEWTON:8; then (e . o) * (b |^ o) = (b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * (b |^ 1))) ; then ((b |^ o) * (e . o)) / (b |^ o) = ((b |^ o) * ((n div (b |^ o)) - ((n div (b |^ o1)) * b))) / (b |^ o) by NEWTON:5; hence d . a = e . a by A238, A284, XCMPLX_1:89; ::_thesis: verum end; end; end; hence d = e by A75, FUNCT_1:2; ::_thesis: verum end; assume that n = 0 and A285: ( d = <%0%> & e = <%0%> ) ; ::_thesis: d = e thus d = e by A285; ::_thesis: verum end; end; :: deftheorem Def2 defines digits NUMERAL1:def_2_:_ for n, b being Nat st b > 1 holds for b3 being XFinSequence of NAT holds ( ( n <> 0 implies ( b3 = digits (n,b) iff ( value (b3,b) = n & b3 . ((len b3) - 1) <> 0 & ( for i being Nat st i in dom b3 holds ( 0 <= b3 . i & b3 . i < b ) ) ) ) ) & ( not n <> 0 implies ( b3 = digits (n,b) iff b3 = <%0%> ) ) ); theorem Th4: :: NUMERAL1:4 for n, b being Nat st b > 1 holds len (digits (n,b)) >= 1 proof let n, b be Nat; ::_thesis: ( b > 1 implies len (digits (n,b)) >= 1 ) assume A1: b > 1 ; ::_thesis: len (digits (n,b)) >= 1 percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: len (digits (n,b)) >= 1 then digits (n,b) = <%0%> by A1, Def2; hence len (digits (n,b)) >= 1 by AFINSQ_1:33; ::_thesis: verum end; suppose n <> 0 ; ::_thesis: len (digits (n,b)) >= 1 then (digits (n,b)) . ((len (digits (n,b))) - 1) <> 0 by A1, Def2; then (len (digits (n,b))) - 1 in dom (digits (n,b)) by FUNCT_1:def_2; hence len (digits (n,b)) >= 1 by NAT_1:14; ::_thesis: verum end; end; end; theorem Th5: :: NUMERAL1:5 for n, b being Nat st b > 1 holds value ((digits (n,b)),b) = n proof let n, b be Nat; ::_thesis: ( b > 1 implies value ((digits (n,b)),b) = n ) assume A1: b > 1 ; ::_thesis: value ((digits (n,b)),b) = n percases ( n <> 0 or n = 0 ) ; suppose n <> 0 ; ::_thesis: value ((digits (n,b)),b) = n hence value ((digits (n,b)),b) = n by A1, Def2; ::_thesis: verum end; supposeA2: n = 0 ; ::_thesis: value ((digits (n,b)),b) = n then A3: digits (n,b) = <%0%> by A1, Def2; now__::_thesis:_for_i_being_Nat_st_i_in_dom_<%0%>_holds_ <%0%>_._i_=_((digits_(n,b))_._i)_*_(b_|^_i) let i be Nat; ::_thesis: ( i in dom <%0%> implies <%0%> . i = ((digits (n,b)) . i) * (b |^ i) ) assume i in dom <%0%> ; ::_thesis: <%0%> . i = ((digits (n,b)) . i) * (b |^ i) then i in {0} by AFINSQ_1:def_4, CARD_1:49; then A4: i = 0 by TARSKI:def_1; hence <%0%> . i = 0 * (b |^ i) by AFINSQ_1:def_4 .= ((digits (n,b)) . i) * (b |^ i) by A3, A4, AFINSQ_1:def_4 ; ::_thesis: verum end; then value ((digits (n,b)),b) = Sum <%0%> by A3, Def1; hence value ((digits (n,b)),b) = n by A2, AFINSQ_2:53; ::_thesis: verum end; end; end; begin theorem Th6: :: NUMERAL1:6 for n, k being Nat st k = (10 |^ n) - 1 holds 9 divides k proof defpred S1[ Nat] means ex k being Nat st ( k = (10 |^ $1) - 1 & 9 divides k ); let n, k be Nat; ::_thesis: ( k = (10 |^ n) - 1 implies 9 divides k ) A1: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then consider l being Nat such that A2: l = (10 |^ k) - 1 and A3: 9 divides l ; consider m being Nat such that A4: l = 9 * m by A3, NAT_D:def_3; A5: 9 divides 9 * ((m * 10) + 1) by NAT_D:def_3; (10 |^ (k + 1)) - 1 = (((9 * m) + 1) * 10) - 1 by A2, A4, NEWTON:6 .= 9 * ((m * 10) + 1) ; hence S1[k + 1] by A5; ::_thesis: verum end; (10 |^ 0) - 1 = 1 - 1 by NEWTON:4 .= 0 ; then A6: S1[ 0 ] by NAT_D:6; for k being Nat holds S1[k] from NAT_1:sch_2(A6, A1); then A7: ex l being Nat st ( l = (10 |^ n) - 1 & 9 divides l ) ; assume k = (10 |^ n) - 1 ; ::_thesis: 9 divides k hence 9 divides k by A7; ::_thesis: verum end; theorem :: NUMERAL1:7 for n, b being Nat st b > 1 holds ( b divides n iff (digits (n,b)) . 0 = 0 ) proof let n, b be Nat; ::_thesis: ( b > 1 implies ( b divides n iff (digits (n,b)) . 0 = 0 ) ) reconsider B = b as Element of NAT by ORDINAL1:def_12; consider d being XFinSequence of NAT such that dom d = dom (digits (n,b)) and A1: for i being Nat st i in dom d holds d . i = ((digits (n,b)) . i) * (b |^ i) and A2: value ((digits (n,b)),b) = Sum d by Def1; assume A3: b > 1 ; ::_thesis: ( b divides n iff (digits (n,b)) . 0 = 0 ) thus ( b divides n implies (digits (n,b)) . 0 = 0 ) ::_thesis: ( (digits (n,b)) . 0 = 0 implies b divides n ) proof A4: len (digits (n,b)) >= 1 by A3, Th4; assume A5: b divides n ; ::_thesis: (digits (n,b)) . 0 = 0 consider d being XFinSequence of NAT such that A6: dom d = dom (digits (n,b)) and A7: for i being Nat st i in dom d holds d . i = ((digits (n,b)) . i) * (b |^ i) and A8: value ((digits (n,b)),b) = Sum d by Def1; percases ( len (digits (n,b)) = 1 or len (digits (n,b)) > 1 ) by A4, XXREAL_0:1; supposeA9: len (digits (n,b)) = 1 ; ::_thesis: (digits (n,b)) . 0 = 0 A10: b divides Sum d by A3, A5, A8, Th5; A11: 0 in dom (digits (n,b)) by A9, NAT_1:44; len d = 1 by A6, A9; then d = <%(d . 0)%> by AFINSQ_1:34; then Sum d = d . 0 by AFINSQ_2:53 .= ((digits (n,b)) . 0) * (b |^ 0) by A6, A7, A11 ; then A12: b divides ((digits (n,b)) . 0) * 1 by A10, NEWTON:4; percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: (digits (n,b)) . 0 = 0 then digits (n,b) = <%0%> by A3, Def2; hence (digits (n,b)) . 0 = 0 by AFINSQ_1:34; ::_thesis: verum end; suppose n <> 0 ; ::_thesis: (digits (n,b)) . 0 = 0 then (digits (n,b)) . 0 < b by A3, A11, Def2; hence (digits (n,b)) . 0 = 0 by A12, NAT_D:7; ::_thesis: verum end; end; end; supposeA13: len (digits (n,b)) > 1 ; ::_thesis: (digits (n,b)) . 0 = 0 then reconsider k = (len (digits (n,b))) - 1 as Element of NAT by NAT_1:21; defpred S1[ Nat, set ] means $2 = d . ($1 + 1); A14: now__::_thesis:_for_l_being_Nat_st_l_in_dom_<%(d_._0)%>_holds_ d_._l_=_<%(d_._0)%>_._l let l be Nat; ::_thesis: ( l in dom <%(d . 0)%> implies d . l = <%(d . 0)%> . l ) assume l in dom <%(d . 0)%> ; ::_thesis: d . l = <%(d . 0)%> . l then l in 1 by AFINSQ_1:def_4; then l < 1 by NAT_1:44; then l = 0 by NAT_1:14; hence d . l = <%(d . 0)%> . l by AFINSQ_1:34; ::_thesis: verum end; A15: for u being Nat st u in k holds ex x being Element of NAT st S1[u,x] ; consider d9 being XFinSequence of NAT such that A16: ( dom d9 = k & ( for x being Nat st x in k holds S1[x,d9 . x] ) ) from STIRL2_1:sch_5(A15); now__::_thesis:_for_i_being_Nat_st_i_in_dom_d9_holds_ b_divides_d9_._i let i be Nat; ::_thesis: ( i in dom d9 implies b divides d9 . i ) assume A17: i in dom d9 ; ::_thesis: b divides d9 . i then i < k by A16, NAT_1:44; then i + 1 < k + 1 by XREAL_1:8; then A18: i + 1 in dom d by A6, NAT_1:44; d9 . i = d . (i + 1) by A16, A17 .= ((digits (n,b)) . (i + 1)) * (b |^ (i + 1)) by A7, A18 .= ((digits (n,b)) . (i + 1)) * ((b |^ i) * b) by NEWTON:6 .= b * (((digits (n,b)) . (i + 1)) * (b |^ i)) ; hence b divides d9 . i by NAT_D:def_3; ::_thesis: verum end; then b divides Sum d9 by Th2; then A19: (Sum d9) mod B = 0 by A3, PEPIN:6; A20: now__::_thesis:_for_l_being_Nat_st_l_in_dom_d9_holds_ d_._((len_<%(d_._0)%>)_+_l)_=_d9_._l let l be Nat; ::_thesis: ( l in dom d9 implies d . ((len <%(d . 0)%>) + l) = d9 . l ) A21: (len <%(d . 0)%>) + l = l + 1 by AFINSQ_1:34; assume l in dom d9 ; ::_thesis: d . ((len <%(d . 0)%>) + l) = d9 . l hence d . ((len <%(d . 0)%>) + l) = d9 . l by A16, A21; ::_thesis: verum end; A22: 0 in dom (digits (n,b)) by A13, NAT_1:44; dom d = k + 1 by A6 .= (len <%(d . 0)%>) + (len d9) by A16, AFINSQ_1:33 ; then d = <%(d . 0)%> ^ d9 by A14, A20, AFINSQ_1:def_3; then Sum d = (Sum <%(d . 0)%>) + (Sum d9) by AFINSQ_2:55; then n = (Sum <%(d . 0)%>) + (Sum d9) by A3, A8, Th5; then n = (d . 0) + (Sum d9) by AFINSQ_2:53; then ((d . 0) + (Sum d9)) mod B = 0 by A3, A5, PEPIN:6; then (d . 0) mod b = 0 by A19, NAT_D:17; then B divides d . 0 by A3, PEPIN:6; then b divides ((digits (n,b)) . 0) * (b |^ 0) by A6, A7, A22; then A23: b divides ((digits (n,b)) . 0) * 1 by NEWTON:4; percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: (digits (n,b)) . 0 = 0 then digits (n,b) = <%0%> by A3, Def2; hence (digits (n,b)) . 0 = 0 by AFINSQ_1:34; ::_thesis: verum end; suppose n <> 0 ; ::_thesis: (digits (n,b)) . 0 = 0 then (digits (n,b)) . 0 < b by A3, A22, Def2; hence (digits (n,b)) . 0 = 0 by A23, NAT_D:7; ::_thesis: verum end; end; end; end; end; assume A24: (digits (n,b)) . 0 = 0 ; ::_thesis: b divides n now__::_thesis:_for_i_being_Nat_st_i_in_dom_d_holds_ b_divides_d_._i let i be Nat; ::_thesis: ( i in dom d implies b divides d . b1 ) assume A25: i in dom d ; ::_thesis: b divides d . b1 percases ( i = 0 or i > 0 ) ; suppose i = 0 ; ::_thesis: b divides d . b1 then d . i = ((digits (n,b)) . 0) * (b |^ 0) by A1, A25 .= ((digits (n,b)) . 0) * 1 by NEWTON:4 ; hence b divides d . i by A24, NAT_D:6; ::_thesis: verum end; suppose i > 0 ; ::_thesis: b divides d . b1 then consider j being Nat such that A26: j + 1 = i by NAT_1:6; d . i = ((digits (n,b)) . i) * (b |^ (j + 1)) by A1, A25, A26 .= ((digits (n,b)) . i) * ((b |^ j) * b) by NEWTON:6 .= b * (((digits (n,b)) . i) * (b |^ j)) ; hence b divides d . i by NAT_D:def_3; ::_thesis: verum end; end; end; then b divides value ((digits (n,b)),b) by A2, Th2; hence b divides n by A3, Th5; ::_thesis: verum end; theorem :: NUMERAL1:8 for n being Nat holds ( 2 divides n iff 2 divides (digits (n,10)) . 0 ) proof let n be Nat; ::_thesis: ( 2 divides n iff 2 divides (digits (n,10)) . 0 ) consider d being XFinSequence of NAT such that dom d = dom (digits (n,10)) and A1: for i being Nat st i in dom d holds d . i = ((digits (n,10)) . i) * (10 |^ i) and A2: value ((digits (n,10)),10) = Sum d by Def1; thus ( 2 divides n implies 2 divides (digits (n,10)) . 0 ) ::_thesis: ( 2 divides (digits (n,10)) . 0 implies 2 divides n ) proof A3: len (digits (n,10)) >= 1 by Th4; assume A4: 2 divides n ; ::_thesis: 2 divides (digits (n,10)) . 0 consider d being XFinSequence of NAT such that A5: dom d = dom (digits (n,10)) and A6: for i being Nat st i in dom d holds d . i = ((digits (n,10)) . i) * (10 |^ i) and A7: value ((digits (n,10)),10) = Sum d by Def1; percases ( len (digits (n,10)) = 1 or len (digits (n,10)) > 1 ) by A3, XXREAL_0:1; supposeA8: len (digits (n,10)) = 1 ; ::_thesis: 2 divides (digits (n,10)) . 0 then A9: 0 in dom (digits (n,10)) by NAT_1:44; A10: 2 divides Sum d by A4, A7, Th5; len d = 1 by A5, A8; then d = <%(d . 0)%> by AFINSQ_1:34; then Sum d = d . 0 by AFINSQ_2:53 .= ((digits (n,10)) . 0) * (10 |^ 0) by A5, A6, A9 ; then 2 divides ((digits (n,10)) . 0) * 1 by A10, NEWTON:4; hence 2 divides (digits (n,10)) . 0 ; ::_thesis: verum end; supposeA11: len (digits (n,10)) > 1 ; ::_thesis: 2 divides (digits (n,10)) . 0 then reconsider k = (len (digits (n,10))) - 1 as Element of NAT by NAT_1:21; defpred S1[ Nat, set ] means $2 = d . ($1 + 1); A12: now__::_thesis:_for_l_being_Nat_st_l_in_dom_<%(d_._0)%>_holds_ d_._l_=_<%(d_._0)%>_._l let l be Nat; ::_thesis: ( l in dom <%(d . 0)%> implies d . l = <%(d . 0)%> . l ) assume l in dom <%(d . 0)%> ; ::_thesis: d . l = <%(d . 0)%> . l then l in 1 by AFINSQ_1:def_4; then l < 1 by NAT_1:44; then l = 0 by NAT_1:14; hence d . l = <%(d . 0)%> . l by AFINSQ_1:34; ::_thesis: verum end; A13: for u being Nat st u in k holds ex x being Element of NAT st S1[u,x] ; consider d9 being XFinSequence of NAT such that A14: ( dom d9 = k & ( for x being Nat st x in k holds S1[x,d9 . x] ) ) from STIRL2_1:sch_5(A13); now__::_thesis:_for_i_being_Nat_st_i_in_dom_d9_holds_ 2_divides_d9_._i let i be Nat; ::_thesis: ( i in dom d9 implies 2 divides d9 . i ) assume A15: i in dom d9 ; ::_thesis: 2 divides d9 . i then i < k by A14, NAT_1:44; then i + 1 < k + 1 by XREAL_1:8; then A16: i + 1 in dom d by A5, NAT_1:44; d9 . i = d . (i + 1) by A14, A15 .= ((digits (n,10)) . (i + 1)) * (10 |^ (i + 1)) by A6, A16 .= ((digits (n,10)) . (i + 1)) * ((10 |^ i) * 10) by NEWTON:6 .= 2 * ((((digits (n,10)) . (i + 1)) * (10 |^ i)) * 5) ; hence 2 divides d9 . i by NAT_D:def_3; ::_thesis: verum end; then 2 divides Sum d9 by Th2; then A17: (Sum d9) mod 2 = 0 by PEPIN:6; A18: now__::_thesis:_for_l_being_Nat_st_l_in_dom_d9_holds_ d_._((len_<%(d_._0)%>)_+_l)_=_d9_._l let l be Nat; ::_thesis: ( l in dom d9 implies d . ((len <%(d . 0)%>) + l) = d9 . l ) A19: (len <%(d . 0)%>) + l = l + 1 by AFINSQ_1:34; assume l in dom d9 ; ::_thesis: d . ((len <%(d . 0)%>) + l) = d9 . l hence d . ((len <%(d . 0)%>) + l) = d9 . l by A14, A19; ::_thesis: verum end; dom d = k + 1 by A5 .= (len <%(d . 0)%>) + (len d9) by A14, AFINSQ_1:33 ; then d = <%(d . 0)%> ^ d9 by A12, A18, AFINSQ_1:def_3; then Sum d = (Sum <%(d . 0)%>) + (Sum d9) by AFINSQ_2:55; then n = (Sum <%(d . 0)%>) + (Sum d9) by A7, Th5; then n = (d . 0) + (Sum d9) by AFINSQ_2:53; then ((d . 0) + (Sum d9)) mod 2 = 0 by A4, PEPIN:6; then (d . 0) mod 2 = 0 by A17, NAT_D:17; then A20: 2 divides d . 0 by PEPIN:6; 0 in dom (digits (n,10)) by A11, NAT_1:44; then 2 divides ((digits (n,10)) . 0) * (10 |^ 0) by A5, A6, A20; then 2 divides ((digits (n,10)) . 0) * 1 by NEWTON:4; hence 2 divides (digits (n,10)) . 0 ; ::_thesis: verum end; end; end; assume A21: 2 divides (digits (n,10)) . 0 ; ::_thesis: 2 divides n now__::_thesis:_for_i_being_Nat_st_i_in_dom_d_holds_ 2_divides_d_._i let i be Nat; ::_thesis: ( i in dom d implies 2 divides d . b1 ) assume A22: i in dom d ; ::_thesis: 2 divides d . b1 percases ( i = 0 or i > 0 ) ; suppose i = 0 ; ::_thesis: 2 divides d . b1 then d . i = ((digits (n,10)) . 0) * (10 |^ 0) by A1, A22 .= ((digits (n,10)) . 0) * 1 by NEWTON:4 ; hence 2 divides d . i by A21; ::_thesis: verum end; suppose i > 0 ; ::_thesis: 2 divides d . b1 then consider j being Nat such that A23: j + 1 = i by NAT_1:6; d . i = ((digits (n,10)) . i) * (10 |^ (j + 1)) by A1, A22, A23 .= ((digits (n,10)) . i) * ((10 |^ j) * 10) by NEWTON:6 .= 2 * ((((digits (n,10)) . i) * (10 |^ j)) * 5) ; hence 2 divides d . i by NAT_D:def_3; ::_thesis: verum end; end; end; then 2 divides value ((digits (n,10)),10) by A2, Th2; hence 2 divides n by Th5; ::_thesis: verum end; theorem :: NUMERAL1:9 for n being Nat holds ( 3 divides n iff 3 divides Sum (digits (n,10)) ) proof let n be Nat; ::_thesis: ( 3 divides n iff 3 divides Sum (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 Def1; reconsider dop = dom p as Element of NAT by ORDINAL1:def_12; defpred S1[ set , set ] means $2 = (p . $1) mod 3; A4: for k being Nat st k in dop holds ex x being Element of NAT st S1[k,x] ; consider p9 being XFinSequence of NAT such that A5: ( dom p9 = dop & ( for k being Nat st k in dop holds S1[k,p9 . k] ) ) from STIRL2_1:sch_5(A4); A6: now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_ p9_._i_=_((digits_(n,10))_._i)_mod_3 let i be Nat; ::_thesis: ( i in dom p implies p9 . i = ((digits (n,10)) . i) mod 3 ) reconsider dz = (10 |^ i) - 1 as Nat by NAT_1:20, NEWTON:83; reconsider dz = dz as Element of NAT by ORDINAL1:def_12; ( 3 divides 3 * 3 & 9 divides dz ) by Th6, NAT_D:def_3; then 3 divides dz by NAT_D:4; then 3 divides ((digits (n,10)) . i) * dz by NAT_D:9; then A7: (((digits (n,10)) . i) * dz) mod 3 = 0 by PEPIN:6; assume A8: i in dom p ; ::_thesis: p9 . i = ((digits (n,10)) . i) mod 3 hence p9 . i = (p . i) mod 3 by A5 .= (((digits (n,10)) . i) * (dz + 1)) mod 3 by A2, A8 .= ((((digits (n,10)) . i) * dz) + ((digits (n,10)) . i)) mod 3 .= (0 + ((digits (n,10)) . i)) mod 3 by A7, NAT_D:22 .= ((digits (n,10)) . i) mod 3 ; ::_thesis: verum end; thus ( 3 divides n implies 3 divides Sum (digits (n,10)) ) ::_thesis: ( 3 divides Sum (digits (n,10)) implies 3 divides n ) proof assume 3 divides n ; ::_thesis: 3 divides Sum (digits (n,10)) then 3 divides Sum p by A3, Th5; then (Sum p) mod 3 = 0 by PEPIN:6; then (Sum p9) mod 3 = 0 by A5, Th3; then (Sum (digits (n,10))) mod 3 = 0 by A1, A5, A6, Th3; hence 3 divides Sum (digits (n,10)) by PEPIN:6; ::_thesis: verum end; assume 3 divides Sum (digits (n,10)) ; ::_thesis: 3 divides n then (Sum (digits (n,10))) mod 3 = 0 by PEPIN:6; then (Sum p9) mod 3 = 0 by A1, A5, A6, Th3; then (Sum p) mod 3 = 0 by A5, Th3; then 3 divides Sum p by PEPIN:6; hence 3 divides n by A3, Th5; ::_thesis: verum end; theorem :: NUMERAL1:10 for n being Nat holds ( 5 divides n iff 5 divides (digits (n,10)) . 0 ) proof let n be Nat; ::_thesis: ( 5 divides n iff 5 divides (digits (n,10)) . 0 ) consider d being XFinSequence of NAT such that dom d = dom (digits (n,10)) and A1: for i being Nat st i in dom d holds d . i = ((digits (n,10)) . i) * (10 |^ i) and A2: value ((digits (n,10)),10) = Sum d by Def1; thus ( 5 divides n implies 5 divides (digits (n,10)) . 0 ) ::_thesis: ( 5 divides (digits (n,10)) . 0 implies 5 divides n ) proof A3: len (digits (n,10)) >= 1 by Th4; assume A4: 5 divides n ; ::_thesis: 5 divides (digits (n,10)) . 0 consider d being XFinSequence of NAT such that A5: dom d = dom (digits (n,10)) and A6: for i being Nat st i in dom d holds d . i = ((digits (n,10)) . i) * (10 |^ i) and A7: value ((digits (n,10)),10) = Sum d by Def1; percases ( len (digits (n,10)) = 1 or len (digits (n,10)) > 1 ) by A3, XXREAL_0:1; supposeA8: len (digits (n,10)) = 1 ; ::_thesis: 5 divides (digits (n,10)) . 0 then A9: 0 in dom (digits (n,10)) by NAT_1:44; A10: 5 divides Sum d by A4, A7, Th5; len d = 1 by A5, A8; then d = <%(d . 0)%> by AFINSQ_1:34; then Sum d = d . 0 by AFINSQ_2:53 .= ((digits (n,10)) . 0) * (10 |^ 0) by A5, A6, A9 ; then 5 divides ((digits (n,10)) . 0) * 1 by A10, NEWTON:4; hence 5 divides (digits (n,10)) . 0 ; ::_thesis: verum end; supposeA11: len (digits (n,10)) > 1 ; ::_thesis: 5 divides (digits (n,10)) . 0 then reconsider k = (len (digits (n,10))) - 1 as Element of NAT by NAT_1:21; defpred S1[ Nat, set ] means $2 = d . ($1 + 1); A12: now__::_thesis:_for_l_being_Nat_st_l_in_dom_<%(d_._0)%>_holds_ d_._l_=_<%(d_._0)%>_._l let l be Nat; ::_thesis: ( l in dom <%(d . 0)%> implies d . l = <%(d . 0)%> . l ) assume l in dom <%(d . 0)%> ; ::_thesis: d . l = <%(d . 0)%> . l then l in 1 by AFINSQ_1:def_4; then l < 1 by NAT_1:44; then l = 0 by NAT_1:14; hence d . l = <%(d . 0)%> . l by AFINSQ_1:34; ::_thesis: verum end; A13: for u being Nat st u in k holds ex x being Element of NAT st S1[u,x] ; consider d9 being XFinSequence of NAT such that A14: ( dom d9 = k & ( for x being Nat st x in k holds S1[x,d9 . x] ) ) from STIRL2_1:sch_5(A13); now__::_thesis:_for_i_being_Nat_st_i_in_dom_d9_holds_ 5_divides_d9_._i let i be Nat; ::_thesis: ( i in dom d9 implies 5 divides d9 . i ) assume A15: i in dom d9 ; ::_thesis: 5 divides d9 . i then i < k by A14, NAT_1:44; then i + 1 < k + 1 by XREAL_1:8; then A16: i + 1 in dom d by A5, NAT_1:44; d9 . i = d . (i + 1) by A14, A15 .= ((digits (n,10)) . (i + 1)) * (10 |^ (i + 1)) by A6, A16 .= ((digits (n,10)) . (i + 1)) * ((10 |^ i) * 10) by NEWTON:6 .= 5 * ((((digits (n,10)) . (i + 1)) * (10 |^ i)) * 2) ; hence 5 divides d9 . i by NAT_D:def_3; ::_thesis: verum end; then 5 divides Sum d9 by Th2; then A17: (Sum d9) mod 5 = 0 by PEPIN:6; A18: now__::_thesis:_for_l_being_Nat_st_l_in_dom_d9_holds_ d_._((len_<%(d_._0)%>)_+_l)_=_d9_._l let l be Nat; ::_thesis: ( l in dom d9 implies d . ((len <%(d . 0)%>) + l) = d9 . l ) A19: (len <%(d . 0)%>) + l = l + 1 by AFINSQ_1:34; assume l in dom d9 ; ::_thesis: d . ((len <%(d . 0)%>) + l) = d9 . l hence d . ((len <%(d . 0)%>) + l) = d9 . l by A14, A19; ::_thesis: verum end; dom d = k + 1 by A5 .= (len <%(d . 0)%>) + (len d9) by A14, AFINSQ_1:33 ; then d = <%(d . 0)%> ^ d9 by A12, A18, AFINSQ_1:def_3; then Sum d = (Sum <%(d . 0)%>) + (Sum d9) by AFINSQ_2:55; then n = (Sum <%(d . 0)%>) + (Sum d9) by A7, Th5; then n = (d . 0) + (Sum d9) by AFINSQ_2:53; then ((d . 0) + (Sum d9)) mod 5 = 0 by A4, PEPIN:6; then (d . 0) mod 5 = 0 by A17, NAT_D:17; then A20: 5 divides d . 0 by PEPIN:6; 0 in dom (digits (n,10)) by A11, NAT_1:44; then 5 divides ((digits (n,10)) . 0) * (10 |^ 0) by A5, A6, A20; then 5 divides ((digits (n,10)) . 0) * 1 by NEWTON:4; hence 5 divides (digits (n,10)) . 0 ; ::_thesis: verum end; end; end; assume A21: 5 divides (digits (n,10)) . 0 ; ::_thesis: 5 divides n now__::_thesis:_for_i_being_Nat_st_i_in_dom_d_holds_ 5_divides_d_._i let i be Nat; ::_thesis: ( i in dom d implies 5 divides d . b1 ) assume A22: i in dom d ; ::_thesis: 5 divides d . b1 percases ( i = 0 or i > 0 ) ; suppose i = 0 ; ::_thesis: 5 divides d . b1 then d . i = ((digits (n,10)) . 0) * (10 |^ 0) by A1, A22 .= ((digits (n,10)) . 0) * 1 by NEWTON:4 ; hence 5 divides d . i by A21; ::_thesis: verum end; suppose i > 0 ; ::_thesis: 5 divides d . b1 then consider j being Nat such that A23: j + 1 = i by NAT_1:6; d . i = ((digits (n,10)) . i) * (10 |^ (j + 1)) by A1, A22, A23 .= ((digits (n,10)) . i) * ((10 |^ j) * 10) by NEWTON:6 .= 5 * ((((digits (n,10)) . i) * (10 |^ j)) * 2) ; hence 5 divides d . i by NAT_D:def_3; ::_thesis: verum end; end; end; then 5 divides value ((digits (n,10)),10) by A2, Th2; hence 5 divides n by Th5; ::_thesis: verum end;