let p be Prime; :: thesis: for k being Nat holds card (NatDivisors (p |^ k)) = k + 1
let k be Nat; :: thesis: card (NatDivisors (p |^ k)) = k + 1
B1: { l where l is Element of NAT : l <= k } = k \/ {k}

proof

thus { l where l is Element of NAT : l <= k } c= k \/ {k} :: according to XBOOLE_0:def 10 :: thesis: k \/ {k} c= { l where l is Element of NAT : l <= k }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { l where l is Element of NAT : l <= k } or x in k \/ {k} )
assume x in { l where l is Element of NAT : l <= k } ; :: thesis: x in k \/ {k}
then consider ll being Element of NAT such that
A1: ( ll = x & ll <= k ) ;
( ll < k or ll = k ) by A1, XXREAL_0:1;
then ( ll in Segm k or ll in {k} ) by NAT_1:44, TARSKI:def 1;
hence x in k \/ {k} by A1, XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in k \/ {k} or x in { l where l is Element of NAT : l <= k } )
assume x in k \/ {k} ; :: thesis: x in { l where l is Element of NAT : l <= k }
then ( x in k or x in {k} ) by XBOOLE_0:def 3;
then A2: ( x in Segm k or x = k ) by TARSKI:def 1;
then reconsider ll = x as Element of NAT by ORDINAL1:def 12;
ll <= k by A2, NAT_1:44;
hence x in { l where l is Element of NAT : l <= k } ; :: thesis: verum

end;

B2: card (NatDivisors (p |^ k)) = card { (p |^ l) where l is Element of NAT : l <= k } by NAT_5:19;
deffunc H₁( Element of NAT ) -> set = p |^ $1;
set X = { l where l is Element of NAT : l <= k } ;
set YY = { H₁(w) where w is Element of NAT : w in { l where l is Element of NAT : l <= k } } ;
ZZ: { H₁(w) where w is Element of NAT : w in { l where l is Element of NAT : l <= k } } = { (p |^ l) where l is Element of NAT : l <= k }

proof

thus { H₁(w) where w is Element of NAT : w in { l where l is Element of NAT : l <= k } } c= { (p |^ l) where l is Element of NAT : l <= k } :: according to XBOOLE_0:def 10 :: thesis: { (p |^ l) where l is Element of NAT : l <= k } c= { H₁(w) where w is Element of NAT : w in { l where l is Element of NAT : l <= k } }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { H₁(w) where w is Element of NAT : w in { l where l is Element of NAT : l <= k } } or a in { (p |^ l) where l is Element of NAT : l <= k } )
assume a in { H₁(w) where w is Element of NAT : w in { l where l is Element of NAT : l <= k } } ; :: thesis: a in { (p |^ l) where l is Element of NAT : l <= k }
then consider w being Element of NAT such that
E1: ( a = H₁(w) & w in { l where l is Element of NAT : l <= k } ) ;
consider ll being Element of NAT such that
E2: ( ll = w & ll <= k ) by E1;
thus a in { (p |^ l) where l is Element of NAT : l <= k } by E1, E2; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (p |^ l) where l is Element of NAT : l <= k } or a in { H₁(w) where w is Element of NAT : w in { l where l is Element of NAT : l <= k } } )
assume a in { (p |^ l) where l is Element of NAT : l <= k } ; :: thesis: a in { H₁(w) where w is Element of NAT : w in { l where l is Element of NAT : l <= k } }
then consider ll being Element of NAT such that
E3: ( a = p |^ ll & ll <= k ) ;
( a = H₁(ll) & ll in { l where l is Element of NAT : l <= k } ) by E3;
hence a in { H₁(w) where w is Element of NAT : w in { l where l is Element of NAT : l <= k } } ; :: thesis: verum

end;

{ H₁(w) where w is Element of NAT : w in { l where l is Element of NAT : l <= k } } c= (Seg (p |^ k)) \/ {(p |^ k)}

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { H₁(w) where w is Element of NAT : w in { l where l is Element of NAT : l <= k } } or u in (Seg (p |^ k)) \/ {(p |^ k)} )
assume u in { H₁(w) where w is Element of NAT : w in { l where l is Element of NAT : l <= k } } ; :: thesis: u in (Seg (p |^ k)) \/ {(p |^ k)}
then consider ll being Element of NAT such that
W1: ( u = p |^ ll & ll <= k ) by ZZ;
W0: p > 1 by INT_2:def 4;
then p |^ ll >= p |^ 0 by PREPOWER:93;
then W2: 1 <= p |^ ll by NEWTON:4;
p |^ ll <= p |^ k by W1, W0, PREPOWER:93;
then p |^ ll in Seg (p |^ k) by W2;
hence u in (Seg (p |^ k)) \/ {(p |^ k)} by W1, XBOOLE_0:def 3; :: thesis: verum

