defpred S₁[ Nat] means for n being non zero Nat st ( for p being Prime st p divides n holds
p <= $1 ) holds
card (divisors (n,4,3)) <= card (divisors (n,4,1));
A1: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let i be Nat; :: thesis: ( ( for n being Nat st n < i holds
S₁[n] ) implies S₁[i] )
assume A2: for n being Nat st n < i holds
S₁[n] ; :: thesis: S₁[i]
let n be non zero Nat; :: thesis: ( ( for p being Prime st p divides n holds
p <= i ) implies card (divisors (n,4,3)) <= card (divisors (n,4,1)) )
assume A3: for p being Prime st p divides n holds
p <= i ; :: thesis: card (divisors (n,4,3)) <= card (divisors (n,4,1))

per cases ( n = 1 or n <> 1 ) ;

suppose A4: n = 1 ; :: thesis: card (divisors (n,4,3)) <= card (divisors (n,4,1))

( 2 is prime & 2 |^ 0 = 1 ) by NEWTON:4, INT_2:28;
hence card (divisors (n,4,3)) <= card (divisors (n,4,1)) by A4, Lm6; :: thesis: verum

end;

suppose A5: n <> 1 ; :: thesis: card (divisors (n,4,3)) <= card (divisors (n,4,1))

n >= 1 + 0 by NAT_1:9;
then n > 1 by A5, XXREAL_0:1;
then consider p being Prime such that
A6: p divides n and
A7: for q being Prime st q divides n holds
q <= p by Th20;
consider k, m being positive Nat such that
A8: ( 0 < k & n = m * (p |^ k) & m,p are_coprime ) by A6, Th21;
m >= 1 by NAT_1:14;

per cases then ( m = 1 or m > 1 ) by XXREAL_0:1;

suppose m = 1 ; :: thesis: card (divisors (n,4,3)) <= card (divisors (n,4,1))

hence card (divisors (n,4,3)) <= card (divisors (n,4,1)) by A8, Lm6; :: thesis: verum

end;

suppose m > 1 ; :: thesis: card (divisors (n,4,3)) <= card (divisors (n,4,1))

then consider q being Prime such that
A9: q divides m and
A10: for r being Prime st r divides m holds
r <= q by Th20;
A11: p <= i by A3, A6;
q < p

proof

A12: q <= p by A7, A9, A8, INT_2:2;
assume q >= p ; :: thesis: contradiction
then p divides 1 * m by A9, A12, XXREAL_0:1;
then p divides 1 by A8, INT_2:25;
then ( p = 1 or p = - 1 ) by INT_2:13;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

then A13: q < i by A11, XXREAL_0:2;
set B1 = divisors (m,4,1);
set B3 = divisors (m,4,3);
set C1 = divisors ((p |^ k),4,1);
set C3 = divisors ((p |^ k),4,3);
set X1 = divisors (n,4,1);
set X3 = divisors (n,4,3);
A14: card (divisors (m,4,3)) <= card (divisors (m,4,1)) by A10, A13, A2;
defpred S₂[ object , object ] means for x, y being Nat st $1 = [x,y] holds
$2 = x * y;
A15: for x being object st x in [:((divisors (m,4,1)) \/ (divisors (m,4,3))),((divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3))):] holds
ex y being object st
( y in (divisors (n,4,1)) \/ (divisors (n,4,3)) & S₂[x,y] )

proof

let x be object ; :: thesis: ( x in [:((divisors (m,4,1)) \/ (divisors (m,4,3))),((divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3))):] implies ex y being object st
( y in (divisors (n,4,1)) \/ (divisors (n,4,3)) & S₂[x,y] ) )
assume A16: x in [:((divisors (m,4,1)) \/ (divisors (m,4,3))),((divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3))):] ; :: thesis: ex y being object st
( y in (divisors (n,4,1)) \/ (divisors (n,4,3)) & S₂[x,y] )
consider b, c being object such that
A17: ( b in (divisors (m,4,1)) \/ (divisors (m,4,3)) & c in (divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3)) & x = [b,c] ) by A16, ZFMISC_1:def 2;
reconsider b = b, c = c as Nat by A17;
take bc = b * c; :: thesis: ( bc in (divisors (n,4,1)) \/ (divisors (n,4,3)) & S₂[x,bc] )
A18: ( ( b mod 4 = 1 or b mod 4 = 3 ) & b divides m ) by A17, Th13;
( ( c mod 4 = 1 or c mod 4 = 3 ) & c divides p |^ k ) by A17, Th13;
then ( ( (b * c) mod 4 = 1 or (b * c) mod 4 = 3 ) & b * c divides n ) by A8, A18, NAT_3:1, Th8, Th9;
hence bc in (divisors (n,4,1)) \/ (divisors (n,4,3)) by Th13; :: thesis: S₂[x,bc]
let i, j be Nat; :: thesis: ( x = [i,j] implies bc = i * j )
assume x = [i,j] ; :: thesis: bc = i * j
then ( i = b & j = c ) by A17, XTUPLE_0:1;
hence bc = i * j ; :: thesis: verum

