bposlem2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > bposlem2		GIF version

Theorem bposlem2 16312

Description: There are no odd primes in the range (2𝑁 / 3, 𝑁] dividing the 𝑁-th central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)

**Hypotheses**
Ref	Expression
bposlem2.1	⊢ (𝜑 → 𝑁 ∈ ℕ)
bposlem2.2	⊢ (𝜑 → 𝑃 ∈ ℙ)
bposlem2.3	⊢ (𝜑 → 2 < 𝑃)
bposlem2.4	⊢ (𝜑 → ((2 · 𝑁) / 3) < 𝑃)
bposlem2.5	⊢ (𝜑 → 𝑃 ≤ 𝑁)

**Assertion**
Ref	Expression
bposlem2	⊢ (𝜑 → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = 0)

Proof of Theorem bposlem2 Dummy variables 𝐴 𝑘 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bposlem2.1	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
2		bposlem2.2	. . 3 ⊢ (𝜑 → 𝑃 ∈ ℙ)
3		pcbcctr 16303	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))))
4	1, 2, 3	syl2anc 415	. 2 ⊢ (𝜑 → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))))
5		elfznn 10477	. . . . . 6 ⊢ (𝑘 ∈ (1...(2 · 𝑁)) → 𝑘 ∈ ℕ)
6		elnn1uz2 10023	. . . . . 6 ⊢ (𝑘 ∈ ℕ ↔ (𝑘 = 1 ∨ 𝑘 ∈ (ℤ_≥‘2)))
7	5, 6	sylib 122	. . . . 5 ⊢ (𝑘 ∈ (1...(2 · 𝑁)) → (𝑘 = 1 ∨ 𝑘 ∈ (ℤ_≥‘2)))
8		oveq2 6096	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (𝑃↑𝑘) = (𝑃↑1))
9		prmnn 12913	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
10	2, 9	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ ℕ)
11	10	nncnd 9327	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℂ)
12	11	exp1d 11127	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃↑1) = 𝑃)
13	8, 12	sylan9eqr 2293	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 = 1) → (𝑃↑𝑘) = 𝑃)
14	13	oveq2d 6104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = 1) → ((2 · 𝑁) / (𝑃↑𝑘)) = ((2 · 𝑁) / 𝑃))
15	14	fveq2d 5702	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 = 1) → (⌊‘((2 · 𝑁) / (𝑃↑𝑘))) = (⌊‘((2 · 𝑁) / 𝑃)))
16		2t1e2 9467	. . . . . . . . . . . . 13 ⊢ (2 · 1) = 2
17	11	mullidd 8350	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · 𝑃) = 𝑃)
18		bposlem2.5	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ≤ 𝑁)
19	17, 18	eqbrtrd 4153	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · 𝑃) ≤ 𝑁)
20		1red 8347	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℝ)
21	1	nnred 9326	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℝ)
22	10	nnred 9326	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℝ)
23	10	nngt0d 9357	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < 𝑃)
24		lemuldiv 9219	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → ((1 · 𝑃) ≤ 𝑁 ↔ 1 ≤ (𝑁 / 𝑃)))
25	20, 21, 22, 23, 24	syl112anc 1282	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1 · 𝑃) ≤ 𝑁 ↔ 1 ≤ (𝑁 / 𝑃)))
26	19, 25	mpbid 147	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 1 ≤ (𝑁 / 𝑃))
27	21, 10	nndivred 9363	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℝ)
28		1re 8331	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ
29		2re 9383	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
30		2pos 9404	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 2
31	29, 30	pm3.2i 272	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℝ ∧ 0 < 2)
32		lemul2 9195	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℝ ∧ (𝑁 / 𝑃) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (1 ≤ (𝑁 / 𝑃) ↔ (2 · 1) ≤ (2 · (𝑁 / 𝑃))))
33	28, 31, 32	mp3an13 1369	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 / 𝑃) ∈ ℝ → (1 ≤ (𝑁 / 𝑃) ↔ (2 · 1) ≤ (2 · (𝑁 / 𝑃))))
34	27, 33	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 ≤ (𝑁 / 𝑃) ↔ (2 · 1) ≤ (2 · (𝑁 / 𝑃))))
35	26, 34	mpbid 147	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 1) ≤ (2 · (𝑁 / 𝑃)))
36	16, 35	eqbrtrrid 4167	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ≤ (2 · (𝑁 / 𝑃)))
37		2cnd 9386	. . . . . . . . . . . . 13 ⊢ (𝜑 → 2 ∈ ℂ)
38	1	nncnd 9327	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
39	10	nnap0d 9359	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 # 0)
40	37, 38, 11, 39	divassapd 9164	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 𝑁) / 𝑃) = (2 · (𝑁 / 𝑃)))
41	36, 40	breqtrrd 4159	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≤ ((2 · 𝑁) / 𝑃))
42		bposlem2.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝑁) / 3) < 𝑃)
43		2nn 9477	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
44		nnmulcl 9334	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
45	43, 1, 44	sylancr 418	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · 𝑁) ∈ ℕ)
46	45	nnred 9326	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ)
47		3re 9387	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℝ
48		3pos 9407	. . . . . . . . . . . . . . . 16 ⊢ 0 < 3
49	47, 48	pm3.2i 272	. . . . . . . . . . . . . . 15 ⊢ (3 ∈ ℝ ∧ 0 < 3)
50		ltdiv23 9230	. . . . . . . . . . . . . . 15 ⊢ (((2 · 𝑁) ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3) ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((2 · 𝑁) / 3) < 𝑃 ↔ ((2 · 𝑁) / 𝑃) < 3))
51	49, 50	mp3an2 1366	. . . . . . . . . . . . . 14 ⊢ (((2 · 𝑁) ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (((2 · 𝑁) / 3) < 𝑃 ↔ ((2 · 𝑁) / 𝑃) < 3))
52	46, 22, 23, 51	syl12anc 1276	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · 𝑁) / 3) < 𝑃 ↔ ((2 · 𝑁) / 𝑃) < 3))
53	42, 52	mpbid 147	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 𝑁) / 𝑃) < 3)
54		df-3 9373	. . . . . . . . . . . 12 ⊢ 3 = (2 + 1)
55	53, 54	breqtrdi 4172	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁) / 𝑃) < (2 + 1))
56	45	nnzd 9778	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 𝑁) ∈ ℤ)
57		znq 10040	. . . . . . . . . . . . 13 ⊢ (((2 · 𝑁) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((2 · 𝑁) / 𝑃) ∈ ℚ)
58	56, 10, 57	syl2anc 415	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 𝑁) / 𝑃) ∈ ℚ)
59		2z 9683	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
60		flqbi 10746	. . . . . . . . . . . 12 ⊢ ((((2 · 𝑁) / 𝑃) ∈ ℚ ∧ 2 ∈ ℤ) → ((⌊‘((2 · 𝑁) / 𝑃)) = 2 ↔ (2 ≤ ((2 · 𝑁) / 𝑃) ∧ ((2 · 𝑁) / 𝑃) < (2 + 1))))
61	58, 59, 60	sylancl 417	. . . . . . . . . . 11 ⊢ (𝜑 → ((⌊‘((2 · 𝑁) / 𝑃)) = 2 ↔ (2 ≤ ((2 · 𝑁) / 𝑃) ∧ ((2 · 𝑁) / 𝑃) < (2 + 1))))
62	41, 55, 61	mpbir2and 957	. . . . . . . . . 10 ⊢ (𝜑 → (⌊‘((2 · 𝑁) / 𝑃)) = 2)
63	62	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 = 1) → (⌊‘((2 · 𝑁) / 𝑃)) = 2)
64	15, 63	eqtrd 2271	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 1) → (⌊‘((2 · 𝑁) / (𝑃↑𝑘))) = 2)
65	13	oveq2d 6104	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 = 1) → (𝑁 / (𝑃↑𝑘)) = (𝑁 / 𝑃))
66	65	fveq2d 5702	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 = 1) → (⌊‘(𝑁 / (𝑃↑𝑘))) = (⌊‘(𝑁 / 𝑃)))
67		remulcl 8313	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ ∧ (𝑁 / 𝑃) ∈ ℝ) → (2 · (𝑁 / 𝑃)) ∈ ℝ)
68	29, 27, 67	sylancr 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑁 / 𝑃)) ∈ ℝ)
69	47	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ∈ ℝ)
70		4re 9390	. . . . . . . . . . . . . . . . . 18 ⊢ 4 ∈ ℝ
71	70	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 4 ∈ ℝ)
72	40, 53	eqbrtrrd 4155	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑁 / 𝑃)) < 3)
73		3lt4 9488	. . . . . . . . . . . . . . . . . 18 ⊢ 3 < 4
74	73	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 < 4)
75	68, 69, 71, 72, 74	lttrd 8459	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑁 / 𝑃)) < 4)
76		2t2e4 9468	. . . . . . . . . . . . . . . 16 ⊢ (2 · 2) = 4
77	75, 76	breqtrrdi 4173	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑁 / 𝑃)) < (2 · 2))
78		ltmul2 9194	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 / 𝑃) ∈ ℝ ∧ 2 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑁 / 𝑃) < 2 ↔ (2 · (𝑁 / 𝑃)) < (2 · 2)))
79	29, 31, 78	mp3an23 1370	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 / 𝑃) ∈ ℝ → ((𝑁 / 𝑃) < 2 ↔ (2 · (𝑁 / 𝑃)) < (2 · 2)))
80	27, 79	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑁 / 𝑃) < 2 ↔ (2 · (𝑁 / 𝑃)) < (2 · 2)))
81	77, 80	mpbird 167	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 𝑃) < 2)
82		df-2 9372	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
83	81, 82	breqtrdi 4172	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 / 𝑃) < (1 + 1))
84	1	nnzd 9778	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℤ)
85		znq 10040	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑁 / 𝑃) ∈ ℚ)
86	84, 10, 85	syl2anc 415	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℚ)
87		1z 9681	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
88		flqbi 10746	. . . . . . . . . . . . . 14 ⊢ (((𝑁 / 𝑃) ∈ ℚ ∧ 1 ∈ ℤ) → ((⌊‘(𝑁 / 𝑃)) = 1 ↔ (1 ≤ (𝑁 / 𝑃) ∧ (𝑁 / 𝑃) < (1 + 1))))
89	86, 87, 88	sylancl 417	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((⌊‘(𝑁 / 𝑃)) = 1 ↔ (1 ≤ (𝑁 / 𝑃) ∧ (𝑁 / 𝑃) < (1 + 1))))
90	26, 83, 89	mpbir2and 957	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(𝑁 / 𝑃)) = 1)
91	90	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 = 1) → (⌊‘(𝑁 / 𝑃)) = 1)
92	66, 91	eqtrd 2271	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = 1) → (⌊‘(𝑁 / (𝑃↑𝑘))) = 1)
93	92	oveq2d 6104	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 = 1) → (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))) = (2 · 1))
94	93, 16	eqtrdi 2287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 1) → (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))) = 2)
95	64, 94	oveq12d 6106	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 = 1) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = (2 − 2))
96		2cn 9384	. . . . . . . 8 ⊢ 2 ∈ ℂ
97	96	subidi 8604	. . . . . . 7 ⊢ (2 − 2) = 0
98	95, 97	eqtrdi 2287	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 = 1) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = 0)
99	45	nnrpd 10112	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ⁺)
100	99	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (2 · 𝑁) ∈ ℝ⁺)
101		eluzge2nn0 9986	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 𝑘 ∈ ℕ₀)
102		nnexpcl 11010	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ₀) → (𝑃↑𝑘) ∈ ℕ)
103	10, 101, 102	syl2an 289	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃↑𝑘) ∈ ℕ)
104	103	nnrpd 10112	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃↑𝑘) ∈ ℝ⁺)
105	100, 104	rpdivcld 10132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((2 · 𝑁) / (𝑃↑𝑘)) ∈ ℝ⁺)
106	105	rpge0d 10118	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 0 ≤ ((2 · 𝑁) / (𝑃↑𝑘)))
107	46	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (2 · 𝑁) ∈ ℝ)
108		remulcl 8313	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (3 · 𝑃) ∈ ℝ)
109	47, 22, 108	sylancr 418	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · 𝑃) ∈ ℝ)
110	109	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (3 · 𝑃) ∈ ℝ)
111	103	nnred 9326	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃↑𝑘) ∈ ℝ)
112		ltdivmul 9214	. . . . . . . . . . . . . . . . 17 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (((2 · 𝑁) / 3) < 𝑃 ↔ (2 · 𝑁) < (3 · 𝑃)))
113	49, 112	mp3an3 1367	. . . . . . . . . . . . . . . 16 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 𝑃 ∈ ℝ) → (((2 · 𝑁) / 3) < 𝑃 ↔ (2 · 𝑁) < (3 · 𝑃)))
114	46, 22, 113	syl2anc 415	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · 𝑁) / 3) < 𝑃 ↔ (2 · 𝑁) < (3 · 𝑃)))
115	42, 114	mpbid 147	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 𝑁) < (3 · 𝑃))
116	115	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (2 · 𝑁) < (3 · 𝑃))
117	22, 22	remulcld 8362	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 · 𝑃) ∈ ℝ)
118	117	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃 · 𝑃) ∈ ℝ)
119		bposlem2.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 2 < 𝑃)
120		nnltp1le 9716	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℕ ∧ 𝑃 ∈ ℕ) → (2 < 𝑃 ↔ (2 + 1) ≤ 𝑃))
121	43, 10, 120	sylancr 418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (2 < 𝑃 ↔ (2 + 1) ≤ 𝑃))
122	119, 121	mpbid 147	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 + 1) ≤ 𝑃)
123	54, 122	eqbrtrid 4166	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 3 ≤ 𝑃)
124		lemul1 8929	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (3 ≤ 𝑃 ↔ (3 · 𝑃) ≤ (𝑃 · 𝑃)))
125	47, 124	mp3an1 1365	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℝ ∧ (𝑃 ∈ ℝ ∧ 0 < 𝑃)) → (3 ≤ 𝑃 ↔ (3 · 𝑃) ≤ (𝑃 · 𝑃)))
126	22, 22, 23, 125	syl12anc 1276	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (3 ≤ 𝑃 ↔ (3 · 𝑃) ≤ (𝑃 · 𝑃)))
127	123, 126	mpbid 147	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (3 · 𝑃) ≤ (𝑃 · 𝑃))
128	127	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (3 · 𝑃) ≤ (𝑃 · 𝑃))
129	11	sqvald 11129	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃↑2) = (𝑃 · 𝑃))
130	129	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃↑2) = (𝑃 · 𝑃))
131	22	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑃 ∈ ℝ)
132	10	nnge1d 9356	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ≤ 𝑃)
133	132	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 1 ≤ 𝑃)
134		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑘 ∈ (ℤ_≥‘2))
135	131, 133, 134	leexp2ad 11161	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃↑2) ≤ (𝑃↑𝑘))
136	130, 135	eqbrtrrd 4155	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃 · 𝑃) ≤ (𝑃↑𝑘))
137	110, 118, 111, 128, 136	letrd 8457	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (3 · 𝑃) ≤ (𝑃↑𝑘))
138	107, 110, 111, 116, 137	ltletrd 8758	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (2 · 𝑁) < (𝑃↑𝑘))
139	103	nncnd 9327	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃↑𝑘) ∈ ℂ)
140	139	mulridd 8349	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((𝑃↑𝑘) · 1) = (𝑃↑𝑘))
141	138, 140	breqtrrd 4159	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (2 · 𝑁) < ((𝑃↑𝑘) · 1))
142		1red 8347	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 1 ∈ ℝ)
143	107, 142, 104	ltdivmuld 10166	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (((2 · 𝑁) / (𝑃↑𝑘)) < 1 ↔ (2 · 𝑁) < ((𝑃↑𝑘) · 1)))
144	141, 143	mpbird 167	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((2 · 𝑁) / (𝑃↑𝑘)) < 1)
145		1e0p1 9834	. . . . . . . . . 10 ⊢ 1 = (0 + 1)
146	144, 145	breqtrdi 4172	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((2 · 𝑁) / (𝑃↑𝑘)) < (0 + 1))
147		znq 10040	. . . . . . . . . . 11 ⊢ (((2 · 𝑁) ∈ ℤ ∧ (𝑃↑𝑘) ∈ ℕ) → ((2 · 𝑁) / (𝑃↑𝑘)) ∈ ℚ)
148	56, 103, 147	syl2an2r 603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((2 · 𝑁) / (𝑃↑𝑘)) ∈ ℚ)
149		0z 9666	. . . . . . . . . 10 ⊢ 0 ∈ ℤ
150		flqbi 10746	. . . . . . . . . 10 ⊢ ((((2 · 𝑁) / (𝑃↑𝑘)) ∈ ℚ ∧ 0 ∈ ℤ) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) = 0 ↔ (0 ≤ ((2 · 𝑁) / (𝑃↑𝑘)) ∧ ((2 · 𝑁) / (𝑃↑𝑘)) < (0 + 1))))
151	148, 149, 150	sylancl 417	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) = 0 ↔ (0 ≤ ((2 · 𝑁) / (𝑃↑𝑘)) ∧ ((2 · 𝑁) / (𝑃↑𝑘)) < (0 + 1))))
152	106, 146, 151	mpbir2and 957	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (⌊‘((2 · 𝑁) / (𝑃↑𝑘))) = 0)
153	1	nnrpd 10112	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
154	153	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑁 ∈ ℝ⁺)
155	154, 104	rpdivcld 10132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑁 / (𝑃↑𝑘)) ∈ ℝ⁺)
156	155	rpge0d 10118	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 0 ≤ (𝑁 / (𝑃↑𝑘)))
157	21	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑁 ∈ ℝ)
158	21, 153	ltaddrpd 10148	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 < (𝑁 + 𝑁))
159	38	2timesd 9559	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁))
160	158, 159	breqtrrd 4159	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 < (2 · 𝑁))
161	160	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑁 < (2 · 𝑁))
162	157, 107, 111, 161, 138	lttrd 8459	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑁 < (𝑃↑𝑘))
163	162, 140	breqtrrd 4159	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑁 < ((𝑃↑𝑘) · 1))
164	157, 142, 104	ltdivmuld 10166	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((𝑁 / (𝑃↑𝑘)) < 1 ↔ 𝑁 < ((𝑃↑𝑘) · 1)))
165	163, 164	mpbird 167	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑁 / (𝑃↑𝑘)) < 1)
166	165, 145	breqtrdi 4172	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑁 / (𝑃↑𝑘)) < (0 + 1))
167		znq 10040	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ (𝑃↑𝑘) ∈ ℕ) → (𝑁 / (𝑃↑𝑘)) ∈ ℚ)
168	84, 103, 167	syl2an2r 603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑁 / (𝑃↑𝑘)) ∈ ℚ)
169		flqbi 10746	. . . . . . . . . . . 12 ⊢ (((𝑁 / (𝑃↑𝑘)) ∈ ℚ ∧ 0 ∈ ℤ) → ((⌊‘(𝑁 / (𝑃↑𝑘))) = 0 ↔ (0 ≤ (𝑁 / (𝑃↑𝑘)) ∧ (𝑁 / (𝑃↑𝑘)) < (0 + 1))))
170	168, 149, 169	sylancl 417	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((⌊‘(𝑁 / (𝑃↑𝑘))) = 0 ↔ (0 ≤ (𝑁 / (𝑃↑𝑘)) ∧ (𝑁 / (𝑃↑𝑘)) < (0 + 1))))
171	156, 166, 170	mpbir2and 957	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (⌊‘(𝑁 / (𝑃↑𝑘))) = 0)
172	171	oveq2d 6104	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))) = (2 · 0))
173		2t0e0 9475	. . . . . . . . 9 ⊢ (2 · 0) = 0
174	172, 173	eqtrdi 2287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))) = 0)
175	152, 174	oveq12d 6106	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = (0 − 0))
176		0m0e0 9425	. . . . . . 7 ⊢ (0 − 0) = 0
177	175, 176	eqtrdi 2287	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = 0)
178	98, 177	jaodan 809	. . . . 5 ⊢ ((𝜑 ∧ (𝑘 = 1 ∨ 𝑘 ∈ (ℤ_≥‘2))) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = 0)
179	7, 178	sylan2 286	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = 0)
180	179	sumeq2dv 12159	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = Σ𝑘 ∈ (1...(2 · 𝑁))0)
181		1zzd 9682	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
182	181, 56	fzfigd 10889	. . . 4 ⊢ (𝜑 → (1...(2 · 𝑁)) ∈ Fin)
183		isumz 12181	. . . . 5 ⊢ (((𝐴 ∈ ℤ ∧ (1...(2 · 𝑁)) ⊆ (ℤ_≥‘𝐴) ∧ ∀𝑥 ∈ (ℤ_≥‘𝐴)DECID 𝑥 ∈ (1...(2 · 𝑁))) ∨ (1...(2 · 𝑁)) ∈ Fin) → Σ𝑘 ∈ (1...(2 · 𝑁))0 = 0)
184	183	olcs 748	. . . 4 ⊢ ((1...(2 · 𝑁)) ∈ Fin → Σ𝑘 ∈ (1...(2 · 𝑁))0 = 0)
185	182, 184	syl 14	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ (1...(2 · 𝑁))0 = 0)
186	180, 185	eqtrd 2271	. 2 ⊢ (𝜑 → Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = 0)
187	4, 186	eqtrd 2271	1 ⊢ (𝜑 → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = 0)