end;

then reconsider YY = { H₁(w) where w is Element of NAT : w in { l where l is Element of NAT : l <= k } } as finite set ;
set FF = { l where l is Element of NAT : l <= k } ;
deffunc H₂( Element of NAT ) -> Element of NAT = In ((p |^ $1),NAT);
ex f being Function of NAT,NAT st
for x being Element of NAT holds f . x = H₂(x) from FUNCT_2:sch 4();
then consider ff being Function of NAT,NAT such that
C0: for x being Element of NAT holds ff . x = H₂(x) ;
set f = ff | { l where l is Element of NAT : l <= k } ;
{ l where l is Element of NAT : l <= k } c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { l where l is Element of NAT : l <= k } or x in NAT )
assume x in { l where l is Element of NAT : l <= k } ; :: thesis: x in NAT
then consider ll being Element of NAT such that
G1: ( x = ll & ll <= k ) ;
thus x in NAT by G1; :: thesis: verum

end;

then { l where l is Element of NAT : l <= k } c= dom ff by FUNCT_2:def 1;
then Z1: dom (ff | { l where l is Element of NAT : l <= k } ) = { l where l is Element of NAT : l <= k } by RELAT_1:62;
Z2: rng (ff | { l where l is Element of NAT : l <= k } ) = YY

proof

thus rng (ff | { l where l is Element of NAT : l <= k } ) c= YY :: according to XBOOLE_0:def 10 :: thesis: YY c= rng (ff | { l where l is Element of NAT : l <= k } )

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (ff | { l where l is Element of NAT : l <= k } ) or y in YY )
assume y in rng (ff | { l where l is Element of NAT : l <= k } ) ; :: thesis: y in YY
then consider yy being object such that
C1: ( yy in dom (ff | { l where l is Element of NAT : l <= k } ) & y = (ff | { l where l is Element of NAT : l <= k } ) . yy ) by FUNCT_1:def 3;
consider ll being Element of NAT such that
C2: ( ll = yy & ll <= k ) by C1, Z1;
C3: y = (ff | { l where l is Element of NAT : l <= k } ) . ll by C1, C2;
ll in { l where l is Element of NAT : l <= k } by C2;
then y = ff . ll by C3, FUNCT_1:49;
then y = In ((p |^ ll),NAT) by C0;
hence y in YY by ZZ, C2; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in YY or y in rng (ff | { l where l is Element of NAT : l <= k } ) )
assume y in YY ; :: thesis: y in rng (ff | { l where l is Element of NAT : l <= k } )
then consider ll being Element of NAT such that
D1: ( y = p |^ ll & ll <= k ) by ZZ;
D5: ll in { l where l is Element of NAT : l <= k } by D1;
then D6: ll in dom (ff | { l where l is Element of NAT : l <= k } ) by Z1;
D7: (ff | { l where l is Element of NAT : l <= k } ) . ll = ff . ll by D5, FUNCT_1:49;
ff . ll = In ((p |^ ll),NAT) by C0
.= p |^ ll ;
hence y in rng (ff | { l where l is Element of NAT : l <= k } ) by D1, D7, D6, FUNCT_1:def 3; :: thesis: verum

end;

for x1, x2 being object st x1 in dom ff & x2 in dom ff & ff . x1 = ff . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom ff & x2 in dom ff & ff . x1 = ff . x2 implies x1 = x2 )
assume DD: ( x1 in dom ff & x2 in dom ff & ff . x1 = ff . x2 ) ; :: thesis: x1 = x2
then reconsider n1 = x1, n2 = x2 as Element of NAT by FUNCT_2:def 1;
DA: ( p > 0 & p <> 1 ) by INT_2:def 4;
D9: ff . x1 = In ((p |^ n1),NAT) by C0
.= p |^ n1 ;
ff . x2 = In ((p |^ n2),NAT) by C0
.= p |^ n2 ;
then p to_power n1 = p to_power n2 by DD, D9;
hence x1 = x2 by DA, POWER:50; :: thesis: verum

end;

then ff is one-to-one by FUNCT_1:def 4;
then card (dom (ff | { l where l is Element of NAT : l <= k } )) = card (rng (ff | { l where l is Element of NAT : l <= k } )) by CARD_1:70;
then card { (p |^ l) where l is Element of NAT : l <= k } = card { l where l is Element of NAT : l <= k } by ZZ, Z1, Z2;
hence card (NatDivisors (p |^ k)) = k + 1 by B1, B2, CardSucc; :: thesis: verum