MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bposlem3 Structured version   Visualization version   GIF version

Theorem bposlem3 26618
Description: Lemma for bpos 26625. Since the binomial coefficient does not have any primes in the range (2𝑁 / 3, 𝑁] or (2𝑁, +∞) by bposlem2 26617 and prmfac1 16589, respectively, and it does not have any in the range (𝑁, 2𝑁] by hypothesis, the product of the primes up through 2𝑁 / 3 must be sufficient to compose the whole binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)
Hypotheses
Ref Expression
bpos.1 (𝜑𝑁 ∈ (ℤ‘5))
bpos.2 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
bpos.3 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
bpos.4 𝐾 = (⌊‘((2 · 𝑁) / 3))
Assertion
Ref Expression
bposlem3 (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁))
Distinct variable groups:   𝐹,𝑝   𝑛,𝑝,𝐾   𝑛,𝑁,𝑝   𝜑,𝑛,𝑝
Allowed substitution hint:   𝐹(𝑛)

Proof of Theorem bposlem3
StepHypRef Expression
1 bpos.3 . . . . 5 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
2 simpr 485 . . . . . . . 8 ((𝜑𝑛 ∈ ℙ) → 𝑛 ∈ ℙ)
3 5nn 12235 . . . . . . . . . . . 12 5 ∈ ℕ
4 bpos.1 . . . . . . . . . . . 12 (𝜑𝑁 ∈ (ℤ‘5))
5 eluznn 12835 . . . . . . . . . . . 12 ((5 ∈ ℕ ∧ 𝑁 ∈ (ℤ‘5)) → 𝑁 ∈ ℕ)
63, 4, 5sylancr 587 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ)
76nnnn0d 12469 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
8 fzctr 13545 . . . . . . . . . 10 (𝑁 ∈ ℕ0𝑁 ∈ (0...(2 · 𝑁)))
9 bccl2 14215 . . . . . . . . . 10 (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
107, 8, 93syl 18 . . . . . . . . 9 (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ)
1110adantr 481 . . . . . . . 8 ((𝜑𝑛 ∈ ℙ) → ((2 · 𝑁)C𝑁) ∈ ℕ)
122, 11pccld 16714 . . . . . . 7 ((𝜑𝑛 ∈ ℙ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
1312ralrimiva 3141 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
1413adantr 481 . . . . 5 ((𝜑𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
15 bpos.4 . . . . . . . . 9 𝐾 = (⌊‘((2 · 𝑁) / 3))
16 2nn 12222 . . . . . . . . . . . . 13 2 ∈ ℕ
17 nnmulcl 12173 . . . . . . . . . . . . 13 ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
1816, 6, 17sylancr 587 . . . . . . . . . . . 12 (𝜑 → (2 · 𝑁) ∈ ℕ)
1918nnred 12164 . . . . . . . . . . 11 (𝜑 → (2 · 𝑁) ∈ ℝ)
20 3nn 12228 . . . . . . . . . . 11 3 ∈ ℕ
21 nndivre 12190 . . . . . . . . . . 11 (((2 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((2 · 𝑁) / 3) ∈ ℝ)
2219, 20, 21sylancl 586 . . . . . . . . . 10 (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ)
2322flcld 13695 . . . . . . . . 9 (𝜑 → (⌊‘((2 · 𝑁) / 3)) ∈ ℤ)
2415, 23eqeltrid 2842 . . . . . . . 8 (𝜑𝐾 ∈ ℤ)
25 3re 12229 . . . . . . . . . . . . . 14 3 ∈ ℝ
2625a1i 11 . . . . . . . . . . . . 13 (𝜑 → 3 ∈ ℝ)
27 5re 12236 . . . . . . . . . . . . . 14 5 ∈ ℝ
2827a1i 11 . . . . . . . . . . . . 13 (𝜑 → 5 ∈ ℝ)
296nnred 12164 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℝ)
30 3lt5 12327 . . . . . . . . . . . . . . 15 3 < 5
3125, 27, 30ltleii 11274 . . . . . . . . . . . . . 14 3 ≤ 5
3231a1i 11 . . . . . . . . . . . . 13 (𝜑 → 3 ≤ 5)
33 eluzle 12772 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘5) → 5 ≤ 𝑁)
344, 33syl 17 . . . . . . . . . . . . 13 (𝜑 → 5 ≤ 𝑁)
3526, 28, 29, 32, 34letrd 11308 . . . . . . . . . . . 12 (𝜑 → 3 ≤ 𝑁)
36 2re 12223 . . . . . . . . . . . . . . 15 2 ∈ ℝ
37 2pos 12252 . . . . . . . . . . . . . . 15 0 < 2
3836, 37pm3.2i 471 . . . . . . . . . . . . . 14 (2 ∈ ℝ ∧ 0 < 2)
39 lemul2 12004 . . . . . . . . . . . . . 14 ((3 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (3 ≤ 𝑁 ↔ (2 · 3) ≤ (2 · 𝑁)))
4025, 38, 39mp3an13 1452 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ → (3 ≤ 𝑁 ↔ (2 · 3) ≤ (2 · 𝑁)))
4129, 40syl 17 . . . . . . . . . . . 12 (𝜑 → (3 ≤ 𝑁 ↔ (2 · 3) ≤ (2 · 𝑁)))
4235, 41mpbid 231 . . . . . . . . . . 11 (𝜑 → (2 · 3) ≤ (2 · 𝑁))
43 3pos 12254 . . . . . . . . . . . . . 14 0 < 3
4425, 43pm3.2i 471 . . . . . . . . . . . . 13 (3 ∈ ℝ ∧ 0 < 3)
45 lemuldiv 12031 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → ((2 · 3) ≤ (2 · 𝑁) ↔ 2 ≤ ((2 · 𝑁) / 3)))
4636, 44, 45mp3an13 1452 . . . . . . . . . . . 12 ((2 · 𝑁) ∈ ℝ → ((2 · 3) ≤ (2 · 𝑁) ↔ 2 ≤ ((2 · 𝑁) / 3)))
4719, 46syl 17 . . . . . . . . . . 11 (𝜑 → ((2 · 3) ≤ (2 · 𝑁) ↔ 2 ≤ ((2 · 𝑁) / 3)))
4842, 47mpbid 231 . . . . . . . . . 10 (𝜑 → 2 ≤ ((2 · 𝑁) / 3))
49 2z 12531 . . . . . . . . . . 11 2 ∈ ℤ
50 flge 13702 . . . . . . . . . . 11 ((((2 · 𝑁) / 3) ∈ ℝ ∧ 2 ∈ ℤ) → (2 ≤ ((2 · 𝑁) / 3) ↔ 2 ≤ (⌊‘((2 · 𝑁) / 3))))
5122, 49, 50sylancl 586 . . . . . . . . . 10 (𝜑 → (2 ≤ ((2 · 𝑁) / 3) ↔ 2 ≤ (⌊‘((2 · 𝑁) / 3))))
5248, 51mpbid 231 . . . . . . . . 9 (𝜑 → 2 ≤ (⌊‘((2 · 𝑁) / 3)))
5352, 15breqtrrdi 5145 . . . . . . . 8 (𝜑 → 2 ≤ 𝐾)
5449eluz1i 12767 . . . . . . . 8 (𝐾 ∈ (ℤ‘2) ↔ (𝐾 ∈ ℤ ∧ 2 ≤ 𝐾))
5524, 53, 54sylanbrc 583 . . . . . . 7 (𝜑𝐾 ∈ (ℤ‘2))
56 eluz2nn 12801 . . . . . . 7 (𝐾 ∈ (ℤ‘2) → 𝐾 ∈ ℕ)
5755, 56syl 17 . . . . . 6 (𝜑𝐾 ∈ ℕ)
5857adantr 481 . . . . 5 ((𝜑𝑝 ∈ ℙ) → 𝐾 ∈ ℕ)
59 simpr 485 . . . . 5 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
60 oveq1 7360 . . . . 5 (𝑛 = 𝑝 → (𝑛 pCnt ((2 · 𝑁)C𝑁)) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
611, 14, 58, 59, 60pcmpt 16756 . . . 4 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt (seq1( · , 𝐹)‘𝐾)) = if(𝑝𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0))
62 iftrue 4490 . . . . . 6 (𝑝𝐾 → if(𝑝𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
6362adantl 482 . . . . 5 (((𝜑𝑝 ∈ ℙ) ∧ 𝑝𝐾) → if(𝑝𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
64 iffalse 4493 . . . . . . 7 𝑝𝐾 → if(𝑝𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = 0)
6564adantl 482 . . . . . 6 (((𝜑𝑝 ∈ ℙ) ∧ ¬ 𝑝𝐾) → if(𝑝𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = 0)
6624zred 12603 . . . . . . . . 9 (𝜑𝐾 ∈ ℝ)
67 prmz 16543 . . . . . . . . . 10 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
6867zred 12603 . . . . . . . . 9 (𝑝 ∈ ℙ → 𝑝 ∈ ℝ)
69 ltnle 11230 . . . . . . . . 9 ((𝐾 ∈ ℝ ∧ 𝑝 ∈ ℝ) → (𝐾 < 𝑝 ↔ ¬ 𝑝𝐾))
7066, 68, 69syl2an 596 . . . . . . . 8 ((𝜑𝑝 ∈ ℙ) → (𝐾 < 𝑝 ↔ ¬ 𝑝𝐾))
7170biimpar 478 . . . . . . 7 (((𝜑𝑝 ∈ ℙ) ∧ ¬ 𝑝𝐾) → 𝐾 < 𝑝)
726ad2antrr 724 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → 𝑁 ∈ ℕ)
73 simplr 767 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → 𝑝 ∈ ℙ)
7436a1i 11 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → 2 ∈ ℝ)
7566ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → 𝐾 ∈ ℝ)
7667ad2antlr 725 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → 𝑝 ∈ ℤ)
7776zred 12603 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → 𝑝 ∈ ℝ)
7853ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → 2 ≤ 𝐾)
79 simprl 769 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → 𝐾 < 𝑝)
8074, 75, 77, 78, 79lelttrd 11309 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → 2 < 𝑝)
8115, 79eqbrtrrid 5139 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → (⌊‘((2 · 𝑁) / 3)) < 𝑝)
8222ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → ((2 · 𝑁) / 3) ∈ ℝ)
83 fllt 13703 . . . . . . . . . . . 12 ((((2 · 𝑁) / 3) ∈ ℝ ∧ 𝑝 ∈ ℤ) → (((2 · 𝑁) / 3) < 𝑝 ↔ (⌊‘((2 · 𝑁) / 3)) < 𝑝))
8482, 76, 83syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → (((2 · 𝑁) / 3) < 𝑝 ↔ (⌊‘((2 · 𝑁) / 3)) < 𝑝))
8581, 84mpbird 256 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → ((2 · 𝑁) / 3) < 𝑝)
86 simprr 771 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → 𝑝𝑁)
8772, 73, 80, 85, 86bposlem2 26617 . . . . . . . . 9 (((𝜑𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝𝑝𝑁)) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0)
8887expr 457 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝐾 < 𝑝) → (𝑝𝑁 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0))
89 rspe 3230 . . . . . . . . . . . . . 14 ((𝑝 ∈ ℙ ∧ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁))) → ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
9089adantll 712 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ ℙ) ∧ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁))) → ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
91 bpos.2 . . . . . . . . . . . . . 14 (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
9291ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑝 ∈ ℙ) ∧ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁))) → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁)))
9390, 92pm2.21dd 194 . . . . . . . . . . . 12 (((𝜑𝑝 ∈ ℙ) ∧ (𝑁 < 𝑝𝑝 ≤ (2 · 𝑁))) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0)
9493expr 457 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ 𝑁 < 𝑝) → (𝑝 ≤ (2 · 𝑁) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0))
9510nnzd 12522 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℤ)
967faccld 14176 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (!‘𝑁) ∈ ℕ)
9796, 96nnmulcld 12202 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((!‘𝑁) · (!‘𝑁)) ∈ ℕ)
9897nnzd 12522 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((!‘𝑁) · (!‘𝑁)) ∈ ℤ)
99 dvdsmul1 16152 . . . . . . . . . . . . . . . . . . 19 ((((2 · 𝑁)C𝑁) ∈ ℤ ∧ ((!‘𝑁) · (!‘𝑁)) ∈ ℤ) → ((2 · 𝑁)C𝑁) ∥ (((2 · 𝑁)C𝑁) · ((!‘𝑁) · (!‘𝑁))))
10095, 98, 99syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2 · 𝑁)C𝑁) ∥ (((2 · 𝑁)C𝑁) · ((!‘𝑁) · (!‘𝑁))))
101 bcctr 26607 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → ((2 · 𝑁)C𝑁) = ((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁))))
1027, 101syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 · 𝑁)C𝑁) = ((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁))))
103102oveq1d 7368 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2 · 𝑁)C𝑁) · ((!‘𝑁) · (!‘𝑁))) = (((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁))) · ((!‘𝑁) · (!‘𝑁))))
10418nnnn0d 12469 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (2 · 𝑁) ∈ ℕ0)
105104faccld 14176 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (!‘(2 · 𝑁)) ∈ ℕ)
106105nncnd 12165 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (!‘(2 · 𝑁)) ∈ ℂ)
10797nncnd 12165 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((!‘𝑁) · (!‘𝑁)) ∈ ℂ)
10897nnne0d 12199 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((!‘𝑁) · (!‘𝑁)) ≠ 0)
109106, 107, 108divcan1d 11928 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁))) · ((!‘𝑁) · (!‘𝑁))) = (!‘(2 · 𝑁)))
110103, 109eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((2 · 𝑁)C𝑁) · ((!‘𝑁) · (!‘𝑁))) = (!‘(2 · 𝑁)))
111100, 110breqtrd 5129 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2 · 𝑁)C𝑁) ∥ (!‘(2 · 𝑁)))
112111adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → ((2 · 𝑁)C𝑁) ∥ (!‘(2 · 𝑁)))
11367adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → 𝑝 ∈ ℤ)
11495adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → ((2 · 𝑁)C𝑁) ∈ ℤ)
115105nnzd 12522 . . . . . . . . . . . . . . . . . 18 (𝜑 → (!‘(2 · 𝑁)) ∈ ℤ)
116115adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑝 ∈ ℙ) → (!‘(2 · 𝑁)) ∈ ℤ)
117 dvdstr 16168 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℤ ∧ ((2 · 𝑁)C𝑁) ∈ ℤ ∧ (!‘(2 · 𝑁)) ∈ ℤ) → ((𝑝 ∥ ((2 · 𝑁)C𝑁) ∧ ((2 · 𝑁)C𝑁) ∥ (!‘(2 · 𝑁))) → 𝑝 ∥ (!‘(2 · 𝑁))))
118113, 114, 116, 117syl3anc 1371 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ℙ) → ((𝑝 ∥ ((2 · 𝑁)C𝑁) ∧ ((2 · 𝑁)C𝑁) ∥ (!‘(2 · 𝑁))) → 𝑝 ∥ (!‘(2 · 𝑁))))
119112, 118mpan2d 692 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ ℙ) → (𝑝 ∥ ((2 · 𝑁)C𝑁) → 𝑝 ∥ (!‘(2 · 𝑁))))
120 prmfac1 16589 . . . . . . . . . . . . . . . . 17 (((2 · 𝑁) ∈ ℕ0𝑝 ∈ ℙ ∧ 𝑝 ∥ (!‘(2 · 𝑁))) → 𝑝 ≤ (2 · 𝑁))
1211203expia 1121 . . . . . . . . . . . . . . . 16 (((2 · 𝑁) ∈ ℕ0𝑝 ∈ ℙ) → (𝑝 ∥ (!‘(2 · 𝑁)) → 𝑝 ≤ (2 · 𝑁)))
122104, 121sylan 580 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ ℙ) → (𝑝 ∥ (!‘(2 · 𝑁)) → 𝑝 ≤ (2 · 𝑁)))
123119, 122syld 47 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ ℙ) → (𝑝 ∥ ((2 · 𝑁)C𝑁) → 𝑝 ≤ (2 · 𝑁)))
124123con3d 152 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ ℙ) → (¬ 𝑝 ≤ (2 · 𝑁) → ¬ 𝑝 ∥ ((2 · 𝑁)C𝑁)))
125 id 22 . . . . . . . . . . . . . 14 (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
126 pceq0 16735 . . . . . . . . . . . . . 14 ((𝑝 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0 ↔ ¬ 𝑝 ∥ ((2 · 𝑁)C𝑁)))
127125, 10, 126syl2anr 597 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0 ↔ ¬ 𝑝 ∥ ((2 · 𝑁)C𝑁)))
128124, 127sylibrd 258 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ ℙ) → (¬ 𝑝 ≤ (2 · 𝑁) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0))
129128adantr 481 . . . . . . . . . . 11 (((𝜑𝑝 ∈ ℙ) ∧ 𝑁 < 𝑝) → (¬ 𝑝 ≤ (2 · 𝑁) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0))
13094, 129pm2.61d 179 . . . . . . . . . 10 (((𝜑𝑝 ∈ ℙ) ∧ 𝑁 < 𝑝) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0)
131130ex 413 . . . . . . . . 9 ((𝜑𝑝 ∈ ℙ) → (𝑁 < 𝑝 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0))
132131adantr 481 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝐾 < 𝑝) → (𝑁 < 𝑝 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0))
133 lelttric 11258 . . . . . . . . . 10 ((𝑝 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑝𝑁𝑁 < 𝑝))
13468, 29, 133syl2anr 597 . . . . . . . . 9 ((𝜑𝑝 ∈ ℙ) → (𝑝𝑁𝑁 < 𝑝))
135134adantr 481 . . . . . . . 8 (((𝜑𝑝 ∈ ℙ) ∧ 𝐾 < 𝑝) → (𝑝𝑁𝑁 < 𝑝))
13688, 132, 135mpjaod 858 . . . . . . 7 (((𝜑𝑝 ∈ ℙ) ∧ 𝐾 < 𝑝) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0)
13771, 136syldan 591 . . . . . 6 (((𝜑𝑝 ∈ ℙ) ∧ ¬ 𝑝𝐾) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0)
13865, 137eqtr4d 2779 . . . . 5 (((𝜑𝑝 ∈ ℙ) ∧ ¬ 𝑝𝐾) → if(𝑝𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
13963, 138pm2.61dan 811 . . . 4 ((𝜑𝑝 ∈ ℙ) → if(𝑝𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
14061, 139eqtrd 2776 . . 3 ((𝜑𝑝 ∈ ℙ) → (𝑝 pCnt (seq1( · , 𝐹)‘𝐾)) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
141140ralrimiva 3141 . 2 (𝜑 → ∀𝑝 ∈ ℙ (𝑝 pCnt (seq1( · , 𝐹)‘𝐾)) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
1421, 13pcmptcl 16755 . . . . . 6 (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
143142simprd 496 . . . . 5 (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ)
144143, 57ffvelcdmd 7032 . . . 4 (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℕ)
145144nnnn0d 12469 . . 3 (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℕ0)
14610nnnn0d 12469 . . 3 (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ0)
147 pc11 16744 . . 3 (((seq1( · , 𝐹)‘𝐾) ∈ ℕ0 ∧ ((2 · 𝑁)C𝑁) ∈ ℕ0) → ((seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (seq1( · , 𝐹)‘𝐾)) = (𝑝 pCnt ((2 · 𝑁)C𝑁))))
148145, 146, 147syl2anc 584 . 2 (𝜑 → ((seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (seq1( · , 𝐹)‘𝐾)) = (𝑝 pCnt ((2 · 𝑁)C𝑁))))
149141, 148mpbird 256 1 (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wcel 2106  wral 3062  wrex 3071  ifcif 4484   class class class wbr 5103  cmpt 5186  wf 6489  cfv 6493  (class class class)co 7353  cr 11046  0cc0 11047  1c1 11048   · cmul 11052   < clt 11185  cle 11186   / cdiv 11808  cn 12149  2c2 12204  3c3 12205  5c5 12207  0cn0 12409  cz 12495  cuz 12759  ...cfz 13416  cfl 13687  seqcseq 13898  cexp 13959  !cfa 14165  Ccbc 14194  cdvds 16128  cprime 16539   pCnt cpc 16700
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7668  ax-inf2 9573  ax-cnex 11103  ax-resscn 11104  ax-1cn 11105  ax-icn 11106  ax-addcl 11107  ax-addrcl 11108  ax-mulcl 11109  ax-mulrcl 11110  ax-mulcom 11111  ax-addass 11112  ax-mulass 11113  ax-distr 11114  ax-i2m1 11115  ax-1ne0 11116  ax-1rid 11117  ax-rnegex 11118  ax-rrecex 11119  ax-cnre 11120  ax-pre-lttri 11121  ax-pre-lttrn 11122  ax-pre-ltadd 11123  ax-pre-mulgt0 11124  ax-pre-sup 11125
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7309  df-ov 7356  df-oprab 7357  df-mpo 7358  df-om 7799  df-1st 7917  df-2nd 7918  df-frecs 8208  df-wrecs 8239  df-recs 8313  df-rdg 8352  df-1o 8408  df-2o 8409  df-er 8644  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-sup 9374  df-inf 9375  df-oi 9442  df-card 9871  df-pnf 11187  df-mnf 11188  df-xr 11189  df-ltxr 11190  df-le 11191  df-sub 11383  df-neg 11384  df-div 11809  df-nn 12150  df-2 12212  df-3 12213  df-4 12214  df-5 12215  df-n0 12410  df-z 12496  df-uz 12760  df-q 12866  df-rp 12908  df-fz 13417  df-fzo 13560  df-fl 13689  df-mod 13767  df-seq 13899  df-exp 13960  df-fac 14166  df-bc 14195  df-hash 14223  df-cj 14976  df-re 14977  df-im 14978  df-sqrt 15112  df-abs 15113  df-clim 15362  df-sum 15563  df-dvds 16129  df-gcd 16367  df-prm 16540  df-pc 16701
This theorem is referenced by:  bposlem6  26621
  Copyright terms: Public domain W3C validator