end;

consider f being Function such that
A19: ( dom f = [:((divisors (m,4,1)) \/ (divisors (m,4,3))),((divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3))):] & rng f c= (divisors (n,4,1)) \/ (divisors (n,4,3)) ) and
A20: for x being object st x in [:((divisors (m,4,1)) \/ (divisors (m,4,3))),((divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3))):] holds
S₂[x,f . x] from FUNCT_1:sch 6(A15);
A21: (divisors (n,4,1)) \/ (divisors (n,4,3)) c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (divisors (n,4,1)) \/ (divisors (n,4,3)) or x in rng f )
assume A22: x in (divisors (n,4,1)) \/ (divisors (n,4,3)) ; :: thesis: x in rng f
then reconsider x = x as Nat ;
A23: ( ( x mod 4 = 1 or x mod 4 = 3 ) & x divides m * (p |^ k) ) by A8, A22, Th13;
consider a, b being Nat such that
A24: ( a divides m & b divides p |^ k & x = a * b ) by A8, A22, Th13, NUMBER12:14;
( ( a mod 4 = 1 or a mod 4 = 3 ) & ( b mod 4 = 1 or b mod 4 = 3 ) ) by A23, A24, Th7, Th6;
then ( a in (divisors (m,4,1)) \/ (divisors (m,4,3)) & b in (divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3)) ) by A24, Th13;
then A25: [a,b] in [:((divisors (m,4,1)) \/ (divisors (m,4,3))),((divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3))):] by ZFMISC_1:def 2;
then f . [a,b] = x by A24, A20;
hence x in rng f by A25, A19, FUNCT_1:def 3; :: thesis: verum

end;

then A26: rng f = (divisors (n,4,1)) \/ (divisors (n,4,3)) by A19, XBOOLE_0:def 10;
A27: f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume A28: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
consider b1, c1 being object such that
A29: ( b1 in (divisors (m,4,1)) \/ (divisors (m,4,3)) & c1 in (divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3)) & x1 = [b1,c1] ) by A19, A28, ZFMISC_1:def 2;
consider b2, c2 being object such that
A30: ( b2 in (divisors (m,4,1)) \/ (divisors (m,4,3)) & c2 in (divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3)) & x2 = [b2,c2] ) by A19, A28, ZFMISC_1:def 2;
reconsider b1 = b1, c1 = c1, b2 = b2, c2 = c2 as Nat by A29, A30;
consider t1 being Element of NAT such that
A31: ( c1 = p |^ t1 & t1 <= k ) by PEPIN:34, A29, Th13;
consider t2 being Element of NAT such that
A32: ( c2 = p |^ t2 & t2 <= k ) by A30, Th13, PEPIN:34;
A33: ( c1 in NatDivisors (p |^ k) & c2 in NatDivisors (p |^ k) ) by A31, A32, A29, A30, Th13, MOEBIUS1:39;
( ( b1 mod 4 = 1 or b1 mod 4 = 3 ) & ( b2 mod 4 = 1 or b2 mod 4 = 3 ) ) by A29, A30, Th13;
then ( b1 <> 0 & b2 <> 0 ) ;
then A34: ( b1 in NatDivisors m & b2 in NatDivisors m ) by A29, A30, Th13, MOEBIUS1:39;
A35: m,p |^ k are_coprime by A8, WSIERP_1:10;
( f . x1 = b1 * c1 & f . x1 = b2 * c2 ) by A28, A29, A30, A19, A20;
then ( b1 = b2 & c1 = c2 ) by A33, A34, A35, NAT_5:15;
hence x1 = x2 by A29, A30; :: thesis: verum

