MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  chtublem Unicode version

Theorem chtublem 20466
Description: Lemma for chtub 20467. (Contributed by Mario Carneiro, 13-Mar-2014.)
Assertion
Ref Expression
chtublem  |-  ( N  e.  NN  ->  ( theta `  ( ( 2  x.  N )  - 
1 ) )  <_ 
( ( theta `  N
)  +  ( ( log `  4 )  x.  ( N  - 
1 ) ) ) )

Proof of Theorem chtublem
Dummy variables  k  n  p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2nn 9893 . . . . . 6  |-  2  e.  NN
2 nnmulcl 9785 . . . . . 6  |-  ( ( 2  e.  NN  /\  N  e.  NN )  ->  ( 2  x.  N
)  e.  NN )
31, 2mpan 651 . . . . 5  |-  ( N  e.  NN  ->  (
2  x.  N )  e.  NN )
43nnred 9777 . . . 4  |-  ( N  e.  NN  ->  (
2  x.  N )  e.  RR )
5 peano2rem 9129 . . . 4  |-  ( ( 2  x.  N )  e.  RR  ->  (
( 2  x.  N
)  -  1 )  e.  RR )
64, 5syl 15 . . 3  |-  ( N  e.  NN  ->  (
( 2  x.  N
)  -  1 )  e.  RR )
7 chtcl 20363 . . 3  |-  ( ( ( 2  x.  N
)  -  1 )  e.  RR  ->  ( theta `  ( ( 2  x.  N )  - 
1 ) )  e.  RR )
86, 7syl 15 . 2  |-  ( N  e.  NN  ->  ( theta `  ( ( 2  x.  N )  - 
1 ) )  e.  RR )
9 nnre 9769 . . . 4  |-  ( N  e.  NN  ->  N  e.  RR )
10 chtcl 20363 . . . 4  |-  ( N  e.  RR  ->  ( theta `  N )  e.  RR )
119, 10syl 15 . . 3  |-  ( N  e.  NN  ->  ( theta `  N )  e.  RR )
12 nnnn0 9988 . . . . . . 7  |-  ( N  e.  NN  ->  N  e.  NN0 )
13 df-2 9820 . . . . . . . . . . . . 13  |-  2  =  ( 1  +  1 )
1413oveq1i 5884 . . . . . . . . . . . 12  |-  ( 2  -  1 )  =  ( ( 1  +  1 )  -  1 )
15 ax-1cn 8811 . . . . . . . . . . . . 13  |-  1  e.  CC
16 pncan 9073 . . . . . . . . . . . . 13  |-  ( ( 1  e.  CC  /\  1  e.  CC )  ->  ( ( 1  +  1 )  -  1 )  =  1 )
1715, 15, 16mp2an 653 . . . . . . . . . . . 12  |-  ( ( 1  +  1 )  -  1 )  =  1
1814, 17eqtri 2316 . . . . . . . . . . 11  |-  ( 2  -  1 )  =  1
1918oveq2i 5885 . . . . . . . . . 10  |-  ( ( 2  x.  N )  -  ( 2  -  1 ) )  =  ( ( 2  x.  N )  -  1 )
203nncnd 9778 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
2  x.  N )  e.  CC )
21 2cn 9832 . . . . . . . . . . . . 13  |-  2  e.  CC
22 subsub 9093 . . . . . . . . . . . . 13  |-  ( ( ( 2  x.  N
)  e.  CC  /\  2  e.  CC  /\  1  e.  CC )  ->  (
( 2  x.  N
)  -  ( 2  -  1 ) )  =  ( ( ( 2  x.  N )  -  2 )  +  1 ) )
2321, 15, 22mp3an23 1269 . . . . . . . . . . . 12  |-  ( ( 2  x.  N )  e.  CC  ->  (
( 2  x.  N
)  -  ( 2  -  1 ) )  =  ( ( ( 2  x.  N )  -  2 )  +  1 ) )
2420, 23syl 15 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( 2  x.  N
)  -  ( 2  -  1 ) )  =  ( ( ( 2  x.  N )  -  2 )  +  1 ) )
25 nncn 9770 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  N  e.  CC )
26 subdi 9229 . . . . . . . . . . . . . . 15  |-  ( ( 2  e.  CC  /\  N  e.  CC  /\  1  e.  CC )  ->  (
2  x.  ( N  -  1 ) )  =  ( ( 2  x.  N )  -  ( 2  x.  1 ) ) )
2721, 15, 26mp3an13 1268 . . . . . . . . . . . . . 14  |-  ( N  e.  CC  ->  (
2  x.  ( N  -  1 ) )  =  ( ( 2  x.  N )  -  ( 2  x.  1 ) ) )
2825, 27syl 15 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  (
2  x.  ( N  -  1 ) )  =  ( ( 2  x.  N )  -  ( 2  x.  1 ) ) )
2921mulid1i 8855 . . . . . . . . . . . . . 14  |-  ( 2  x.  1 )  =  2
3029oveq2i 5885 . . . . . . . . . . . . 13  |-  ( ( 2  x.  N )  -  ( 2  x.  1 ) )  =  ( ( 2  x.  N )  -  2 )
3128, 30syl6eq 2344 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
2  x.  ( N  -  1 ) )  =  ( ( 2  x.  N )  - 
2 ) )
3231oveq1d 5889 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( 2  x.  ( N  -  1 ) )  +  1 )  =  ( ( ( 2  x.  N )  -  2 )  +  1 ) )
3324, 32eqtr4d 2331 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( 2  x.  N
)  -  ( 2  -  1 ) )  =  ( ( 2  x.  ( N  - 
1 ) )  +  1 ) )
3419, 33syl5eqr 2342 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( 2  x.  N
)  -  1 )  =  ( ( 2  x.  ( N  - 
1 ) )  +  1 ) )
35 2nn0 9998 . . . . . . . . . . 11  |-  2  e.  NN0
36 nnm1nn0 10021 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  NN0 )
37 nn0mulcl 10016 . . . . . . . . . . 11  |-  ( ( 2  e.  NN0  /\  ( N  -  1
)  e.  NN0 )  ->  ( 2  x.  ( N  -  1 ) )  e.  NN0 )
3835, 36, 37sylancr 644 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
2  x.  ( N  -  1 ) )  e.  NN0 )
39 nn0p1nn 10019 . . . . . . . . . 10  |-  ( ( 2  x.  ( N  -  1 ) )  e.  NN0  ->  ( ( 2  x.  ( N  -  1 ) )  +  1 )  e.  NN )
4038, 39syl 15 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( 2  x.  ( N  -  1 ) )  +  1 )  e.  NN )
4134, 40eqeltrd 2370 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( 2  x.  N
)  -  1 )  e.  NN )
42 nnnn0 9988 . . . . . . . 8  |-  ( ( ( 2  x.  N
)  -  1 )  e.  NN  ->  (
( 2  x.  N
)  -  1 )  e.  NN0 )
4341, 42syl 15 . . . . . . 7  |-  ( N  e.  NN  ->  (
( 2  x.  N
)  -  1 )  e.  NN0 )
44 1re 8853 . . . . . . . . . . 11  |-  1  e.  RR
4544a1i 10 . . . . . . . . . 10  |-  ( N  e.  NN  ->  1  e.  RR )
46 nnge1 9788 . . . . . . . . . 10  |-  ( N  e.  NN  ->  1  <_  N )
4745, 9, 9, 46leadd2dd 9403 . . . . . . . . 9  |-  ( N  e.  NN  ->  ( N  +  1 )  <_  ( N  +  N ) )
48252timesd 9970 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
2  x.  N )  =  ( N  +  N ) )
4947, 48breqtrrd 4065 . . . . . . . 8  |-  ( N  e.  NN  ->  ( N  +  1 )  <_  ( 2  x.  N ) )
50 leaddsub 9266 . . . . . . . . 9  |-  ( ( N  e.  RR  /\  1  e.  RR  /\  (
2  x.  N )  e.  RR )  -> 
( ( N  + 
1 )  <_  (
2  x.  N )  <-> 
N  <_  ( (
2  x.  N )  -  1 ) ) )
519, 45, 4, 50syl3anc 1182 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( N  +  1 )  <_  ( 2  x.  N )  <->  N  <_  ( ( 2  x.  N
)  -  1 ) ) )
5249, 51mpbid 201 . . . . . . 7  |-  ( N  e.  NN  ->  N  <_  ( ( 2  x.  N )  -  1 ) )
53 elfz2nn0 10837 . . . . . . 7  |-  ( N  e.  ( 0 ... ( ( 2  x.  N )  -  1 ) )  <->  ( N  e.  NN0  /\  ( ( 2  x.  N )  -  1 )  e. 
NN0  /\  N  <_  ( ( 2  x.  N
)  -  1 ) ) )
5412, 43, 52, 53syl3anbrc 1136 . . . . . 6  |-  ( N  e.  NN  ->  N  e.  ( 0 ... (
( 2  x.  N
)  -  1 ) ) )
55 bccl2 11351 . . . . . 6  |-  ( N  e.  ( 0 ... ( ( 2  x.  N )  -  1 ) )  ->  (
( ( 2  x.  N )  -  1 )  _C  N )  e.  NN )
5654, 55syl 15 . . . . 5  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  _C  N )  e.  NN )
5756nnrpd 10405 . . . 4  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  _C  N )  e.  RR+ )
5857relogcld 19990 . . 3  |-  ( N  e.  NN  ->  ( log `  ( ( ( 2  x.  N )  -  1 )  _C  N ) )  e.  RR )
5911, 58readdcld 8878 . 2  |-  ( N  e.  NN  ->  (
( theta `  N )  +  ( log `  (
( ( 2  x.  N )  -  1 )  _C  N ) ) )  e.  RR )
60 4re 9835 . . . . . 6  |-  4  e.  RR
61 4pos 9848 . . . . . 6  |-  0  <  4
6260, 61elrpii 10373 . . . . 5  |-  4  e.  RR+
63 relogcl 19948 . . . . 5  |-  ( 4  e.  RR+  ->  ( log `  4 )  e.  RR )
6462, 63ax-mp 8 . . . 4  |-  ( log `  4 )  e.  RR
6536nn0red 10035 . . . 4  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  RR )
66 remulcl 8838 . . . 4  |-  ( ( ( log `  4
)  e.  RR  /\  ( N  -  1
)  e.  RR )  ->  ( ( log `  4 )  x.  ( N  -  1 ) )  e.  RR )
6764, 65, 66sylancr 644 . . 3  |-  ( N  e.  NN  ->  (
( log `  4
)  x.  ( N  -  1 ) )  e.  RR )
6811, 67readdcld 8878 . 2  |-  ( N  e.  NN  ->  (
( theta `  N )  +  ( ( log `  4 )  x.  ( N  -  1 ) ) )  e.  RR )
69 iftrue 3584 . . . . . . . . . . . 12  |-  ( p  <_  ( ( 2  x.  N )  - 
1 )  ->  if ( p  <_  ( ( 2  x.  N )  -  1 ) ,  1 ,  0 )  =  1 )
7069adantl 452 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  p  <_  ( ( 2  x.  N )  -  1 ) )  ->  if ( p  <_  ( ( 2  x.  N )  - 
1 ) ,  1 ,  0 )  =  1 )
71 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  p  e.  Prime )  ->  p  e.  Prime )
7256adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( ( 2  x.  N )  - 
1 )  _C  N
)  e.  NN )
7371, 72pccld 12919 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) )  e.  NN0 )
74 nn0addge1 10026 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  RR  /\  ( p  pCnt  ( ( ( 2  x.  N
)  -  1 )  _C  N ) )  e.  NN0 )  -> 
1  <_  ( 1  +  ( p  pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
7544, 73, 74sylancr 644 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
1  <_  ( 1  +  ( p  pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
76 iftrue 3584 . . . . . . . . . . . . . . . 16  |-  ( p  <_  N  ->  if ( p  <_  N , 
1 ,  0 )  =  1 )
7776oveq1d 5889 . . . . . . . . . . . . . . 15  |-  ( p  <_  N  ->  ( if ( p  <_  N ,  1 ,  0 )  +  ( p 
pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) )  =  ( 1  +  ( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
7877breq2d 4051 . . . . . . . . . . . . . 14  |-  ( p  <_  N  ->  (
1  <_  ( if ( p  <_  N , 
1 ,  0 )  +  ( p  pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) )  <->  1  <_  ( 1  +  ( p 
pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) ) )
7975, 78syl5ibrcom 213 . . . . . . . . . . . . 13  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  <_  N  ->  1  <_  ( if ( p  <_  N , 
1 ,  0 )  +  ( p  pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) ) )
8079adantr 451 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  p  <_  ( ( 2  x.  N )  -  1 ) )  ->  ( p  <_  N  ->  1  <_  ( if ( p  <_  N ,  1 ,  0 )  +  ( p 
pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) ) )
81 prmnn 12777 . . . . . . . . . . . . . . . . . 18  |-  ( p  e.  Prime  ->  p  e.  NN )
8281ad2antlr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  ->  p  e.  NN )
83 simprl 732 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  ->  p  <_  ( ( 2  x.  N )  - 
1 ) )
84 prmz 12778 . . . . . . . . . . . . . . . . . . . 20  |-  ( p  e.  Prime  ->  p  e.  ZZ )
8541nnzd 10132 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN  ->  (
( 2  x.  N
)  -  1 )  e.  ZZ )
86 eluz 10257 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( p  e.  ZZ  /\  ( ( 2  x.  N )  -  1 )  e.  ZZ )  ->  ( ( ( 2  x.  N )  -  1 )  e.  ( ZZ>= `  p )  <->  p  <_  ( ( 2  x.  N )  - 
1 ) ) )
8784, 85, 86syl2anr 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( ( 2  x.  N )  - 
1 )  e.  (
ZZ>= `  p )  <->  p  <_  ( ( 2  x.  N
)  -  1 ) ) )
8887adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( ( ( 2  x.  N )  - 
1 )  e.  (
ZZ>= `  p )  <->  p  <_  ( ( 2  x.  N
)  -  1 ) ) )
8983, 88mpbird 223 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( ( 2  x.  N )  -  1 )  e.  ( ZZ>= `  p ) )
90 dvdsfac 12599 . . . . . . . . . . . . . . . . 17  |-  ( ( p  e.  NN  /\  ( ( 2  x.  N )  -  1 )  e.  ( ZZ>= `  p ) )  ->  p  ||  ( ! `  ( ( 2  x.  N )  -  1 ) ) )
9182, 89, 90syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  ->  p  ||  ( ! `  ( ( 2  x.  N )  -  1 ) ) )
92 id 19 . . . . . . . . . . . . . . . . . 18  |-  ( p  e.  Prime  ->  p  e. 
Prime )
93 faccl 11314 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 2  x.  N
)  -  1 )  e.  NN0  ->  ( ! `
 ( ( 2  x.  N )  - 
1 ) )  e.  NN )
9443, 93syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  ( ! `  ( (
2  x.  N )  -  1 ) )  e.  NN )
95 pcelnn 12938 . . . . . . . . . . . . . . . . . 18  |-  ( ( p  e.  Prime  /\  ( ! `  ( (
2  x.  N )  -  1 ) )  e.  NN )  -> 
( ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) )  e.  NN  <->  p  ||  ( ! `  ( (
2  x.  N )  -  1 ) ) ) )
9692, 94, 95syl2anr 464 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) )  e.  NN  <->  p  ||  ( ! `  ( (
2  x.  N )  -  1 ) ) ) )
9796adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) )  e.  NN  <->  p  ||  ( ! `  ( (
2  x.  N )  -  1 ) ) ) )
9891, 97mpbird 223 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( p  pCnt  ( ! `  ( (
2  x.  N )  -  1 ) ) )  e.  NN )
9998nnge1d 9804 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
1  <_  ( p  pCnt  ( ! `  (
( 2  x.  N
)  -  1 ) ) ) )
100 iffalse 3585 . . . . . . . . . . . . . . . . 17  |-  ( -.  p  <_  N  ->  if ( p  <_  N ,  1 ,  0 )  =  0 )
101100oveq1d 5889 . . . . . . . . . . . . . . . 16  |-  ( -.  p  <_  N  ->  ( if ( p  <_  N ,  1 , 
0 )  +  ( p  pCnt  ( (
( 2  x.  N
)  -  1 )  _C  N ) ) )  =  ( 0  +  ( p  pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
102101ad2antll 709 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( if ( p  <_  N ,  1 ,  0 )  +  ( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) ) )  =  ( 0  +  ( p 
pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
10373nn0cnd 10036 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) )  e.  CC )
104103addid2d 9029 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( 0  +  ( p  pCnt  ( (
( 2  x.  N
)  -  1 )  _C  N ) ) )  =  ( p 
pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) )
105104adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( 0  +  ( p  pCnt  ( (
( 2  x.  N
)  -  1 )  _C  N ) ) )  =  ( p 
pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) )
106 bcval2 11334 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  ( 0 ... ( ( 2  x.  N )  -  1 ) )  ->  (
( ( 2  x.  N )  -  1 )  _C  N )  =  ( ( ! `
 ( ( 2  x.  N )  - 
1 ) )  / 
( ( ! `  ( ( ( 2  x.  N )  - 
1 )  -  N
) )  x.  ( ! `  N )
) ) )
10754, 106syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  _C  N )  =  ( ( ! `
 ( ( 2  x.  N )  - 
1 ) )  / 
( ( ! `  ( ( ( 2  x.  N )  - 
1 )  -  N
) )  x.  ( ! `  N )
) ) )
10848oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  e.  NN  ->  (
( 2  x.  N
)  -  1 )  =  ( ( N  +  N )  - 
1 ) )
10915a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( N  e.  NN  ->  1  e.  CC )
11025, 25, 109addsubassd 9193 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( N  e.  NN  ->  (
( N  +  N
)  -  1 )  =  ( N  +  ( N  -  1
) ) )
111108, 110eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  NN  ->  (
( 2  x.  N
)  -  1 )  =  ( N  +  ( N  -  1
) ) )
112111oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  -  N )  =  ( ( N  +  ( N  - 
1 ) )  -  N ) )
11336nn0cnd 10036 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  CC )
11425, 113pncan2d 9175 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  NN  ->  (
( N  +  ( N  -  1 ) )  -  N )  =  ( N  - 
1 ) )
115112, 114eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  -  N )  =  ( N  - 
1 ) )
116115fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  NN  ->  ( ! `  ( (
( 2  x.  N
)  -  1 )  -  N ) )  =  ( ! `  ( N  -  1
) ) )
117116oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  NN  ->  (
( ! `  (
( ( 2  x.  N )  -  1 )  -  N ) )  x.  ( ! `
 N ) )  =  ( ( ! `
 ( N  - 
1 ) )  x.  ( ! `  N
) ) )
118117oveq2d 5890 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN  ->  (
( ! `  (
( 2  x.  N
)  -  1 ) )  /  ( ( ! `  ( ( ( 2  x.  N
)  -  1 )  -  N ) )  x.  ( ! `  N ) ) )  =  ( ( ! `
 ( ( 2  x.  N )  - 
1 ) )  / 
( ( ! `  ( N  -  1
) )  x.  ( ! `  N )
) ) )
119107, 118eqtrd 2328 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  _C  N )  =  ( ( ! `
 ( ( 2  x.  N )  - 
1 ) )  / 
( ( ! `  ( N  -  1
) )  x.  ( ! `  N )
) ) )
120119adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( ( 2  x.  N )  - 
1 )  _C  N
)  =  ( ( ! `  ( ( 2  x.  N )  -  1 ) )  /  ( ( ! `
 ( N  - 
1 ) )  x.  ( ! `  N
) ) ) )
121120oveq2d 5890 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) )  =  ( p 
pCnt  ( ( ! `
 ( ( 2  x.  N )  - 
1 ) )  / 
( ( ! `  ( N  -  1
) )  x.  ( ! `  N )
) ) ) )
122 nnz 10061 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ! `  ( ( 2  x.  N )  -  1 ) )  e.  NN  ->  ( ! `  ( (
2  x.  N )  -  1 ) )  e.  ZZ )
123 nnne0 9794 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ! `  ( ( 2  x.  N )  -  1 ) )  e.  NN  ->  ( ! `  ( (
2  x.  N )  -  1 ) )  =/=  0 )
124122, 123jca 518 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ! `  ( ( 2  x.  N )  -  1 ) )  e.  NN  ->  (
( ! `  (
( 2  x.  N
)  -  1 ) )  e.  ZZ  /\  ( ! `  ( ( 2  x.  N )  -  1 ) )  =/=  0 ) )
12594, 124syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN  ->  (
( ! `  (
( 2  x.  N
)  -  1 ) )  e.  ZZ  /\  ( ! `  ( ( 2  x.  N )  -  1 ) )  =/=  0 ) )
126125adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( ! `  ( ( 2  x.  N )  -  1 ) )  e.  ZZ  /\  ( ! `  (
( 2  x.  N
)  -  1 ) )  =/=  0 ) )
127 faccl 11314 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( N  -  1 )  e.  NN0  ->  ( ! `
 ( N  - 
1 ) )  e.  NN )
12836, 127syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN  ->  ( ! `  ( N  -  1 ) )  e.  NN )
129 faccl 11314 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  NN0  ->  ( ! `
 N )  e.  NN )
13012, 129syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN  ->  ( ! `  N )  e.  NN )
131128, 130nnmulcld 9809 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN  ->  (
( ! `  ( N  -  1 ) )  x.  ( ! `
 N ) )  e.  NN )
