bposlem3 - Metamath Proof Explorer

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

Theorem bposlem3 27268

Description: Lemma for bpos 27275. Since the binomial coefficient does not have any primes in the range (2𝑁 / 3, 𝑁] or (2𝑁, +∞) by bposlem2 27267 and prmfac1 16682, 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**
Step	Hyp	Ref	Expression
1		bpos.3	. . . . 5 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
2		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ ℙ)
3		5nn 12259	. . . . . . . . . . . 12 ⊢ 5 ∈ ℕ
4		bpos.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘5))
5		eluznn 12860	. . . . . . . . . . . 12 ⊢ ((5 ∈ ℕ ∧ 𝑁 ∈ (ℤ_≥‘5)) → 𝑁 ∈ ℕ)
6	3, 4, 5	sylancr 593	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ)
7	6	nnnn0d 12490	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
8		fzctr 13586	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ (0...(2 · 𝑁)))
9		bccl2 14277	. . . . . . . . . 10 ⊢ (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
10	7, 8, 9	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ)
11	10	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℙ) → ((2 · 𝑁)C𝑁) ∈ ℕ)
12	2, 11	pccld 16813	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
13	12	ralrimiva 3131	. . . . . 6 ⊢ (𝜑 → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
14	13	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
15		bpos.4	. . . . . . . . 9 ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))
16		2nn 12246	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ
17		nnmulcl 12190	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
18	16, 6, 17	sylancr 593	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℕ)
19	18	nnred 12181	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ)
20		3nn 12252	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ
21		nndivre 12210	. . . . . . . . . . 11 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((2 · 𝑁) / 3) ∈ ℝ)
22	19, 20, 21	sylancl 592	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ)
23	22	flcld 13749	. . . . . . . . 9 ⊢ (𝜑 → (⌊‘((2 · 𝑁) / 3)) ∈ ℤ)
24	15, 23	eqeltrid 2843	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ ℤ)
25		3re 12253	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℝ
26	25	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 3 ∈ ℝ)
27		5re 12260	. . . . . . . . . . . . . 14 ⊢ 5 ∈ ℝ
28	27	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 5 ∈ ℝ)
29	6	nnred 12181	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℝ)
30		3lt5 12346	. . . . . . . . . . . . . . 15 ⊢ 3 < 5
31	25, 27, 30	ltleii 11261	. . . . . . . . . . . . . 14 ⊢ 3 ≤ 5
32	31	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 3 ≤ 5)
33		eluzle 12793	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘5) → 5 ≤ 𝑁)
34	4, 33	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 5 ≤ 𝑁)
35	26, 28, 29, 32, 34	letrd 11295	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ≤ 𝑁)
36		2re 12247	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
37		2pos 12276	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
38	36, 37	pm3.2i 471	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℝ ∧ 0 < 2)
39		lemul2 12000	. . . . . . . . . . . . . 14 ⊢ ((3 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (3 ≤ 𝑁 ↔ (2 · 3) ≤ (2 · 𝑁)))
40	25, 38, 39	mp3an13 1460	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ → (3 ≤ 𝑁 ↔ (2 · 3) ≤ (2 · 𝑁)))
41	29, 40	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (3 ≤ 𝑁 ↔ (2 · 3) ≤ (2 · 𝑁)))
42	35, 41	mpbid 233	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · 3) ≤ (2 · 𝑁))
43		3pos 12278	. . . . . . . . . . . . . 14 ⊢ 0 < 3
44	25, 43	pm3.2i 471	. . . . . . . . . . . . 13 ⊢ (3 ∈ ℝ ∧ 0 < 3)
45		lemuldiv 12028	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → ((2 · 3) ≤ (2 · 𝑁) ↔ 2 ≤ ((2 · 𝑁) / 3)))
46	36, 44, 45	mp3an13 1460	. . . . . . . . . . . 12 ⊢ ((2 · 𝑁) ∈ ℝ → ((2 · 3) ≤ (2 · 𝑁) ↔ 2 ≤ ((2 · 𝑁) / 3)))
47	19, 46	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 3) ≤ (2 · 𝑁) ↔ 2 ≤ ((2 · 𝑁) / 3)))
48	42, 47	mpbid 233	. . . . . . . . . 10 ⊢ (𝜑 → 2 ≤ ((2 · 𝑁) / 3))
49		2z 12551	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
50		flge 13756	. . . . . . . . . . 11 ⊢ ((((2 · 𝑁) / 3) ∈ ℝ ∧ 2 ∈ ℤ) → (2 ≤ ((2 · 𝑁) / 3) ↔ 2 ≤ (⌊‘((2 · 𝑁) / 3))))
51	22, 49, 50	sylancl 592	. . . . . . . . . 10 ⊢ (𝜑 → (2 ≤ ((2 · 𝑁) / 3) ↔ 2 ≤ (⌊‘((2 · 𝑁) / 3))))
52	48, 51	mpbid 233	. . . . . . . . 9 ⊢ (𝜑 → 2 ≤ (⌊‘((2 · 𝑁) / 3)))
53	52, 15	breqtrrdi 5115	. . . . . . . 8 ⊢ (𝜑 → 2 ≤ 𝐾)
54	49	eluz1i 12788	. . . . . . . 8 ⊢ (𝐾 ∈ (ℤ_≥‘2) ↔ (𝐾 ∈ ℤ ∧ 2 ≤ 𝐾))
55	24, 53, 54	sylanbrc 589	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘2))
56		eluz2nn 12830	. . . . . . 7 ⊢ (𝐾 ∈ (ℤ_≥‘2) → 𝐾 ∈ ℕ)
57	55, 56	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ)
58	57	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝐾 ∈ ℕ)
59		simpr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
60		oveq1 7364	. . . . 5 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt ((2 · 𝑁)C𝑁)) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
61	1, 14, 58, 59, 60	pcmpt 16855	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (seq1( · , 𝐹)‘𝐾)) = if(𝑝 ≤ 𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0))
62		iftrue 4461	. . . . . 6 ⊢ (𝑝 ≤ 𝐾 → if(𝑝 ≤ 𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
63	62	adantl 482	. . . . 5 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ≤ 𝐾) → if(𝑝 ≤ 𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
64		iffalse 4464	. . . . . . 7 ⊢ (¬ 𝑝 ≤ 𝐾 → if(𝑝 ≤ 𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = 0)
65	64	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ ¬ 𝑝 ≤ 𝐾) → if(𝑝 ≤ 𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = 0)
66	24	zred 12625	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℝ)
67		prmz 16636	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
68	67	zred 12625	. . . . . . . . 9 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℝ)
69		ltnle 11217	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℝ ∧ 𝑝 ∈ ℝ) → (𝐾 < 𝑝 ↔ ¬ 𝑝 ≤ 𝐾))
70	66, 68, 69	syl2an 602	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐾 < 𝑝 ↔ ¬ 𝑝 ≤ 𝐾))
71	70	biimpar 478	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ ¬ 𝑝 ≤ 𝐾) → 𝐾 < 𝑝)
72	6	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → 𝑁 ∈ ℕ)
73		simplr 774	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → 𝑝 ∈ ℙ)
74	36	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → 2 ∈ ℝ)
75	66	ad2antrr 732	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → 𝐾 ∈ ℝ)
76	67	ad2antlr 733	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → 𝑝 ∈ ℤ)
77	76	zred 12625	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → 𝑝 ∈ ℝ)
78	53	ad2antrr 732	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → 2 ≤ 𝐾)
79		simprl 776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → 𝐾 < 𝑝)
80	74, 75, 77, 78, 79	lelttrd 11296	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → 2 < 𝑝)
81	15, 79	eqbrtrrid 5109	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → (⌊‘((2 · 𝑁) / 3)) < 𝑝)
82	22	ad2antrr 732	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → ((2 · 𝑁) / 3) ∈ ℝ)
83		fllt 13757	. . . . . . . . . . . 12 ⊢ ((((2 · 𝑁) / 3) ∈ ℝ ∧ 𝑝 ∈ ℤ) → (((2 · 𝑁) / 3) < 𝑝 ↔ (⌊‘((2 · 𝑁) / 3)) < 𝑝))
84	82, 76, 83	syl2anc 590	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → (((2 · 𝑁) / 3) < 𝑝 ↔ (⌊‘((2 · 𝑁) / 3)) < 𝑝))
85	81, 84	mpbird 258	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → ((2 · 𝑁) / 3) < 𝑝)
86		simprr 778	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → 𝑝 ≤ 𝑁)
87	72, 73, 80, 85, 86	bposlem2 27267	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝐾 < 𝑝 ∧ 𝑝 ≤ 𝑁)) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0)
88	87	expr 457	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝐾 < 𝑝) → (𝑝 ≤ 𝑁 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0))
89		rspe 3229	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℙ ∧ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
90	89	adantll 720	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) → ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
91		bpos.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
92	91	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
93	90, 92	pm2.21dd 196	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁))) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0)
94	93	expr 457	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑁 < 𝑝) → (𝑝 ≤ (2 · 𝑁) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0))
95	10	nnzd 12542	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℤ)
96	7	faccld 14238	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (!‘𝑁) ∈ ℕ)
97	96, 96	nnmulcld 12222	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((!‘𝑁) · (!‘𝑁)) ∈ ℕ)
98	97	nnzd 12542	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((!‘𝑁) · (!‘𝑁)) ∈ ℤ)
99		dvdsmul1 16238	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((2 · 𝑁)C𝑁) ∈ ℤ ∧ ((!‘𝑁) · (!‘𝑁)) ∈ ℤ) → ((2 · 𝑁)C𝑁) ∥ (((2 · 𝑁)C𝑁) · ((!‘𝑁) · (!‘𝑁))))
100	95, 98, 99	syl2anc 590	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∥ (((2 · 𝑁)C𝑁) · ((!‘𝑁) · (!‘𝑁))))
101		bcctr 27257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → ((2 · 𝑁)C𝑁) = ((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁))))
102	7, 101	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) = ((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁))))
103	102	oveq1d 7372	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((2 · 𝑁)C𝑁) · ((!‘𝑁) · (!‘𝑁))) = (((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁))) · ((!‘𝑁) · (!‘𝑁))))
104	18	nnnn0d 12490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (2 · 𝑁) ∈ ℕ₀)
105	104	faccld 14238	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (!‘(2 · 𝑁)) ∈ ℕ)
106	105	nncnd 12182	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (!‘(2 · 𝑁)) ∈ ℂ)
107	97	nncnd 12182	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((!‘𝑁) · (!‘𝑁)) ∈ ℂ)
108	97	nnne0d 12219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((!‘𝑁) · (!‘𝑁)) ≠ 0)
109	106, 107, 108	divcan1d 11924	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((!‘(2 · 𝑁)) / ((!‘𝑁) · (!‘𝑁))) · ((!‘𝑁) · (!‘𝑁))) = (!‘(2 · 𝑁)))
110	103, 109	eqtrd 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((2 · 𝑁)C𝑁) · ((!‘𝑁) · (!‘𝑁))) = (!‘(2 · 𝑁)))
111	100, 110	breqtrd 5099	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∥ (!‘(2 · 𝑁)))
112	111	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((2 · 𝑁)C𝑁) ∥ (!‘(2 · 𝑁)))
113	67	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ)
114	95	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((2 · 𝑁)C𝑁) ∈ ℤ)
115	105	nnzd 12542	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (!‘(2 · 𝑁)) ∈ ℤ)
116	115	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (!‘(2 · 𝑁)) ∈ ℤ)
117		dvdstr 16255	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℤ ∧ ((2 · 𝑁)C𝑁) ∈ ℤ ∧ (!‘(2 · 𝑁)) ∈ ℤ) → ((𝑝 ∥ ((2 · 𝑁)C𝑁) ∧ ((2 · 𝑁)C𝑁) ∥ (!‘(2 · 𝑁))) → 𝑝 ∥ (!‘(2 · 𝑁))))
118	113, 114, 116, 117	syl3anc 1379	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ ((2 · 𝑁)C𝑁) ∧ ((2 · 𝑁)C𝑁) ∥ (!‘(2 · 𝑁))) → 𝑝 ∥ (!‘(2 · 𝑁))))
119	112, 118	mpan2d 700	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((2 · 𝑁)C𝑁) → 𝑝 ∥ (!‘(2 · 𝑁))))
120		prmfac1 16682	. . . . . . . . . . . . . . . . 17 ⊢ (((2 · 𝑁) ∈ ℕ₀ ∧ 𝑝 ∈ ℙ ∧ 𝑝 ∥ (!‘(2 · 𝑁))) → 𝑝 ≤ (2 · 𝑁))
121	120	3expia 1127	. . . . . . . . . . . . . . . 16 ⊢ (((2 · 𝑁) ∈ ℕ₀ ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘(2 · 𝑁)) → 𝑝 ≤ (2 · 𝑁)))
122	104, 121	sylan 586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (!‘(2 · 𝑁)) → 𝑝 ≤ (2 · 𝑁)))
123	119, 122	syld 47	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ ((2 · 𝑁)C𝑁) → 𝑝 ≤ (2 · 𝑁)))
124	123	con3d 152	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (¬ 𝑝 ≤ (2 · 𝑁) → ¬ 𝑝 ∥ ((2 · 𝑁)C𝑁)))
125		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
126		pceq0 16834	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0 ↔ ¬ 𝑝 ∥ ((2 · 𝑁)C𝑁)))
127	125, 10, 126	syl2anr 603	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0 ↔ ¬ 𝑝 ∥ ((2 · 𝑁)C𝑁)))
128	124, 127	sylibrd 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (¬ 𝑝 ≤ (2 · 𝑁) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0))
129	128	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑁 < 𝑝) → (¬ 𝑝 ≤ (2 · 𝑁) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0))
130	94, 129	pm2.61d 180	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝑁 < 𝑝) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0)
131	130	ex 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑁 < 𝑝 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0))
132	131	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝐾 < 𝑝) → (𝑁 < 𝑝 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0))
133		lelttric 11245	. . . . . . . . . 10 ⊢ ((𝑝 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑝 ≤ 𝑁 ∨ 𝑁 < 𝑝))
134	68, 29, 133	syl2anr 603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ≤ 𝑁 ∨ 𝑁 < 𝑝))
135	134	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝐾 < 𝑝) → (𝑝 ≤ 𝑁 ∨ 𝑁 < 𝑝))
136	88, 132, 135	mpjaod 866	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ 𝐾 < 𝑝) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0)
137	71, 136	syldan 597	. . . . . 6 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ ¬ 𝑝 ≤ 𝐾) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) = 0)
138	65, 137	eqtr4d 2777	. . . . 5 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ ¬ 𝑝 ≤ 𝐾) → if(𝑝 ≤ 𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
139	63, 138	pm2.61dan 818	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → if(𝑝 ≤ 𝐾, (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
140	61, 139	eqtrd 2774	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (seq1( · , 𝐹)‘𝐾)) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
141	140	ralrimiva 3131	. 2 ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 pCnt (seq1( · , 𝐹)‘𝐾)) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
142	1, 13	pcmptcl 16854	. . . . . 6 ⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
143	142	simprd 496	. . . . 5 ⊢ (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ)
144	143, 57	ffvelcdmd 7027	. . . 4 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℕ)
145	144	nnnn0d 12490	. . 3 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℕ₀)
146	10	nnnn0d 12490	. . 3 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ₀)
147		pc11 16843	. . 3 ⊢ (((seq1( · , 𝐹)‘𝐾) ∈ ℕ₀ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ₀) → ((seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (seq1( · , 𝐹)‘𝐾)) = (𝑝 pCnt ((2 · 𝑁)C𝑁))))
148	145, 146, 147	syl2anc 590	. 2 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (seq1( · , 𝐹)‘𝐾)) = (𝑝 pCnt ((2 · 𝑁)C𝑁))))
149	141, 148	mpbird 258	1 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 853 = wceq 1547 ∈ wcel 2119 ∀wral 3053 ∃wrex 3063 ifcif 4455 class class class wbr 5073 ↦ cmpt 5154 ⟶wf 6482 ‘cfv 6486 (class class class)co 7357 ℝcr 11029 0cc0 11030 1c1 11031 · cmul 11035 < clt 11171 ≤ cle 11172 / cdiv 11799 ℕcn 12166 2c2 12228 3c3 12229 5c5 12231 ℕ₀cn0 12429 ℤcz 12516 ℤ_≥cuz 12780 ...cfz 13453 ⌊cfl 13741 seqcseq 13955 ↑cexp 14015 !cfa 14227 Ccbc 14256 ∥ cdvds 16213 ℙcprime 16632 pCnt cpc 16799

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5200 ax-sep 5219 ax-nul 5229 ax-pow 5295 ax-pr 5363 ax-un 7679 ax-inf2 9554 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107 ax-pre-sup 11108

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4263 df-if 4456 df-pw 4532 df-sn 4557 df-pr 4559 df-op 4563 df-uni 4840 df-int 4879 df-iun 4924 df-br 5074 df-opab 5136 df-mpt 5155 df-tr 5181 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7314 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7808 df-1st 7932 df-2nd 7933 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-2o 8397 df-er 8634 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-sup 9346 df-inf 9347 df-oi 9416 df-card 9855 df-pnf 11173 df-mnf 11174 df-xr 11175 df-ltxr 11176 df-le 11177 df-sub 11371 df-neg 11372 df-div 11800 df-nn 12167 df-2 12236 df-3 12237 df-4 12238 df-5 12239 df-n0 12430 df-z 12517 df-uz 12781 df-q 12891 df-rp 12935 df-fz 13454 df-fzo 13601 df-fl 13743 df-mod 13821 df-seq 13956 df-exp 14016 df-fac 14228 df-bc 14257 df-hash 14285 df-cj 15053 df-re 15054 df-im 15055 df-sqrt 15189 df-abs 15190 df-clim 15442 df-sum 15641 df-dvds 16214 df-gcd 16456 df-prm 16633 df-pc 16800

This theorem is referenced by: bposlem6 27271

W3C validator