end;

A36: card [:((divisors (m,4,1)) \/ (divisors (m,4,3))),((divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3))):] = (card ((divisors (m,4,1)) \/ (divisors (m,4,3)))) * (card ((divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3)))) by CARD_2:46;
A37: ( divisors (m,4,1) misses divisors (m,4,3) & divisors ((p |^ k),4,1) misses divisors ((p |^ k),4,3) & divisors (n,4,1) misses divisors (n,4,3) ) by Th14;
A38: ( card ((divisors (m,4,1)) \/ (divisors (m,4,3))) = (card (divisors (m,4,1))) + (card (divisors (m,4,3))) & card ((divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3))) = (card (divisors ((p |^ k),4,1))) + (card (divisors ((p |^ k),4,3))) & card ((divisors (n,4,1)) \/ (divisors (n,4,3))) = (card (divisors (n,4,1))) + (card (divisors (n,4,3))) ) by Th14, CARD_2:40;
A39: f .: [:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] c= divisors (n,4,3)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: [:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] or y in divisors (n,4,3) )
assume y in f .: [:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] ; :: thesis: y in divisors (n,4,3)
then consider x being object such that
A40: ( x in dom f & x in [:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] & y = f . x ) by FUNCT_1:def 6;
consider b, c being object such that
A41: ( b in divisors (m,4,1) & c in divisors ((p |^ k),4,3) & x = [b,c] ) by A40, ZFMISC_1:def 2;
reconsider b = b, c = c as Nat by A41;
A42: f . x = b * c by A19, A20, A40, A41;
( b mod 4 = 1 & b divides m & c mod 4 = 3 & c divides p |^ k ) by A41, Th12;
then ( (b * c) mod 4 = 3 & b * c divides n ) by A8, Th9, NAT_3:1;
hence y in divisors (n,4,3) by A42, A40; :: thesis: verum

end;

f .: [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):] c= divisors (n,4,3)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):] or y in divisors (n,4,3) )
assume y in f .: [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):] ; :: thesis: y in divisors (n,4,3)
then consider x being object such that
A43: ( x in dom f & x in [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):] & y = f . x ) by FUNCT_1:def 6;
consider b, c being object such that
A44: ( b in divisors (m,4,3) & c in divisors ((p |^ k),4,1) & x = [b,c] ) by A43, ZFMISC_1:def 2;
reconsider b = b, c = c as Nat by A44;
A45: f . x = b * c by A19, A20, A43, A44;
( b mod 4 = 3 & b divides m & c mod 4 = 1 & c divides p |^ k ) by A44, Th12;
then ( (b * c) mod 4 = 3 & b * c divides n ) by A8, Th9, NAT_3:1;
hence y in divisors (n,4,3) by A45, A43; :: thesis: verum

end;

then (f .: [:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):]) \/ (f .: [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):]) c= divisors (n,4,3) by A39, XBOOLE_1:8;
then A46: f .: ([:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):]) c= divisors (n,4,3) by RELAT_1:120;
dom f = (([:(divisors (m,4,1)),(divisors ((p |^ k),4,1)):] \/ [:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):]) \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):]) \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,3)):] by A19, ZFMISC_1:98
.= ([:(divisors (m,4,1)),(divisors ((p |^ k),4,1)):] \/ ([:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):])) \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,3)):] by XBOOLE_1:4
.= ([:(divisors (m,4,1)),(divisors ((p |^ k),4,1)):] \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,3)):]) \/ ([:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):]) by XBOOLE_1:4 ;
then A47: [:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):] c= dom f by XBOOLE_1:7;
divisors (n,4,3) c= f .: ([:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):])

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in divisors (n,4,3) or y in f .: ([:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):]) )
assume A48: y in divisors (n,4,3) ; :: thesis: y in f .: ([:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):])
then y in (divisors (n,4,1)) \/ (divisors (n,4,3)) by XBOOLE_0:def 3;
then consider x being object such that
A49: ( x in dom f & f . x = y ) by A21, FUNCT_1:def 3;
consider b, c being object such that
A50: ( b in (divisors (m,4,1)) \/ (divisors (m,4,3)) & c in (divisors ((p |^ k),4,1)) \/ (divisors ((p |^ k),4,3)) & x = [b,c] ) by A19, A49, ZFMISC_1:def 2;
reconsider b = b, c = c as Nat by A50;
A51: ( b divides m & c divides p |^ k ) by A50, Th13;
b * c = y by A49, A50, A20, A19;
then (b * c) mod 4 = 3 by A48, Th12;
then ( ( b mod 4 = 1 & c mod 4 = 3 ) or ( b mod 4 = 3 & c mod 4 = 1 ) ) by Th7;
then ( ( b in divisors (m,4,1) & c in divisors ((p |^ k),4,3) ) or ( b in divisors (m,4,3) & c in divisors ((p |^ k),4,1) ) ) by A51;
then ( [b,c] in [:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] or [b,c] in [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):] ) by ZFMISC_1:def 2;
then [b,c] in [:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):] by XBOOLE_0:def 3;
hence y in f .: ([:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):]) by A49, A50, FUNCT_1:def 6; :: thesis: verum

