Metamath Proof Explorer

Theorem bposlem3

Description: Lemma for bpos . Since the binomial coefficient does not have any primes in the range ( 2 N / 3 , N ] or ( 2 N , +oo ) by bposlem2 and prmfac1 , respectively, and it does not have any in the range ( N , 2 N ] by hypothesis, the product of the primes up through 2 N / 3 must be sufficient to compose the whole binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Hypotheses bpos.1 
|- ( ph -> N e. ( ZZ>= ` 5 ) )
bpos.2 
|- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
bpos.3 
|- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
bpos.4 
|- K = ( |_ ` ( ( 2 x. N ) / 3 ) )
Assertion bposlem3 
|- ( ph -> ( seq 1 ( x. , F ) ` K ) = ( ( 2 x. N ) _C N ) )

Proof

Step Hyp Ref Expression
1 bpos.1 
 |-  ( ph -> N e. ( ZZ>= ` 5 ) )
2 bpos.2 
 |-  ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
3 bpos.3 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
4 bpos.4 
 |-  K = ( |_ ` ( ( 2 x. N ) / 3 ) )
5 simpr 
 |-  ( ( ph /\ n e. Prime ) -> n e. Prime )
6 5nn 
 |-  5 e. NN
7 eluznn 
 |-  ( ( 5 e. NN /\ N e. ( ZZ>= ` 5 ) ) -> N e. NN )
8 6 1 7 sylancr 
 |-  ( ph -> N e. NN )
9 8 nnnn0d 
 |-  ( ph -> N e. NN0 )
10 fzctr 
 |-  ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
11 bccl2 
 |-  ( N e. ( 0 ... ( 2 x. N ) ) -> ( ( 2 x. N ) _C N ) e. NN )
12 9 10 11 3syl 
 |-  ( ph -> ( ( 2 x. N ) _C N ) e. NN )
13 12 adantr 
 |-  ( ( ph /\ n e. Prime ) -> ( ( 2 x. N ) _C N ) e. NN )