Colors of variables: wff set class

This proof depends on syntax axioms: → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 DECID wdc 846 ∧ w3a 1009 = wceq 1402 ∈ wcel 2209 ∀wral 2528 ⊆ wss 3220 class class class wbr 4131 ‘cfv 5380 (class class class)co 6088 Fincfn 7026 ℝcr 8184 0cc0 8185 1c1 8186 + caddc 8188 · cmul 8190 < clt 8366 ≤ cle 8367 − cmin 8504 / cdiv 9010 ℕcn 9313 2c2 9364 3c3 9365 4c4 9366 ℕ₀cn0 9574 ℤcz 9655 ℤ_≥cuz 9937 ℚcq 10035 ℝ⁺crp 10071 ...cfz 10428 ⌊cfl 10720 ↑cexp 10996 Ccbc 11207 Σcsu 12144 ℙcprime 12910 pCnt cpc 13092

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-iinf 4737 ax-cnex 8276 ax-resscn 8277 ax-1cn 8278 ax-1re 8279 ax-icn 8280 ax-addcl 8281 ax-addrcl 8282 ax-mulcl 8283 ax-mulrcl 8284 ax-addcom 8285 ax-mulcom 8286 ax-addass 8287 ax-mulass 8288 ax-distr 8289 ax-i2m1 8290 ax-0lt1 8291 ax-1rid 8292 ax-0id 8293 ax-rnegex 8294 ax-precex 8295 ax-cnre 8296 ax-pre-ltirr 8297 ax-pre-ltwlin 8298 ax-pre-lttrn 8299 ax-pre-apti 8300 ax-pre-ltadd 8301 ax-pre-mulgt0 8302 ax-pre-mulext 8303 ax-arch 8304 ax-caucvg 8305

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4132 df-opab 4194 df-mpt 4195 df-tr 4232 df-id 4440 df-po 4443 df-iso 4444 df-iord 4513 df-on 4515 df-ilim 4516 df-suc 4518 df-iom 4740 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-isom 5389 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-1st 6378 df-2nd 6379 df-recs 6580 df-irdg 6645 df-frec 6666 df-1o 6691 df-2o 6692 df-oadd 6695 df-er 6811 df-en 7027 df-dom 7028 df-fin 7029 df-sup 7330 df-inf 7331 df-pnf 8368 df-mnf 8369 df-xr 8370 df-ltxr 8371 df-le 8372 df-sub 8506 df-neg 8507 df-reap 8911 df-ap 8918 df-div 9011 df-inn 9314 df-2 9372 df-3 9373 df-4 9374 df-n0 9575 df-z 9656 df-uz 9938 df-q 10036 df-rp 10072 df-fz 10429 df-fzo 10567 df-fl 10722 df-mod 10781 df-seqfrec 10906 df-exp 10997 df-fac 11186 df-bc 11208 df-ihash 11237 df-cj 11629 df-re 11630 df-im 11631 df-rsqrt 11786 df-abs 11787 df-clim 12070 df-sumdc 12145 df-dvds 12580 df-gcd 12756 df-prm 12911 df-pc 13093

This theorem is used by: bposlem3 16313

W3C validator