bposlem2 - Intuitionistic Logic Explorer

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

Theorem bposlem2 16210

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 16201	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))))
4	1, 2, 3	syl2anc 415	. 2 ⊢ (𝜑 → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))))
5		elfznn 10470	. . . . . 6 ⊢ (𝑘 ∈ (1...(2 · 𝑁)) → 𝑘 ∈ ℕ)
6		elnn1uz2 10016	. . . . . 6 ⊢ (𝑘 ∈ ℕ ↔ (𝑘 = 1 ∨ 𝑘 ∈ (ℤ_≥‘2)))
7	5, 6	sylib 122	. . . . 5 ⊢ (𝑘 ∈ (1...(2 · 𝑁)) → (𝑘 = 1 ∨ 𝑘 ∈ (ℤ_≥‘2)))
8		oveq2 6093	. . . . . . . . . . . 12 ⊢ (𝑘 = 1 → (𝑃↑𝑘) = (𝑃↑1))
9		prmnn 12904	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
10	2, 9	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑃 ∈ ℕ)
11	10	nncnd 9320	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℂ)
12	11	exp1d 11119	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃↑1) = 𝑃)
13	8, 12	sylan9eqr 2293	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 = 1) → (𝑃↑𝑘) = 𝑃)
14	13	oveq2d 6101	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 = 1) → ((2 · 𝑁) / (𝑃↑𝑘)) = ((2 · 𝑁) / 𝑃))
15	14	fveq2d 5699	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 = 1) → (⌊‘((2 · 𝑁) / (𝑃↑𝑘))) = (⌊‘((2 · 𝑁) / 𝑃)))
16		2t1e2 9460	. . . . . . . . . . . . 13 ⊢ (2 · 1) = 2
17	11	mullidd 8344	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 · 𝑃) = 𝑃)
18		bposlem2.5	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ≤ 𝑁)
19	17, 18	eqbrtrd 4152	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · 𝑃) ≤ 𝑁)
20		1red 8341	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 1 ∈ ℝ)
21	1	nnred 9319	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℝ)
22	10	nnred 9319	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℝ)
23	10	nngt0d 9350	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 < 𝑃)
24		lemuldiv 9213	. . . . . . . . . . . . . . . 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 9356	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℝ)
28		1re 8325	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ
29		2re 9376	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
30		2pos 9397	. . . . . . . . . . . . . . . . 17 ⊢ 0 < 2
31	29, 30	pm3.2i 272	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℝ ∧ 0 < 2)
32		lemul2 9189	. . . . . . . . . . . . . . . 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 4166	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ≤ (2 · (𝑁 / 𝑃)))
37		2cnd 9379	. . . . . . . . . . . . 13 ⊢ (𝜑 → 2 ∈ ℂ)
38	1	nncnd 9320	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
39	10	nnap0d 9352	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 # 0)
40	37, 38, 11, 39	divassapd 9158	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 𝑁) / 𝑃) = (2 · (𝑁 / 𝑃)))
41	36, 40	breqtrrd 4158	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≤ ((2 · 𝑁) / 𝑃))
42		bposlem2.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝑁) / 3) < 𝑃)
43		2nn 9470	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
44		nnmulcl 9327	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
45	43, 1, 44	sylancr 418	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · 𝑁) ∈ ℕ)
46	45	nnred 9319	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ)
47		3re 9380	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℝ
48		3pos 9400	. . . . . . . . . . . . . . . 16 ⊢ 0 < 3
49	47, 48	pm3.2i 272	. . . . . . . . . . . . . . 15 ⊢ (3 ∈ ℝ ∧ 0 < 3)
50		ltdiv23 9224	. . . . . . . . . . . . . . 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 9366	. . . . . . . . . . . 12 ⊢ 3 = (2 + 1)
55	53, 54	breqtrdi 4171	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁) / 𝑃) < (2 + 1))
56	45	nnzd 9771	. . . . . . . . . . . . 13 ⊢ (𝜑 → (2 · 𝑁) ∈ ℤ)
57		znq 10033	. . . . . . . . . . . . 13 ⊢ (((2 · 𝑁) ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((2 · 𝑁) / 𝑃) ∈ ℚ)
58	56, 10, 57	syl2anc 415	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 𝑁) / 𝑃) ∈ ℚ)
59		2z 9676	. . . . . . . . . . . 12 ⊢ 2 ∈ ℤ
60		flqbi 10738	. . . . . . . . . . . 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 6101	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 = 1) → (𝑁 / (𝑃↑𝑘)) = (𝑁 / 𝑃))
66	65	fveq2d 5699	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 = 1) → (⌊‘(𝑁 / (𝑃↑𝑘))) = (⌊‘(𝑁 / 𝑃)))
67		remulcl 8307	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℝ ∧ (𝑁 / 𝑃) ∈ ℝ) → (2 · (𝑁 / 𝑃)) ∈ ℝ)
68	29, 27, 67	sylancr 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑁 / 𝑃)) ∈ ℝ)
69	47	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 ∈ ℝ)
70		4re 9383	. . . . . . . . . . . . . . . . . 18 ⊢ 4 ∈ ℝ
71	70	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 4 ∈ ℝ)
72	40, 53	eqbrtrrd 4154	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · (𝑁 / 𝑃)) < 3)
73		3lt4 9481	. . . . . . . . . . . . . . . . . 18 ⊢ 3 < 4
74	73	a1i 9	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 3 < 4)
75	68, 69, 71, 72, 74	lttrd 8453	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (2 · (𝑁 / 𝑃)) < 4)
76		2t2e4 9461	. . . . . . . . . . . . . . . 16 ⊢ (2 · 2) = 4
77	75, 76	breqtrrdi 4172	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (2 · (𝑁 / 𝑃)) < (2 · 2))
78		ltmul2 9188	. . . . . . . . . . . . . . . . 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 9365	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
83	81, 82	breqtrdi 4171	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 / 𝑃) < (1 + 1))
84	1	nnzd 9771	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℤ)
85		znq 10033	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑁 / 𝑃) ∈ ℚ)
86	84, 10, 85	syl2anc 415	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℚ)
87		1z 9674	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
88		flqbi 10738	. . . . . . . . . . . . . 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 6101	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 = 1) → (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))) = (2 · 1))
94	93, 16	eqtrdi 2287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 = 1) → (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))) = 2)
95	64, 94	oveq12d 6103	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 = 1) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = (2 − 2))
96		2cn 9377	. . . . . . . 8 ⊢ 2 ∈ ℂ
97	96	subidi 8598	. . . . . . 7 ⊢ (2 − 2) = 0
98	95, 97	eqtrdi 2287	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 = 1) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = 0)
99	45	nnrpd 10105	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ⁺)
100	99	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (2 · 𝑁) ∈ ℝ⁺)
101		eluzge2nn0 9979	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ℤ_≥‘2) → 𝑘 ∈ ℕ₀)
102		nnexpcl 11002	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ₀) → (𝑃↑𝑘) ∈ ℕ)
103	10, 101, 102	syl2an 289	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃↑𝑘) ∈ ℕ)
104	103	nnrpd 10105	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃↑𝑘) ∈ ℝ⁺)
105	100, 104	rpdivcld 10125	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((2 · 𝑁) / (𝑃↑𝑘)) ∈ ℝ⁺)
106	105	rpge0d 10111	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 0 ≤ ((2 · 𝑁) / (𝑃↑𝑘)))
107	46	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (2 · 𝑁) ∈ ℝ)
108		remulcl 8307	. . . . . . . . . . . . . . 15 ⊢ ((3 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (3 · 𝑃) ∈ ℝ)
109	47, 22, 108	sylancr 418	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · 𝑃) ∈ ℝ)
110	109	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (3 · 𝑃) ∈ ℝ)
111	103	nnred 9319	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃↑𝑘) ∈ ℝ)
112		ltdivmul 9208	. . . . . . . . . . . . . . . . 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 8356	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑃 · 𝑃) ∈ ℝ)
118	117	adantr 276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃 · 𝑃) ∈ ℝ)
119		bposlem2.3	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 2 < 𝑃)
120		nnltp1le 9709	. . . . . . . . . . . . . . . . . . 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 4165	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 3 ≤ 𝑃)
124		lemul1 8923	. . . . . . . . . . . . . . . . . 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 11121	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃↑2) = (𝑃 · 𝑃))
130	129	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃↑2) = (𝑃 · 𝑃))
131	22	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑃 ∈ ℝ)
132	10	nnge1d 9349	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ≤ 𝑃)
133	132	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 1 ≤ 𝑃)
134		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑘 ∈ (ℤ_≥‘2))
135	131, 133, 134	leexp2ad 11153	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃↑2) ≤ (𝑃↑𝑘))
136	130, 135	eqbrtrrd 4154	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃 · 𝑃) ≤ (𝑃↑𝑘))
137	110, 118, 111, 128, 136	letrd 8451	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (3 · 𝑃) ≤ (𝑃↑𝑘))
138	107, 110, 111, 116, 137	ltletrd 8752	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (2 · 𝑁) < (𝑃↑𝑘))
139	103	nncnd 9320	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑃↑𝑘) ∈ ℂ)
140	139	mulridd 8343	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((𝑃↑𝑘) · 1) = (𝑃↑𝑘))
141	138, 140	breqtrrd 4158	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (2 · 𝑁) < ((𝑃↑𝑘) · 1))
142		1red 8341	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 1 ∈ ℝ)
143	107, 142, 104	ltdivmuld 10159	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (((2 · 𝑁) / (𝑃↑𝑘)) < 1 ↔ (2 · 𝑁) < ((𝑃↑𝑘) · 1)))
144	141, 143	mpbird 167	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((2 · 𝑁) / (𝑃↑𝑘)) < 1)
145		1e0p1 9827	. . . . . . . . . 10 ⊢ 1 = (0 + 1)
146	144, 145	breqtrdi 4171	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((2 · 𝑁) / (𝑃↑𝑘)) < (0 + 1))
147		znq 10033	. . . . . . . . . . 11 ⊢ (((2 · 𝑁) ∈ ℤ ∧ (𝑃↑𝑘) ∈ ℕ) → ((2 · 𝑁) / (𝑃↑𝑘)) ∈ ℚ)
148	56, 103, 147	syl2an2r 603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((2 · 𝑁) / (𝑃↑𝑘)) ∈ ℚ)
149		0z 9659	. . . . . . . . . 10 ⊢ 0 ∈ ℤ
150		flqbi 10738	. . . . . . . . . 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 10105	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
154	153	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑁 ∈ ℝ⁺)
155	154, 104	rpdivcld 10125	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑁 / (𝑃↑𝑘)) ∈ ℝ⁺)
156	155	rpge0d 10111	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 0 ≤ (𝑁 / (𝑃↑𝑘)))
157	21	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑁 ∈ ℝ)
158	21, 153	ltaddrpd 10141	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 < (𝑁 + 𝑁))
159	38	2timesd 9552	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁))
160	158, 159	breqtrrd 4158	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 < (2 · 𝑁))
161	160	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑁 < (2 · 𝑁))
162	157, 107, 111, 161, 138	lttrd 8453	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑁 < (𝑃↑𝑘))
163	162, 140	breqtrrd 4158	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → 𝑁 < ((𝑃↑𝑘) · 1))
164	157, 142, 104	ltdivmuld 10159	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((𝑁 / (𝑃↑𝑘)) < 1 ↔ 𝑁 < ((𝑃↑𝑘) · 1)))
165	163, 164	mpbird 167	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑁 / (𝑃↑𝑘)) < 1)
166	165, 145	breqtrdi 4171	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑁 / (𝑃↑𝑘)) < (0 + 1))
167		znq 10033	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℤ ∧ (𝑃↑𝑘) ∈ ℕ) → (𝑁 / (𝑃↑𝑘)) ∈ ℚ)
168	84, 103, 167	syl2an2r 603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (𝑁 / (𝑃↑𝑘)) ∈ ℚ)
169		flqbi 10738	. . . . . . . . . . . 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 6101	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))) = (2 · 0))
173		2t0e0 9468	. . . . . . . . 9 ⊢ (2 · 0) = 0
174	172, 173	eqtrdi 2287	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))) = 0)
175	152, 174	oveq12d 6103	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘2)) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = (0 − 0))
176		0m0e0 9418	. . . . . . 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 12150	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = Σ𝑘 ∈ (1...(2 · 𝑁))0)
181		1zzd 9675	. . . . 5 ⊢ (𝜑 → 1 ∈ ℤ)
182	181, 56	fzfigd 10881	. . . 4 ⊢ (𝜑 → (1...(2 · 𝑁)) ∈ Fin)
183		isumz 12172	. . . . 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 4130 ‘cfv 5377 (class class class)co 6085 Fincfn 7022 ℝcr 8178 0cc0 8179 1c1 8180 + caddc 8182 · cmul 8184 < clt 8360 ≤ cle 8361 − cmin 8498 / cdiv 9004 ℕcn 9306 2c2 9357 3c3 9358 4c4 9359 ℕ₀cn0 9567 ℤcz 9648 ℤ_≥cuz 9930 ℚcq 10028 ℝ⁺crp 10064 ...cfz 10421 ⌊cfl 10713 ↑cexp 10988 Ccbc 11199 Σcsu 12135 ℙcprime 12901 pCnt cpc 13083

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 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298 ax-caucvg 8299

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 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-irdg 6641 df-frec 6662 df-1o 6687 df-2o 6688 df-oadd 6691 df-er 6807 df-en 7023 df-dom 7024 df-fin 7025 df-sup 7324 df-inf 7325 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8500 df-neg 8501 df-reap 8905 df-ap 8912 df-div 9005 df-inn 9307 df-2 9365 df-3 9366 df-4 9367 df-n0 9568 df-z 9649 df-uz 9931 df-q 10029 df-rp 10065 df-fz 10422 df-fzo 10560 df-fl 10715 df-mod 10773 df-seqfrec 10898 df-exp 10989 df-fac 11178 df-bc 11200 df-ihash 11229 df-cj 11621 df-re 11622 df-im 11623 df-rsqrt 11778 df-abs 11779 df-clim 12061 df-sumdc 12136 df-dvds 12571 df-gcd 12747 df-prm 12902 df-pc 13084

This theorem is used by: bposlem3 16211

W3C validator