end;

then divisors (n,4,3) = f .: ([:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):]) by A46, XBOOLE_0:def 10;
then A52: card (divisors (n,4,3)) = card ([:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):]) by A47, A27, CARD_1:33, CARD_1:5;
[:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] misses [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):] by A37, ZFMISC_1:104;
then A53: card ([:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):] \/ [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):]) = (card [:(divisors (m,4,1)),(divisors ((p |^ k),4,3)):]) + (card [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):]) by CARD_2:40
.= ((card (divisors (m,4,1))) * (card (divisors ((p |^ k),4,3)))) + (card [:(divisors (m,4,3)),(divisors ((p |^ k),4,1)):]) by CARD_2:46
.= ((card (divisors (m,4,1))) * (card (divisors ((p |^ k),4,3)))) + ((card (divisors (m,4,3))) * (card (divisors ((p |^ k),4,1)))) by CARD_2:46 ;
A54: (card (divisors (n,4,1))) + (card (divisors (n,4,3))) = ((card (divisors (m,4,1))) + (card (divisors (m,4,3)))) * ((card (divisors ((p |^ k),4,1))) + (card (divisors ((p |^ k),4,3)))) by A19, A26, CARD_1:70, A27, A36, A38;
( 0 <= (card (divisors (m,4,1))) - (card (divisors (m,4,3))) & 0 <= (card (divisors ((p |^ k),4,1))) - (card (divisors ((p |^ k),4,3))) ) by A14, Lm6, XREAL_1:48;
then 0 <= ((card (divisors (m,4,1))) - (card (divisors (m,4,3)))) * ((card (divisors ((p |^ k),4,1))) - (card (divisors ((p |^ k),4,3)))) ;
then 0 <= (((card (divisors (m,4,1))) * (card (divisors ((p |^ k),4,1)))) + ((card (divisors (m,4,3))) * (card (divisors ((p |^ k),4,3))))) - (((card (divisors (m,4,1))) * (card (divisors ((p |^ k),4,3)))) + ((card (divisors (m,4,3))) * (card (divisors ((p |^ k),4,1))))) ;
hence card (divisors (n,4,3)) <= card (divisors (n,4,1)) by A54, A52, A53, XREAL_1:49; :: thesis: verum

end;

end;

end;

end;

end;

A55: for k being Nat holds S₁[k] from NAT_1:sch 4(A1);
let n be non zero Nat; :: thesis: card (divisors (n,4,3)) <= card (divisors (n,4,1))

per cases ( n = 1 or n <> 1 ) ;

suppose A56: n = 1 ; :: thesis: card (divisors (n,4,3)) <= card (divisors (n,4,1))

( 2 is prime & 2 |^ 0 = 1 ) by NEWTON:4, INT_2:28;
hence card (divisors (n,4,3)) <= card (divisors (n,4,1)) by A56, Lm6; :: thesis: verum

end;

suppose A57: n <> 1 ; :: thesis: card (divisors (n,4,3)) <= card (divisors (n,4,1))

n >= 1 + 0 by NAT_1:9;
then n > 1 by A57, XXREAL_0:1;
then ex p being Prime st
( p divides n & ( for q being Prime st q divides n holds
q <= p ) ) by Th20;
hence card (divisors (n,4,3)) <= card (divisors (n,4,1)) by A55; :: thesis: verum

end;

end;