132131adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( ! `  ( N  -  1
) )  x.  ( ! `  N )
)  e.  NN )
133 pcdiv 12921 . . . . . . . . . . . . . . . . . . 19  |-  ( ( p  e.  Prime  /\  (
( ! `  (
( 2  x.  N
)  -  1 ) )  e.  ZZ  /\  ( ! `  ( ( 2  x.  N )  -  1 ) )  =/=  0 )  /\  ( ( ! `  ( N  -  1
) )  x.  ( ! `  N )
)  e.  NN )  ->  ( p  pCnt  ( ( ! `  (
( 2  x.  N
)  -  1 ) )  /  ( ( ! `  ( N  -  1 ) )  x.  ( ! `  N ) ) ) )  =  ( ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) )  -  ( p  pCnt  ( ( ! `  ( N  -  1 ) )  x.  ( ! `  N ) ) ) ) )
13471, 126, 132, 133syl3anc 1182 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  (
( ! `  (
( 2  x.  N
)  -  1 ) )  /  ( ( ! `  ( N  -  1 ) )  x.  ( ! `  N ) ) ) )  =  ( ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) )  -  ( p  pCnt  ( ( ! `  ( N  -  1 ) )  x.  ( ! `  N ) ) ) ) )
135 nnz 10061 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ! `  ( N  -  1 ) )  e.  NN  ->  ( ! `  ( N  -  1 ) )  e.  ZZ )
136 nnne0 9794 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ! `  ( N  -  1 ) )  e.  NN  ->  ( ! `  ( N  -  1 ) )  =/=  0 )
137135, 136jca 518 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ! `  ( N  -  1 ) )  e.  NN  ->  (
( ! `  ( N  -  1 ) )  e.  ZZ  /\  ( ! `  ( N  -  1 ) )  =/=  0 ) )
138128, 137syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN  ->  (
( ! `  ( N  -  1 ) )  e.  ZZ  /\  ( ! `  ( N  -  1 ) )  =/=  0 ) )
139138adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( ! `  ( N  -  1
) )  e.  ZZ  /\  ( ! `  ( N  -  1 ) )  =/=  0 ) )
140 nnz 10061 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ! `  N )  e.  NN  ->  ( ! `  N )  e.  ZZ )
141 nnne0 9794 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ! `  N )  e.  NN  ->  ( ! `  N )  =/=  0 )
142140, 141jca 518 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ! `  N )  e.  NN  ->  (
( ! `  N
)  e.  ZZ  /\  ( ! `  N )  =/=  0 ) )
143130, 142syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN  ->  (
( ! `  N
)  e.  ZZ  /\  ( ! `  N )  =/=  0 ) )
144143adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( ! `  N )  e.  ZZ  /\  ( ! `  N
)  =/=  0 ) )
145 pcmul 12920 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( p  e.  Prime  /\  (
( ! `  ( N  -  1 ) )  e.  ZZ  /\  ( ! `  ( N  -  1 ) )  =/=  0 )  /\  ( ( ! `  N )  e.  ZZ  /\  ( ! `  N
)  =/=  0 ) )  ->  ( p  pCnt  ( ( ! `  ( N  -  1
) )  x.  ( ! `  N )
) )  =  ( ( p  pCnt  ( ! `  ( N  -  1 ) ) )  +  ( p 
pCnt  ( ! `  N ) ) ) )
14671, 139, 144, 145syl3anc 1182 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  (
( ! `  ( N  -  1 ) )  x.  ( ! `
 N ) ) )  =  ( ( p  pCnt  ( ! `  ( N  -  1 ) ) )  +  ( p  pCnt  ( ! `  N )
) ) )
147146oveq2d 5890 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) )  -  ( p 
pCnt  ( ( ! `
 ( N  - 
1 ) )  x.  ( ! `  N
) ) ) )  =  ( ( p 
pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) )  -  ( ( p  pCnt  ( ! `  ( N  -  1 ) ) )  +  ( p 
pCnt  ( ! `  N ) ) ) ) )
148121, 134, 1473eqtrd 2332 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) )  =  ( ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) )  -  ( ( p  pCnt  ( ! `  ( N  -  1 ) ) )  +  ( p 
pCnt  ( ! `  N ) ) ) ) )
149148adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) )  =  ( ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) )  -  ( ( p  pCnt  ( ! `  ( N  -  1 ) ) )  +  ( p 
pCnt  ( ! `  N ) ) ) ) )
150 simprr 733 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  ->  -.  p  <_  N )
151 prmfac1 12813 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( N  e.  NN0  /\  p  e.  Prime  /\  p  ||  ( ! `  N
) )  ->  p  <_  N )
1521513expia 1153 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  NN0  /\  p  e.  Prime )  -> 
( p  ||  ( ! `  N )  ->  p  <_  N )
)
15312, 152sylan 457 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  ||  ( ! `  N )  ->  p  <_  N )
)
154153adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( p  ||  ( ! `  N )  ->  p  <_  N )
)
155150, 154mtod 168 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  ->  -.  p  ||  ( ! `
 N ) )
15684adantl 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  NN  /\  p  e.  Prime )  ->  p  e.  ZZ )
157139simpld 445 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ! `  ( N  -  1 ) )  e.  ZZ )
158 nnz 10061 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  NN  ->  N  e.  ZZ )
159158adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  NN  /\  p  e.  Prime )  ->  N  e.  ZZ )
160 dvdsmultr1 12579 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( p  e.  ZZ  /\  ( ! `  ( N  -  1 ) )  e.  ZZ  /\  N  e.  ZZ )  ->  (
p  ||  ( ! `  ( N  -  1 ) )  ->  p  ||  ( ( ! `  ( N  -  1
) )  x.  N
) ) )
161156, 157, 159, 160syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  ||  ( ! `  ( N  -  1 ) )  ->  p  ||  (
( ! `  ( N  -  1 ) )  x.  N ) ) )
162 facnn2 11313 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  NN  ->  ( ! `  N )  =  ( ( ! `
 ( N  - 
1 ) )  x.  N ) )
163162adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ! `  N
)  =  ( ( ! `  ( N  -  1 ) )  x.  N ) )
164163breq2d 4051 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  ||  ( ! `  N )  <->  p 
||  ( ( ! `
 ( N  - 
1 ) )  x.  N ) ) )
165161, 164sylibrd 225 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  ||  ( ! `  ( N  -  1 ) )  ->  p  ||  ( ! `  N )
) )
166165adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( p  ||  ( ! `  ( N  -  1 ) )  ->  p  ||  ( ! `  N )
) )
167155, 166mtod 168 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  ->  -.  p  ||  ( ! `
 ( N  - 
1 ) ) )
168 pceq0 12939 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( p  e.  Prime  /\  ( ! `  ( N  -  1 ) )  e.  NN )  -> 
( ( p  pCnt  ( ! `  ( N  -  1 ) ) )  =  0  <->  -.  p  ||  ( ! `  ( N  -  1
) ) ) )
16992, 128, 168syl2anr 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( p  pCnt  ( ! `  ( N  -  1 ) ) )  =  0  <->  -.  p  ||  ( ! `  ( N  -  1
) ) ) )
170169adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( ( p  pCnt  ( ! `  ( N  -  1 ) ) )  =  0  <->  -.  p  ||  ( ! `  ( N  -  1
) ) ) )
171167, 170mpbird 223 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( p  pCnt  ( ! `  ( N  -  1 ) ) )  =  0 )
172 pceq0 12939 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( p  e.  Prime  /\  ( ! `  N )  e.  NN )  ->  (
( p  pCnt  ( ! `  N )
)  =  0  <->  -.  p  ||  ( ! `  N ) ) )
17392, 130, 172syl2anr 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( p  pCnt  ( ! `  N ) )  =  0  <->  -.  p  ||  ( ! `  N ) ) )
174173adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( ( p  pCnt  ( ! `  N ) )  =  0  <->  -.  p  ||  ( ! `  N ) ) )
175155, 174mpbird 223 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( p  pCnt  ( ! `  N )
)  =  0 )
176171, 175oveq12d 5892 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( ( p  pCnt  ( ! `  ( N  -  1 ) ) )  +  ( p 
pCnt  ( ! `  N ) ) )  =  ( 0  +  0 ) )
177 00id 9003 . . . . . . . . . . . . . . . . . 18  |-  ( 0  +  0 )  =  0
178176, 177syl6eq 2344 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( ( p  pCnt  ( ! `  ( N  -  1 ) ) )  +  ( p 
pCnt  ( ! `  N ) ) )  =  0 )
179178oveq2d 5890 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) )  -  ( ( p  pCnt  ( ! `  ( N  -  1 ) ) )  +  ( p  pCnt  ( ! `  N )
) ) )  =  ( ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) )  -  0 ) )
180 pccl 12918 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( p  e.  Prime  /\  ( ! `  ( (
2  x.  N )  -  1 ) )  e.  NN )  -> 
( p  pCnt  ( ! `  ( (
2  x.  N )  -  1 ) ) )  e.  NN0 )
18192, 94, 180syl2anr 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  ( ! `  ( (
2  x.  N )  -  1 ) ) )  e.  NN0 )
182181nn0cnd 10036 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  ( ! `  ( (
2  x.  N )  -  1 ) ) )  e.  CC )
183182subid1d 9162 . . . . . . . . . . . . . . . . 17  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) )  -  0 )  =  ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) ) )
184183adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) )  -  0 )  =  ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) ) )
185149, 179, 1843eqtrd 2332 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) )  =  ( p 
pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) ) )
186102, 105, 1853eqtrd 2332 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
( if ( p  <_  N ,  1 ,  0 )  +  ( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) ) )  =  ( p  pCnt  ( ! `  ( ( 2  x.  N )  -  1 ) ) ) )
18799, 186breqtrrd 4065 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  ( p  <_  (
( 2  x.  N
)  -  1 )  /\  -.  p  <_  N ) )  -> 
1  <_  ( if ( p  <_  N , 
1 ,  0 )  +  ( p  pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
188187expr 598 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  p  <_  ( ( 2  x.  N )  -  1 ) )  ->  ( -.  p  <_  N  ->  1  <_  ( if ( p  <_  N ,  1 , 
0 )  +  ( p  pCnt  ( (
( 2  x.  N
)  -  1 )  _C  N ) ) ) ) )
18980, 188pm2.61d 150 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  p  <_  ( ( 2  x.  N )  -  1 ) )  ->  1  <_  ( if ( p  <_  N ,  1 ,  0 )  +  ( p 
pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
19070, 189eqbrtrd 4059 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  p  <_  ( ( 2  x.  N )  -  1 ) )  ->  if ( p  <_  ( ( 2  x.  N )  - 
1 ) ,  1 ,  0 )  <_ 
( if ( p  <_  N ,  1 ,  0 )  +  ( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
191190ex 423 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  <_  (
( 2  x.  N
)  -  1 )  ->  if ( p  <_  ( ( 2  x.  N )  - 
1 ) ,  1 ,  0 )  <_ 
( if ( p  <_  N ,  1 ,  0 )  +  ( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) ) ) ) )
192 1nn0 9997 . . . . . . . . . . . . 13  |-  1  e.  NN0
193 0nn0 9996 . . . . . . . . . . . . 13  |-  0  e.  NN0
194192, 193keepel 3635 . . . . . . . . . . . 12  |-  if ( p  <_  N , 
1 ,  0 )  e.  NN0
195 nn0addcl 10015 . . . . . . . . . . . 12  |-  ( ( if ( p  <_  N ,  1 , 
0 )  e.  NN0  /\  ( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) )  e.  NN0 )  ->  ( if ( p  <_  N ,  1 ,  0 )  +  ( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) ) )  e.  NN0 )
196194, 73, 195sylancr 644 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( if ( p  <_  N ,  1 ,  0 )  +  ( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) ) )  e.  NN0 )
197196nn0ge0d 10037 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
0  <_  ( if ( p  <_  N , 
1 ,  0 )  +  ( p  pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
198 iffalse 3585 . . . . . . . . . . 11  |-  ( -.  p  <_  ( (
2  x.  N )  -  1 )  ->  if ( p  <_  (
( 2  x.  N
)  -  1 ) ,  1 ,  0 )  =  0 )
199198breq1d 4049 . . . . . . . . . 10  |-  ( -.  p  <_  ( (
2  x.  N )  -  1 )  -> 
( if ( p  <_  ( ( 2  x.  N )  - 
1 ) ,  1 ,  0 )  <_ 
( if ( p  <_  N ,  1 ,  0 )  +  ( p  pCnt  (
( ( 2  x.  N )  -  1 )  _C  N ) ) )  <->  0  <_  ( if ( p  <_  N ,  1 , 
0 )  +  ( p  pCnt  ( (
( 2  x.  N
)  -  1 )  _C  N ) ) ) ) )
200197, 199syl5ibrcom 213 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( -.  p  <_ 
( ( 2  x.  N )  -  1 )  ->  if (
p  <_  ( (
2  x.  N )  -  1 ) ,  1 ,  0 )  <_  ( if ( p  <_  N , 
1 ,  0 )  +  ( p  pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) ) )
201191, 200pm2.61d 150 . . . . . . . 8  |-  ( ( N  e.  NN  /\  p  e.  Prime )  ->  if ( p  <_  (
( 2  x.  N
)  -  1 ) ,  1 ,  0 )  <_  ( if ( p  <_  N , 
1 ,  0 )  +  ( p  pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
202 eqid 2296 . . . . . . . . . . . . 13  |-  ( n  e.  NN  |->  if ( n  e.  Prime ,  n ,  1 ) )  =  ( n  e.  NN  |->  if ( n  e.  Prime ,  n ,  1 ) )
203202prmorcht 20432 . . . . . . . . . . . 12  |-  ( ( ( 2  x.  N
)  -  1 )  e.  NN  ->  ( exp `  ( theta `  (
( 2  x.  N
)  -  1 ) ) )  =  (  seq  1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  n ,  1 ) ) ) `
 ( ( 2  x.  N )  - 
1 ) ) )
20441, 203syl 15 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  ( exp `  ( theta `  (
( 2  x.  N
)  -  1 ) ) )  =  (  seq  1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  n ,  1 ) ) ) `
 ( ( 2  x.  N )  - 
1 ) ) )
205204oveq2d 5890 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
p  pCnt  ( exp `  ( theta `  ( (
2  x.  N )  -  1 ) ) ) )  =  ( p  pCnt  (  seq  1 (  x.  , 
( n  e.  NN  |->  if ( n  e.  Prime ,  n ,  1 ) ) ) `  (
( 2  x.  N
)  -  1 ) ) ) )
206205adantr 451 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  ( exp `  ( theta `  (
( 2  x.  N
)  -  1 ) ) ) )  =  ( p  pCnt  (  seq  1 (  x.  , 
( n  e.  NN  |->  if ( n  e.  Prime ,  n ,  1 ) ) ) `  (
( 2  x.  N
)  -  1 ) ) ) )
207 nncn 9770 . . . . . . . . . . . . . 14  |-  ( n  e.  NN  ->  n  e.  CC )
208207exp1d 11256 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  (
n ^ 1 )  =  n )
209208ifeq1d 3592 . . . . . . . . . . . 12  |-  ( n  e.  NN  ->  if ( n  e.  Prime ,  ( n ^ 1 ) ,  1 )  =  if ( n  e.  Prime ,  n ,  1 ) )
210209mpteq2ia 4118 . . . . . . . . . . 11  |-  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( n ^ 1 ) ,  1 ) )  =  ( n  e.  NN  |->  if ( n  e.  Prime ,  n ,  1 ) )
211210eqcomi 2300 . . . . . . . . . 10  |-  ( n  e.  NN  |->  if ( n  e.  Prime ,  n ,  1 ) )  =  ( n  e.  NN  |->  if ( n  e.  Prime ,  ( n ^ 1 ) ,  1 ) )
212192a1i 10 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  p  e.  Prime )  /\  n  e.  Prime )  ->  1  e.  NN0 )
213212ralrimiva 2639 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  p  e.  Prime )  ->  A. n  e.  Prime  1  e.  NN0 )
21441adantr 451 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( 2  x.  N )  -  1 )  e.  NN )
215 eqidd 2297 . . . . . . . . . 10  |-  ( n  =  p  ->  1  =  1 )
216211, 213, 214, 71, 215pcmpt 12956 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  (  seq  1 (  x.  , 
( n  e.  NN  |->  if ( n  e.  Prime ,  n ,  1 ) ) ) `  (
( 2  x.  N
)  -  1 ) ) )  =  if ( p  <_  (
( 2  x.  N
)  -  1 ) ,  1 ,  0 ) )
217206, 216eqtrd 2328 . . . . . . . 8  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  ( exp `  ( theta `  (
( 2  x.  N
)  -  1 ) ) ) )  =  if ( p  <_ 
( ( 2  x.  N )  -  1 ) ,  1 ,  0 ) )
218 efchtcl 20365 . . . . . . . . . . . . 13  |-  ( N  e.  RR  ->  ( exp `  ( theta `  N
) )  e.  NN )
2199, 218syl 15 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  ( exp `  ( theta `  N
) )  e.  NN )
220219adantr 451 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( exp `  ( theta `  N ) )  e.  NN )
221 nnz 10061 . . . . . . . . . . . 12  |-  ( ( exp `  ( theta `  N ) )  e.  NN  ->  ( exp `  ( theta `  N )
)  e.  ZZ )
222 nnne0 9794 . . . . . . . . . . . 12  |-  ( ( exp `  ( theta `  N ) )  e.  NN  ->  ( exp `  ( theta `  N )
)  =/=  0 )
223221, 222jca 518 . . . . . . . . . . 11  |-  ( ( exp `  ( theta `  N ) )  e.  NN  ->  ( ( exp `  ( theta `  N
) )  e.  ZZ  /\  ( exp `  ( theta `  N ) )  =/=  0 ) )
224220, 223syl 15 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( exp `  ( theta `  N ) )  e.  ZZ  /\  ( exp `  ( theta `  N
) )  =/=  0
) )
225 nnz 10061 . . . . . . . . . . . 12  |-  ( ( ( ( 2  x.  N )  -  1 )  _C  N )  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  _C  N )  e.  ZZ )
226 nnne0 9794 . . . . . . . . . . . 12  |-  ( ( ( ( 2  x.  N )  -  1 )  _C  N )  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  _C  N )  =/=  0 )
227225, 226jca 518 . . . . . . . . . . 11  |-  ( ( ( ( 2  x.  N )  -  1 )  _C  N )  e.  NN  ->  (
( ( ( 2  x.  N )  - 
1 )  _C  N
)  e.  ZZ  /\  ( ( ( 2  x.  N )  - 
1 )  _C  N
)  =/=  0 ) )
22872, 227syl 15 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( ( ( 2  x.  N )  -  1 )  _C  N )  e.  ZZ  /\  ( ( ( 2  x.  N )  - 
1 )  _C  N
)  =/=  0 ) )
229 pcmul 12920 . . . . . . . . . 10  |-  ( ( p  e.  Prime  /\  (
( exp `  ( theta `  N ) )  e.  ZZ  /\  ( exp `  ( theta `  N
) )  =/=  0
)  /\  ( (
( ( 2  x.  N )  -  1 )  _C  N )  e.  ZZ  /\  (
( ( 2  x.  N )  -  1 )  _C  N )  =/=  0 ) )  ->  ( p  pCnt  ( ( exp `  ( theta `  N ) )  x.  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) )  =  ( ( p 
pCnt  ( exp `  ( theta `  N ) ) )  +  ( p 
pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
23071, 224, 228, 229syl3anc 1182 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  (
( exp `  ( theta `  N ) )  x.  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) )  =  ( ( p 
pCnt  ( exp `  ( theta `  N ) ) )  +  ( p 
pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
231202prmorcht 20432 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  ( exp `  ( theta `  N
) )  =  (  seq  1 (  x.  ,  ( n  e.  NN  |->  if ( n  e.  Prime ,  n ,  1 ) ) ) `
 N ) )
232231oveq2d 5890 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
p  pCnt  ( exp `  ( theta `  N )
) )  =  ( p  pCnt  (  seq  1 (  x.  , 
( n  e.  NN  |->  if ( n  e.  Prime ,  n ,  1 ) ) ) `  N
) ) )
233232adantr 451 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  ( exp `  ( theta `  N
) ) )  =  ( p  pCnt  (  seq  1 (  x.  , 
( n  e.  NN  |->  if ( n  e.  Prime ,  n ,  1 ) ) ) `  N
) ) )
234 simpl 443 . . . . . . . . . . . 12  |-  ( ( N  e.  NN  /\  p  e.  Prime )  ->  N  e.  NN )
235211, 213, 234, 71, 215pcmpt 12956 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  (  seq  1 (  x.  , 
( n  e.  NN  |->  if ( n  e.  Prime ,  n ,  1 ) ) ) `  N
) )  =  if ( p  <_  N ,  1 ,  0 ) )
236233, 235eqtrd 2328 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  ( exp `  ( theta `  N
) ) )  =  if ( p  <_  N ,  1 , 
0 ) )
237236oveq1d 5889 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( ( p  pCnt  ( exp `  ( theta `  N ) ) )  +  ( p  pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) )  =  ( if ( p  <_  N ,  1 , 
0 )  +  ( p  pCnt  ( (
( 2  x.  N
)  -  1 )  _C  N ) ) ) )
238230, 237eqtrd 2328 . . . . . . . 8  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  (
( exp `  ( theta `  N ) )  x.  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) )  =  ( if ( p  <_  N , 
1 ,  0 )  +  ( p  pCnt  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
239201, 217, 2383brtr4d 4069 . . . . . . 7  |-  ( ( N  e.  NN  /\  p  e.  Prime )  -> 
( p  pCnt  ( exp `  ( theta `  (
( 2  x.  N
)  -  1 ) ) ) )  <_ 
( p  pCnt  (
( exp `  ( theta `  N ) )  x.  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
240239ralrimiva 2639 . . . . . 6  |-  ( N  e.  NN  ->  A. p  e.  Prime  ( p  pCnt  ( exp `  ( theta `  ( ( 2  x.  N )  -  1 ) ) ) )  <_  ( p  pCnt  ( ( exp `  ( theta `  N ) )  x.  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )
241 efchtcl 20365 . . . . . . . . 9  |-  ( ( ( 2  x.  N
)  -  1 )  e.  RR  ->  ( exp `  ( theta `  (
( 2  x.  N
)  -  1 ) ) )  e.  NN )
2426, 241syl 15 . . . . . . . 8  |-  ( N  e.  NN  ->  ( exp `  ( theta `  (
( 2  x.  N
)  -  1 ) ) )  e.  NN )
243242nnzd 10132 . . . . . . 7  |-  ( N  e.  NN  ->  ( exp `  ( theta `  (
( 2  x.  N
)  -  1 ) ) )  e.  ZZ )
244219, 56nnmulcld 9809 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( exp `  ( theta `  N ) )  x.  ( ( ( 2  x.  N )  -  1 )  _C  N ) )  e.  NN )
245244nnzd 10132 . . . . . . 7  |-  ( N  e.  NN  ->  (
( exp `  ( theta `  N ) )  x.  ( ( ( 2  x.  N )  -  1 )  _C  N ) )  e.  ZZ )
246 pc2dvds 12947 . . . . . . 7  |-  ( ( ( exp `  ( theta `  ( ( 2  x.  N )  - 
1 ) ) )  e.  ZZ  /\  (
( exp `  ( theta `  N ) )  x.  ( ( ( 2  x.  N )  -  1 )  _C  N ) )  e.  ZZ )  ->  (
( exp `  ( theta `  ( ( 2  x.  N )  - 
1 ) ) ) 
||  ( ( exp `  ( theta `  N )
)  x.  ( ( ( 2  x.  N
)  -  1 )  _C  N ) )  <->  A. p  e.  Prime  ( p  pCnt  ( exp `  ( theta `  ( (
2  x.  N )  -  1 ) ) ) )  <_  (
p  pCnt  ( ( exp `  ( theta `  N
) )  x.  (
( ( 2  x.  N )  -  1 )  _C  N ) ) ) ) )
247243, 245, 246syl2anc 642 . . . . . 6  |-  ( N  e.  NN  ->  (
( exp `  ( theta `  ( ( 2  x.  N )  - 
1 ) ) ) 
||  ( ( exp `  ( theta `  N )
)  x.  ( ( ( 2  x.  N
)  -  1 )  _C  N ) )  <->  A. p  e.  Prime  ( p  pCnt  ( exp `  ( theta `  ( (
2  x.  N )  -  1 ) ) ) )  <_  (
p  pCnt  ( ( exp `  ( theta `  N
) )  x.  (
( ( 2  x.  N )  -  1 )  _C  N ) ) ) ) )
248240, 247mpbird 223 . . . . 5  |-  ( N  e.  NN  ->  ( exp `  ( theta `  (
( 2  x.  N
)  -  1 ) ) )  ||  (
( exp `  ( theta `  N ) )  x.  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) )
249 dvdsle 12590 . . . . . 6  |-  ( ( ( exp `  ( theta `  ( ( 2  x.  N )  - 
1 ) ) )  e.  ZZ  /\  (
( exp `  ( theta `  N ) )  x.  ( ( ( 2  x.  N )  -  1 )  _C  N ) )  e.  NN )  ->  (
( exp `  ( theta `  ( ( 2  x.  N )  - 
1 ) ) ) 
||  ( ( exp `  ( theta `  N )
)  x.  ( ( ( 2  x.  N
)  -  1 )  _C  N ) )  ->  ( exp `  ( theta `  ( ( 2  x.  N )  - 
1 ) ) )  <_  ( ( exp `  ( theta `  N )
)  x.  ( ( ( 2  x.  N
)  -  1 )  _C  N ) ) ) )
250243, 244, 249syl2anc 642 . . . . 5  |-  ( N  e.  NN  ->  (
( exp `  ( theta `  ( ( 2  x.  N )  - 
1 ) ) ) 
||  ( ( exp `  ( theta `  N )
)  x.  ( ( ( 2  x.  N
)  -  1 )  _C  N ) )  ->  ( exp `  ( theta `  ( ( 2  x.  N )  - 
1 ) ) )  <_  ( ( exp `  ( theta `  N )
)  x.  ( ( ( 2  x.  N
)  -  1 )  _C  N ) ) ) )
251248, 250mpd 14 . . . 4  |-  ( N  e.  NN  ->  ( exp `  ( theta `  (
( 2  x.  N
)  -  1 ) ) )  <_  (
( exp `  ( theta `  N ) )  x.  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) )
25211recnd 8877 . . . . . 6  |-  ( N  e.  NN  ->  ( theta `  N )  e.  CC )
25358recnd 8877 . . . . . 6  |-  ( N  e.  NN  ->  ( log `  ( ( ( 2  x.  N )  -  1 )  _C  N ) )  e.  CC )
254 efadd 12391 . . . . . 6  |-  ( ( ( theta `  N )  e.  CC  /\  ( log `  ( ( ( 2  x.  N )  - 
1 )  _C  N
) )  e.  CC )  ->  ( exp `  (
( theta `  N )  +  ( log `  (
( ( 2  x.  N )  -  1 )  _C  N ) ) ) )  =  ( ( exp `  ( theta `  N ) )  x.  ( exp `  ( log `  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) ) )
255252, 253, 254syl2anc 642 . . . . 5  |-  ( N  e.  NN  ->  ( exp `  ( ( theta `  N )  +  ( log `  ( ( ( 2  x.  N
)  -  1 )  _C  N ) ) ) )  =  ( ( exp `  ( theta `  N ) )  x.  ( exp `  ( log `  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) ) )
25657reeflogd 19991 . . . . . 6  |-  ( N  e.  NN  ->  ( exp `  ( log `  (
( ( 2  x.  N )  -  1 )  _C  N ) ) )  =  ( ( ( 2  x.  N )  -  1 )  _C  N ) )
257256oveq2d 5890 . . . . 5  |-  ( N  e.  NN  ->  (
( exp `  ( theta `  N ) )  x.  ( exp `  ( log `  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) ) )  =  ( ( exp `  ( theta `  N ) )  x.  ( ( ( 2  x.  N )  - 
1 )  _C  N
) ) )
258255, 257eqtrd 2328 . . . 4  |-  ( N  e.  NN  ->  ( exp `  ( ( theta `  N )  +  ( log `  ( ( ( 2  x.  N
)  -  1 )  _C  N ) ) ) )  =  ( ( exp `  ( theta `  N ) )  x.  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) )
259251, 258breqtrrd 4065 . . 3  |-  ( N  e.  NN  ->  ( exp `  ( theta `  (
( 2  x.  N
)  -  1 ) ) )  <_  ( exp `  ( ( theta `  N )  +  ( log `  ( ( ( 2  x.  N
)  -  1 )  _C  N ) ) ) ) )
260 efle 12414 . . . 4  |-  ( ( ( theta `  ( (
2  x.  N )  -  1 ) )  e.  RR  /\  (
( theta `  N )  +  ( log `  (
( ( 2  x.  N )  -  1 )  _C  N ) ) )  e.  RR )  ->  ( ( theta `  ( ( 2  x.  N )  -  1 ) )  <_  (
( theta `  N )  +  ( log `  (
( ( 2  x.  N )  -  1 )  _C  N ) ) )  <->  ( exp `  ( theta `  ( (
2  x.  N )  -  1 ) ) )  <_  ( exp `  ( ( theta `  N
)  +  ( log `  ( ( ( 2  x.  N )  - 
1 )  _C  N
) ) ) ) ) )
2618, 59, 260syl2anc 642 . . 3  |-  ( N  e.  NN  ->  (
( theta `  ( (
2  x.  N )  -  1 ) )  <_  ( ( theta `  N )  +  ( log `  ( ( ( 2  x.  N
)  -  1 )  _C  N ) ) )  <->  ( exp `  ( theta `  ( ( 2  x.  N )  - 
1 ) ) )  <_  ( exp `  (
( theta `  N )  +  ( log `  (
( ( 2  x.  N )  -  1 )  _C  N ) ) ) ) ) )
262259, 261mpbird 223 . 2  |-  ( N  e.  NN  ->  ( theta `  ( ( 2  x.  N )  - 
1 ) )  <_ 
( ( theta `  N
)  +  ( log `  ( ( ( 2  x.  N )  - 
1 )  _C  N
) ) ) )
263 fzfid 11051 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
0 ... ( ( 2  x.  N )  - 
1 ) )  e. 
Fin )
264 elfzelz 10814 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... ( ( 2  x.  N )  -  1 ) )  ->  k  e.  ZZ )
265 bccl 11350 . . . . . . . . . . 11  |-  ( ( ( ( 2  x.  N )  -  1 )  e.  NN0  /\  k  e.  ZZ )  ->  ( ( ( 2  x.  N )  - 
1 )  _C  k
)  e.  NN0 )
26643, 264, 265syl2an 463 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  k  e.  ( 0 ... ( ( 2  x.  N )  - 
1 ) ) )  ->  ( ( ( 2  x.  N )  -  1 )  _C  k )  e.  NN0 )
267266nn0red 10035 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  k  e.  ( 0 ... ( ( 2  x.  N )  - 
1 ) ) )  ->  ( ( ( 2  x.  N )  -  1 )  _C  k )  e.  RR )
268266nn0ge0d 10037 . . . . . . . . 9  |-  ( ( N  e.  NN  /\  k  e.  ( 0 ... ( ( 2  x.  N )  - 
1 ) ) )  ->  0  <_  (
( ( 2  x.  N )  -  1 )  _C  k ) )
269 nn0uz 10278 . . . . . . . . . . . 12  |-  NN0  =  ( ZZ>= `  0 )
27036, 269syl6eleq 2386 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  ( ZZ>= `  0
) )
271 fzss1 10846 . . . . . . . . . . 11  |-  ( ( N  -  1 )  e.  ( ZZ>= `  0
)  ->  ( ( N  -  1 ) ... N )  C_  ( 0 ... N
) )
272270, 271syl 15 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( N  -  1 ) ... N ) 
C_  ( 0 ... N ) )
273 eluz 10257 . . . . . . . . . . . . 13  |-  ( ( N  e.  ZZ  /\  ( ( 2  x.  N )  -  1 )  e.  ZZ )  ->  ( ( ( 2  x.  N )  -  1 )  e.  ( ZZ>= `  N )  <->  N  <_  ( ( 2  x.  N )  - 
1 ) ) )
274158, 85, 273syl2anc 642 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  e.  ( ZZ>= `  N )  <->  N  <_  ( ( 2  x.  N
)  -  1 ) ) )
27552, 274mpbird 223 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( 2  x.  N
)  -  1 )  e.  ( ZZ>= `  N
) )
276 fzss2 10847 . . . . . . . . . . 11  |-  ( ( ( 2  x.  N
)  -  1 )  e.  ( ZZ>= `  N
)  ->  ( 0 ... N )  C_  ( 0 ... (
( 2  x.  N
)  -  1 ) ) )
277275, 276syl 15 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
0 ... N )  C_  ( 0 ... (
( 2  x.  N
)  -  1 ) ) )
278272, 277sstrd 3202 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( N  -  1 ) ... N ) 
C_  ( 0 ... ( ( 2  x.  N )  -  1 ) ) )
279263, 267, 268, 278fsumless 12270 . . . . . . . 8  |-  ( N  e.  NN  ->  sum_ k  e.  ( ( N  - 
1 ) ... N
) ( ( ( 2  x.  N )  -  1 )  _C  k )  <_  sum_ k  e.  ( 0 ... (
( 2  x.  N
)  -  1 ) ) ( ( ( 2  x.  N )  -  1 )  _C  k ) )
28036nn0zd 10131 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  ZZ )
281 bccmpl 11338 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 2  x.  N )  -  1 )  e.  NN0  /\  N  e.  ZZ )  ->  ( ( ( 2  x.  N )  - 
1 )  _C  N
)  =  ( ( ( 2  x.  N
)  -  1 )  _C  ( ( ( 2  x.  N )  -  1 )  -  N ) ) )
28243, 158, 281syl2anc 642 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  _C  N )  =  ( ( ( 2  x.  N )  -  1 )  _C  ( ( ( 2  x.  N )  - 
1 )  -  N
) ) )
283115oveq2d 5890 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  _C  ( ( ( 2  x.  N
)  -  1 )  -  N ) )  =  ( ( ( 2  x.  N )  -  1 )  _C  ( N  -  1 ) ) )
284282, 283eqtrd 2328 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  _C  N )  =  ( ( ( 2  x.  N )  -  1 )  _C  ( N  -  1 ) ) )
28556nncnd 9778 . . . . . . . . . . . . 13  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  _C  N )  e.  CC )
286284, 285eqeltrrd 2371 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  _C  ( N  -  1 ) )  e.  CC )
287 oveq2 5882 . . . . . . . . . . . . 13  |-  ( k  =  ( N  - 
1 )  ->  (
( ( 2  x.  N )  -  1 )  _C  k )  =  ( ( ( 2  x.  N )  -  1 )  _C  ( N  -  1 ) ) )
288287fsum1 12230 . . . . . . . . . . . 12  |-  ( ( ( N  -  1 )  e.  ZZ  /\  ( ( ( 2  x.  N )  - 
1 )  _C  ( N  -  1 ) )  e.  CC )  ->  sum_ k  e.  ( ( N  -  1 ) ... ( N  -  1 ) ) ( ( ( 2  x.  N )  - 
1 )  _C  k
)  =  ( ( ( 2  x.  N
)  -  1 )  _C  ( N  - 
1 ) ) )
289280, 286, 288syl2anc 642 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  sum_ k  e.  ( ( N  - 
1 ) ... ( N  -  1 ) ) ( ( ( 2  x.  N )  -  1 )  _C  k )  =  ( ( ( 2  x.  N )  -  1 )  _C  ( N  -  1 ) ) )
290289, 284eqtr4d 2331 . . . . . . . . . 10  |-  ( N  e.  NN  ->  sum_ k  e.  ( ( N  - 
1 ) ... ( N  -  1 ) ) ( ( ( 2  x.  N )  -  1 )  _C  k )  =  ( ( ( 2  x.  N )  -  1 )  _C  N ) )
291290oveq1d 5889 . . . . . . . . 9  |-  ( N  e.  NN  ->  ( sum_ k  e.  ( ( N  -  1 ) ... ( N  - 
1 ) ) ( ( ( 2  x.  N )  -  1 )  _C  k )  +  ( ( ( 2  x.  N )  -  1 )  _C  N ) )  =  ( ( ( ( 2  x.  N )  -  1 )  _C  N )  +  ( ( ( 2  x.  N )  -  1 )  _C  N ) ) )
29225, 109npcand 9177 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( N  -  1 )  +  1 )  =  N )
293 uzid 10258 . . . . . . . . . . . . 13  |-  ( ( N  -  1 )  e.  ZZ  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
294280, 293syl 15 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
295 peano2uz 10288 . . . . . . . . . . . 12  |-  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
296294, 295syl 15 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
( N  -  1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
297292, 296eqeltrrd 2371 . . . . . . . . . 10  |-  ( N  e.  NN  ->  N  e.  ( ZZ>= `  ( N  -  1 ) ) )
298278sselda 3193 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  k  e.  ( ( N  -  1 ) ... N ) )  ->  k  e.  ( 0 ... ( ( 2  x.  N )  -  1 ) ) )
299266nn0cnd 10036 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  k  e.  ( 0 ... ( ( 2  x.  N )  - 
1 ) ) )  ->  ( ( ( 2  x.  N )  -  1 )  _C  k )  e.  CC )
300298, 299syldan 456 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  k  e.  ( ( N  -  1 ) ... N ) )  ->  ( ( ( 2  x.  N )  -  1 )  _C  k )  e.  CC )
301 oveq2 5882 . . . . . . . . . 10  |-  ( k  =  N  ->  (
( ( 2  x.  N )  -  1 )  _C  k )  =  ( ( ( 2  x.  N )  -  1 )  _C  N ) )
302297, 300, 301fsumm1 12232 . . . . . . . . 9  |-  ( N  e.  NN  ->  sum_ k  e.  ( ( N  - 
1 ) ... N
) ( ( ( 2  x.  N )  -  1 )  _C  k )  =  (
sum_ k  e.  ( ( N  -  1 ) ... ( N  -  1 ) ) ( ( ( 2  x.  N )  - 
1 )  _C  k
)  +  ( ( ( 2  x.  N
)  -  1 )  _C  N ) ) )
3032852timesd 9970 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
2  x.  ( ( ( 2  x.  N
)  -  1 )  _C  N ) )  =  ( ( ( ( 2  x.  N
)  -  1 )  _C  N )  +  ( ( ( 2  x.  N )  - 
1 )  _C  N
) ) )
304291, 302, 3033eqtr4rd 2339 . . . . . . . 8  |-  ( N  e.  NN  ->  (
2  x.  ( ( ( 2  x.  N
)  -  1 )  _C  N ) )  =  sum_ k  e.  ( ( N  -  1 ) ... N ) ( ( ( 2  x.  N )  - 
1 )  _C  k
) )
305 binom11 12306 . . . . . . . . 9  |-  ( ( ( 2  x.  N
)  -  1 )  e.  NN0  ->  ( 2 ^ ( ( 2  x.  N )  - 
1 ) )  = 
sum_ k  e.  ( 0 ... ( ( 2  x.  N )  -  1 ) ) ( ( ( 2  x.  N )  - 
1 )  _C  k
) )
30643, 305syl 15 . . . . . . . 8  |-  ( N  e.  NN  ->  (
2 ^ ( ( 2  x.  N )  -  1 ) )  =  sum_ k  e.  ( 0 ... ( ( 2  x.  N )  -  1 ) ) ( ( ( 2  x.  N )  - 
1 )  _C  k
) )
307279, 304, 3063brtr4d 4069 . . . . . . 7  |-  ( N  e.  NN  ->  (
2  x.  ( ( ( 2  x.  N
)  -  1 )  _C  N ) )  <_  ( 2 ^ ( ( 2  x.  N )  -  1 ) ) )
308 mulcom 8839 . . . . . . . 8  |-  ( ( 2  e.  CC  /\  ( ( ( 2  x.  N )  - 
1 )  _C  N
)  e.  CC )  ->  ( 2  x.  ( ( ( 2  x.  N )  - 
1 )  _C  N
) )  =  ( ( ( ( 2  x.  N )  - 
1 )  _C  N
)  x.  2 ) )
30921, 285, 308sylancr 644 . . . . . . 7  |-  ( N  e.  NN  ->  (
2  x.  ( ( ( 2  x.  N
)  -  1 )  _C  N ) )  =  ( ( ( ( 2  x.  N
)  -  1 )  _C  N )  x.  2 ) )
31034oveq2d 5890 . . . . . . . 8  |-  ( N  e.  NN  ->  (
2 ^ ( ( 2  x.  N )  -  1 ) )  =  ( 2 ^ ( ( 2  x.  ( N  -  1 ) )  +  1 ) ) )
311 expp1 11126 . . . . . . . . 9  |-  ( ( 2  e.  CC  /\  ( 2  x.  ( N  -  1 ) )  e.  NN0 )  ->  ( 2 ^ (
( 2  x.  ( N  -  1 ) )  +  1 ) )  =  ( ( 2 ^ ( 2  x.  ( N  - 
1 ) ) )  x.  2 ) )
31221, 38, 311sylancr 644 . . . . . . . 8  |-  ( N  e.  NN  ->  (
2 ^ ( ( 2  x.  ( N  -  1 ) )  +  1 ) )  =  ( ( 2 ^ ( 2  x.  ( N  -  1 ) ) )  x.  2 ) )
31321a1i 10 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  2  e.  CC )
31435a1i 10 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  2  e.  NN0 )
315313, 36, 314expmuld 11264 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
2 ^ ( 2  x.  ( N  - 
1 ) ) )  =  ( ( 2 ^ 2 ) ^
( N  -  1 ) ) )
316 sq2 11215 . . . . . . . . . . 11  |-  ( 2 ^ 2 )  =  4
317316oveq1i 5884 . . . . . . . . . 10  |-  ( ( 2 ^ 2 ) ^ ( N  - 
1 ) )  =  ( 4 ^ ( N  -  1 ) )
318315, 317syl6eq 2344 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
2 ^ ( 2  x.  ( N  - 
1 ) ) )  =  ( 4 ^ ( N  -  1 ) ) )
319318oveq1d 5889 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( 2 ^ (
2  x.  ( N  -  1 ) ) )  x.  2 )  =  ( ( 4 ^ ( N  - 
1 ) )  x.  2 ) )
320310, 312, 3193eqtrd 2332 . . . . . . 7  |-  ( N  e.  NN  ->  (
2 ^ ( ( 2  x.  N )  -  1 ) )  =  ( ( 4 ^ ( N  - 
1 ) )  x.  2 ) )
321307, 309, 3203brtr3d 4068 . . . . . 6  |-  ( N  e.  NN  ->  (
( ( ( 2  x.  N )  - 
1 )  _C  N
)  x.  2 )  <_  ( ( 4 ^ ( N  - 
1 ) )  x.  2 ) )
32256nnred 9777 . . . . . . 7  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  _C  N )  e.  RR )
323 reexpcl 11136 . . . . . . . 8  |-  ( ( 4  e.  RR  /\  ( N  -  1
)  e.  NN0 )  ->  ( 4 ^ ( N  -  1 ) )  e.  RR )
32460, 36, 323sylancr 644 . . . . . . 7  |-  ( N  e.  NN  ->  (
4 ^ ( N  -  1 ) )  e.  RR )
325 2re 9831 . . . . . . . . 9  |-  2  e.  RR
326 2pos 9844 . . . . . . . . 9  |-  0  <  2
327325, 326pm3.2i 441 . . . . . . . 8  |-  ( 2  e.  RR  /\  0  <  2 )
328327a1i 10 . . . . . . 7  |-  ( N  e.  NN  ->  (
2  e.  RR  /\  0  <  2 ) )
329 lemul1 9624 . . . . . . 7  |-  ( ( ( ( ( 2  x.  N )  - 
1 )  _C  N
)  e.  RR  /\  ( 4 ^ ( N  -  1 ) )  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( (
( ( 2  x.  N )  -  1 )  _C  N )  <_  ( 4 ^ ( N  -  1 ) )  <->  ( (
( ( 2  x.  N )  -  1 )  _C  N )  x.  2 )  <_ 
( ( 4 ^ ( N  -  1 ) )  x.  2 ) ) )
330322, 324, 328, 329syl3anc 1182 . . . . . 6  |-  ( N  e.  NN  ->  (
( ( ( 2  x.  N )  - 
1 )  _C  N
)  <_  ( 4 ^ ( N  - 
1 ) )  <->  ( (
( ( 2  x.  N )  -  1 )  _C  N )  x.  2 )  <_ 
( ( 4 ^ ( N  -  1 ) )  x.  2 ) ) )
331321, 330mpbird 223 . . . . 5  |-  ( N  e.  NN  ->  (
( ( 2  x.  N )  -  1 )  _C  N )  <_  ( 4 ^ ( N  -  1 ) ) )
33264recni 8865 . . . . . . . 8  |-  ( log `  4 )  e.  CC
333 mulcom 8839 . . . . . . . 8  |-  ( ( ( log `  4
)  e.  CC  /\  ( N  -  1
)  e.  CC )  ->  ( ( log `  4 )  x.  ( N  -  1 ) )  =  ( ( N  -  1 )  x.  ( log `  4 ) ) )
334332, 113, 333sylancr 644 . . . . . . 7  |-  ( N  e.  NN  ->  (
( log `  4
)  x.  ( N  -  1 ) )  =  ( ( N  -  1 )  x.  ( log `  4
) ) )
335334fveq2d 5545 . . . . . 6  |-  ( N  e.  NN  ->  ( exp `  ( ( log `  4 )  x.  ( N  -  1 ) ) )  =  ( exp `  (
( N  -  1 )  x.  ( log `  4 ) ) ) )
336 reexplog 19964 . . . . . . 7  |-  ( ( 4  e.  RR+  /\  ( N  -  1 )  e.  ZZ )  -> 
( 4 ^ ( N  -  1 ) )  =  ( exp `  ( ( N  - 
1 )  x.  ( log `  4 ) ) ) )
33762, 280, 336sylancr 644 . . . . . 6  |-  ( N  e.  NN  ->  (
4 ^ ( N  -  1 ) )  =  ( exp `  (
( N  -  1 )  x.  ( log `  4 ) ) ) )
338335, 337eqtr4d 2331 . . . . 5  |-  ( N  e.  NN  ->  ( exp `  ( ( log `  4 )  x.  ( N  -  1 ) ) )  =  ( 4 ^ ( N  -  1 ) ) )
339331, 256, 3383brtr4d 4069 . . . 4  |-  ( N  e.  NN  ->  ( exp `  ( log `  (
( ( 2  x.  N )  -  1 )  _C  N ) ) )  <_  ( exp `  ( ( log `  4 )  x.  ( N  -  1 ) ) ) )
340 efle 12414 . . . . 5  |-  ( ( ( log `  (
( ( 2  x.  N )  -  1 )  _C  N ) )  e.  RR  /\  ( ( log `  4
)  x.  ( N  -  1 ) )  e.  RR )  -> 
( ( log `  (
( ( 2  x.  N )  -  1 )  _C  N ) )  <_  ( ( log `  4 )  x.  ( N  -  1 ) )  <->  ( exp `  ( log `  (
( ( 2  x.  N )  -  1 )  _C  N ) ) )  <_  ( exp `  ( ( log `  4 )  x.  ( N  -  1 ) ) ) ) )
34158, 67, 340syl2anc 642 . . . 4  |-  ( N  e.  NN  ->  (
( log `  (
( ( 2  x.  N )  -  1 )  _C  N ) )  <_  ( ( log `  4 )  x.  ( N  -  1 ) )  <->  ( exp `  ( log `  (
( ( 2  x.  N )  -  1 )  _C  N ) ) )  <_  ( exp `  ( ( log `  4 )  x.  ( N  -  1 ) ) ) ) )
342339, 341mpbird 223 . . 3  |-  ( N  e.  NN  ->  ( log `  ( ( ( 2  x.  N )  -  1 )  _C  N ) )  <_ 
( ( log `  4
)  x.  ( N  -  1 ) ) )
34358, 67, 11, 342leadd2dd 9403 . 2  |-  ( N  e.  NN  ->  (
( theta `  N )  +  ( log `  (
( ( 2  x.  N )  -  1 )  _C  N ) ) )  <_  (
( theta `  N )  +  ( ( log `  4 )  x.  ( N  -  1 ) ) ) )
3448, 59, 68, 262, 343letrd 8989 1  |-  ( N  e.  NN  ->  ( theta `  ( ( 2  x.  N )  - 
1 ) )  <_ 
( ( theta `  N
)  +  ( ( log `  4 )  x.  ( N  - 
1 ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696    =/= wne 2459   A.wral 2556    C_ wss 3165   ifcif 3578   class class class wbr 4039    e. cmpt 4093   ` cfv 5271  (class class class)co 5874   CCcc 8751   RRcr 8752   0cc0 8753   1c1 8754    + caddc 8756    x. cmul 8758    < clt 8883    <_ cle 8884    - cmin 9053    / cdiv 9439   NNcn 9762   2c2 9811   4c4 9813   NN0cn0 9981   ZZcz 10040   ZZ>=cuz 10246   RR+crp 10370   ...cfz 10798    seq cseq 11062   ^cexp 11120   !cfa 11304    _C cbc 11331   sum_csu 12174   expce 12359    || cdivides 12547   Primecprime 12774    pCnt cpc 12905   logclog 19928   thetaccht 20344
This theorem is referenced by:  chtub  20467
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-inf2 7358  ax-cnex 8809  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830  ax-pre-sup 8831  ax-addf 8832  ax-mulf 8833
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-iin 3924  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-se 4369  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-isom 5280  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-of 6094  df-1st 6138  df-2nd 6139  df-riota 6320  df-recs 6404  df-rdg 6439  df-1o 6495  df-2o 6496  df-oadd 6499  df-er 6676  df-map 6790  df-pm 6791  df-ixp 6834  df-en 6880  df-dom 6881  df-sdom 6882  df-fin 6883  df-fi 7181  df-sup 7210  df-oi 7241  df-card 7588  df-cda 7810  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-div 9440  df-nn 9763  df-2 9820  df-3 9821  df-4 9822  df-5 9823  df-6 9824  df-7 9825  df-8 9826  df-9 9827  df-10 9828  df-n0 9982  df-z 10041  df-dec 10141  df-uz 10247  df-q 10333  df-rp 10371  df-xneg 10468  df-xadd 10469  df-xmul 10470  df-ioo 10676  df-ioc 10677  df-ico 10678  df-icc 10679  df-fz 10799  df-fzo 10887  df-fl 10941  df-mod 10990  df-seq 11063  df-exp 11121  df-fac 11305  df-bc 11332  df-hash 11354  df-shft 11578  df-cj 11600  df-re 11601  df-im 11602  df-sqr 11736  df-abs 11737  df-limsup 11961  df-clim 11978  df-rlim 11979  df-sum 12175  df-ef 12365  df-sin 12367  df-cos 12368  df-pi 12370  df-dvds 12548  df-gcd 12702  df-prm 12775  df-pc 12906  df-struct 13166  df-ndx 13167  df-slot 13168  df-base 13169  df-sets 13170  df-ress 13171  df-plusg 13237  df-mulr 13238  df-starv 13239  df-sca 13240  df-vsca 13241  df-tset 13243  df-ple 13244  df-ds 13246  df-hom 13248  df-cco 13249  df-rest 13343  df-topn 13344  df-topgen 13360  df-pt 13361  df-prds 13364  df-xrs 13419  df-0g 13420  df-gsum 13421  df-qtop 13426  df-imas 13427  df-xps 13429  df-mre 13504  df-mrc 13505  df-acs 13507  df-mnd 14383  df-submnd 14432  df-mulg 14508  df-cntz 14809  df-cmn 15107  df-xmet 16389  df-met 16390  df-bl 16391  df-mopn 16392  df-cnfld 16394  df-top 16652  df-bases 16654  df-topon 16655  df-topsp 16656  df-cld 16772  df-ntr 16773  df-cls 16774  df-nei 16851  df-lp 16884  df-perf 16885  df-cn 16973  df-cnp 16974  df-haus 17059  df-tx 17273  df-hmeo 17462  df-fbas 17536  df-fg 17537  df-fil 17557  df-fm 17649  df-flim 17650  df-flf 17651  df-xms 17901  df-ms 17902  df-tms 17903  df-cncf 18398  df-limc 19232  df-dv 19233  df-log 19930  df-cht 20350
  Copyright terms: Public domain W3C validator