:: NAT_3 semantic presentation begin registration cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like natural-valued finite-support for set ; existence ex b1 being FinSequence st b1 is natural-valued proof set f = the FinSequence of NAT ; take the FinSequence of NAT ; ::_thesis: the FinSequence of NAT is natural-valued thus the FinSequence of NAT is natural-valued ; ::_thesis: verum end; end; registration let a be non empty Nat; let b be Nat; clustera |^ b -> non empty ; coherence not a |^ b is empty proof a is Real by XREAL_0:def_1; hence not a |^ b is empty by CARD_4:3; ::_thesis: verum end; end; registration cluster natural prime -> non empty for set ; coherence for b1 being Prime holds not b1 is empty by INT_2:def_4; end; theorem Th1: :: NAT_3:1 for a, b, c, d being Nat st a divides c & b divides d holds a * b divides c * d proof let a, b, c, d be Nat; ::_thesis: ( a divides c & b divides d implies a * b divides c * d ) given x being Nat such that A1: c = a * x ; :: according to NAT_D:def_3 ::_thesis: ( not b divides d or a * b divides c * d ) given y being Nat such that A2: d = b * y ; :: according to NAT_D:def_3 ::_thesis: a * b divides c * d take x * y ; :: according to NAT_D:def_3 ::_thesis: c * d = (a * b) * (x * y) thus c * d = (a * b) * (x * y) by A1, A2; ::_thesis: verum end; theorem Th2: :: NAT_3:2 for a, b being Nat st 1 < a holds b <= a |^ b proof let a, b be Nat; ::_thesis: ( 1 < a implies b <= a |^ b ) defpred S1[ Nat] means $1 <= a |^ $1; assume A1: 1 < a ; ::_thesis: b <= a |^ b then reconsider a1 = a - 1 as Element of NAT by INT_1:5; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then A3: k + 1 <= (a |^ k) + 1 by XREAL_1:6; A4: now__::_thesis:_not_(a_|^_k)_+_1_>_(a_|^_k)_*_a set x = a |^ k; assume (a |^ k) + 1 > (a |^ k) * a ; ::_thesis: contradiction then ((a |^ k) * a) - ((a |^ k) + 1) < ((a |^ k) + 1) - ((a |^ k) + 1) by XREAL_1:14; then (((a |^ k) * a1) - 1) + 1 < 0 + 1 by XREAL_1:6; then ( a |^ k = 0 or a1 = 0 ) by NAT_1:13; hence contradiction by A1; ::_thesis: verum end; a |^ (k + 1) = (a |^ k) * a by NEWTON:6; hence S1[k + 1] by A3, A4, XXREAL_0:2; ::_thesis: verum end; A5: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A5, A2); hence b <= a |^ b ; ::_thesis: verum end; theorem Th3: :: NAT_3:3 for a, n being Nat st a <> 0 holds n divides n |^ a proof let a, n be Nat; ::_thesis: ( a <> 0 implies n divides n |^ a ) assume a <> 0 ; ::_thesis: n divides n |^ a then consider b being Nat such that A1: a = b + 1 by NAT_1:6; reconsider b = b as Element of NAT by ORDINAL1:def_12; n |^ 1 divides n |^ (b + 1) by NAT_1:12, NEWTON:89; hence n divides n |^ a by A1, NEWTON:5; ::_thesis: verum end; theorem Th4: :: NAT_3:4 for i, j, m, n being Nat st i < j & m |^ j divides n holds m |^ (i + 1) divides n proof let i, j, m, n be Nat; ::_thesis: ( i < j & m |^ j divides n implies m |^ (i + 1) divides n ) assume that A1: i < j and A2: m |^ j divides n ; ::_thesis: m |^ (i + 1) divides n reconsider i = i, j = j, m = m as Element of NAT by ORDINAL1:def_12; i + 1 <= j by A1, NAT_1:13; then m |^ (i + 1) divides m |^ j by NEWTON:89; hence m |^ (i + 1) divides n by A2, NAT_D:4; ::_thesis: verum end; theorem Th5: :: NAT_3:5 for a, b being Nat for p being Prime st p divides a |^ b holds p divides a proof let a, b be Nat; ::_thesis: for p being Prime st p divides a |^ b holds p divides a let p be Prime; ::_thesis: ( p divides a |^ b implies p divides a ) assume that A1: p divides a |^ b and A2: not p divides a ; ::_thesis: contradiction reconsider p = p, a = a as Element of NAT by ORDINAL1:def_12; defpred S1[ Nat] means p divides a |^ ($1 + 1); A3: for k being Nat st k <> 0 & S1[k] holds ex n being Nat st ( n < k & S1[n] ) proof let k be Nat; ::_thesis: ( k <> 0 & S1[k] implies ex n being Nat st ( n < k & S1[n] ) ) assume that A4: k <> 0 and A5: S1[k] ; ::_thesis: ex n being Nat st ( n < k & S1[n] ) A6: p divides (a |^ k) * a by A5, NEWTON:6; take k -' 1 ; ::_thesis: ( k -' 1 < k & S1[k -' 1] ) A7: k >= 0 + 1 by A4, NAT_1:13; then k - 1 >= (0 + 1) - 1 by XREAL_1:13; then k -' 1 = k - 1 by XREAL_0:def_2; then k -' 1 < k - 0 by XREAL_1:15; hence k -' 1 < k ; ::_thesis: S1[k -' 1] (k -' 1) + 1 = k by A7, XREAL_1:235; hence S1[k -' 1] by A2, A6, NEWTON:80; ::_thesis: verum end; now__::_thesis:_not_0_+_1_>_b assume 0 + 1 > b ; ::_thesis: contradiction then b = 0 by NAT_1:13; then p divides 1 by A1, NEWTON:4; then p = 1 by WSIERP_1:15; hence contradiction by INT_2:def_4; ::_thesis: verum end; then b = (b -' 1) + 1 by XREAL_1:235; then A8: ex k being Nat st S1[k] by A1; S1[ 0 ] from NAT_1:sch_7(A8, A3); hence contradiction by A2, NEWTON:5; ::_thesis: verum end; theorem Th6: :: NAT_3:6 for b being Nat for p, a being Prime st a divides p |^ b holds a = p proof let b be Nat; ::_thesis: for p, a being Prime st a divides p |^ b holds a = p let p, a be Prime; ::_thesis: ( a divides p |^ b implies a = p ) assume a divides p |^ b ; ::_thesis: a = p then ( a <> 1 & a divides p ) by Th5, INT_2:def_4; hence a = p by INT_2:def_4; ::_thesis: verum end; theorem :: NAT_3:7 for a being Nat for f being FinSequence of NAT st a in rng f holds a divides Product f proof let a be Nat; ::_thesis: for f being FinSequence of NAT st a in rng f holds a divides Product f defpred S1[ FinSequence of NAT ] means for a being Nat st a in rng $1 holds a divides Product $1; A1: for p being FinSequence of NAT for n being Element of NAT st S1[p] holds S1[p ^ <*n*>] proof let p be FinSequence of NAT ; ::_thesis: for n being Element of NAT st S1[p] holds S1[p ^ <*n*>] let n be Element of NAT ; ::_thesis: ( S1[p] implies S1[p ^ <*n*>] ) assume A2: S1[p] ; ::_thesis: S1[p ^ <*n*>] set p1 = p ^ <*n*>; A3: rng (p ^ <*n*>) = (rng p) \/ (rng <*n*>) by FINSEQ_1:31; A4: Product (p ^ <*n*>) = (Product p) * n by RVSUM_1:96; let a be Nat; ::_thesis: ( a in rng (p ^ <*n*>) implies a divides Product (p ^ <*n*>) ) assume A5: a in rng (p ^ <*n*>) ; ::_thesis: a divides Product (p ^ <*n*>) percases ( a in rng p or a in rng <*n*> ) by A5, A3, XBOOLE_0:def_3; suppose a in rng p ; ::_thesis: a divides Product (p ^ <*n*>) hence a divides Product (p ^ <*n*>) by A2, A4, NAT_D:9; ::_thesis: verum end; suppose a in rng <*n*> ; ::_thesis: a divides Product (p ^ <*n*>) then a in {n} by FINSEQ_1:39; then a = n by TARSKI:def_1; hence a divides Product (p ^ <*n*>) by A4, NAT_D:9; ::_thesis: verum end; end; end; A6: S1[ <*> NAT] ; for p being FinSequence of NAT holds S1[p] from FINSEQ_2:sch_2(A6, A1); hence for f being FinSequence of NAT st a in rng f holds a divides Product f ; ::_thesis: verum end; theorem :: NAT_3:8 for p being Prime for f being FinSequence of SetPrimes st p divides Product f holds p in rng f proof let p be Prime; ::_thesis: for f being FinSequence of SetPrimes st p divides Product f holds p in rng f defpred S1[ FinSequence of SetPrimes ] means for p being Prime st p divides Product $1 holds p in rng $1; A1: now__::_thesis:_for_f_being_FinSequence_of_SetPrimes_ for_n_being_Element_of_SetPrimes_st_S1[f]_holds_ S1[f_^_<*n*>] let f be FinSequence of SetPrimes ; ::_thesis: for n being Element of SetPrimes st S1[f] holds S1[f ^ <*n*>] let n be Element of SetPrimes ; ::_thesis: ( S1[f] implies S1[f ^ <*n*>] ) set f1 = f ^ <*n*>; assume A2: S1[f] ; ::_thesis: S1[f ^ <*n*>] thus S1[f ^ <*n*>] ::_thesis: verum proof reconsider nn = n as Nat ; reconsider ff = f as FinSequence of NAT ; let p be Prime; ::_thesis: ( p divides Product (f ^ <*n*>) implies p in rng (f ^ <*n*>) ) assume p divides Product (f ^ <*n*>) ; ::_thesis: p in rng (f ^ <*n*>) then A3: p divides (Product ff) * n by RVSUM_1:96; percases ( p divides Product f or p divides nn ) by A3, NEWTON:80; supposeA4: p divides Product f ; ::_thesis: p in rng (f ^ <*n*>) A5: rng f c= rng (f ^ <*n*>) by FINSEQ_1:29; p in rng f by A2, A4; hence p in rng (f ^ <*n*>) by A5; ::_thesis: verum end; supposeA6: p divides nn ; ::_thesis: p in rng (f ^ <*n*>) nn is prime by NEWTON:def_6; then ( p = 1 or p = n ) by A6, INT_2:def_4; then p in {n} by INT_2:def_4, TARSKI:def_1; then A7: p in rng <*n*> by FINSEQ_1:38; rng <*n*> c= rng (f ^ <*n*>) by FINSEQ_1:30; hence p in rng (f ^ <*n*>) by A7; ::_thesis: verum end; end; end; end; A8: S1[ <*> SetPrimes] proof let p be Prime; ::_thesis: ( p divides Product (<*> SetPrimes) implies p in rng (<*> SetPrimes) ) assume p divides Product (<*> SetPrimes) ; ::_thesis: p in rng (<*> SetPrimes) then p <= 1 by NAT_D:7, RVSUM_1:94; hence p in rng (<*> SetPrimes) by INT_2:def_4; ::_thesis: verum end; for p being FinSequence of SetPrimes holds S1[p] from FINSEQ_2:sch_2(A8, A1); hence for f being FinSequence of SetPrimes st p divides Product f holds p in rng f ; ::_thesis: verum end; definition let f be real-valued FinSequence; let a be Nat; funcf |^ a -> FinSequence means :Def1: :: NAT_3:def 1 ( len it = len f & ( for i being set st i in dom it holds it . i = (f . i) |^ a ) ); existence ex b1 being FinSequence st ( len b1 = len f & ( for i being set st i in dom b1 holds b1 . i = (f . i) |^ a ) ) proof deffunc H1( Nat) -> Element of REAL = (f . $1) |^ a; consider p being FinSequence such that A1: len p = len f and A2: for k being Nat st k in dom p holds p . k = H1(k) from FINSEQ_1:sch_2(); take p ; ::_thesis: ( len p = len f & ( for i being set st i in dom p holds p . i = (f . i) |^ a ) ) thus len p = len f by A1; ::_thesis: for i being set st i in dom p holds p . i = (f . i) |^ a let i be set ; ::_thesis: ( i in dom p implies p . i = (f . i) |^ a ) assume i in dom p ; ::_thesis: p . i = (f . i) |^ a hence p . i = (f . i) |^ a by A2; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence st len b1 = len f & ( for i being set st i in dom b1 holds b1 . i = (f . i) |^ a ) & len b2 = len f & ( for i being set st i in dom b2 holds b2 . i = (f . i) |^ a ) holds b1 = b2 proof let g, h be FinSequence; ::_thesis: ( len g = len f & ( for i being set st i in dom g holds g . i = (f . i) |^ a ) & len h = len f & ( for i being set st i in dom h holds h . i = (f . i) |^ a ) implies g = h ) assume that A3: len g = len f and A4: for i being set st i in dom g holds g . i = (f . i) |^ a and A5: len h = len f and A6: for i being set st i in dom h holds h . i = (f . i) |^ a ; ::_thesis: g = h A7: ( dom g = Seg (len g) & dom h = Seg (len h) ) by FINSEQ_1:def_3; for k being Nat st k in dom g holds g . k = h . k proof let k be Nat; ::_thesis: ( k in dom g implies g . k = h . k ) assume A8: k in dom g ; ::_thesis: g . k = h . k thus g . k = (f . k) |^ a by A4, A8 .= h . k by A3, A5, A6, A7, A8 ; ::_thesis: verum end; hence g = h by A3, A5, A7, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def1 defines |^ NAT_3:def_1_:_ for f being real-valued FinSequence for a being Nat for b3 being FinSequence holds ( b3 = f |^ a iff ( len b3 = len f & ( for i being set st i in dom b3 holds b3 . i = (f . i) |^ a ) ) ); registration let f be real-valued FinSequence; let a be Nat; clusterf |^ a -> real-valued ; coherence f |^ a is real-valued proof let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (f |^ a) or not (f |^ a) . x is V37() ) set g = f |^ a; assume x in dom (f |^ a) ; ::_thesis: (f |^ a) . x is V37() then (f |^ a) . x = (f . x) |^ a by Def1; hence (f |^ a) . x is V37() ; ::_thesis: verum end; end; registration let f be natural-valued FinSequence; let a be Nat; clusterf |^ a -> natural-valued ; coherence f |^ a is natural-valued proof let x be set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in dom (f |^ a) or (f |^ a) . x is natural ) set g = f |^ a; assume x in dom (f |^ a) ; ::_thesis: (f |^ a) . x is natural then (f |^ a) . x = (f . x) |^ a by Def1; hence (f |^ a) . x is natural ; ::_thesis: verum end; end; definition let f be FinSequence of REAL ; let a be Nat; :: original: |^ redefine funcf |^ a -> FinSequence of REAL ; coherence f |^ a is FinSequence of REAL proof thus rng (f |^ a) c= REAL ; :: according to FINSEQ_1:def_4 ::_thesis: verum end; end; definition let f be FinSequence of NAT ; let a be Nat; :: original: |^ redefine funcf |^ a -> FinSequence of NAT ; coherence f |^ a is FinSequence of NAT proof thus rng (f |^ a) c= NAT by VALUED_0:def_6; :: according to FINSEQ_1:def_4 ::_thesis: verum end; end; theorem Th9: :: NAT_3:9 for f being FinSequence of REAL holds f |^ 0 = (len f) |-> 1 proof let f be FinSequence of REAL ; ::_thesis: f |^ 0 = (len f) |-> 1 A1: len (f |^ 0) = len f by Def1; A2: for k being Nat st 1 <= k & k <= len (f |^ 0) holds (f |^ 0) . k = ((len f) |-> 1) . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len (f |^ 0) implies (f |^ 0) . k = ((len f) |-> 1) . k ) assume A3: ( 1 <= k & k <= len (f |^ 0) ) ; ::_thesis: (f |^ 0) . k = ((len f) |-> 1) . k then A4: k in dom (f |^ 0) by FINSEQ_3:25; then A5: k in Seg (len f) by A1, A3; thus (f |^ 0) . k = (f . k) |^ 0 by A4, Def1 .= 1 by NEWTON:4 .= ((len f) |-> 1) . k by A5, FUNCOP_1:7 ; ::_thesis: verum end; len ((len f) |-> 1) = len f by CARD_1:def_7; hence f |^ 0 = (len f) |-> 1 by A1, A2, FINSEQ_1:14; ::_thesis: verum end; theorem :: NAT_3:10 for f being FinSequence of REAL holds f |^ 1 = f proof let f be FinSequence of REAL ; ::_thesis: f |^ 1 = f A1: for k being Nat st 1 <= k & k <= len (f |^ 1) holds (f |^ 1) . k = f . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len (f |^ 1) implies (f |^ 1) . k = f . k ) assume ( 1 <= k & k <= len (f |^ 1) ) ; ::_thesis: (f |^ 1) . k = f . k then k in dom (f |^ 1) by FINSEQ_3:25; hence (f |^ 1) . k = (f . k) |^ 1 by Def1 .= f . k by NEWTON:5 ; ::_thesis: verum end; len (f |^ 1) = len f by Def1; hence f |^ 1 = f by A1, FINSEQ_1:14; ::_thesis: verum end; theorem Th11: :: NAT_3:11 for a being Nat holds (<*> REAL) |^ a = <*> REAL proof let a be Nat; ::_thesis: (<*> REAL) |^ a = <*> REAL len ((<*> REAL) |^ a) = len (<*> REAL) by Def1 .= 0 ; hence (<*> REAL) |^ a = <*> REAL ; ::_thesis: verum end; theorem Th12: :: NAT_3:12 for a being Nat for r being Real holds <*r*> |^ a = <*(r |^ a)*> proof let a be Nat; ::_thesis: for r being Real holds <*r*> |^ a = <*(r |^ a)*> let r be Real; ::_thesis: <*r*> |^ a = <*(r |^ a)*> A1: len (<*r*> |^ a) = len <*r*> by Def1 .= 1 by FINSEQ_1:40 ; 0 + 1 in Seg (0 + 1) ; then 1 in dom (<*r*> |^ a) by A1, FINSEQ_1:def_3; then (<*r*> |^ a) . 1 = (<*r*> . 1) |^ a by Def1 .= r |^ a by FINSEQ_1:40 ; hence <*r*> |^ a = <*(r |^ a)*> by A1, FINSEQ_1:40; ::_thesis: verum end; theorem Th13: :: NAT_3:13 for a being Nat for r being Real for f being FinSequence of REAL holds (f ^ <*r*>) |^ a = (f |^ a) ^ (<*r*> |^ a) proof let a be Nat; ::_thesis: for r being Real for f being FinSequence of REAL holds (f ^ <*r*>) |^ a = (f |^ a) ^ (<*r*> |^ a) let r be Real; ::_thesis: for f being FinSequence of REAL holds (f ^ <*r*>) |^ a = (f |^ a) ^ (<*r*> |^ a) let f be FinSequence of REAL ; ::_thesis: (f ^ <*r*>) |^ a = (f |^ a) ^ (<*r*> |^ a) A1: len (f |^ a) = len f by Def1; A2: len ((f ^ <*r*>) |^ a) = len (f ^ <*r*>) by Def1 .= (len f) + (len <*r*>) by FINSEQ_1:22 .= (len f) + 1 by FINSEQ_1:40 ; then A3: dom ((f ^ <*r*>) |^ a) = Seg ((len f) + 1) by FINSEQ_1:def_3; A4: now__::_thesis:_for_i_being_Nat_st_i_in_dom_((f_^_<*r*>)_|^_a)_holds_ ((f_^_<*r*>)_|^_a)_._i_=_((f_|^_a)_^_(<*r*>_|^_a))_._i let i be Nat; ::_thesis: ( i in dom ((f ^ <*r*>) |^ a) implies ((f ^ <*r*>) |^ a) . b1 = ((f |^ a) ^ (<*r*> |^ a)) . b1 ) assume A5: i in dom ((f ^ <*r*>) |^ a) ; ::_thesis: ((f ^ <*r*>) |^ a) . b1 = ((f |^ a) ^ (<*r*> |^ a)) . b1 A6: 1 <= i by A3, A5, FINSEQ_1:1; A7: i <= (len f) + 1 by A3, A5, FINSEQ_1:1; percases ( i < (len f) + 1 or i = (len f) + 1 ) by A7, XXREAL_0:1; suppose i < (len f) + 1 ; ::_thesis: ((f ^ <*r*>) |^ a) . b1 = ((f |^ a) ^ (<*r*> |^ a)) . b1 then A8: i <= len f by NAT_1:13; then A9: i in dom f by A6, FINSEQ_3:25; A10: i in dom (f |^ a) by A1, A6, A8, FINSEQ_3:25; thus ((f ^ <*r*>) |^ a) . i = ((f ^ <*r*>) . i) |^ a by A5, Def1 .= (f . i) |^ a by A9, FINSEQ_1:def_7 .= (f |^ a) . i by A10, Def1 .= ((f |^ a) ^ (<*r*> |^ a)) . i by A10, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA11: i = (len f) + 1 ; ::_thesis: ((f ^ <*r*>) |^ a) . b1 = ((f |^ a) ^ (<*r*> |^ a)) . b1 thus ((f ^ <*r*>) |^ a) . i = ((f ^ <*r*>) . i) |^ a by A5, Def1 .= r |^ a by A11, FINSEQ_1:42 .= ((f |^ a) ^ <*(r |^ a)*>) . i by A1, A11, FINSEQ_1:42 .= ((f |^ a) ^ (<*r*> |^ a)) . i by Th12 ; ::_thesis: verum end; end; end; len ((f |^ a) ^ (<*r*> |^ a)) = (len (f |^ a)) + (len (<*r*> |^ a)) by FINSEQ_1:22 .= (len f) + (len (<*r*> |^ a)) by Def1 .= (len f) + (len <*(r |^ a)*>) by Th12 .= (len f) + 1 by FINSEQ_1:40 ; hence (f ^ <*r*>) |^ a = (f |^ a) ^ (<*r*> |^ a) by A2, A4, FINSEQ_2:9; ::_thesis: verum end; theorem Th14: :: NAT_3:14 for b being Nat for f being FinSequence of REAL holds Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f) proof let b be Nat; ::_thesis: for f being FinSequence of REAL holds Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f) let f be FinSequence of REAL ; ::_thesis: Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f) defpred S1[ FinSequence of REAL ] means for b being Nat holds Product ($1 |^ (b + 1)) = (Product ($1 |^ b)) * (Product $1); A1: now__::_thesis:_for_p_being_FinSequence_of_REAL_ for_x_being_Element_of_REAL_st_S1[p]_holds_ S1[p_^_<*x*>] let p be FinSequence of REAL ; ::_thesis: for x being Element of REAL st S1[p] holds S1[p ^ <*x*>] let x be Element of REAL ; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] ) assume A2: S1[p] ; ::_thesis: S1[p ^ <*x*>] thus S1[p ^ <*x*>] ::_thesis: verum proof set p1 = p ^ <*x*>; let b be Nat; ::_thesis: Product ((p ^ <*x*>) |^ (b + 1)) = (Product ((p ^ <*x*>) |^ b)) * (Product (p ^ <*x*>)) (p ^ <*x*>) |^ (b + 1) = (p |^ (b + 1)) ^ (<*x*> |^ (b + 1)) by Th13; hence Product ((p ^ <*x*>) |^ (b + 1)) = (Product (p |^ (b + 1))) * (Product (<*x*> |^ (b + 1))) by RVSUM_1:97 .= ((Product (p |^ b)) * (Product p)) * (Product (<*x*> |^ (b + 1))) by A2 .= ((Product (p |^ b)) * (Product p)) * (Product <*(x |^ (b + 1))*>) by Th12 .= ((Product (p |^ b)) * (Product p)) * (x |^ (b + 1)) by RVSUM_1:95 .= ((Product (p |^ b)) * (Product p)) * ((x |^ b) * x) by NEWTON:6 .= (((Product (p |^ b)) * (x |^ b)) * x) * (Product p) .= ((Product ((p |^ b) ^ <*(x |^ b)*>)) * x) * (Product p) by RVSUM_1:96 .= ((Product ((p |^ b) ^ (<*x*> |^ b))) * x) * (Product p) by Th12 .= ((Product ((p ^ <*x*>) |^ b)) * x) * (Product p) by Th13 .= (Product ((p ^ <*x*>) |^ b)) * ((Product p) * x) .= (Product ((p ^ <*x*>) |^ b)) * (Product (p ^ <*x*>)) by RVSUM_1:96 ; ::_thesis: verum end; end; A3: S1[ <*> REAL] proof set f = <*> REAL; let b be Nat; ::_thesis: Product ((<*> REAL) |^ (b + 1)) = (Product ((<*> REAL) |^ b)) * (Product (<*> REAL)) thus Product ((<*> REAL) |^ (b + 1)) = 1 by Th11, RVSUM_1:94 .= (Product ((<*> REAL) |^ b)) * (Product (<*> REAL)) by Th11, RVSUM_1:94 ; ::_thesis: verum end; for p being FinSequence of REAL holds S1[p] from FINSEQ_2:sch_2(A3, A1); hence Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f) ; ::_thesis: verum end; theorem :: NAT_3:15 for a being Nat for f being FinSequence of REAL holds Product (f |^ a) = (Product f) |^ a proof let a be Nat; ::_thesis: for f being FinSequence of REAL holds Product (f |^ a) = (Product f) |^ a let f be FinSequence of REAL ; ::_thesis: Product (f |^ a) = (Product f) |^ a defpred S1[ Nat] means Product (f |^ $1) = (Product f) |^ $1; A1: for b being Nat st S1[b] holds S1[b + 1] proof let b be Nat; ::_thesis: ( S1[b] implies S1[b + 1] ) assume A2: S1[b] ; ::_thesis: S1[b + 1] thus Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f) by Th14 .= (Product f) |^ (b + 1) by A2, NEWTON:6 ; ::_thesis: verum end; Product (f |^ 0) = Product ((len f) |-> 1) by Th9 .= 1 by RVSUM_1:102 .= (Product f) |^ 0 by NEWTON:4 ; then A3: S1[ 0 ] ; for b being Nat holds S1[b] from NAT_1:sch_2(A3, A1); hence Product (f |^ a) = (Product f) |^ a ; ::_thesis: verum end; begin registration let X be set ; cluster Relation-like X -defined Function-like V14(X) natural-valued finite-support for set ; existence ex b1 being ManySortedSet of X st ( b1 is natural-valued & b1 is finite-support ) proof set r = the natural-valued finite-support ManySortedSet of X; the natural-valued finite-support ManySortedSet of X = the natural-valued finite-support ManySortedSet of X ; hence ex b1 being ManySortedSet of X st ( b1 is natural-valued & b1 is finite-support ) ; ::_thesis: verum end; end; definition let X be set ; let b be real-valued ManySortedSet of X; let a be Nat; funca * b -> ManySortedSet of X means :Def2: :: NAT_3:def 2 for i being set holds it . i = a * (b . i); existence ex b1 being ManySortedSet of X st for i being set holds b1 . i = a * (b . i) proof deffunc H1( set ) -> Element of REAL = a * (b . $1); consider f being ManySortedSet of X such that A1: for i being set st i in X holds f . i = H1(i) from PBOOLE:sch_4(); take f ; ::_thesis: for i being set holds f . i = a * (b . i) let i be set ; ::_thesis: f . i = a * (b . i) percases ( i in X or not i in X ) ; suppose i in X ; ::_thesis: f . i = a * (b . i) hence f . i = a * (b . i) by A1; ::_thesis: verum end; supposeA2: not i in X ; ::_thesis: f . i = a * (b . i) A3: dom b = X by PARTFUN1:def_2; dom f = X by PARTFUN1:def_2; hence f . i = a * 0 by A2, FUNCT_1:def_2 .= a * (b . i) by A2, A3, FUNCT_1:def_2 ; ::_thesis: verum end; end; end; uniqueness for b1, b2 being ManySortedSet of X st ( for i being set holds b1 . i = a * (b . i) ) & ( for i being set holds b2 . i = a * (b . i) ) holds b1 = b2 proof let f, g be ManySortedSet of X; ::_thesis: ( ( for i being set holds f . i = a * (b . i) ) & ( for i being set holds g . i = a * (b . i) ) implies f = g ) assume that A4: for i being set holds f . i = a * (b . i) and A5: for i being set holds g . i = a * (b . i) ; ::_thesis: f = g for i being set st i in X holds f . i = g . i proof let i be set ; ::_thesis: ( i in X implies f . i = g . i ) assume i in X ; ::_thesis: f . i = g . i thus f . i = a * (b . i) by A4 .= g . i by A5 ; ::_thesis: verum end; hence f = g by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def2 defines * NAT_3:def_2_:_ for X being set for b being real-valued ManySortedSet of X for a being Nat for b4 being ManySortedSet of X holds ( b4 = a * b iff for i being set holds b4 . i = a * (b . i) ); registration let X be set ; let b be real-valued ManySortedSet of X; let a be Nat; clustera * b -> real-valued ; coherence a * b is real-valued proof let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (a * b) or not (a * b) . x is V37() ) assume x in dom (a * b) ; ::_thesis: (a * b) . x is V37() (a * b) . x = a * (b . x) by Def2; hence (a * b) . x is V37() ; ::_thesis: verum end; end; registration let X be set ; let b be natural-valued ManySortedSet of X; let a be Nat; clustera * b -> natural-valued ; coherence a * b is natural-valued proof let x be set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in dom (a * b) or (a * b) . x is natural ) assume x in dom (a * b) ; ::_thesis: (a * b) . x is natural (a * b) . x = a * (b . x) by Def2; hence (a * b) . x is natural ; ::_thesis: verum end; end; registration let X be set ; let b be real-valued ManySortedSet of X; cluster support (0 * b) -> empty ; coherence support (0 * b) is empty proof assume not support (0 * b) is empty ; ::_thesis: contradiction then consider x being set such that A1: x in support (0 * b) by XBOOLE_0:def_1; (0 * b) . x <> 0 by A1, PRE_POLY:def_7; then 0 * (b . x) <> 0 by Def2; hence contradiction ; ::_thesis: verum end; end; theorem Th16: :: NAT_3:16 for a being Nat for X being set for b being real-valued ManySortedSet of X st a <> 0 holds support b = support (a * b) proof let a be Nat; ::_thesis: for X being set for b being real-valued ManySortedSet of X st a <> 0 holds support b = support (a * b) let X be set ; ::_thesis: for b being real-valued ManySortedSet of X st a <> 0 holds support b = support (a * b) let b be real-valued ManySortedSet of X; ::_thesis: ( a <> 0 implies support b = support (a * b) ) assume A1: a <> 0 ; ::_thesis: support b = support (a * b) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: support (a * b) c= support b let x be set ; ::_thesis: ( x in support b implies x in support (a * b) ) assume x in support b ; ::_thesis: x in support (a * b) then b . x <> 0 by PRE_POLY:def_7; then a * (b . x) <> 0 by A1; then (a * b) . x <> 0 by Def2; hence x in support (a * b) by PRE_POLY:def_7; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (a * b) or x in support b ) assume x in support (a * b) ; ::_thesis: x in support b then (a * b) . x <> 0 by PRE_POLY:def_7; then a * (b . x) <> 0 by Def2; then b . x <> 0 ; hence x in support b by PRE_POLY:def_7; ::_thesis: verum end; registration let X be set ; let b be real-valued finite-support ManySortedSet of X; let a be Nat; clustera * b -> finite-support ; coherence a * b is finite-support proof percases ( a = 0 or a <> 0 ) ; suppose a = 0 ; ::_thesis: a * b is finite-support hence support (a * b) is finite ; :: according to PRE_POLY:def_8 ::_thesis: verum end; suppose a <> 0 ; ::_thesis: a * b is finite-support then support (a * b) = support b by Th16; hence support (a * b) is finite ; :: according to PRE_POLY:def_8 ::_thesis: verum end; end; end; end; definition let X be set ; let b1, b2 be real-valued ManySortedSet of X; func min (b1,b2) -> ManySortedSet of X means :Def3: :: NAT_3:def 3 for i being set holds ( ( b1 . i <= b2 . i implies it . i = b1 . i ) & ( b1 . i > b2 . i implies it . i = b2 . i ) ); existence ex b1 being ManySortedSet of X st for i being set holds ( ( b1 . i <= b2 . i implies b1 . i = b1 . i ) & ( b1 . i > b2 . i implies b1 . i = b2 . i ) ) proof deffunc H1( set ) -> Element of REAL = b2 . $1; deffunc H2( set ) -> Element of REAL = b1 . $1; defpred S1[ set ] means b1 . $1 <= b2 . $1; consider f being ManySortedSet of X such that A1: for i being Element of X st i in X holds ( ( S1[i] implies f . i = H2(i) ) & ( not S1[i] implies f . i = H1(i) ) ) from PRE_CIRC:sch_2(); take f ; ::_thesis: for i being set holds ( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) ) let i be set ; ::_thesis: ( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) ) percases ( i in X or not i in X ) ; suppose i in X ; ::_thesis: ( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) ) hence ( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) ) by A1; ::_thesis: verum end; supposeA2: not i in X ; ::_thesis: ( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) ) then not i in dom f by PARTFUN1:def_2; then A3: f . i = 0 by FUNCT_1:def_2; ( not i in dom b1 & not i in dom b2 ) by A2, PARTFUN1:def_2; hence ( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) ) by A3, FUNCT_1:def_2; ::_thesis: verum end; end; end; uniqueness for b1, b2 being ManySortedSet of X st ( for i being set holds ( ( b1 . i <= b2 . i implies b1 . i = b1 . i ) & ( b1 . i > b2 . i implies b1 . i = b2 . i ) ) ) & ( for i being set holds ( ( b1 . i <= b2 . i implies b2 . i = b1 . i ) & ( b1 . i > b2 . i implies b2 . i = b2 . i ) ) ) holds b1 = b2 proof let f, g be ManySortedSet of X; ::_thesis: ( ( for i being set holds ( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) ) ) & ( for i being set holds ( ( b1 . i <= b2 . i implies g . i = b1 . i ) & ( b1 . i > b2 . i implies g . i = b2 . i ) ) ) implies f = g ) assume that A4: for i being set holds ( ( b1 . i <= b2 . i implies f . i = b1 . i ) & ( b1 . i > b2 . i implies f . i = b2 . i ) ) and A5: for i being set holds ( ( b1 . i <= b2 . i implies g . i = b1 . i ) & ( b1 . i > b2 . i implies g . i = b2 . i ) ) ; ::_thesis: f = g now__::_thesis:_for_i_being_set_st_i_in_X_holds_ f_._i_=_g_._i let i be set ; ::_thesis: ( i in X implies f . b1 = g . b1 ) assume i in X ; ::_thesis: f . b1 = g . b1 percases ( b1 . i <= b2 . i or b1 . i > b2 . i ) ; supposeA6: b1 . i <= b2 . i ; ::_thesis: f . b1 = g . b1 hence f . i = b1 . i by A4 .= g . i by A5, A6 ; ::_thesis: verum end; supposeA7: b1 . i > b2 . i ; ::_thesis: f . b1 = g . b1 hence f . i = b2 . i by A4 .= g . i by A5, A7 ; ::_thesis: verum end; end; end; hence f = g by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def3 defines min NAT_3:def_3_:_ for X being set for b1, b2 being real-valued ManySortedSet of X for b4 being ManySortedSet of X holds ( b4 = min (b1,b2) iff for i being set holds ( ( b1 . i <= b2 . i implies b4 . i = b1 . i ) & ( b1 . i > b2 . i implies b4 . i = b2 . i ) ) ); registration let X be set ; let b1, b2 be real-valued ManySortedSet of X; cluster min (b1,b2) -> real-valued ; coherence min (b1,b2) is real-valued proof let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (min (b1,b2)) or not (min (b1,b2)) . x is V37() ) set f = min (b1,b2); assume x in dom (min (b1,b2)) ; ::_thesis: (min (b1,b2)) . x is V37() ( b1 . x <= b2 . x or b1 . x > b2 . x ) ; hence (min (b1,b2)) . x is V37() by Def3; ::_thesis: verum end; end; registration let X be set ; let b1, b2 be natural-valued ManySortedSet of X; cluster min (b1,b2) -> natural-valued ; coherence min (b1,b2) is natural-valued proof let x be set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in dom (min (b1,b2)) or (min (b1,b2)) . x is natural ) set f = min (b1,b2); assume x in dom (min (b1,b2)) ; ::_thesis: (min (b1,b2)) . x is natural ( b1 . x <= b2 . x or b1 . x > b2 . x ) ; hence (min (b1,b2)) . x is natural by Def3; ::_thesis: verum end; end; theorem Th17: :: NAT_3:17 for X being set for b1, b2 being real-valued finite-support ManySortedSet of X holds support (min (b1,b2)) c= (support b1) \/ (support b2) proof let X be set ; ::_thesis: for b1, b2 being real-valued finite-support ManySortedSet of X holds support (min (b1,b2)) c= (support b1) \/ (support b2) let b1, b2 be real-valued finite-support ManySortedSet of X; ::_thesis: support (min (b1,b2)) c= (support b1) \/ (support b2) set f = min (b1,b2); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (min (b1,b2)) or x in (support b1) \/ (support b2) ) assume x in support (min (b1,b2)) ; ::_thesis: x in (support b1) \/ (support b2) then A1: (min (b1,b2)) . x <> 0 by PRE_POLY:def_7; ( (min (b1,b2)) . x = b1 . x or (min (b1,b2)) . x = b2 . x ) by Def3; then ( x in support b1 or x in support b2 ) by A1, PRE_POLY:def_7; hence x in (support b1) \/ (support b2) by XBOOLE_0:def_3; ::_thesis: verum end; registration let X be set ; let b1, b2 be real-valued finite-support ManySortedSet of X; cluster min (b1,b2) -> finite-support ; coherence min (b1,b2) is finite-support proof support (min (b1,b2)) c= (support b1) \/ (support b2) by Th17; hence support (min (b1,b2)) is finite ; :: according to PRE_POLY:def_8 ::_thesis: verum end; end; definition let X be set ; let b1, b2 be real-valued ManySortedSet of X; func max (b1,b2) -> ManySortedSet of X means :Def4: :: NAT_3:def 4 for i being set holds ( ( b1 . i <= b2 . i implies it . i = b2 . i ) & ( b1 . i > b2 . i implies it . i = b1 . i ) ); existence ex b1 being ManySortedSet of X st for i being set holds ( ( b1 . i <= b2 . i implies b1 . i = b2 . i ) & ( b1 . i > b2 . i implies b1 . i = b1 . i ) ) proof deffunc H1( set ) -> Element of REAL = b1 . $1; deffunc H2( set ) -> Element of REAL = b2 . $1; defpred S1[ set ] means b1 . $1 <= b2 . $1; consider f being ManySortedSet of X such that A1: for i being Element of X st i in X holds ( ( S1[i] implies f . i = H2(i) ) & ( not S1[i] implies f . i = H1(i) ) ) from PRE_CIRC:sch_2(); take f ; ::_thesis: for i being set holds ( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) ) let i be set ; ::_thesis: ( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) ) percases ( i in X or not i in X ) ; suppose i in X ; ::_thesis: ( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) ) hence ( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) ) by A1; ::_thesis: verum end; supposeA2: not i in X ; ::_thesis: ( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) ) then not i in dom f by PARTFUN1:def_2; then A3: f . i = 0 by FUNCT_1:def_2; ( not i in dom b1 & not i in dom b2 ) by A2, PARTFUN1:def_2; hence ( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) ) by A3, FUNCT_1:def_2; ::_thesis: verum end; end; end; uniqueness for b1, b2 being ManySortedSet of X st ( for i being set holds ( ( b1 . i <= b2 . i implies b1 . i = b2 . i ) & ( b1 . i > b2 . i implies b1 . i = b1 . i ) ) ) & ( for i being set holds ( ( b1 . i <= b2 . i implies b2 . i = b2 . i ) & ( b1 . i > b2 . i implies b2 . i = b1 . i ) ) ) holds b1 = b2 proof let f, g be ManySortedSet of X; ::_thesis: ( ( for i being set holds ( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) ) ) & ( for i being set holds ( ( b1 . i <= b2 . i implies g . i = b2 . i ) & ( b1 . i > b2 . i implies g . i = b1 . i ) ) ) implies f = g ) assume that A4: for i being set holds ( ( b1 . i <= b2 . i implies f . i = b2 . i ) & ( b1 . i > b2 . i implies f . i = b1 . i ) ) and A5: for i being set holds ( ( b1 . i <= b2 . i implies g . i = b2 . i ) & ( b1 . i > b2 . i implies g . i = b1 . i ) ) ; ::_thesis: f = g now__::_thesis:_for_i_being_set_st_i_in_X_holds_ f_._i_=_g_._i let i be set ; ::_thesis: ( i in X implies f . b1 = g . b1 ) assume i in X ; ::_thesis: f . b1 = g . b1 percases ( b1 . i <= b2 . i or b1 . i > b2 . i ) ; supposeA6: b1 . i <= b2 . i ; ::_thesis: f . b1 = g . b1 hence f . i = b2 . i by A4 .= g . i by A5, A6 ; ::_thesis: verum end; supposeA7: b1 . i > b2 . i ; ::_thesis: f . b1 = g . b1 hence f . i = b1 . i by A4 .= g . i by A5, A7 ; ::_thesis: verum end; end; end; hence f = g by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def4 defines max NAT_3:def_4_:_ for X being set for b1, b2 being real-valued ManySortedSet of X for b4 being ManySortedSet of X holds ( b4 = max (b1,b2) iff for i being set holds ( ( b1 . i <= b2 . i implies b4 . i = b2 . i ) & ( b1 . i > b2 . i implies b4 . i = b1 . i ) ) ); registration let X be set ; let b1, b2 be real-valued ManySortedSet of X; cluster max (b1,b2) -> real-valued ; coherence max (b1,b2) is real-valued proof let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (max (b1,b2)) or not (max (b1,b2)) . x is V37() ) set f = max (b1,b2); assume x in dom (max (b1,b2)) ; ::_thesis: (max (b1,b2)) . x is V37() ( b1 . x <= b2 . x or b1 . x > b2 . x ) ; hence (max (b1,b2)) . x is V37() by Def4; ::_thesis: verum end; end; registration let X be set ; let b1, b2 be natural-valued ManySortedSet of X; cluster max (b1,b2) -> natural-valued ; coherence max (b1,b2) is natural-valued proof let x be set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in dom (max (b1,b2)) or (max (b1,b2)) . x is natural ) set f = max (b1,b2); assume x in dom (max (b1,b2)) ; ::_thesis: (max (b1,b2)) . x is natural ( b1 . x <= b2 . x or b1 . x > b2 . x ) ; hence (max (b1,b2)) . x is natural by Def4; ::_thesis: verum end; end; theorem Th18: :: NAT_3:18 for X being set for b1, b2 being real-valued finite-support ManySortedSet of X holds support (max (b1,b2)) c= (support b1) \/ (support b2) proof let X be set ; ::_thesis: for b1, b2 being real-valued finite-support ManySortedSet of X holds support (max (b1,b2)) c= (support b1) \/ (support b2) let b1, b2 be real-valued finite-support ManySortedSet of X; ::_thesis: support (max (b1,b2)) c= (support b1) \/ (support b2) set f = max (b1,b2); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (max (b1,b2)) or x in (support b1) \/ (support b2) ) assume x in support (max (b1,b2)) ; ::_thesis: x in (support b1) \/ (support b2) then A1: (max (b1,b2)) . x <> 0 by PRE_POLY:def_7; ( (max (b1,b2)) . x = b1 . x or (max (b1,b2)) . x = b2 . x ) by Def4; then ( x in support b1 or x in support b2 ) by A1, PRE_POLY:def_7; hence x in (support b1) \/ (support b2) by XBOOLE_0:def_3; ::_thesis: verum end; registration let X be set ; let b1, b2 be real-valued finite-support ManySortedSet of X; cluster max (b1,b2) -> finite-support ; coherence max (b1,b2) is finite-support proof support (max (b1,b2)) c= (support b1) \/ (support b2) by Th18; hence support (max (b1,b2)) is finite ; :: according to PRE_POLY:def_8 ::_thesis: verum end; end; registration let A be set ; cluster Relation-like A -defined Function-like V14(A) complex-yielding finite-support for set ; existence ex b1 being ManySortedSet of A st ( b1 is finite-support & b1 is complex-yielding ) proof set f = the natural-valued finite-support ManySortedSet of A; the natural-valued finite-support ManySortedSet of A is complex-yielding ; hence ex b1 being ManySortedSet of A st ( b1 is finite-support & b1 is complex-yielding ) ; ::_thesis: verum end; end; definition let A be set ; let b be complex-yielding finite-support ManySortedSet of A; func Product b -> complex number means :Def5: :: NAT_3:def 5 ex f being FinSequence of COMPLEX st ( it = Product f & f = b * (canFS (support b)) ); existence ex b1 being complex number ex f being FinSequence of COMPLEX st ( b1 = Product f & f = b * (canFS (support b)) ) proof set cS = canFS (support b); set f = b * (canFS (support b)); A1: rng (b * (canFS (support b))) c= COMPLEX by VALUED_0:def_1; ( support b c= dom b & rng (canFS (support b)) = support b ) by FUNCT_2:def_3, PRE_POLY:37; then dom (b * (canFS (support b))) = dom (canFS (support b)) by RELAT_1:27; then dom (b * (canFS (support b))) = Seg (len (canFS (support b))) by FINSEQ_1:def_3; then b * (canFS (support b)) is FinSequence by FINSEQ_1:def_2; then reconsider f = b * (canFS (support b)) as FinSequence of COMPLEX by A1, FINSEQ_1:def_4; take Product f ; ::_thesis: ex f being FinSequence of COMPLEX st ( Product f = Product f & f = b * (canFS (support b)) ) thus ex f being FinSequence of COMPLEX st ( Product f = Product f & f = b * (canFS (support b)) ) ; ::_thesis: verum end; uniqueness for b1, b2 being complex number st ex f being FinSequence of COMPLEX st ( b1 = Product f & f = b * (canFS (support b)) ) & ex f being FinSequence of COMPLEX st ( b2 = Product f & f = b * (canFS (support b)) ) holds b1 = b2 ; end; :: deftheorem Def5 defines Product NAT_3:def_5_:_ for A being set for b being complex-yielding finite-support ManySortedSet of A for b3 being complex number holds ( b3 = Product b iff ex f being FinSequence of COMPLEX st ( b3 = Product f & f = b * (canFS (support b)) ) ); definition let A be set ; let b be bag of A; :: original: Product redefine func Product b -> Element of NAT ; coherence Product b is Element of NAT proof consider f being FinSequence of COMPLEX such that A1: Product b = Product f and A2: f = b * (canFS (support b)) by Def5; ( rng b c= NAT & rng f c= rng b ) by A2, RELAT_1:26, VALUED_0:def_6; then rng f c= NAT by XBOOLE_1:1; then reconsider g = f as FinSequence of NAT by FINSEQ_1:def_4; Product g in NAT ; hence Product b is Element of NAT by A1; ::_thesis: verum end; end; theorem Th19: :: NAT_3:19 for X being set for a, b being bag of X st support a misses support b holds Product (a + b) = (Product a) * (Product b) proof let X be set ; ::_thesis: for a, b being bag of X st support a misses support b holds Product (a + b) = (Product a) * (Product b) let a, b be bag of X; ::_thesis: ( support a misses support b implies Product (a + b) = (Product a) * (Product b) ) set ab = a + b; set Pa = Product a; set Pb = Product b; set Pab = Product (a + b); set sab = support (a + b); set sa = support a; set sb = support b; set ca = canFS (support a); set cb = canFS (support b); set cg = (canFS (support a)) ^ (canFS (support b)); set cf = canFS (support (a + b)); set p = (((canFS (support a)) ^ (canFS (support b))) ") * (canFS (support (a + b))); A1: rng (canFS (support (a + b))) = support (a + b) by FUNCT_2:def_3; assume support a misses support b ; ::_thesis: Product (a + b) = (Product a) * (Product b) then A2: (support a) /\ (support b) = {} by XBOOLE_0:def_7; A3: rng (canFS (support a)) = support a by FUNCT_2:def_3; A4: support (a + b) = (support a) \/ (support b) by PRE_POLY:38; A5: rng (canFS (support b)) = support b by FUNCT_2:def_3; then A6: rng ((canFS (support a)) ^ (canFS (support b))) = support (a + b) by A4, A3, FINSEQ_1:31; A7: ( len (canFS (support b)) = card (support b) & len (canFS (support a)) = card (support a) ) by UPROOTS:3; then A8: len ((canFS (support a)) ^ (canFS (support b))) = ((card (support a)) + (card (support b))) - (card {}) by FINSEQ_1:22 .= card (support (a + b)) by A2, A4, CARD_2:45 ; then A9: (canFS (support a)) ^ (canFS (support b)) is one-to-one by A6, FINSEQ_4:62; then A10: dom (((canFS (support a)) ^ (canFS (support b))) ") = support (a + b) by A6, FUNCT_1:33; then A11: rng ((((canFS (support a)) ^ (canFS (support b))) ") * (canFS (support (a + b)))) = rng (((canFS (support a)) ^ (canFS (support b))) ") by A1, RELAT_1:28; dom ((canFS (support a)) ^ (canFS (support b))) = Seg (card (support (a + b))) by A8, FINSEQ_1:def_3; then A12: rng (((canFS (support a)) ^ (canFS (support b))) ") = Seg (card (support (a + b))) by A9, FUNCT_1:33; consider fa being FinSequence of COMPLEX such that A13: Product a = Product fa and A14: fa = a * (canFS (support a)) by Def5; consider fb being FinSequence of COMPLEX such that A15: Product b = Product fb and A16: fb = b * (canFS (support b)) by Def5; set g = fa ^ fb; consider f being FinSequence of COMPLEX such that A17: Product (a + b) = Product f and A18: f = (a + b) * (canFS (support (a + b))) by Def5; dom a = X by PARTFUN1:def_2; then A19: dom (canFS (support a)) = dom fa by A14, A3, RELAT_1:27; then A20: len (canFS (support a)) = len fa by FINSEQ_3:29; len (canFS (support (a + b))) = card (support (a + b)) by UPROOTS:3; then A21: dom (canFS (support (a + b))) = Seg (card (support (a + b))) by FINSEQ_1:def_3; then A22: dom ((((canFS (support a)) ^ (canFS (support b))) ") * (canFS (support (a + b)))) = Seg (card (support (a + b))) by A1, A10, RELAT_1:27; A23: dom (a + b) = X by PARTFUN1:def_2; then A24: dom f = Seg (card (support (a + b))) by A18, A21, A1, RELAT_1:27; dom b = X by PARTFUN1:def_2; then dom (canFS (support b)) = dom fb by A16, A5, RELAT_1:27; then A25: len (canFS (support b)) = len fb by FINSEQ_3:29; then len (fa ^ fb) = ((card (support a)) + (card (support b))) - (card {}) by A7, A20, FINSEQ_1:22 .= card (support (a + b)) by A2, A4, CARD_2:45 ; then A26: dom (fa ^ fb) = Seg (card (support (a + b))) by FINSEQ_1:def_3; then reconsider p = (((canFS (support a)) ^ (canFS (support b))) ") * (canFS (support (a + b))) as Function of (dom (fa ^ fb)),(dom (fa ^ fb)) by A12, A22, A11, FUNCT_2:1; p is onto by A12, A26, A11, FUNCT_2:def_3; then reconsider p = p as Permutation of (dom (fa ^ fb)) by A9; A27: dom ((fa ^ fb) * p) = Seg (card (support (a + b))) by A12, A22, A26, A11, RELAT_1:27; A28: len ((canFS (support a)) ^ (canFS (support b))) = (len (canFS (support a))) + (len (canFS (support b))) by FINSEQ_1:22; now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_((fa_^_fb)_*_p)_._x let x be set ; ::_thesis: ( x in dom f implies f . b1 = ((fa ^ fb) * p) . b1 ) set cgx = (((canFS (support a)) ^ (canFS (support b))) ") . ((canFS (support (a + b))) . x); assume A29: x in dom f ; ::_thesis: f . b1 = ((fa ^ fb) * p) . b1 then A30: ((fa ^ fb) * p) . x = (fa ^ fb) . (p . x) by A24, A27, FUNCT_1:12 .= (fa ^ fb) . ((((canFS (support a)) ^ (canFS (support b))) ") . ((canFS (support (a + b))) . x)) by A21, A24, A29, FUNCT_1:13 ; A31: (canFS (support (a + b))) . x in support (a + b) by A21, A1, A24, A29, FUNCT_1:3; then consider d being set such that A32: d in dom ((canFS (support a)) ^ (canFS (support b))) and A33: ((canFS (support a)) ^ (canFS (support b))) . d = (canFS (support (a + b))) . x by A6, FUNCT_1:def_3; (((canFS (support a)) ^ (canFS (support b))) ") . ((canFS (support (a + b))) . x) in Seg (card (support (a + b))) by A10, A12, A31, FUNCT_1:3; then reconsider cgx = (((canFS (support a)) ^ (canFS (support b))) ") . ((canFS (support (a + b))) . x) as Nat ; reconsider cgxN = cgx as Nat ; A34: cgx = d by A9, A32, A33, FUNCT_1:34; then A35: 1 <= cgxN by A32, FINSEQ_3:25; A36: cgxN <= (len fa) + (len fb) by A20, A25, A28, A32, A34, FINSEQ_3:25; percases ( (canFS (support (a + b))) . x in support a or (canFS (support (a + b))) . x in support b ) by A4, A31, XBOOLE_0:def_3; suppose (canFS (support (a + b))) . x in support a ; ::_thesis: f . b1 = ((fa ^ fb) * p) . b1 then A37: not (canFS (support (a + b))) . x in support b by A2, XBOOLE_0:def_4; now__::_thesis:_not_len_fa_<_cgx A38: cgx - (len (canFS (support a))) <= ((len (canFS (support a))) + (len (canFS (support b)))) - (len (canFS (support a))) by A20, A25, A36, XREAL_1:9; assume len fa < cgx ; ::_thesis: contradiction then A39: (len fa) + 1 <= cgx by NAT_1:13; then A40: ((len (canFS (support a))) + 1) - (len (canFS (support a))) <= cgx - (len (canFS (support a))) by A20, XREAL_1:9; then cgx - (len (canFS (support a))) is Element of NAT by INT_1:3; then A41: cgx - (len (canFS (support a))) in dom (canFS (support b)) by A40, A38, FINSEQ_3:25; ((canFS (support a)) ^ (canFS (support b))) . cgxN = (canFS (support b)) . (cgx - (len (canFS (support a)))) by A20, A25, A36, A39, FINSEQ_1:23; hence contradiction by A5, A33, A34, A37, A41, FUNCT_1:3; ::_thesis: verum end; then A42: cgxN in dom fa by A35, FINSEQ_3:25; then A43: ((canFS (support a)) ^ (canFS (support b))) . cgx = (canFS (support a)) . cgx by A19, FINSEQ_1:def_7; A44: (fa ^ fb) . cgx = fa . cgxN by A42, FINSEQ_1:def_7 .= a . ((canFS (support (a + b))) . x) by A14, A19, A33, A34, A42, A43, FUNCT_1:13 ; thus f . x = (a + b) . ((canFS (support (a + b))) . x) by A18, A29, FUNCT_1:12 .= (a . ((canFS (support (a + b))) . x)) + (b . ((canFS (support (a + b))) . x)) by PRE_POLY:def_5 .= (a . ((canFS (support (a + b))) . x)) + 0 by A37, PRE_POLY:def_7 .= ((fa ^ fb) * p) . x by A30, A44 ; ::_thesis: verum end; supposeA45: (canFS (support (a + b))) . x in support b ; ::_thesis: f . b1 = ((fa ^ fb) * p) . b1 A46: now__::_thesis:_not_(len_fa)_+_1_>_cgx assume (len fa) + 1 > cgx ; ::_thesis: contradiction then cgx <= len fa by NAT_1:13; then A47: cgx in dom (canFS (support a)) by A19, A35, FINSEQ_3:25; then (canFS (support a)) . cgx in support a by A3, FUNCT_1:3; then ((canFS (support a)) ^ (canFS (support b))) . cgxN in support a by A47, FINSEQ_1:def_7; hence contradiction by A2, A33, A34, A45, XBOOLE_0:def_4; ::_thesis: verum end; then A48: ((canFS (support a)) ^ (canFS (support b))) . cgx = (canFS (support b)) . (cgx - (len (canFS (support a)))) by A20, A25, A36, FINSEQ_1:23; A49: cgx - (len (canFS (support a))) <= ((len (canFS (support a))) + (len (canFS (support b)))) - (len (canFS (support a))) by A20, A25, A36, XREAL_1:9; A50: ((len (canFS (support a))) + 1) - (len (canFS (support a))) <= cgx - (len (canFS (support a))) by A20, A46, XREAL_1:9; then cgxN - (len (canFS (support a))) in NAT by INT_1:3; then A51: cgxN - (len (canFS (support a))) in dom (canFS (support b)) by A49, A50, FINSEQ_3:25; A52: (fa ^ fb) . cgx = fb . (cgxN - (len fa)) by A36, A46, FINSEQ_1:23 .= b . ((canFS (support (a + b))) . x) by A16, A20, A33, A34, A48, A51, FUNCT_1:13 ; A53: not (canFS (support (a + b))) . x in support a by A2, A45, XBOOLE_0:def_4; thus f . x = (a + b) . ((canFS (support (a + b))) . x) by A18, A29, FUNCT_1:12 .= (a . ((canFS (support (a + b))) . x)) + (b . ((canFS (support (a + b))) . x)) by PRE_POLY:def_5 .= 0 + (b . ((canFS (support (a + b))) . x)) by A53, PRE_POLY:def_7 .= ((fa ^ fb) * p) . x by A30, A52 ; ::_thesis: verum end; end; end; then A54: f = (fa ^ fb) * p by A18, A21, A1, A23, A27, FUNCT_1:2, RELAT_1:27; thus Product (a + b) = multcomplex $$ f by A17, RVSUM_1:def_13 .= multcomplex $$ (fa ^ fb) by A54, FINSOP_1:7 .= Product (fa ^ fb) by RVSUM_1:def_13 .= (Product a) * (Product b) by A13, A15, RVSUM_1:97 ; ::_thesis: verum end; definition let X be set ; let b be real-valued ManySortedSet of X; let n be non empty Nat; funcb |^ n -> ManySortedSet of X means :Def6: :: NAT_3:def 6 ( support it = support b & ( for i being set holds it . i = (b . i) |^ n ) ); existence ex b1 being ManySortedSet of X st ( support b1 = support b & ( for i being set holds b1 . i = (b . i) |^ n ) ) proof reconsider n1 = n as Element of NAT by ORDINAL1:def_12; deffunc H1( Element of X) -> Element of REAL = (b . $1) |^ n; defpred S1[ set , set ] means ex a being Element of X st ( a = $1 & $2 = H1(a) ); A1: n1 >= 1 by NAT_1:53; A2: for e being set st e in X holds ex u being set st S1[e,u] proof let e be set ; ::_thesis: ( e in X implies ex u being set st S1[e,u] ) assume e in X ; ::_thesis: ex u being set st S1[e,u] then reconsider f = e as Element of X ; take H1(f) ; ::_thesis: S1[e,H1(f)] take f ; ::_thesis: ( f = e & H1(f) = H1(f) ) thus ( f = e & H1(f) = H1(f) ) ; ::_thesis: verum end; consider f being Function such that A3: dom f = X and A4: for x being set st x in X holds S1[x,f . x] from CLASSES1:sch_1(A2); reconsider f = f as ManySortedSet of X by A3, PARTFUN1:def_2, RELAT_1:def_18; take f ; ::_thesis: ( support f = support b & ( for i being set holds f . i = (b . i) |^ n ) ) A5: dom b = X by PARTFUN1:def_2; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_support_f_implies_x_in_support_b_)_&_(_x_in_support_b_implies_x_in_support_f_)_) let x be set ; ::_thesis: ( ( x in support f implies x in support b ) & ( x in support b implies x in support f ) ) hereby ::_thesis: ( x in support b implies x in support f ) assume A6: x in support f ; ::_thesis: x in support b assume not x in support b ; ::_thesis: contradiction then b . x = 0 by PRE_POLY:def_7; then A7: (b . x) |^ n = 0 by A1, NEWTON:11; support f c= X by A3, PRE_POLY:37; then S1[x,f . x] by A4, A6; hence contradiction by A6, A7, PRE_POLY:def_7; ::_thesis: verum end; A8: now__::_thesis:_f_._x_=_(b_._x)_|^_n1 percases ( x in X or not x in X ) ; suppose x in X ; ::_thesis: f . x = (b . x) |^ n1 then S1[x,f . x] by A4; hence f . x = (b . x) |^ n1 ; ::_thesis: verum end; supposeA9: not x in X ; ::_thesis: f . x = (b . x) |^ n1 hence f . x = 0 by A3, FUNCT_1:def_2 .= 0 |^ n1 by A1, NEWTON:11 .= (b . x) |^ n1 by A5, A9, FUNCT_1:def_2 ; ::_thesis: verum end; end; end; assume x in support b ; ::_thesis: x in support f then b . x <> 0 by PRE_POLY:def_7; then f . x <> 0 by A8, CARD_4:3; hence x in support f by PRE_POLY:def_7; ::_thesis: verum end; hence support f = support b by TARSKI:1; ::_thesis: for i being set holds f . i = (b . i) |^ n let i be set ; ::_thesis: f . i = (b . i) |^ n percases ( i in X or not i in X ) ; suppose i in X ; ::_thesis: f . i = (b . i) |^ n then S1[i,f . i] by A4; hence f . i = (b . i) |^ n ; ::_thesis: verum end; supposeA10: not i in X ; ::_thesis: f . i = (b . i) |^ n hence f . i = 0 by A3, FUNCT_1:def_2 .= 0 |^ n by A1, NEWTON:11 .= (b . i) |^ n by A5, A10, FUNCT_1:def_2 ; ::_thesis: verum end; end; end; uniqueness for b1, b2 being ManySortedSet of X st support b1 = support b & ( for i being set holds b1 . i = (b . i) |^ n ) & support b2 = support b & ( for i being set holds b2 . i = (b . i) |^ n ) holds b1 = b2 proof let it1, it2 be ManySortedSet of X; ::_thesis: ( support it1 = support b & ( for i being set holds it1 . i = (b . i) |^ n ) & support it2 = support b & ( for i being set holds it2 . i = (b . i) |^ n ) implies it1 = it2 ) assume that support it1 = support b and A11: for i being set holds it1 . i = (b . i) |^ n and support it2 = support b and A12: for i being set holds it2 . i = (b . i) |^ n ; ::_thesis: it1 = it2 now__::_thesis:_for_x_being_set_st_x_in_X_holds_ it1_._x_=_it2_._x let x be set ; ::_thesis: ( x in X implies it1 . x = it2 . x ) assume x in X ; ::_thesis: it1 . x = it2 . x thus it1 . x = (b . x) |^ n by A11 .= it2 . x by A12 ; ::_thesis: verum end; hence it1 = it2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def6 defines |^ NAT_3:def_6_:_ for X being set for b being real-valued ManySortedSet of X for n being non empty Nat for b4 being ManySortedSet of X holds ( b4 = b |^ n iff ( support b4 = support b & ( for i being set holds b4 . i = (b . i) |^ n ) ) ); registration let X be set ; let b be natural-valued ManySortedSet of X; let n be non empty Nat; clusterb |^ n -> natural-valued ; coherence b |^ n is natural-valued proof let x be set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in dom (b |^ n) or (b |^ n) . x is natural ) set f = b |^ n; assume x in dom (b |^ n) ; ::_thesis: (b |^ n) . x is natural (b |^ n) . x = (b . x) |^ n by Def6; hence (b |^ n) . x is natural ; ::_thesis: verum end; end; registration let X be set ; let b be real-valued finite-support ManySortedSet of X; let n be non empty Nat; clusterb |^ n -> finite-support ; coherence b |^ n is finite-support proof support (b |^ n) = support b by Def6; hence support (b |^ n) is finite ; :: according to PRE_POLY:def_8 ::_thesis: verum end; end; theorem Th20: :: NAT_3:20 for A being set holds Product (EmptyBag A) = 1 proof let A be set ; ::_thesis: Product (EmptyBag A) = 1 set b = EmptyBag A; set cS = canFS (support (EmptyBag A)); support (EmptyBag A) = {} by BAGORDER:18; then (EmptyBag A) * (canFS (support (EmptyBag A))) = <*> COMPLEX ; hence Product (EmptyBag A) = 1 by Def5, RVSUM_1:94; ::_thesis: verum end; begin definition let n, d be Nat; assume that B1: d <> 1 and B2: n <> 0 ; funcd |-count n -> Nat means :Def7: :: NAT_3:def 7 ( d |^ it divides n & not d |^ (it + 1) divides n ); existence ex b1 being Nat st ( d |^ b1 divides n & not d |^ (b1 + 1) divides n ) proof reconsider n1 = n as Element of NAT by ORDINAL1:def_12; percases ( d = 0 or d <> 0 ) ; supposeA1: d = 0 ; ::_thesis: ex b1 being Nat st ( d |^ b1 divides n & not d |^ (b1 + 1) divides n ) take 0 ; ::_thesis: ( d |^ 0 divides n & not d |^ (0 + 1) divides n ) 0 |^ 0 = 1 by NEWTON:4; hence d |^ 0 divides n by A1, NAT_D:6; ::_thesis: not d |^ (0 + 1) divides n not 0 divides n1 by B2, INT_2:3; hence not d |^ (0 + 1) divides n by A1, NEWTON:11; ::_thesis: verum end; supposeA2: d <> 0 ; ::_thesis: ex b1 being Nat st ( d |^ b1 divides n & not d |^ (b1 + 1) divides n ) defpred S1[ Nat] means d |^ $1 divides n; A3: for k being Nat st S1[k] holds k <= n1 proof let k be Nat; ::_thesis: ( S1[k] implies k <= n1 ) assume S1[k] ; ::_thesis: k <= n1 then A4: d |^ k <= n by B2, NAT_D:7; k <= d |^ k by B1, A2, Th2, NAT_1:25; hence k <= n1 by A4, XXREAL_0:2; ::_thesis: verum end; A5: ex k being Nat st S1[k] proof take 0 ; ::_thesis: S1[ 0 ] d |^ 0 = 1 by NEWTON:4; hence S1[ 0 ] by NAT_D:6; ::_thesis: verum end; consider k being Nat such that A6: ( S1[k] & ( for n being Nat st S1[n] holds n <= k ) ) from NAT_1:sch_6(A3, A5); take k ; ::_thesis: ( d |^ k divides n & not d |^ (k + 1) divides n ) k + 0 < k + 1 by XREAL_1:6; hence ( d |^ k divides n & not d |^ (k + 1) divides n ) by A6; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Nat st d |^ b1 divides n & not d |^ (b1 + 1) divides n & d |^ b2 divides n & not d |^ (b2 + 1) divides n holds b1 = b2 proof reconsider d1 = d as Element of NAT by ORDINAL1:def_12; let a, b be Nat; ::_thesis: ( d |^ a divides n & not d |^ (a + 1) divides n & d |^ b divides n & not d |^ (b + 1) divides n implies a = b ) assume that A7: d |^ a divides n and A8: ( not d |^ (a + 1) divides n & d |^ b divides n ) and A9: not d |^ (b + 1) divides n and A10: a <> b ; ::_thesis: contradiction reconsider a = a, b = b as Element of NAT by ORDINAL1:def_12; percases ( a < b or b < a ) by A10, XXREAL_0:1; supposeA11: a < b ; ::_thesis: contradiction then consider x being Nat such that A12: a + x = b by NAT_1:10; reconsider x = x as Element of NAT by ORDINAL1:def_12; now__::_thesis:_not_0_+_1_>_x assume 0 + 1 > x ; ::_thesis: contradiction then x = 0 by NAT_1:13; hence contradiction by A11, A12; ::_thesis: verum end; then a + 1 <= a + x by XREAL_1:6; then d1 |^ (a + 1) divides d1 |^ (a + x) by NEWTON:89; hence contradiction by A8, A12, NAT_D:4; ::_thesis: verum end; supposeA13: b < a ; ::_thesis: contradiction then consider x being Nat such that A14: b + x = a by NAT_1:10; reconsider x = x as Element of NAT by ORDINAL1:def_12; now__::_thesis:_not_0_+_1_>_x assume 0 + 1 > x ; ::_thesis: contradiction then x = 0 by NAT_1:13; hence contradiction by A13, A14; ::_thesis: verum end; then b + 1 <= b + x by XREAL_1:6; then d1 |^ (b + 1) divides d1 |^ (b + x) by NEWTON:89; hence contradiction by A7, A9, A14, NAT_D:4; ::_thesis: verum end; end; end; end; :: deftheorem Def7 defines |-count NAT_3:def_7_:_ for n, d being Nat st d <> 1 & n <> 0 holds for b3 being Nat holds ( b3 = d |-count n iff ( d |^ b3 divides n & not d |^ (b3 + 1) divides n ) ); definition let n, d be Nat; :: original: |-count redefine funcd |-count n -> Element of NAT ; coherence d |-count n is Element of NAT by ORDINAL1:def_12; end; theorem Th21: :: NAT_3:21 for n being Nat st n <> 1 holds n |-count 1 = 0 proof let n be Nat; ::_thesis: ( n <> 1 implies n |-count 1 = 0 ) assume A1: 1 <> n ; ::_thesis: n |-count 1 = 0 A2: now__::_thesis:_not_n_|^_(0_+_1)_divides_1 assume A3: n |^ (0 + 1) divides 1 ; ::_thesis: contradiction then n |^ 1 <= 1 by NAT_D:7; then n <= 1 by NEWTON:5; then n = 0 by A1, NAT_1:25; then 0 divides 1 by A3, NEWTON:5; hence contradiction by INT_2:3; ::_thesis: verum end; n |^ 0 divides 1 by NEWTON:4; hence n |-count 1 = 0 by A1, A2, Def7; ::_thesis: verum end; theorem :: NAT_3:22 for n being Nat st 1 < n holds n |-count n = 1 proof let n be Nat; ::_thesis: ( 1 < n implies n |-count n = 1 ) assume A1: 1 < n ; ::_thesis: n |-count n = 1 A2: now__::_thesis:_not_n_|^_(1_+_1)_divides_n assume n |^ (1 + 1) divides n ; ::_thesis: contradiction then n |^ 2 <= n by A1, NAT_D:7; hence contradiction by A1, PREPOWER:13; ::_thesis: verum end; n |^ 1 divides n by NEWTON:5; hence n |-count n = 1 by A1, A2, Def7; ::_thesis: verum end; theorem Th23: :: NAT_3:23 for b, a being Nat st b <> 0 & b < a & a <> 1 holds a |-count b = 0 proof let b, a be Nat; ::_thesis: ( b <> 0 & b < a & a <> 1 implies a |-count b = 0 ) assume that A1: b <> 0 and A2: b < a and A3: a <> 1 ; ::_thesis: a |-count b = 0 a |^ 0 = 1 by NEWTON:4; then A4: a |^ 0 divides b by NAT_D:6; a |^ 1 = a by NEWTON:5; then not a |^ (0 + 1) divides b by A1, A2, NAT_D:7; hence a |-count b = 0 by A1, A3, A4, Def7; ::_thesis: verum end; theorem :: NAT_3:24 for a being Nat for p being Prime st a <> 1 & a <> p holds a |-count p = 0 proof let a be Nat; ::_thesis: for p being Prime st a <> 1 & a <> p holds a |-count p = 0 let p be Prime; ::_thesis: ( a <> 1 & a <> p implies a |-count p = 0 ) assume that A1: a <> 1 and A2: a <> p ; ::_thesis: a |-count p = 0 a |^ 0 = 1 by NEWTON:4; then A3: a |^ 0 divides p by NAT_D:6; a |^ 1 = a by NEWTON:5; then not a |^ (0 + 1) divides p by A1, A2, INT_2:def_4; hence a |-count p = 0 by A1, A3, Def7; ::_thesis: verum end; theorem Th25: :: NAT_3:25 for b, a being Nat st 1 < b holds b |-count (b |^ a) = a proof let b, a be Nat; ::_thesis: ( 1 < b implies b |-count (b |^ a) = a ) reconsider a = a as Element of NAT by ORDINAL1:def_12; assume A1: b > 1 ; ::_thesis: b |-count (b |^ a) = a then reconsider b = b as non empty Element of NAT by ORDINAL1:def_12; now__::_thesis:_not_b_|^_(a_+_1)_divides_b_|^_a b |^ a divides b |^ (a + 1) by NAT_1:11, NEWTON:89; then A2: b |^ a <= b |^ (a + 1) by NAT_D:7; assume b |^ (a + 1) divides b |^ a ; ::_thesis: contradiction then b |^ (a + 1) <= b |^ a by NAT_D:7; then b |^ a = b |^ (a + 1) by A2, XXREAL_0:1; then a + 0 = a + 1 by A1, PEPIN:30; hence contradiction ; ::_thesis: verum end; hence b |-count (b |^ a) = a by A1, Def7; ::_thesis: verum end; theorem Th26: :: NAT_3:26 for b, a being Nat st b <> 1 & a <> 0 & b divides b |^ (b |-count a) holds b divides a proof let b, a be Nat; ::_thesis: ( b <> 1 & a <> 0 & b divides b |^ (b |-count a) implies b divides a ) assume that A1: ( b <> 1 & a <> 0 ) and A2: b divides b |^ (b |-count a) ; ::_thesis: b divides a b |^ (b |-count a) divides a by A1, Def7; hence b divides a by A2, NAT_D:4; ::_thesis: verum end; theorem Th27: :: NAT_3:27 for b, a being Nat st b <> 1 holds ( ( a <> 0 & b |-count a = 0 ) iff not b divides a ) proof let b, a be Nat; ::_thesis: ( b <> 1 implies ( ( a <> 0 & b |-count a = 0 ) iff not b divides a ) ) 1 divides a by NAT_D:6; then A1: b |^ 0 divides a by NEWTON:4; assume A2: b <> 1 ; ::_thesis: ( ( a <> 0 & b |-count a = 0 ) iff not b divides a ) thus ( a <> 0 & b |-count a = 0 implies not b divides a ) ::_thesis: ( not b divides a implies ( a <> 0 & b |-count a = 0 ) ) proof assume that A3: ( a <> 0 & b |-count a = 0 ) and A4: b divides a ; ::_thesis: contradiction not b |^ (0 + 1) divides a by A2, A3, Def7; hence contradiction by A4, NEWTON:5; ::_thesis: verum end; assume not b divides a ; ::_thesis: ( a <> 0 & b |-count a = 0 ) then ( not b |^ (0 + 1) divides a & a <> 0 ) by NAT_D:6, NEWTON:5; hence ( a <> 0 & b |-count a = 0 ) by A2, A1, Def7; ::_thesis: verum end; theorem Th28: :: NAT_3:28 for p being Prime for a, b being non empty Nat holds p |-count (a * b) = (p |-count a) + (p |-count b) proof let p be Prime; ::_thesis: for a, b being non empty Nat holds p |-count (a * b) = (p |-count a) + (p |-count b) let a, b be non empty Nat; ::_thesis: p |-count (a * b) = (p |-count a) + (p |-count b) set x = p |-count a; set y = p |-count b; A1: p <> 1 by INT_2:def_4; then A2: p |^ (p |-count b) divides b by Def7; A3: p |^ (p |-count a) divides a by A1, Def7; A4: now__::_thesis:_not_p_|^_(((p_|-count_a)_+_(p_|-count_b))_+_1)_divides_a_*_b assume p |^ (((p |-count a) + (p |-count b)) + 1) divides a * b ; ::_thesis: contradiction then consider v being Nat such that A5: a * b = (p |^ (((p |-count a) + (p |-count b)) + 1)) * v by NAT_D:def_3; p |^ (((p |-count a) + (p |-count b)) + 1) = (p |^ ((p |-count a) + (p |-count b))) * p by NEWTON:6; then A6: a * b = (p |^ ((p |-count a) + (p |-count b))) * (p * v) by A5; consider t being Nat such that A7: a = (p |^ (p |-count a)) * t by A3, NAT_D:def_3; A8: not p |^ ((p |-count a) + 1) divides a by A1, Def7; A9: not p |^ ((p |-count b) + 1) divides b by A1, Def7; consider u being Nat such that A10: b = (p |^ (p |-count b)) * u by A2, NAT_D:def_3; a * b = (((p |^ (p |-count a)) * (p |^ (p |-count b))) * t) * u by A7, A10 .= ((p |^ ((p |-count a) + (p |-count b))) * t) * u by NEWTON:8 .= (p |^ ((p |-count a) + (p |-count b))) * (t * u) ; then p * v = t * u by A6, XCMPLX_1:5; then A11: p divides t * u by NAT_D:def_3; percases ( p divides t or p divides u ) by A11, NEWTON:80; suppose p divides t ; ::_thesis: contradiction then consider t1 being Nat such that A12: t = p * t1 by NAT_D:def_3; a = ((p |^ (p |-count a)) * p) * t1 by A7, A12 .= (p |^ ((p |-count a) + 1)) * t1 by NEWTON:6 ; hence contradiction by A8, NAT_D:def_3; ::_thesis: verum end; suppose p divides u ; ::_thesis: contradiction then consider t1 being Nat such that A13: u = p * t1 by NAT_D:def_3; b = ((p |^ (p |-count b)) * p) * t1 by A10, A13 .= (p |^ ((p |-count b) + 1)) * t1 by NEWTON:6 ; hence contradiction by A9, NAT_D:def_3; ::_thesis: verum end; end; end; p |^ ((p |-count a) + (p |-count b)) = (p |^ (p |-count a)) * (p |^ (p |-count b)) by NEWTON:8; then p |^ ((p |-count a) + (p |-count b)) divides a * b by A3, A2, Th1; hence p |-count (a * b) = (p |-count a) + (p |-count b) by A1, A4, Def7; ::_thesis: verum end; theorem Th29: :: NAT_3:29 for p being Prime for a, b being non empty Nat holds p |^ (p |-count (a * b)) = (p |^ (p |-count a)) * (p |^ (p |-count b)) proof let p be Prime; ::_thesis: for a, b being non empty Nat holds p |^ (p |-count (a * b)) = (p |^ (p |-count a)) * (p |^ (p |-count b)) let a, b be non empty Nat; ::_thesis: p |^ (p |-count (a * b)) = (p |^ (p |-count a)) * (p |^ (p |-count b)) set x = p |-count a; set y = p |-count b; thus p |^ (p |-count (a * b)) = p |^ ((p |-count a) + (p |-count b)) by Th28 .= (p |^ (p |-count a)) * (p |^ (p |-count b)) by NEWTON:8 ; ::_thesis: verum end; theorem Th30: :: NAT_3:30 for p being Prime for a, b being non empty Nat st b divides a holds p |-count b <= p |-count a proof let p be Prime; ::_thesis: for a, b being non empty Nat st b divides a holds p |-count b <= p |-count a let a, b be non empty Nat; ::_thesis: ( b divides a implies p |-count b <= p |-count a ) set x = p |-count a; set y = p |-count b; set z = p |-count (a div b); 0 + 1 <= p |^ (p |-count (a div b)) by NAT_1:13; then A1: 1 * (p |^ (p |-count b)) <= (p |^ (p |-count (a div b))) * (p |^ (p |-count b)) by XREAL_1:66; assume b divides a ; ::_thesis: p |-count b <= p |-count a then A2: a = b * (a div b) by NAT_D:3; then a div b <> 0 ; then ( p > 1 & p |^ (p |-count b) <= p |^ (p |-count a) ) by A2, A1, Th29, INT_2:def_4; hence p |-count b <= p |-count a by PEPIN:66; ::_thesis: verum end; theorem Th31: :: NAT_3:31 for p being Prime for a, b being non empty Nat st b divides a holds p |-count (a div b) = (p |-count a) -' (p |-count b) proof let p be Prime; ::_thesis: for a, b being non empty Nat st b divides a holds p |-count (a div b) = (p |-count a) -' (p |-count b) let a, b be non empty Nat; ::_thesis: ( b divides a implies p |-count (a div b) = (p |-count a) -' (p |-count b) ) set x = p |-count a; set y = p |-count b; set z = p |-count (a div b); assume A1: b divides a ; ::_thesis: p |-count (a div b) = (p |-count a) -' (p |-count b) then a = b * (a div b) by NAT_D:3; then a div b <> 0 ; then p |-count (b * (a div b)) = (p |-count b) + (p |-count (a div b)) by Th28; then A2: (p |-count (a div b)) + (p |-count b) = (p |-count a) + 0 by A1, NAT_D:3; p |-count b <= p |-count a by A1, Th30; then (p |-count b) - (p |-count b) <= (p |-count a) - (p |-count b) by XREAL_1:13; hence p |-count (a div b) = (p |-count a) -' (p |-count b) by A2, XREAL_0:def_2; ::_thesis: verum end; theorem Th32: :: NAT_3:32 for b being Nat for p being Prime for a being non empty Nat holds p |-count (a |^ b) = b * (p |-count a) proof let b be Nat; ::_thesis: for p being Prime for a being non empty Nat holds p |-count (a |^ b) = b * (p |-count a) let p be Prime; ::_thesis: for a being non empty Nat holds p |-count (a |^ b) = b * (p |-count a) let a be non empty Nat; ::_thesis: p |-count (a |^ b) = b * (p |-count a) A1: p <> 1 by INT_2:def_4; defpred S1[ Nat] means p |-count (a |^ $1) = $1 * (p |-count a); A2: for x being Nat st S1[x] holds S1[x + 1] proof let x be Nat; ::_thesis: ( S1[x] implies S1[x + 1] ) assume A3: S1[x] ; ::_thesis: S1[x + 1] thus p |-count (a |^ (x + 1)) = p |-count ((a |^ x) * a) by NEWTON:6 .= (x * (p |-count a)) + (1 * (p |-count a)) by A3, Th28 .= (x + 1) * (p |-count a) ; ::_thesis: verum end; p |-count (a |^ 0) = p |-count 1 by NEWTON:4 .= 0 * (p |-count a) by A1, Th21 ; then A4: S1[ 0 ] ; for x being Nat holds S1[x] from NAT_1:sch_2(A4, A2); hence p |-count (a |^ b) = b * (p |-count a) ; ::_thesis: verum end; begin definition let n be Nat; func prime_exponents n -> ManySortedSet of SetPrimes means :Def8: :: NAT_3:def 8 for p being Prime holds it . p = p |-count n; existence ex b1 being ManySortedSet of SetPrimes st for p being Prime holds b1 . p = p |-count n proof deffunc H1( Nat) -> Element of NAT = $1 |-count n; defpred S1[ set , set ] means ex w being Nat st ( w = $1 & $2 = H1(w) ); A1: for i being set st i in SetPrimes holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in SetPrimes implies ex j being set st S1[i,j] ) assume i in SetPrimes ; ::_thesis: ex j being set st S1[i,j] then reconsider i = i as prime Element of NAT by NEWTON:def_6; take H1(i) ; ::_thesis: S1[i,H1(i)] take i ; ::_thesis: ( i = i & H1(i) = H1(i) ) thus ( i = i & H1(i) = H1(i) ) ; ::_thesis: verum end; consider f being ManySortedSet of SetPrimes such that A2: for i being set st i in SetPrimes holds S1[i,f . i] from PBOOLE:sch_3(A1); take f ; ::_thesis: for p being Prime holds f . p = p |-count n let i be Prime; ::_thesis: f . i = i |-count n i in SetPrimes by NEWTON:def_6; then S1[i,f . i] by A2; hence f . i = i |-count n ; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of SetPrimes st ( for p being Prime holds b1 . p = p |-count n ) & ( for p being Prime holds b2 . p = p |-count n ) holds b1 = b2 proof let f, g be ManySortedSet of SetPrimes ; ::_thesis: ( ( for p being Prime holds f . p = p |-count n ) & ( for p being Prime holds g . p = p |-count n ) implies f = g ) assume that A3: for i being Prime holds f . i = i |-count n and A4: for i being Prime holds g . i = i |-count n ; ::_thesis: f = g now__::_thesis:_for_i_being_set_st_i_in_SetPrimes_holds_ f_._i_=_g_._i let i be set ; ::_thesis: ( i in SetPrimes implies f . i = g . i ) assume i in SetPrimes ; ::_thesis: f . i = g . i then reconsider a = i as prime Element of NAT by NEWTON:def_6; thus f . i = a |-count n by A3 .= g . i by A4 ; ::_thesis: verum end; hence f = g by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def8 defines prime_exponents NAT_3:def_8_:_ for n being Nat for b2 being ManySortedSet of SetPrimes holds ( b2 = prime_exponents n iff for p being Prime holds b2 . p = p |-count n ); notation let n be Nat; synonym pfexp n for prime_exponents n; end; theorem Th33: :: NAT_3:33 for n being Nat for x being set st x in dom (pfexp n) holds x is Prime proof let n be Nat; ::_thesis: for x being set st x in dom (pfexp n) holds x is Prime let x be set ; ::_thesis: ( x in dom (pfexp n) implies x is Prime ) assume x in dom (pfexp n) ; ::_thesis: x is Prime then x in SetPrimes by PARTFUN1:def_2; hence x is Prime by NEWTON:def_6; ::_thesis: verum end; theorem Th34: :: NAT_3:34 for n being Nat for x being set st x in support (pfexp n) holds x is Prime proof let n be Nat; ::_thesis: for x being set st x in support (pfexp n) holds x is Prime let x be set ; ::_thesis: ( x in support (pfexp n) implies x is Prime ) set f = pfexp n; A1: support (pfexp n) c= dom (pfexp n) by PRE_POLY:37; assume x in support (pfexp n) ; ::_thesis: x is Prime hence x is Prime by A1, Th33; ::_thesis: verum end; theorem Th35: :: NAT_3:35 for a, n being Nat st a > n & n <> 0 holds (pfexp n) . a = 0 proof let a, n be Nat; ::_thesis: ( a > n & n <> 0 implies (pfexp n) . a = 0 ) assume A1: ( a > n & n <> 0 ) ; ::_thesis: (pfexp n) . a = 0 reconsider a = a as Element of NAT by ORDINAL1:def_12; percases ( not a is prime or a is prime ) ; suppose not a is prime ; ::_thesis: (pfexp n) . a = 0 then not a in dom (pfexp n) by Th33; hence (pfexp n) . a = 0 by FUNCT_1:def_2; ::_thesis: verum end; supposeA2: a is prime ; ::_thesis: (pfexp n) . a = 0 then a <> 1 by INT_2:def_4; then a |-count n = 0 by A1, Th23; hence (pfexp n) . a = 0 by A2, Def8; ::_thesis: verum end; end; end; registration let n be Nat; cluster prime_exponents n -> natural-valued ; coherence pfexp n is natural-valued proof let x be set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in dom (pfexp n) or (pfexp n) . x is natural ) set f = pfexp n; assume x in dom (pfexp n) ; ::_thesis: (pfexp n) . x is natural then reconsider x = x as Prime by Th33; (pfexp n) . x = x |-count n by Def8; hence (pfexp n) . x is natural ; ::_thesis: verum end; end; theorem :: NAT_3:36 for a, b being Nat st a in support (pfexp b) holds a divides b proof let a, b be Nat; ::_thesis: ( a in support (pfexp b) implies a divides b ) set f = pfexp b; assume A1: a in support (pfexp b) ; ::_thesis: a divides b then reconsider a = a as Prime by Th34; A2: ( a <> 1 & (pfexp b) . a = a |-count b ) by Def8, INT_2:def_4; (pfexp b) . a <> 0 by A1, PRE_POLY:def_7; hence a divides b by A2, Th27; ::_thesis: verum end; theorem Th37: :: NAT_3:37 for b, a being Nat st not b is empty & a is Prime & a divides b holds a in support (pfexp b) proof let b, a be Nat; ::_thesis: ( not b is empty & a is Prime & a divides b implies a in support (pfexp b) ) assume that A1: not b is empty and A2: a is Prime and A3: a divides b ; ::_thesis: a in support (pfexp b) 1 < a by A2, INT_2:def_4; then A4: a |-count b <> 0 by A1, A3, Th27; (pfexp b) . a = a |-count b by A2, Def8; hence a in support (pfexp b) by A4, PRE_POLY:def_7; ::_thesis: verum end; registration let n be non empty Nat; cluster prime_exponents n -> finite-support ; coherence pfexp n is finite-support proof defpred S1[ Nat] means n is prime ; deffunc H1( set ) -> set = n; set f = pfexp n; reconsider n = n as Element of NAT by ORDINAL1:def_12; set A = { H1(i) where i is Element of NAT : ( 0 <= i & i <= n & S1[i] ) } ; A1: support (pfexp n) c= { H1(i) where i is Element of NAT : ( 0 <= i & i <= n & S1[i] ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (pfexp n) or x in { H1(i) where i is Element of NAT : ( 0 <= i & i <= n & S1[i] ) } ) assume A2: x in support (pfexp n) ; ::_thesis: x in { H1(i) where i is Element of NAT : ( 0 <= i & i <= n & S1[i] ) } then reconsider x = x as Prime by Th34; (pfexp n) . x <> 0 by A2, PRE_POLY:def_7; then ( x is prime Element of NAT & x <= n ) by Th35, ORDINAL1:def_12; hence x in { H1(i) where i is Element of NAT : ( 0 <= i & i <= n & S1[i] ) } ; ::_thesis: verum end; { H1(i) where i is Element of NAT : ( 0 <= i & i <= n & S1[i] ) } is finite from FINSEQ_1:sch_6(); hence support (pfexp n) is finite by A1; :: according to PRE_POLY:def_8 ::_thesis: verum end; end; theorem Th38: :: NAT_3:38 for p being Prime for a being non empty Nat st p divides a holds (pfexp a) . p <> 0 proof let p be Prime; ::_thesis: for a being non empty Nat st p divides a holds (pfexp a) . p <> 0 let a be non empty Nat; ::_thesis: ( p divides a implies (pfexp a) . p <> 0 ) assume p divides a ; ::_thesis: (pfexp a) . p <> 0 then A1: p |^ (0 + 1) divides a by NEWTON:5; ( (pfexp a) . p = p |-count a & p <> 1 ) by Def8, INT_2:def_4; hence (pfexp a) . p <> 0 by A1, Def7; ::_thesis: verum end; theorem Th39: :: NAT_3:39 pfexp 1 = EmptyBag SetPrimes proof set f = pfexp 1; for z being set st z in dom (pfexp 1) holds (pfexp 1) . z = 0 proof let z be set ; ::_thesis: ( z in dom (pfexp 1) implies (pfexp 1) . z = 0 ) assume z in dom (pfexp 1) ; ::_thesis: (pfexp 1) . z = 0 then reconsider z = z as Prime by Th33; A1: z <> 1 by INT_2:def_4; (pfexp 1) . z = z |-count 1 by Def8 .= 0 by A1, Th21 ; hence (pfexp 1) . z = 0 ; ::_thesis: verum end; then pfexp 1 = (dom (pfexp 1)) --> 0 by FUNCOP_1:11; hence pfexp 1 = EmptyBag SetPrimes by PARTFUN1:def_2; ::_thesis: verum end; registration cluster support (pfexp 1) -> empty ; coherence support (pfexp 1) is empty proof set f = pfexp 1; assume not support (pfexp 1) is empty ; ::_thesis: contradiction then consider x being set such that A1: x in support (pfexp 1) by XBOOLE_0:def_1; (pfexp 1) . x <> 0 by A1, PRE_POLY:def_7; hence contradiction by Th39, PRE_POLY:52; ::_thesis: verum end; end; theorem Th40: :: NAT_3:40 for a being Nat for p being Prime holds (pfexp (p |^ a)) . p = a proof let a be Nat; ::_thesis: for p being Prime holds (pfexp (p |^ a)) . p = a let p be Prime; ::_thesis: (pfexp (p |^ a)) . p = a set f = pfexp (p |^ a); ( p > 1 & (pfexp (p |^ a)) . p = p |-count (p |^ a) ) by Def8, INT_2:def_4; hence (pfexp (p |^ a)) . p = a by Th25; ::_thesis: verum end; theorem :: NAT_3:41 for p being Prime holds (pfexp p) . p = 1 proof let p be Prime; ::_thesis: (pfexp p) . p = 1 p = p |^ 1 by NEWTON:5; hence (pfexp p) . p = 1 by Th40; ::_thesis: verum end; theorem Th42: :: NAT_3:42 for a being Nat for p being Prime st a <> 0 holds support (pfexp (p |^ a)) = {p} proof let a be Nat; ::_thesis: for p being Prime st a <> 0 holds support (pfexp (p |^ a)) = {p} let p be Prime; ::_thesis: ( a <> 0 implies support (pfexp (p |^ a)) = {p} ) set f = pfexp (p |^ a); assume a <> 0 ; ::_thesis: support (pfexp (p |^ a)) = {p} then p divides p |^ a by Th3; then A1: (pfexp (p |^ a)) . p <> 0 by Th38; thus support (pfexp (p |^ a)) c= {p} :: according to XBOOLE_0:def_10 ::_thesis: {p} c= support (pfexp (p |^ a)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (pfexp (p |^ a)) or x in {p} ) assume A2: x in support (pfexp (p |^ a)) ; ::_thesis: x in {p} then reconsider x = x as Prime by Th34; A3: ( x <> 1 & (pfexp (p |^ a)) . x = x |-count (p |^ a) ) by Def8, INT_2:def_4; (pfexp (p |^ a)) . x <> 0 by A2, PRE_POLY:def_7; then x divides p |^ a by A3, Th27; then x = p by Th6; hence x in {p} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p} or x in support (pfexp (p |^ a)) ) assume x in {p} ; ::_thesis: x in support (pfexp (p |^ a)) then x = p by TARSKI:def_1; hence x in support (pfexp (p |^ a)) by A1, PRE_POLY:def_7; ::_thesis: verum end; theorem Th43: :: NAT_3:43 for p being Prime holds support (pfexp p) = {p} proof let p be Prime; ::_thesis: support (pfexp p) = {p} p = p |^ 1 by NEWTON:5; hence support (pfexp p) = {p} by Th42; ::_thesis: verum end; registration let p be Prime; let a be non empty Nat; cluster support (pfexp (p |^ a)) -> 1 -element ; coherence support (pfexp (p |^ a)) is 1 -element proof support (pfexp (p |^ a)) = {p} by Th42; hence support (pfexp (p |^ a)) is 1 -element ; ::_thesis: verum end; end; registration let p be Prime; cluster support (pfexp p) -> 1 -element ; coherence support (pfexp p) is 1 -element proof support (pfexp p) = {p} by Th43; hence support (pfexp p) is 1 -element ; ::_thesis: verum end; end; theorem Th44: :: NAT_3:44 for a, b being non empty Nat st a,b are_relative_prime holds support (pfexp a) misses support (pfexp b) proof let a, b be non empty Nat; ::_thesis: ( a,b are_relative_prime implies support (pfexp a) misses support (pfexp b) ) set f = pfexp a; set g = pfexp b; assume a,b are_relative_prime ; ::_thesis: support (pfexp a) misses support (pfexp b) then A1: a gcd b = 1 by INT_2:def_3; assume support (pfexp a) meets support (pfexp b) ; ::_thesis: contradiction then consider x being set such that A2: x in support (pfexp a) and A3: x in support (pfexp b) by XBOOLE_0:3; reconsider x = x as Prime by A2, Th34; A4: (pfexp a) . x = x |-count a by Def8; A5: (pfexp b) . x = x |-count b by Def8; (pfexp b) . x <> 0 by A3, PRE_POLY:def_7; then A6: x divides x |^ (x |-count b) by A5, Th3; A7: x <> 1 by INT_2:def_4; then x |^ (x |-count b) divides b by Def7; then A8: x divides b by A6, NAT_D:4; (pfexp a) . x <> 0 by A2, PRE_POLY:def_7; then A9: x divides x |^ (x |-count a) by A4, Th3; x |^ (x |-count a) divides a by A7, Def7; then x divides a by A9, NAT_D:4; then x divides 1 by A1, A8, NAT_D:def_5; hence contradiction by A7, WSIERP_1:15; ::_thesis: verum end; theorem Th45: :: NAT_3:45 for a, b being non empty Nat holds support (pfexp a) c= support (pfexp (a * b)) proof let a, b be non empty Nat; ::_thesis: support (pfexp a) c= support (pfexp (a * b)) set f = pfexp a; set h = pfexp (a * b); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (pfexp a) or x in support (pfexp (a * b)) ) assume A1: x in support (pfexp a) ; ::_thesis: x in support (pfexp (a * b)) then reconsider x = x as Prime by Th34; A2: (pfexp a) . x = x |-count a by Def8; (pfexp a) . x <> 0 by A1, PRE_POLY:def_7; then A3: x divides x |^ (x |-count a) by A2, Th3; A4: x <> 1 by INT_2:def_4; then x |^ (x |-count a) divides a by Def7; then x divides a by A3, NAT_D:4; then x |^ 1 divides a by NEWTON:5; then A5: x |^ (0 + 1) divides a * b by NAT_D:9; (pfexp (a * b)) . x = x |-count (a * b) by Def8; then (pfexp (a * b)) . x <> 0 by A4, A5, Def7; hence x in support (pfexp (a * b)) by PRE_POLY:def_7; ::_thesis: verum end; theorem Th46: :: NAT_3:46 for a, b being non empty Nat holds support (pfexp (a * b)) = (support (pfexp a)) \/ (support (pfexp b)) proof let a, b be non empty Nat; ::_thesis: support (pfexp (a * b)) = (support (pfexp a)) \/ (support (pfexp b)) set f = pfexp a; set g = pfexp b; set h = pfexp (a * b); thus support (pfexp (a * b)) c= (support (pfexp a)) \/ (support (pfexp b)) :: according to XBOOLE_0:def_10 ::_thesis: (support (pfexp a)) \/ (support (pfexp b)) c= support (pfexp (a * b)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (pfexp (a * b)) or x in (support (pfexp a)) \/ (support (pfexp b)) ) assume A1: x in support (pfexp (a * b)) ; ::_thesis: x in (support (pfexp a)) \/ (support (pfexp b)) then reconsider x = x as Prime by Th34; A2: (pfexp (a * b)) . x <> 0 by A1, PRE_POLY:def_7; A3: x <> 1 by INT_2:def_4; A4: ( (pfexp (a * b)) . x = x |-count (a * b) & x |^ (x |-count (a * b)) = (x |^ (x |-count a)) * (x |^ (x |-count b)) ) by Def8, Th29; percases ( x divides x |^ (x |-count a) or x divides x |^ (x |-count b) ) by A2, A4, Th3, NEWTON:80; suppose x divides x |^ (x |-count a) ; ::_thesis: x in (support (pfexp a)) \/ (support (pfexp b)) then x divides a by A3, Th26; then (pfexp a) . x <> 0 by Th38; then x in support (pfexp a) by PRE_POLY:def_7; hence x in (support (pfexp a)) \/ (support (pfexp b)) by XBOOLE_0:def_3; ::_thesis: verum end; suppose x divides x |^ (x |-count b) ; ::_thesis: x in (support (pfexp a)) \/ (support (pfexp b)) then x divides b by A3, Th26; then (pfexp b) . x <> 0 by Th38; then x in support (pfexp b) by PRE_POLY:def_7; hence x in (support (pfexp a)) \/ (support (pfexp b)) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; ( support (pfexp a) c= support (pfexp (a * b)) & support (pfexp b) c= support (pfexp (a * b)) ) by Th45; hence (support (pfexp a)) \/ (support (pfexp b)) c= support (pfexp (a * b)) by XBOOLE_1:8; ::_thesis: verum end; theorem :: NAT_3:47 for a, b being non empty Nat st a,b are_relative_prime holds card (support (pfexp (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b))) proof let a, b be non empty Nat; ::_thesis: ( a,b are_relative_prime implies card (support (pfexp (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b))) ) assume A1: a,b are_relative_prime ; ::_thesis: card (support (pfexp (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b))) support (pfexp (a * b)) = (support (pfexp a)) \/ (support (pfexp b)) by Th46; hence card (support (pfexp (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b))) by A1, Th44, CARD_2:40; ::_thesis: verum end; theorem :: NAT_3:48 for a, b being non empty Nat holds support (pfexp a) = support (pfexp (a |^ b)) proof let a, b be non empty Nat; ::_thesis: support (pfexp a) = support (pfexp (a |^ b)) set f = pfexp a; set g = pfexp (a |^ b); a |^ b = (a |^ (b -' 1)) * a by PEPIN:26; hence support (pfexp a) c= support (pfexp (a |^ b)) by Th45; :: according to XBOOLE_0:def_10 ::_thesis: support (pfexp (a |^ b)) c= support (pfexp a) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (pfexp (a |^ b)) or x in support (pfexp a) ) assume A1: x in support (pfexp (a |^ b)) ; ::_thesis: x in support (pfexp a) then reconsider x = x as Prime by Th34; A2: ( (pfexp (a |^ b)) . x = x |-count (a |^ b) & x <> 1 ) by Def8, INT_2:def_4; (pfexp (a |^ b)) . x <> 0 by A1, PRE_POLY:def_7; then x divides a |^ b by A2, Th27; then (pfexp a) . x <> 0 by Th5, Th38; hence x in support (pfexp a) by PRE_POLY:def_7; ::_thesis: verum end; theorem :: NAT_3:49 for n, m being non empty Nat holds pfexp (n * m) = (pfexp n) + (pfexp m) proof let n, m be non empty Nat; ::_thesis: pfexp (n * m) = (pfexp n) + (pfexp m) for i being set st i in SetPrimes holds (pfexp (n * m)) . i = ((pfexp n) + (pfexp m)) . i proof let i be set ; ::_thesis: ( i in SetPrimes implies (pfexp (n * m)) . i = ((pfexp n) + (pfexp m)) . i ) assume i in SetPrimes ; ::_thesis: (pfexp (n * m)) . i = ((pfexp n) + (pfexp m)) . i then reconsider a = i as prime Element of NAT by NEWTON:def_6; thus (pfexp (n * m)) . i = a |-count (n * m) by Def8 .= (a |-count n) + (a |-count m) by Th28 .= ((pfexp n) . i) + (a |-count m) by Def8 .= ((pfexp n) . i) + ((pfexp m) . i) by Def8 .= ((pfexp n) + (pfexp m)) . i by PRE_POLY:def_5 ; ::_thesis: verum end; hence pfexp (n * m) = (pfexp n) + (pfexp m) by PBOOLE:3; ::_thesis: verum end; theorem :: NAT_3:50 for m, n being non empty Nat st m divides n holds pfexp (n div m) = (pfexp n) -' (pfexp m) proof let m, n be non empty Nat; ::_thesis: ( m divides n implies pfexp (n div m) = (pfexp n) -' (pfexp m) ) assume A1: m divides n ; ::_thesis: pfexp (n div m) = (pfexp n) -' (pfexp m) for i being set st i in SetPrimes holds (pfexp (n div m)) . i = ((pfexp n) -' (pfexp m)) . i proof let i be set ; ::_thesis: ( i in SetPrimes implies (pfexp (n div m)) . i = ((pfexp n) -' (pfexp m)) . i ) assume i in SetPrimes ; ::_thesis: (pfexp (n div m)) . i = ((pfexp n) -' (pfexp m)) . i then reconsider a = i as prime Element of NAT by NEWTON:def_6; thus (pfexp (n div m)) . i = a |-count (n div m) by Def8 .= (a |-count n) -' (a |-count m) by A1, Th31 .= ((pfexp n) . i) -' (a |-count m) by Def8 .= ((pfexp n) . i) -' ((pfexp m) . i) by Def8 .= ((pfexp n) -' (pfexp m)) . i by PRE_POLY:def_6 ; ::_thesis: verum end; hence pfexp (n div m) = (pfexp n) -' (pfexp m) by PBOOLE:3; ::_thesis: verum end; theorem :: NAT_3:51 for a being Nat for n being non empty Nat holds pfexp (n |^ a) = a * (pfexp n) proof let a be Nat; ::_thesis: for n being non empty Nat holds pfexp (n |^ a) = a * (pfexp n) let n be non empty Nat; ::_thesis: pfexp (n |^ a) = a * (pfexp n) for i being set st i in SetPrimes holds (pfexp (n |^ a)) . i = (a * (pfexp n)) . i proof let i be set ; ::_thesis: ( i in SetPrimes implies (pfexp (n |^ a)) . i = (a * (pfexp n)) . i ) assume i in SetPrimes ; ::_thesis: (pfexp (n |^ a)) . i = (a * (pfexp n)) . i then reconsider x = i as prime Element of NAT by NEWTON:def_6; thus (pfexp (n |^ a)) . i = x |-count (n |^ a) by Def8 .= a * (x |-count n) by Th32 .= a * ((pfexp n) . i) by Def8 .= (a * (pfexp n)) . i by Def2 ; ::_thesis: verum end; hence pfexp (n |^ a) = a * (pfexp n) by PBOOLE:3; ::_thesis: verum end; theorem Th52: :: NAT_3:52 for n being non empty Nat st support (pfexp n) = {} holds n = 1 proof let n be non empty Nat; ::_thesis: ( support (pfexp n) = {} implies n = 1 ) assume that A1: support (pfexp n) = {} and A2: n <> 1 ; ::_thesis: contradiction n >= 0 + 1 by NAT_1:13; then n > 1 by A2, XXREAL_0:1; then n >= 1 + 1 by NAT_1:13; then consider p being Element of NAT such that A3: p is prime and A4: p divides n by INT_2:31; p > 1 by A3, INT_2:def_4; then p |-count n <> 0 by A4, Th27; then (pfexp n) . p <> 0 by A3, Def8; hence contradiction by A1, PRE_POLY:def_7; ::_thesis: verum end; theorem :: NAT_3:53 for m, n being non empty Nat holds pfexp (n gcd m) = min ((pfexp n),(pfexp m)) proof let m, n be non empty Nat; ::_thesis: pfexp (n gcd m) = min ((pfexp n),(pfexp m)) now__::_thesis:_for_i_being_set_st_i_in_SetPrimes_holds_ (pfexp_(n_gcd_m))_._i_=_(min_((pfexp_n),(pfexp_m)))_._i set rhs = min ((pfexp n),(pfexp m)); set lhs = pfexp (n gcd m); let i be set ; ::_thesis: ( i in SetPrimes implies (pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i ) assume i in SetPrimes ; ::_thesis: (pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i then reconsider j = i as prime Element of NAT by NEWTON:def_6; set x = j |-count n; set y = j |-count m; set z = j |-count (n gcd m); A1: (pfexp (n gcd m)) . j = j |-count (n gcd m) by Def8; A2: j <> 1 by INT_2:def_4; then A3: j |^ (j |-count n) divides n by Def7; A4: n gcd m <> 0 by INT_2:5; then A5: j |^ (j |-count (n gcd m)) divides n gcd m by A2, Def7; A6: not j |^ ((j |-count (n gcd m)) + 1) divides n gcd m by A2, A4, Def7; A7: not j |^ ((j |-count m) + 1) divides m by A2, Def7; A8: j |^ (j |-count m) divides m by A2, Def7; n gcd m divides m by NAT_D:def_5; then A9: j |^ (j |-count (n gcd m)) divides m by A5, NAT_D:4; A10: (pfexp n) . j = j |-count n by Def8; n gcd m divides n by NAT_D:def_5; then A11: j |^ (j |-count (n gcd m)) divides n by A5, NAT_D:4; A12: (pfexp m) . j = j |-count m by Def8; A13: not j |^ ((j |-count n) + 1) divides n by A2, Def7; thus (pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i ::_thesis: verum proof percases ( (pfexp n) . j <= (pfexp m) . j or (pfexp n) . j > (pfexp m) . j ) ; supposeA14: (pfexp n) . j <= (pfexp m) . j ; ::_thesis: (pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i A15: now__::_thesis:_not_j_|-count_(n_gcd_m)_<_j_|-count_n assume A16: j |-count (n gcd m) < j |-count n ; ::_thesis: contradiction then j |-count (n gcd m) < j |-count m by A10, A12, A14, XXREAL_0:2; then A17: j |^ ((j |-count (n gcd m)) + 1) divides m by A8, Th4; j |^ ((j |-count (n gcd m)) + 1) divides n by A3, A16, Th4; hence contradiction by A6, A17, NAT_D:def_5; ::_thesis: verum end; A18: j |-count (n gcd m) <= j |-count n by A13, A11, Th4; (min ((pfexp n),(pfexp m))) . j = j |-count n by A10, A14, Def3; hence (pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i by A1, A18, A15, XXREAL_0:1; ::_thesis: verum end; supposeA19: (pfexp n) . j > (pfexp m) . j ; ::_thesis: (pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i A20: now__::_thesis:_not_j_|-count_(n_gcd_m)_<_j_|-count_m assume A21: j |-count (n gcd m) < j |-count m ; ::_thesis: contradiction then j |-count (n gcd m) < j |-count n by A10, A12, A19, XXREAL_0:2; then A22: j |^ ((j |-count (n gcd m)) + 1) divides n by A3, Th4; j |^ ((j |-count (n gcd m)) + 1) divides m by A8, A21, Th4; hence contradiction by A6, A22, NAT_D:def_5; ::_thesis: verum end; A23: j |-count (n gcd m) <= j |-count m by A7, A9, Th4; (min ((pfexp n),(pfexp m))) . j = j |-count m by A12, A19, Def3; hence (pfexp (n gcd m)) . i = (min ((pfexp n),(pfexp m))) . i by A1, A23, A20, XXREAL_0:1; ::_thesis: verum end; end; end; end; hence pfexp (n gcd m) = min ((pfexp n),(pfexp m)) by PBOOLE:3; ::_thesis: verum end; theorem :: NAT_3:54 for m, n being non empty Nat holds pfexp (n lcm m) = max ((pfexp n),(pfexp m)) proof let m, n be non empty Nat; ::_thesis: pfexp (n lcm m) = max ((pfexp n),(pfexp m)) now__::_thesis:_for_i_being_set_st_i_in_SetPrimes_holds_ (pfexp_(n_lcm_m))_._i_=_(max_((pfexp_n),(pfexp_m)))_._i set rhs = max ((pfexp n),(pfexp m)); set lhs = pfexp (n lcm m); let i be set ; ::_thesis: ( i in SetPrimes implies (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i ) A1: m divides n lcm m by NAT_D:def_4; assume i in SetPrimes ; ::_thesis: (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i then reconsider j = i as prime Element of NAT by NEWTON:def_6; set x = j |-count n; set y = j |-count m; set z = j |-count (n lcm m); A2: (pfexp (n lcm m)) . j = j |-count (n lcm m) by Def8; A3: (pfexp n) . j = j |-count n by Def8; A4: j > 1 by INT_2:def_4; then A5: not j |^ ((j |-count n) + 1) divides n by Def7; A6: n lcm m <> 0 by INT_2:4; then A7: j |^ (j |-count (n lcm m)) divides n lcm m by A4, Def7; A8: not j |^ ((j |-count (n lcm m)) + 1) divides n lcm m by A4, A6, Def7; A9: (pfexp m) . j = j |-count m by Def8; A10: n divides n lcm m by NAT_D:def_4; A11: j |^ (j |-count n) divides n by A4, Def7; then A12: j |^ (j |-count n) divides n lcm m by A10, NAT_D:4; A13: not j |^ ((j |-count m) + 1) divides m by A4, Def7; A14: j |^ (j |-count m) divides m by A4, Def7; then A15: j |^ (j |-count m) divides n lcm m by A1, NAT_D:4; thus (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i ::_thesis: verum proof percases ( (pfexp n) . j <= (pfexp m) . j or (pfexp n) . j > (pfexp m) . j ) ; supposeA16: (pfexp n) . j <= (pfexp m) . j ; ::_thesis: (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i A17: now__::_thesis:_not_j_|-count_m_<_j_|-count_(n_lcm_m) consider p being Nat such that A18: j |-count m = (j |-count n) + p by A3, A9, A16, NAT_1:10; consider t being Nat such that A19: n = (j |^ (j |-count n)) * t by A11, NAT_D:def_3; A20: now__::_thesis:_not_j_divides_t assume j divides t ; ::_thesis: contradiction then consider w being Nat such that A21: t = j * w by NAT_D:def_3; n = ((j |^ (j |-count n)) * j) * w by A19, A21 .= (j |^ ((j |-count n) + 1)) * w by NEWTON:6 ; hence contradiction by A5, NAT_D:def_3; ::_thesis: verum end; consider u being Nat such that A22: n lcm m = n * u by A10, NAT_D:def_3; assume j |-count m < j |-count (n lcm m) ; ::_thesis: contradiction then j |^ ((j |-count m) + 1) divides n lcm m by A7, Th4; then consider k being Nat such that A23: n lcm m = (j |^ ((j |-count m) + 1)) * k by NAT_D:def_3; A24: n lcm m = ((j |^ (j |-count m)) * j) * k by A23, NEWTON:6 .= (j |^ (j |-count m)) * (k * j) ; (j |^ (j |-count n)) * ((j |^ p) * (k * j)) = ((j |^ (j |-count n)) * (j |^ p)) * (k * j) .= (j |^ (j |-count n)) * (t * u) by A24, A19, A22, A18, NEWTON:8 ; then ((j |^ p) * k) * j = t * u by XCMPLX_1:5; then j divides t * u by NAT_D:def_3; then j divides u by A20, NEWTON:80; then consider w being Nat such that A25: u = j * w by NAT_D:def_3; ((j |^ (j |-count m)) * k) * j = (n * w) * j by A24, A22, A25; then (j |^ (j |-count m)) * k = n * w by XCMPLX_1:5; then A26: n divides (j |^ (j |-count m)) * k by NAT_D:def_3; consider t being Nat such that A27: m = (j |^ (j |-count m)) * t by A14, NAT_D:def_3; A28: now__::_thesis:_not_j_divides_t assume j divides t ; ::_thesis: contradiction then consider w being Nat such that A29: t = j * w by NAT_D:def_3; m = ((j |^ (j |-count m)) * j) * w by A27, A29 .= (j |^ ((j |-count m) + 1)) * w by NEWTON:6 ; hence contradiction by A13, NAT_D:def_3; ::_thesis: verum end; consider u being Nat such that A30: n lcm m = m * u by A1, NAT_D:def_3; (j |^ (j |-count m)) * (k * j) = (j |^ (j |-count m)) * (t * u) by A24, A27, A30; then k * j = t * u by XCMPLX_1:5; then j divides t * u by NAT_D:def_3; then j divides u by A28, NEWTON:80; then consider w being Nat such that A31: u = j * w by NAT_D:def_3; ((j |^ (j |-count m)) * k) * j = (m * w) * j by A24, A30, A31; then (j |^ (j |-count m)) * k = m * w by XCMPLX_1:5; then m divides (j |^ (j |-count m)) * k by NAT_D:def_3; then A32: n lcm m divides (j |^ (j |-count m)) * k by A26, NAT_D:def_4; 0 <> k by A23, INT_2:4; then j |^ ((j |-count m) + 1) <= j |^ (j |-count m) by A23, A32, NAT_D:7, XREAL_1:68; then (j |^ (j |-count m)) * j <= (j |^ (j |-count m)) * 1 by NEWTON:6; then j <= 1 by XREAL_1:68; hence contradiction by INT_2:def_4; ::_thesis: verum end; A33: j |-count m <= j |-count (n lcm m) by A8, A15, Th4; (max ((pfexp n),(pfexp m))) . j = j |-count m by A9, A16, Def4; hence (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i by A2, A33, A17, XXREAL_0:1; ::_thesis: verum end; supposeA34: (pfexp n) . j > (pfexp m) . j ; ::_thesis: (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i A35: now__::_thesis:_not_j_|-count_n_<_j_|-count_(n_lcm_m) consider p being Nat such that A36: j |-count n = (j |-count m) + p by A3, A9, A34, NAT_1:10; consider t being Nat such that A37: m = (j |^ (j |-count m)) * t by A14, NAT_D:def_3; A38: now__::_thesis:_not_j_divides_t assume j divides t ; ::_thesis: contradiction then consider w being Nat such that A39: t = j * w by NAT_D:def_3; m = ((j |^ (j |-count m)) * j) * w by A37, A39 .= (j |^ ((j |-count m) + 1)) * w by NEWTON:6 ; hence contradiction by A13, NAT_D:def_3; ::_thesis: verum end; consider u being Nat such that A40: n lcm m = m * u by A1, NAT_D:def_3; assume j |-count n < j |-count (n lcm m) ; ::_thesis: contradiction then j |^ ((j |-count n) + 1) divides n lcm m by A7, Th4; then consider k being Nat such that A41: n lcm m = (j |^ ((j |-count n) + 1)) * k by NAT_D:def_3; A42: n lcm m = ((j |^ (j |-count n)) * j) * k by A41, NEWTON:6 .= (j |^ (j |-count n)) * (k * j) ; (j |^ (j |-count m)) * ((j |^ p) * (k * j)) = ((j |^ (j |-count m)) * (j |^ p)) * (k * j) .= (j |^ (j |-count m)) * (t * u) by A42, A37, A40, A36, NEWTON:8 ; then t * u = ((j |^ p) * k) * j by XCMPLX_1:5; then j divides t * u by NAT_D:def_3; then j divides u by A38, NEWTON:80; then consider w being Nat such that A43: u = j * w by NAT_D:def_3; ((j |^ (j |-count n)) * k) * j = (m * w) * j by A42, A40, A43; then (j |^ (j |-count n)) * k = m * w by XCMPLX_1:5; then A44: m divides (j |^ (j |-count n)) * k by NAT_D:def_3; consider t being Nat such that A45: n = (j |^ (j |-count n)) * t by A11, NAT_D:def_3; A46: now__::_thesis:_not_j_divides_t assume j divides t ; ::_thesis: contradiction then consider w being Nat such that A47: t = j * w by NAT_D:def_3; n = ((j |^ (j |-count n)) * j) * w by A45, A47 .= (j |^ ((j |-count n) + 1)) * w by NEWTON:6 ; hence contradiction by A5, NAT_D:def_3; ::_thesis: verum end; consider u being Nat such that A48: n lcm m = n * u by A10, NAT_D:def_3; (j |^ (j |-count n)) * (k * j) = (j |^ (j |-count n)) * (t * u) by A42, A45, A48; then k * j = t * u by XCMPLX_1:5; then j divides t * u by NAT_D:def_3; then j divides u by A46, NEWTON:80; then consider w being Nat such that A49: u = j * w by NAT_D:def_3; ((j |^ (j |-count n)) * k) * j = (n * w) * j by A42, A48, A49; then (j |^ (j |-count n)) * k = n * w by XCMPLX_1:5; then n divides (j |^ (j |-count n)) * k by NAT_D:def_3; then A50: n lcm m divides (j |^ (j |-count n)) * k by A44, NAT_D:def_4; 0 <> k by A41, INT_2:4; then j |^ ((j |-count n) + 1) <= j |^ (j |-count n) by A41, A50, NAT_D:7, XREAL_1:68; then (j |^ (j |-count n)) * j <= (j |^ (j |-count n)) * 1 by NEWTON:6; then j <= 1 by XREAL_1:68; hence contradiction by INT_2:def_4; ::_thesis: verum end; A51: j |-count n <= j |-count (n lcm m) by A8, A12, Th4; (max ((pfexp n),(pfexp m))) . j = j |-count n by A3, A34, Def4; hence (pfexp (n lcm m)) . i = (max ((pfexp n),(pfexp m))) . i by A2, A51, A35, XXREAL_0:1; ::_thesis: verum end; end; end; end; hence pfexp (n lcm m) = max ((pfexp n),(pfexp m)) by PBOOLE:3; ::_thesis: verum end; begin definition let n be non empty Nat; func prime_factorization n -> ManySortedSet of SetPrimes means :Def9: :: NAT_3:def 9 ( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds it . p = p |^ (p |-count n) ) ); existence ex b1 being ManySortedSet of SetPrimes st ( support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds b1 . p = p |^ (p |-count n) ) ) proof defpred S1[ set , set ] means for p being Prime st $1 = p holds ( ( p in support (pfexp n) implies $2 = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies $2 = 0 ) ); A1: for x being set st x in SetPrimes holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in SetPrimes implies ex y being set st S1[x,y] ) assume x in SetPrimes ; ::_thesis: ex y being set st S1[x,y] then reconsider i = x as prime Element of NAT by NEWTON:def_6; percases ( i in support (pfexp n) or not i in support (pfexp n) ) ; supposeA2: i in support (pfexp n) ; ::_thesis: ex y being set st S1[x,y] take i |^ (i |-count n) ; ::_thesis: S1[x,i |^ (i |-count n)] let p be Prime; ::_thesis: ( x = p implies ( ( p in support (pfexp n) implies i |^ (i |-count n) = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies i |^ (i |-count n) = 0 ) ) ) assume p = x ; ::_thesis: ( ( p in support (pfexp n) implies i |^ (i |-count n) = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies i |^ (i |-count n) = 0 ) ) hence ( ( p in support (pfexp n) implies i |^ (i |-count n) = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies i |^ (i |-count n) = 0 ) ) by A2; ::_thesis: verum end; supposeA3: not i in support (pfexp n) ; ::_thesis: ex y being set st S1[x,y] take 0 ; ::_thesis: S1[x, 0 ] let p be Prime; ::_thesis: ( x = p implies ( ( p in support (pfexp n) implies 0 = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies 0 = 0 ) ) ) assume p = x ; ::_thesis: ( ( p in support (pfexp n) implies 0 = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies 0 = 0 ) ) hence ( ( p in support (pfexp n) implies 0 = p |^ (p |-count n) ) & ( not p in support (pfexp n) implies 0 = 0 ) ) by A3; ::_thesis: verum end; end; end; consider f being Function such that A4: dom f = SetPrimes and A5: for x being set st x in SetPrimes holds S1[x,f . x] from CLASSES1:sch_1(A1); A6: support f c= SetPrimes by A4, PRE_POLY:37; A7: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_support_f_implies_x_in_support_(pfexp_n)_)_&_(_x_in_support_(pfexp_n)_implies_x_in_support_f_)_) let x be set ; ::_thesis: ( ( x in support f implies x in support (pfexp n) ) & ( x in support (pfexp n) implies x in support f ) ) hereby ::_thesis: ( x in support (pfexp n) implies x in support f ) assume A8: x in support f ; ::_thesis: x in support (pfexp n) then x in SetPrimes by A6; then reconsider i = x as prime Element of NAT by NEWTON:def_6; assume not x in support (pfexp n) ; ::_thesis: contradiction then f . i = 0 by A5, A6, A8; hence contradiction by A8, PRE_POLY:def_7; ::_thesis: verum end; assume A9: x in support (pfexp n) ; ::_thesis: x in support f then x in SetPrimes ; then reconsider i = x as prime Element of NAT by NEWTON:def_6; f . i = i |^ (i |-count n) by A5, A9; hence x in support f by PRE_POLY:def_7; ::_thesis: verum end; reconsider f = f as ManySortedSet of SetPrimes by A4, PARTFUN1:def_2, RELAT_1:def_18; take f ; ::_thesis: ( support f = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds f . p = p |^ (p |-count n) ) ) thus support f = support (pfexp n) by A7, TARSKI:1; ::_thesis: for p being Nat st p in support (pfexp n) holds f . p = p |^ (p |-count n) let p be Nat; ::_thesis: ( p in support (pfexp n) implies f . p = p |^ (p |-count n) ) assume A10: p in support (pfexp n) ; ::_thesis: f . p = p |^ (p |-count n) then p is Prime by Th34; hence f . p = p |^ (p |-count n) by A5, A10; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of SetPrimes st support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds b1 . p = p |^ (p |-count n) ) & support b2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds b2 . p = p |^ (p |-count n) ) holds b1 = b2 proof let it1, it2 be ManySortedSet of SetPrimes ; ::_thesis: ( support it1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds it1 . p = p |^ (p |-count n) ) & support it2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds it2 . p = p |^ (p |-count n) ) implies it1 = it2 ) assume that A11: support it1 = support (pfexp n) and A12: for p being Nat st p in support (pfexp n) holds it1 . p = p |^ (p |-count n) and A13: support it2 = support (pfexp n) and A14: for p being Nat st p in support (pfexp n) holds it2 . p = p |^ (p |-count n) ; ::_thesis: it1 = it2 now__::_thesis:_for_i_being_set_st_i_in_SetPrimes_holds_ it1_._i_=_it2_._i let i be set ; ::_thesis: ( i in SetPrimes implies it1 . b1 = it2 . b1 ) assume i in SetPrimes ; ::_thesis: it1 . b1 = it2 . b1 then reconsider p = i as prime Element of NAT by NEWTON:def_6; percases ( p in support (pfexp n) or not p in support (pfexp n) ) ; supposeA15: p in support (pfexp n) ; ::_thesis: it1 . b1 = it2 . b1 hence it1 . i = p |^ (p |-count n) by A12 .= it2 . i by A14, A15 ; ::_thesis: verum end; supposeA16: not p in support (pfexp n) ; ::_thesis: it1 . b1 = it2 . b1 hence it1 . i = 0 by A11, PRE_POLY:def_7 .= it2 . i by A13, A16, PRE_POLY:def_7 ; ::_thesis: verum end; end; end; hence it1 = it2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def9 defines prime_factorization NAT_3:def_9_:_ for n being non empty Nat for b2 being ManySortedSet of SetPrimes holds ( b2 = prime_factorization n iff ( support b2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds b2 . p = p |^ (p |-count n) ) ) ); notation let n be non empty Nat; synonym ppf n for prime_factorization n; end; registration let n be non empty Nat; cluster prime_factorization n -> natural-valued finite-support ; coherence ( ppf n is natural-valued & ppf n is finite-support ) proof rng (ppf n) c= NAT proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (ppf n) or y in NAT ) assume y in rng (ppf n) ; ::_thesis: y in NAT then consider x being set such that A1: x in dom (ppf n) and A2: (ppf n) . x = y by FUNCT_1:def_3; dom (ppf n) = SetPrimes by PARTFUN1:def_2; then reconsider x = x as prime Element of NAT by A1, NEWTON:def_6; percases ( x in support (pfexp n) or not x in support (pfexp n) ) ; suppose x in support (pfexp n) ; ::_thesis: y in NAT then (ppf n) . x = x |^ (x |-count n) by Def9; hence y in NAT by A2; ::_thesis: verum end; suppose not x in support (pfexp n) ; ::_thesis: y in NAT then not x in support (ppf n) by Def9; then (ppf n) . x = 0 by PRE_POLY:def_7; hence y in NAT by A2; ::_thesis: verum end; end; end; hence ppf n is natural-valued by VALUED_0:def_6; ::_thesis: ppf n is finite-support support (ppf n) = support (pfexp n) by Def9; hence support (ppf n) is finite ; :: according to PRE_POLY:def_8 ::_thesis: verum end; end; theorem Th55: :: NAT_3:55 for p being Prime for n being non empty Nat st p |-count n = 0 holds (ppf n) . p = 0 proof let p be Prime; ::_thesis: for n being non empty Nat st p |-count n = 0 holds (ppf n) . p = 0 let n be non empty Nat; ::_thesis: ( p |-count n = 0 implies (ppf n) . p = 0 ) assume p |-count n = 0 ; ::_thesis: (ppf n) . p = 0 then (pfexp n) . p = 0 by Def8; then not p in support (pfexp n) by PRE_POLY:def_7; then not p in support (ppf n) by Def9; hence (ppf n) . p = 0 by PRE_POLY:def_7; ::_thesis: verum end; theorem Th56: :: NAT_3:56 for p being Prime for n being non empty Nat st p |-count n <> 0 holds (ppf n) . p = p |^ (p |-count n) proof let p be Prime; ::_thesis: for n being non empty Nat st p |-count n <> 0 holds (ppf n) . p = p |^ (p |-count n) let n be non empty Nat; ::_thesis: ( p |-count n <> 0 implies (ppf n) . p = p |^ (p |-count n) ) assume p |-count n <> 0 ; ::_thesis: (ppf n) . p = p |^ (p |-count n) then (pfexp n) . p <> 0 by Def8; then p in support (pfexp n) by PRE_POLY:def_7; hence (ppf n) . p = p |^ (p |-count n) by Def9; ::_thesis: verum end; theorem :: NAT_3:57 for n being non empty Nat st support (ppf n) = {} holds n = 1 proof let n be non empty Nat; ::_thesis: ( support (ppf n) = {} implies n = 1 ) assume support (ppf n) = {} ; ::_thesis: n = 1 then support (pfexp n) = {} by Def9; hence n = 1 by Th52; ::_thesis: verum end; theorem Th58: :: NAT_3:58 for a, b being non empty Nat st a,b are_relative_prime holds ppf (a * b) = (ppf a) + (ppf b) proof let a, b be non empty Nat; ::_thesis: ( a,b are_relative_prime implies ppf (a * b) = (ppf a) + (ppf b) ) assume A1: a,b are_relative_prime ; ::_thesis: ppf (a * b) = (ppf a) + (ppf b) reconsider an = a, bn = b as non empty Nat ; now__::_thesis:_for_i_being_set_st_i_in_SetPrimes_holds_ (ppf_(a_*_b))_._i_=_((ppf_a)_+_(ppf_b))_._i A2: a gcd b = 1 by A1, INT_2:def_3; let i be set ; ::_thesis: ( i in SetPrimes implies (ppf (a * b)) . b1 = ((ppf a) + (ppf b)) . b1 ) assume i in SetPrimes ; ::_thesis: (ppf (a * b)) . b1 = ((ppf a) + (ppf b)) . b1 then reconsider p = i as prime Element of NAT by NEWTON:def_6; A3: p > 1 by INT_2:def_4; A4: p |-count (an * bn) = (p |-count a) + (p |-count b) by Th28; percases ( p |-count (a * b) = 0 or p |-count (a * b) <> 0 ) ; supposeA5: p |-count (a * b) = 0 ; ::_thesis: (ppf (a * b)) . b1 = ((ppf a) + (ppf b)) . b1 then A6: p |-count b = 0 by A4; A7: p |-count a = 0 by A4, A5; thus (ppf (a * b)) . i = 0 by A5, Th55 .= 0 + ((ppf b) . i) by A6, Th55 .= ((ppf a) . i) + ((ppf b) . i) by A7, Th55 .= ((ppf a) + (ppf b)) . i by PRE_POLY:def_5 ; ::_thesis: verum end; supposeA8: p |-count (a * b) <> 0 ; ::_thesis: (ppf (a * b)) . b1 = ((ppf a) + (ppf b)) . b1 thus (ppf (a * b)) . i = ((ppf a) + (ppf b)) . i ::_thesis: verum proof percases ( p |-count a <> 0 or p |-count b <> 0 ) by A4, A8; supposeA9: p |-count a <> 0 ; ::_thesis: (ppf (a * b)) . i = ((ppf a) + (ppf b)) . i A10: now__::_thesis:_not_p_|-count_b_<>_0 consider ka being Nat such that A11: p |-count a = ka + 1 by A9, NAT_1:6; p |^ (p |-count a) divides a by A3, Def7; then p * (p |^ ka) divides a by A11, NEWTON:6; then consider la being Nat such that A12: a = (p * (p |^ ka)) * la by NAT_D:def_3; a = p * ((p |^ ka) * la) by A12; then A13: p divides a by NAT_D:def_3; assume p |-count b <> 0 ; ::_thesis: contradiction then consider kb being Nat such that A14: p |-count b = kb + 1 by NAT_1:6; p |^ (p |-count b) divides b by A3, Def7; then p * (p |^ kb) divides b by A14, NEWTON:6; then consider lb being Nat such that A15: b = (p * (p |^ kb)) * lb by NAT_D:def_3; b = p * ((p |^ kb) * lb) by A15; then p divides b by NAT_D:def_3; then p divides 1 by A2, A13, NAT_D:def_5; hence contradiction by A3, NAT_D:7; ::_thesis: verum end; hence (ppf (a * b)) . i = p |^ (p |-count a) by A4, A8, Th56 .= ((ppf a) . p) + 0 by A9, Th56 .= ((ppf a) . p) + ((ppf b) . p) by A10, Th55 .= ((ppf a) + (ppf b)) . i by PRE_POLY:def_5 ; ::_thesis: verum end; supposeA16: p |-count b <> 0 ; ::_thesis: (ppf (a * b)) . i = ((ppf a) + (ppf b)) . i A17: now__::_thesis:_not_p_|-count_a_<>_0 assume p |-count a <> 0 ; ::_thesis: contradiction then consider ka being Nat such that A18: p |-count a = ka + 1 by NAT_1:6; p |^ (p |-count a) divides a by A3, Def7; then p * (p |^ ka) divides a by A18, NEWTON:6; then consider la being Nat such that A19: a = (p * (p |^ ka)) * la by NAT_D:def_3; a = p * ((p |^ ka) * la) by A19; then A20: p divides a by NAT_D:def_3; consider kb being Nat such that A21: p |-count b = kb + 1 by A16, NAT_1:6; p |^ (p |-count b) divides b by A3, Def7; then p * (p |^ kb) divides b by A21, NEWTON:6; then consider lb being Nat such that A22: b = (p * (p |^ kb)) * lb by NAT_D:def_3; b = p * ((p |^ kb) * lb) by A22; then p divides b by NAT_D:def_3; then p divides 1 by A2, A20, NAT_D:def_5; hence contradiction by A3, NAT_D:7; ::_thesis: verum end; hence (ppf (a * b)) . i = p |^ (p |-count b) by A4, A8, Th56 .= 0 + ((ppf b) . p) by A16, Th56 .= ((ppf a) . p) + ((ppf b) . p) by A17, Th55 .= ((ppf a) + (ppf b)) . i by PRE_POLY:def_5 ; ::_thesis: verum end; end; end; end; end; end; hence ppf (a * b) = (ppf a) + (ppf b) by PBOOLE:3; ::_thesis: verum end; theorem Th59: :: NAT_3:59 for p being Prime for n being non empty Nat holds (ppf (p |^ n)) . p = p |^ n proof let p be Prime; ::_thesis: for n being non empty Nat holds (ppf (p |^ n)) . p = p |^ n let n be non empty Nat; ::_thesis: (ppf (p |^ n)) . p = p |^ n p > 1 by INT_2:def_4; then p |-count (p |^ n) = n by Th25; hence (ppf (p |^ n)) . p = p |^ n by Th56; ::_thesis: verum end; theorem :: NAT_3:60 for n, m being non empty Nat holds ppf (n |^ m) = (ppf n) |^ m proof let n, m be non empty Nat; ::_thesis: ppf (n |^ m) = (ppf n) |^ m now__::_thesis:_for_i_being_set_st_i_in_SetPrimes_holds_ (ppf_(n_|^_m))_._i_=_((ppf_n)_|^_m)_._i let i be set ; ::_thesis: ( i in SetPrimes implies (ppf (n |^ m)) . b1 = ((ppf n) |^ m) . b1 ) A1: m >= 0 + 1 by NAT_1:13; A2: ((ppf n) |^ m) . i = ((ppf n) . i) |^ m by Def6; assume i in SetPrimes ; ::_thesis: (ppf (n |^ m)) . b1 = ((ppf n) |^ m) . b1 then reconsider p = i as prime Element of NAT by NEWTON:def_6; A3: p |-count (n |^ m) = m * (p |-count n) by Th32; percases ( p |-count n = 0 or p |-count n <> 0 ) ; supposeA4: p |-count n = 0 ; ::_thesis: (ppf (n |^ m)) . b1 = ((ppf n) |^ m) . b1 hence (ppf (n |^ m)) . i = 0 by A3, Th55 .= 0 |^ m by A1, NEWTON:11 .= ((ppf n) |^ m) . i by A2, A4, Th55 ; ::_thesis: verum end; supposeA5: p |-count n <> 0 ; ::_thesis: (ppf (n |^ m)) . b1 = ((ppf n) |^ m) . b1 hence (ppf (n |^ m)) . i = p |^ (p |-count (n |^ m)) by A3, Th56 .= (p |^ (p |-count n)) |^ m by A3, NEWTON:9 .= ((ppf n) |^ m) . i by A2, A5, Th56 ; ::_thesis: verum end; end; end; hence ppf (n |^ m) = (ppf n) |^ m by PBOOLE:3; ::_thesis: verum end; theorem :: NAT_3:61 for n being non empty Nat holds Product (ppf n) = n proof let n be non empty Nat; ::_thesis: Product (ppf n) = n defpred S1[ Nat] means for n being non empty Nat st support (ppf n) c= Seg $1 holds Product (ppf n) = n; A1: support (ppf n) = support (pfexp n) by Def9; A2: S1[ 0 ] proof let n be non empty Nat; ::_thesis: ( support (ppf n) c= Seg 0 implies Product (ppf n) = n ) A3: {} c= support (ppf n) by XBOOLE_1:2; assume support (ppf n) c= Seg 0 ; ::_thesis: Product (ppf n) = n then A4: support (ppf n) = {} by A3, XBOOLE_0:def_10; A5: now__::_thesis:_not_n_<>_1 reconsider k = n as Nat ; assume n <> 1 ; ::_thesis: contradiction then k > 1 by NAT_1:53; then k >= 1 + 1 by NAT_1:13; then ex p being Element of NAT st ( p is prime & p divides k ) by INT_2:31; then not support (pfexp n) is empty by Th37; hence contradiction by A4, Def9; ::_thesis: verum end; ppf n = EmptyBag SetPrimes by A4, BAGORDER:19; hence Product (ppf n) = n by A5, Th20; ::_thesis: verum end; A6: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A7: S1[k] ; ::_thesis: S1[k + 1] let n be non empty Nat; ::_thesis: ( support (ppf n) c= Seg (k + 1) implies Product (ppf n) = n ) assume A8: support (ppf n) c= Seg (k + 1) ; ::_thesis: Product (ppf n) = n A9: support (ppf n) = support (pfexp n) by Def9; percases ( not support (ppf n) c= Seg k or support (ppf n) c= Seg k ) ; supposeA10: not support (ppf n) c= Seg k ; ::_thesis: Product (ppf n) = n set p = k + 1; set e = (k + 1) |-count n; set s = (k + 1) |^ ((k + 1) |-count n); A11: now__::_thesis:_k_+_1_in_support_(ppf_n) assume A12: not k + 1 in support (ppf n) ; ::_thesis: contradiction support (ppf n) c= Seg k proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (ppf n) or x in Seg k ) assume A13: x in support (ppf n) ; ::_thesis: x in Seg k then reconsider m = x as Nat ; m <= k + 1 by A8, A13, FINSEQ_1:1; then m < k + 1 by A12, A13, XXREAL_0:1; then A14: m <= k by NAT_1:13; x is Prime by A9, A13, Th34; then 1 <= m by INT_2:def_4; hence x in Seg k by A14, FINSEQ_1:1; ::_thesis: verum end; hence contradiction by A10; ::_thesis: verum end; then A15: k + 1 is Prime by A9, Th34; then A16: k + 1 > 1 by INT_2:def_4; then (k + 1) |^ ((k + 1) |-count n) divides n by Def7; then consider t being Nat such that A17: n = ((k + 1) |^ ((k + 1) |-count n)) * t by NAT_D:def_3; reconsider s = (k + 1) |^ ((k + 1) |-count n), t = t as non empty Nat by A17; A18: dom (ppf s) = SetPrimes by PARTFUN1:def_2; (pfexp n) . (k + 1) = (k + 1) |-count n by A15, Def8; then A19: (k + 1) |-count n <> 0 by A9, A11, PRE_POLY:def_7; reconsider s1 = s, t1 = t as non empty Nat ; A20: support (ppf t) = support (pfexp t) by Def9; A21: support (ppf t) c= Seg k proof set f = (k + 1) |-count t; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (ppf t) or x in Seg k ) assume A22: x in support (ppf t) ; ::_thesis: x in Seg k then reconsider m = x as Nat ; A23: x in support (pfexp t) by A22, Def9; A24: now__::_thesis:_not_m_=_k_+_1 assume A25: m = k + 1 ; ::_thesis: contradiction (pfexp t) . (k + 1) = (k + 1) |-count t by A15, Def8; then (k + 1) |-count t <> 0 by A23, A25, PRE_POLY:def_7; then (k + 1) |-count t >= 0 + 1 by NAT_1:13; then consider g being Nat such that A26: (k + 1) |-count t = 1 + g by NAT_1:10; (k + 1) |^ ((k + 1) |-count t) divides t by A16, Def7; then consider u being Nat such that A27: t = ((k + 1) |^ ((k + 1) |-count t)) * u by NAT_D:def_3; n = s * ((((k + 1) |^ g) * (k + 1)) * u) by A17, A26, A27, NEWTON:6 .= (s * (k + 1)) * (((k + 1) |^ g) * u) .= ((k + 1) |^ (((k + 1) |-count n) + 1)) * (((k + 1) |^ g) * u) by NEWTON:6 ; then (k + 1) |^ (((k + 1) |-count n) + 1) divides n by NAT_D:def_3; hence contradiction by A16, Def7; ::_thesis: verum end; support (ppf t) c= support (ppf n) by A9, A17, A20, Th45; then m in support (ppf n) by A22; then m <= k + 1 by A8, FINSEQ_1:1; then m < k + 1 by A24, XXREAL_0:1; then A28: m <= k by NAT_1:13; x is Prime by A23, Th34; then 1 <= m by INT_2:def_4; hence x in Seg k by A28, FINSEQ_1:1; ::_thesis: verum end; s1,t1 are_relative_prime proof set u = s1 gcd t1; A29: s1 gcd t1 divides t1 by NAT_D:def_5; s1 gcd t1 <> 0 by INT_2:5; then A30: 0 + 1 <= s1 gcd t1 by NAT_1:13; assume s1 gcd t1 <> 1 ; :: according to INT_2:def_3 ::_thesis: contradiction then s1 gcd t1 > 1 by A30, XXREAL_0:1; then s1 gcd t1 >= 1 + 1 by NAT_1:13; then consider r being Element of NAT such that A31: r is prime and A32: r divides s1 gcd t1 by INT_2:31; s1 gcd t1 divides s1 by NAT_D:def_5; then r divides s1 by A32, NAT_D:4; then r divides k + 1 by A31, Th5; then ( r = 1 or r = k + 1 ) by A15, INT_2:def_4; then k + 1 divides t1 by A31, A32, A29, INT_2:def_4, NAT_D:4; then k + 1 in support (pfexp t) by A15, Th37; then k + 1 <= k by A20, A21, FINSEQ_1:1; hence contradiction by NAT_1:13; ::_thesis: verum end; then A33: ppf n = (ppf s) + (ppf t) by A17, Th58; consider f being FinSequence of COMPLEX such that A34: Product (ppf s) = Product f and A35: f = (ppf s) * (canFS (support (ppf s))) by Def5; support (ppf s) = support (pfexp s) by Def9; then A36: support (ppf s) = {(k + 1)} by A15, A19, Th42; then f = (ppf s) * <*(k + 1)*> by A35, UPROOTS:4 .= <*((ppf s) . (k + 1))*> by A11, A18, FINSEQ_2:34 ; then A37: Product (ppf s) = (ppf s) . (k + 1) by A34, RVSUM_1:95 .= s by A15, A19, Th59 ; now__::_thesis:_not_(support_(ppf_s))_/\_(support_(ppf_t))_<>_{} assume (support (ppf s)) /\ (support (ppf t)) <> {} ; ::_thesis: contradiction then consider x being set such that A38: x in (support (ppf s)) /\ (support (ppf t)) by XBOOLE_0:def_1; x in support (ppf s) by A38, XBOOLE_0:def_4; then A39: x = k + 1 by A36, TARSKI:def_1; x in support (ppf t) by A38, XBOOLE_0:def_4; then k + 1 <= k by A21, A39, FINSEQ_1:1; hence contradiction by NAT_1:13; ::_thesis: verum end; then A40: support (ppf s) misses support (ppf t) by XBOOLE_0:def_7; Product (ppf t) = t by A7, A21; hence Product (ppf n) = n by A17, A40, A33, A37, Th19; ::_thesis: verum end; suppose support (ppf n) c= Seg k ; ::_thesis: Product (ppf n) = n hence Product (ppf n) = n by A7; ::_thesis: verum end; end; end; A41: for k being Nat holds S1[k] from NAT_1:sch_2(A2, A6); percases ( support (ppf n) is empty or not support (ppf n) is empty ) ; suppose support (ppf n) is empty ; ::_thesis: Product (ppf n) = n hence Product (ppf n) = n by A2; ::_thesis: verum end; suppose not support (ppf n) is empty ; ::_thesis: Product (ppf n) = n then reconsider S = support (ppf n) as non empty finite Subset of NAT by XBOOLE_1:1; support (ppf n) c= Seg (max S) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support (ppf n) or x in Seg (max S) ) assume A42: x in support (ppf n) ; ::_thesis: x in Seg (max S) then reconsider m = x as Nat ; x is Prime by A1, A42, Th34; then A43: 1 <= m by INT_2:def_4; m <= max S by A42, XXREAL_2:def_8; hence x in Seg (max S) by A43, FINSEQ_1:1; ::_thesis: verum end; hence Product (ppf n) = n by A41; ::_thesis: verum end; end; end;