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 ( 𝜑𝑁 ∈ ( ℤ ‘ 5 ) )
bpos.2 ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝𝑝 ≤ ( 2 · 𝑁 ) ) )
bpos.3 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) )
bpos.4 𝐾 = ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) )
Assertion bposlem3 ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝐾 ) = ( ( 2 · 𝑁 ) C 𝑁 ) )

Proof

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