:: 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;