14 5 13 pccld 
 |-  ( ( ph /\ n e. Prime ) -> ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
15 14 ralrimiva 
 |-  ( ph -> A. n e. Prime ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
16 15 adantr 
 |-  ( ( ph /\ p e. Prime ) -> A. n e. Prime ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
17 2nn 
 |-  2 e. NN
18 nnmulcl 
 |-  ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
19 17 8 18 sylancr 
 |-  ( ph -> ( 2 x. N ) e. NN )
20 19 nnred 
 |-  ( ph -> ( 2 x. N ) e. RR )
21 3nn 
 |-  3 e. NN
22 nndivre 
 |-  ( ( ( 2 x. N ) e. RR /\ 3 e. NN ) -> ( ( 2 x. N ) / 3 ) e. RR )
23 20 21 22 sylancl 
 |-  ( ph -> ( ( 2 x. N ) / 3 ) e. RR )
24 23 flcld 
 |-  ( ph -> ( |_ ` ( ( 2 x. N ) / 3 ) ) e. ZZ )
25 4 24 eqeltrid 
 |-  ( ph -> K e. ZZ )
26 3re 
 |-  3 e. RR
27 26 a1i 
 |-  ( ph -> 3 e. RR )
28 5re 
 |-  5 e. RR
29 28 a1i 
 |-  ( ph -> 5 e. RR )
30 8 nnred 
 |-  ( ph -> N e. RR )
31 3lt5 
 |-  3 < 5
32 26 28 31 ltleii 
 |-  3 <_ 5
33 32 a1i 
 |-  ( ph -> 3 <_ 5 )
34 eluzle 
 |-  ( N e. ( ZZ>= ` 5 ) -> 5 <_ N )
35 1 34 syl 
 |-  ( ph -> 5 <_ N )
36 27 29 30 33 35 letrd 
 |-  ( ph -> 3 <_ N )
37 2re 
 |-  2 e. RR
38 2pos 
 |-  0 < 2
39 37 38 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
40 lemul2 
 |-  ( ( 3 e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 3 <_ N <-> ( 2 x. 3 ) <_ ( 2 x. N ) ) )
41 26 39 40 mp3an13 
 |-  ( N e. RR -> ( 3 <_ N <-> ( 2 x. 3 ) <_ ( 2 x. N ) ) )
42 30 41 syl 
 |-  ( ph -> ( 3 <_ N <-> ( 2 x. 3 ) <_ ( 2 x. N ) ) )
43 36 42 mpbid 
 |-  ( ph -> ( 2 x. 3 ) <_ ( 2 x. N ) )
44 3pos 
 |-  0 < 3
45 26 44 pm3.2i 
 |-  ( 3 e. RR /\ 0 < 3 )
46 lemuldiv 
 |-  ( ( 2 e. RR /\ ( 2 x. N ) e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( ( 2 x. 3 ) <_ ( 2 x. N ) <-> 2 <_ ( ( 2 x. N ) / 3 ) ) )
47 37 45 46 mp3an13 
 |-  ( ( 2 x. N ) e. RR -> ( ( 2 x. 3 ) <_ ( 2 x. N ) <-> 2 <_ ( ( 2 x. N ) / 3 ) ) )
48 20 47 syl 
 |-  ( ph -> ( ( 2 x. 3 ) <_ ( 2 x. N ) <-> 2 <_ ( ( 2 x. N ) / 3 ) ) )
49 43 48 mpbid 
 |-  ( ph -> 2 <_ ( ( 2 x. N ) / 3 ) )
50 2z 
 |-  2 e. ZZ
51 flge 
 |-  ( ( ( ( 2 x. N ) / 3 ) e. RR /\ 2 e. ZZ ) -> ( 2 <_ ( ( 2 x. N ) / 3 ) <-> 2 <_ ( |_ ` ( ( 2 x. N ) / 3 ) ) ) )
52 23 50 51 sylancl 
 |-  ( ph -> ( 2 <_ ( ( 2 x. N ) / 3 ) <-> 2 <_ ( |_ ` ( ( 2 x. N ) / 3 ) ) ) )
53 49 52 mpbid 
 |-  ( ph -> 2 <_ ( |_ ` ( ( 2 x. N ) / 3 ) ) )
54 53 4 breqtrrdi 
 |-  ( ph -> 2 <_ K )
55 50 eluz1i 
 |-  ( K e. ( ZZ>= ` 2 ) <-> ( K e. ZZ /\ 2 <_ K ) )
56 25 54 55 sylanbrc 
 |-  ( ph -> K e. ( ZZ>= ` 2 ) )
57 eluz2nn 
 |-  ( K e. ( ZZ>= ` 2 ) -> K e. NN )
58 56 57 syl 
 |-  ( ph -> K e. NN )
59 58 adantr 
 |-  ( ( ph /\ p e. Prime ) -> K e. NN )
60 simpr 
 |-  ( ( ph /\ p e. Prime ) -> p e. Prime )
61 oveq1 
 |-  ( n = p -> ( n pCnt ( ( 2 x. N ) _C N ) ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
62 3 16 59 60 61 pcmpt 
 |-  ( ( ph /\ p e. Prime ) -> ( p pCnt ( seq 1 ( x. , F ) ` K ) ) = if ( p <_ K , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) )
63 iftrue 
 |-  ( p <_ K -> if ( p <_ K , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
64 63 adantl 
 |-  ( ( ( ph /\ p e. Prime ) /\ p <_ K ) -> if ( p <_ K , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
65 iffalse 
 |-  ( -. p <_ K -> if ( p <_ K , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = 0 )
66 65 adantl 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p <_ K ) -> if ( p <_ K , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = 0 )
67 25 zred 
 |-  ( ph -> K e. RR )
68 prmz 
 |-  ( p e. Prime -> p e. ZZ )
69 68 zred 
 |-  ( p e. Prime -> p e. RR )
70 ltnle 
 |-  ( ( K e. RR /\ p e. RR ) -> ( K < p <-> -. p <_ K ) )
71 67 69 70 syl2an 
 |-  ( ( ph /\ p e. Prime ) -> ( K < p <-> -. p <_ K ) )
72 71 biimpar 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p <_ K ) -> K < p )
73 8 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> N e. NN )
74 simplr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> p e. Prime )
75 37 a1i 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> 2 e. RR )
76 67 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> K e. RR )
77 68 ad2antlr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> p e. ZZ )
78 77 zred 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> p e. RR )
79 54 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> 2 <_ K )
80 simprl 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> K < p )
81 75 76 78 79 80 lelttrd 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> 2 < p )
82 4 80 eqbrtrrid 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> ( |_ ` ( ( 2 x. N ) / 3 ) ) < p )
83 23 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> ( ( 2 x. N ) / 3 ) e. RR )
84 fllt 
 |-  ( ( ( ( 2 x. N ) / 3 ) e. RR /\ p e. ZZ ) -> ( ( ( 2 x. N ) / 3 ) < p <-> ( |_ ` ( ( 2 x. N ) / 3 ) ) < p ) )
85 83 77 84 syl2anc 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> ( ( ( 2 x. N ) / 3 ) < p <-> ( |_ ` ( ( 2 x. N ) / 3 ) ) < p ) )
86 82 85 mpbird 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> ( ( 2 x. N ) / 3 ) < p )
87 simprr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> p <_ N )
88 73 74 81 86 87 bposlem2 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( K < p /\ p <_ N ) ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) = 0 )
89 88 expr 
 |-  ( ( ( ph /\ p e. Prime ) /\ K < p ) -> ( p <_ N -> ( p pCnt ( ( 2 x. N ) _C N ) ) = 0 ) )
90 rspe 
 |-  ( ( p e. Prime /\ ( N < p /\ p <_ ( 2 x. N ) ) ) -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
91 90 adantll 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( N < p /\ p <_ ( 2 x. N ) ) ) -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
92 2 ad2antrr 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( N < p /\ p <_ ( 2 x. N ) ) ) -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
93 91 92 pm2.21dd 
 |-  ( ( ( ph /\ p e. Prime ) /\ ( N < p /\ p <_ ( 2 x. N ) ) ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) = 0 )
94 93 expr 
 |-  ( ( ( ph /\ p e. Prime ) /\ N < p ) -> ( p <_ ( 2 x. N ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) = 0 ) )
95 12 nnzd 
 |-  ( ph -> ( ( 2 x. N ) _C N ) e. ZZ )
96 9 faccld 
 |-  ( ph -> ( ! ` N ) e. NN )
97 96 96 nnmulcld 
 |-  ( ph -> ( ( ! ` N ) x. ( ! ` N ) ) e. NN )
98 97 nnzd 
 |-  ( ph -> ( ( ! ` N ) x. ( ! ` N ) ) e. ZZ )
99 dvdsmul1 
 |-  ( ( ( ( 2 x. N ) _C N ) e. ZZ /\ ( ( ! ` N ) x. ( ! ` N ) ) e. ZZ ) -> ( ( 2 x. N ) _C N ) || ( ( ( 2 x. N ) _C N ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) )
100 95 98 99 syl2anc 
 |-  ( ph -> ( ( 2 x. N ) _C N ) || ( ( ( 2 x. N ) _C N ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) )
101 bcctr 
 |-  ( N e. NN0 -> ( ( 2 x. N ) _C N ) = ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) )
102 9 101 syl 
 |-  ( ph -> ( ( 2 x. N ) _C N ) = ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) )
103 102 oveq1d 
 |-  ( ph -> ( ( ( 2 x. N ) _C N ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) = ( ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) )
104 19 nnnn0d 
 |-  ( ph -> ( 2 x. N ) e. NN0 )
105 104 faccld 
 |-  ( ph -> ( ! ` ( 2 x. N ) ) e. NN )
106 105 nncnd 
 |-  ( ph -> ( ! ` ( 2 x. N ) ) e. CC )
107 97 nncnd 
 |-  ( ph -> ( ( ! ` N ) x. ( ! ` N ) ) e. CC )
108 97 nnne0d 
 |-  ( ph -> ( ( ! ` N ) x. ( ! ` N ) ) =/= 0 )
109 106 107 108 divcan1d 
 |-  ( ph -> ( ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) = ( ! ` ( 2 x. N ) ) )
110 103 109 eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) _C N ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) = ( ! ` ( 2 x. N ) ) )
111 100 110 breqtrd 
 |-  ( ph -> ( ( 2 x. N ) _C N ) || ( ! ` ( 2 x. N ) ) )
112 111 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( ( 2 x. N ) _C N ) || ( ! ` ( 2 x. N ) ) )
113 68 adantl 
 |-  ( ( ph /\ p e. Prime ) -> p e. ZZ )
114 95 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( ( 2 x. N ) _C N ) e. ZZ )
115 105 nnzd 
 |-  ( ph -> ( ! ` ( 2 x. N ) ) e. ZZ )
116 115 adantr 
 |-  ( ( ph /\ p e. Prime ) -> ( ! ` ( 2 x. N ) ) e. ZZ )
117 dvdstr 
 |-  ( ( p e. ZZ /\ ( ( 2 x. N ) _C N ) e. ZZ /\ ( ! ` ( 2 x. N ) ) e. ZZ ) -> ( ( p || ( ( 2 x. N ) _C N ) /\ ( ( 2 x. N ) _C N ) || ( ! ` ( 2 x. N ) ) ) -> p || ( ! ` ( 2 x. N ) ) ) )
118 113 114 116 117 syl3anc 
 |-  ( ( ph /\ p e. Prime ) -> ( ( p || ( ( 2 x. N ) _C N ) /\ ( ( 2 x. N ) _C N ) || ( ! ` ( 2 x. N ) ) ) -> p || ( ! ` ( 2 x. N ) ) ) )
119 112 118 mpan2d 
 |-  ( ( ph /\ p e. Prime ) -> ( p || ( ( 2 x. N ) _C N ) -> p || ( ! ` ( 2 x. N ) ) ) )
120 prmfac1 
 |-  ( ( ( 2 x. N ) e. NN0 /\ p e. Prime /\ p || ( ! ` ( 2 x. N ) ) ) -> p <_ ( 2 x. N ) )
121 120 3expia 
 |-  ( ( ( 2 x. N ) e. NN0 /\ p e. Prime ) -> ( p || ( ! ` ( 2 x. N ) ) -> p <_ ( 2 x. N ) ) )
122 104 121 sylan 
 |-  ( ( ph /\ p e. Prime ) -> ( p || ( ! ` ( 2 x. N ) ) -> p <_ ( 2 x. N ) ) )
123 119 122 syld 
 |-  ( ( ph /\ p e. Prime ) -> ( p || ( ( 2 x. N ) _C N ) -> p <_ ( 2 x. N ) ) )
124 123 con3d 
 |-  ( ( ph /\ p e. Prime ) -> ( -. p <_ ( 2 x. N ) -> -. p || ( ( 2 x. N ) _C N ) ) )
125 id 
 |-  ( p e. Prime -> p e. Prime )
126 pceq0 
 |-  ( ( p e. Prime /\ ( ( 2 x. N ) _C N ) e. NN ) -> ( ( p pCnt ( ( 2 x. N ) _C N ) ) = 0 <-> -. p || ( ( 2 x. N ) _C N ) ) )
127 125 12 126 syl2anr 
 |-  ( ( ph /\ p e. Prime ) -> ( ( p pCnt ( ( 2 x. N ) _C N ) ) = 0 <-> -. p || ( ( 2 x. N ) _C N ) ) )
128 124 127 sylibrd 
 |-  ( ( ph /\ p e. Prime ) -> ( -. p <_ ( 2 x. N ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) = 0 ) )
129 128 adantr 
 |-  ( ( ( ph /\ p e. Prime ) /\ N < p ) -> ( -. p <_ ( 2 x. N ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) = 0 ) )
130 94 129 pm2.61d 
 |-  ( ( ( ph /\ p e. Prime ) /\ N < p ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) = 0 )
131 130 ex 
 |-  ( ( ph /\ p e. Prime ) -> ( N < p -> ( p pCnt ( ( 2 x. N ) _C N ) ) = 0 ) )
132 131 adantr 
 |-  ( ( ( ph /\ p e. Prime ) /\ K < p ) -> ( N < p -> ( p pCnt ( ( 2 x. N ) _C N ) ) = 0 ) )
133 lelttric 
 |-  ( ( p e. RR /\ N e. RR ) -> ( p <_ N \/ N < p ) )
134 69 30 133 syl2anr 
 |-  ( ( ph /\ p e. Prime ) -> ( p <_ N \/ N < p ) )
135 134 adantr 
 |-  ( ( ( ph /\ p e. Prime ) /\ K < p ) -> ( p <_ N \/ N < p ) )
136 89 132 135 mpjaod 
 |-  ( ( ( ph /\ p e. Prime ) /\ K < p ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) = 0 )
137 72 136 syldan 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p <_ K ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) = 0 )
138 66 137 eqtr4d 
 |-  ( ( ( ph /\ p e. Prime ) /\ -. p <_ K ) -> if ( p <_ K , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
139 64 138 pm2.61dan 
 |-  ( ( ph /\ p e. Prime ) -> if ( p <_ K , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
140 62 139 eqtrd 
 |-  ( ( ph /\ p e. Prime ) -> ( p pCnt ( seq 1 ( x. , F ) ` K ) ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
141 140 ralrimiva 
 |-  ( ph -> A. p e. Prime ( p pCnt ( seq 1 ( x. , F ) ` K ) ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
142 3 15 pcmptcl 
 |-  ( ph -> ( F : NN --> NN /\ seq 1 ( x. , F ) : NN --> NN ) )
143 142 simprd 
 |-  ( ph -> seq 1 ( x. , F ) : NN --> NN )
144 143 58 ffvelrnd 
 |-  ( ph -> ( seq 1 ( x. , F ) ` K ) e. NN )
145 144 nnnn0d 
 |-  ( ph -> ( seq 1 ( x. , F ) ` K ) e. NN0 )
146 12 nnnn0d 
 |-  ( ph -> ( ( 2 x. N ) _C N ) e. NN0 )
147 pc11 
 |-  ( ( ( seq 1 ( x. , F ) ` K ) e. NN0 /\ ( ( 2 x. N ) _C N ) e. NN0 ) -> ( ( seq 1 ( x. , F ) ` K ) = ( ( 2 x. N ) _C N ) <-> A. p e. Prime ( p pCnt ( seq 1 ( x. , F ) ` K ) ) = ( p pCnt ( ( 2 x. N ) _C N ) ) ) )
148 145 146 147 syl2anc 
 |-  ( ph -> ( ( seq 1 ( x. , F ) ` K ) = ( ( 2 x. N ) _C N ) <-> A. p e. Prime ( p pCnt ( seq 1 ( x. , F ) ` K ) ) = ( p pCnt ( ( 2 x. N ) _C N ) ) ) )
149 141 148 mpbird 
 |-  ( ph -> ( seq 1 ( x. , F ) ` K ) = ( ( 2 x. N ) _C N ) )