chebbnd1lem1 - Metamath Proof Explorer

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

Theorem chebbnd1lem1 26962

Description: Lemma for chebbnd1 26965: show a lower bound on π(𝑥) at even integers using similar techniques to those used to prove bpos 26786. (Note that the expression 𝐾 is actually equal to 2 · 𝑁, but proving that is not necessary for the proof, and it's too much work.) The key to the proof is bposlem1 26777, which shows that each term in the expansion ((2 · 𝑁)C𝑁) = ∏𝑝 ∈ ℙ (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) is at most 2 · 𝑁, so that the sum really only has nonzero elements up to 2 · 𝑁, and since each term is at most 2 · 𝑁, after taking logs we get the inequality π(2 · 𝑁) · log(2 · 𝑁) ≤ log((2 · 𝑁)C𝑁), and bclbnd 26773 finishes the proof. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 15-Apr-2016.)

**Hypothesis**
Ref	Expression
chebbnd1lem1.1	⊢ 𝐾 = if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁))

**Assertion**
Ref	Expression
chebbnd1lem1	⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘((4↑𝑁) / 𝑁)) < ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁))))

Proof of Theorem chebbnd1lem1 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		4nn 12292	. . . . . 6 ⊢ 4 ∈ ℕ
2		eluznn 12899	. . . . . . . 8 ⊢ ((4 ∈ ℕ ∧ 𝑁 ∈ (ℤ_≥‘4)) → 𝑁 ∈ ℕ)
3	1, 2	mpan 689	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝑁 ∈ ℕ)
4	3	nnnn0d 12529	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝑁 ∈ ℕ₀)
5		nnexpcl 14037	. . . . . 6 ⊢ ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (4↑𝑁) ∈ ℕ)
6	1, 4, 5	sylancr 588	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (4↑𝑁) ∈ ℕ)
7	6	nnrpd 13011	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (4↑𝑁) ∈ ℝ⁺)
8	3	nnrpd 13011	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝑁 ∈ ℝ⁺)
9	7, 8	rpdivcld 13030	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((4↑𝑁) / 𝑁) ∈ ℝ⁺)
10	9	relogcld 26123	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘((4↑𝑁) / 𝑁)) ∈ ℝ)
11		fzctr 13610	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ (0...(2 · 𝑁)))
12	4, 11	syl 17	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝑁 ∈ (0...(2 · 𝑁)))
13		bccl2 14280	. . . . 5 ⊢ (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
14	12, 13	syl 17	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℕ)
15	14	nnrpd 13011	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℝ⁺)
16	15	relogcld 26123	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘((2 · 𝑁)C𝑁)) ∈ ℝ)
17		2z 12591	. . . . . . 7 ⊢ 2 ∈ ℤ
18		eluzelz 12829	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝑁 ∈ ℤ)
19		zmulcl 12608	. . . . . . 7 ⊢ ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 · 𝑁) ∈ ℤ)
20	17, 18, 19	sylancr 588	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (2 · 𝑁) ∈ ℤ)
21	20	zred 12663	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (2 · 𝑁) ∈ ℝ)
22		ppicl 26625	. . . . 5 ⊢ ((2 · 𝑁) ∈ ℝ → (π‘(2 · 𝑁)) ∈ ℕ₀)
23	21, 22	syl 17	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (π‘(2 · 𝑁)) ∈ ℕ₀)
24	23	nn0red 12530	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (π‘(2 · 𝑁)) ∈ ℝ)
25		2nn 12282	. . . . . 6 ⊢ 2 ∈ ℕ
26		nnmulcl 12233	. . . . . 6 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
27	25, 3, 26	sylancr 588	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (2 · 𝑁) ∈ ℕ)
28	27	nnrpd 13011	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (2 · 𝑁) ∈ ℝ⁺)
29	28	relogcld 26123	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘(2 · 𝑁)) ∈ ℝ)
30	24, 29	remulcld 11241	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁))) ∈ ℝ)
31		bclbnd 26773	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
32		logltb 26100	. . . 4 ⊢ ((((4↑𝑁) / 𝑁) ∈ ℝ⁺ ∧ ((2 · 𝑁)C𝑁) ∈ ℝ⁺) → (((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁) ↔ (log‘((4↑𝑁) / 𝑁)) < (log‘((2 · 𝑁)C𝑁))))
33	9, 15, 32	syl2anc 585	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁) ↔ (log‘((4↑𝑁) / 𝑁)) < (log‘((2 · 𝑁)C𝑁))))
34	31, 33	mpbid 231	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘((4↑𝑁) / 𝑁)) < (log‘((2 · 𝑁)C𝑁)))
35		chebbnd1lem1.1	. . . . . . . 8 ⊢ 𝐾 = if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁))
36	27, 14	ifcld 4574	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘4) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ∈ ℕ)
37	35, 36	eqeltrid 2838	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝐾 ∈ ℕ)
38	37	nnred 12224	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝐾 ∈ ℝ)
39		ppicl 26625	. . . . . 6 ⊢ (𝐾 ∈ ℝ → (π‘𝐾) ∈ ℕ₀)
40	38, 39	syl 17	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (π‘𝐾) ∈ ℕ₀)
41	40	nn0red 12530	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (π‘𝐾) ∈ ℝ)
42	41, 29	remulcld 11241	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) ∈ ℝ)
43		fzfid 13935	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (1...𝐾) ∈ Fin)
44		inss1 4228	. . . . . 6 ⊢ ((1...𝐾) ∩ ℙ) ⊆ (1...𝐾)
45		ssfi 9170	. . . . . 6 ⊢ (((1...𝐾) ∈ Fin ∧ ((1...𝐾) ∩ ℙ) ⊆ (1...𝐾)) → ((1...𝐾) ∩ ℙ) ∈ Fin)
46	43, 44, 45	sylancl 587	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((1...𝐾) ∩ ℙ) ∈ Fin)
47	37	nnzd 12582	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝐾 ∈ ℤ)
48	14	nnzd 12582	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℤ)
49	14	nnred 12224	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℝ)
50		min2 13166	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℝ ∧ ((2 · 𝑁)C𝑁) ∈ ℝ) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ ((2 · 𝑁)C𝑁))
51	21, 49, 50	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘4) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ ((2 · 𝑁)C𝑁))
52	35, 51	eqbrtrid 5183	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝐾 ≤ ((2 · 𝑁)C𝑁))
53		eluz2 12825	. . . . . . . . . 10 ⊢ (((2 · 𝑁)C𝑁) ∈ (ℤ_≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ ((2 · 𝑁)C𝑁) ∈ ℤ ∧ 𝐾 ≤ ((2 · 𝑁)C𝑁)))
54	47, 48, 52, 53	syl3anbrc 1344	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((2 · 𝑁)C𝑁) ∈ (ℤ_≥‘𝐾))
55		fzss2 13538	. . . . . . . . 9 ⊢ (((2 · 𝑁)C𝑁) ∈ (ℤ_≥‘𝐾) → (1...𝐾) ⊆ (1...((2 · 𝑁)C𝑁)))
56	54, 55	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (1...𝐾) ⊆ (1...((2 · 𝑁)C𝑁)))
57	56	ssrind 4235	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((1...𝐾) ∩ ℙ) ⊆ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ))
58	57	sselda 3982	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ))
59		simpr 486	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ))
60	59	elin1d 4198	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ (1...((2 · 𝑁)C𝑁)))
61		elfznn 13527	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...((2 · 𝑁)C𝑁)) → 𝑘 ∈ ℕ)
62	60, 61	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ℕ)
63	59	elin2d 4199	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ℙ)
64	14	adantr 482	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
65	63, 64	pccld 16780	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
66	62, 65	nnexpcld 14205	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℕ)
67	66	nnrpd 13011	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ⁺)
68	67	relogcld 26123	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℝ)
69	58, 68	syldan 592	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℝ)
70	29	adantr 482	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(2 · 𝑁)) ∈ ℝ)
71		elinel2 4196	. . . . . . . 8 ⊢ (𝑘 ∈ ((1...𝐾) ∩ ℙ) → 𝑘 ∈ ℙ)
72		bposlem1 26777	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℙ) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
73	3, 71, 72	syl2an 597	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
74	58, 67	syldan 592	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ⁺)
75	74	reeflogd 26124	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) = (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))
76	28	adantr 482	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (2 · 𝑁) ∈ ℝ⁺)
77	76	reeflogd 26124	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (exp‘(log‘(2 · 𝑁))) = (2 · 𝑁))
78	73, 75, 77	3brtr4d 5180	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) ≤ (exp‘(log‘(2 · 𝑁))))
79		efle 16058	. . . . . . 7 ⊢ (((log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℝ ∧ (log‘(2 · 𝑁)) ∈ ℝ) → ((log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ (log‘(2 · 𝑁)) ↔ (exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) ≤ (exp‘(log‘(2 · 𝑁)))))
80	69, 70, 79	syl2anc 585	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → ((log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ (log‘(2 · 𝑁)) ↔ (exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) ≤ (exp‘(log‘(2 · 𝑁)))))
81	78, 80	mpbird 257	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ (log‘(2 · 𝑁)))
82	46, 69, 70, 81	fsumle 15742	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)))
83	68	recnd 11239	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℂ)
84	58, 83	syldan 592	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℂ)
85		eldifn 4127	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) → ¬ 𝑘 ∈ ((1...𝐾) ∩ ℙ))
86	85	adantl 483	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → ¬ 𝑘 ∈ ((1...𝐾) ∩ ℙ))
87		simpr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)))
88	87	eldifad 3960	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ))
89	88	elin1d 4198	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ (1...((2 · 𝑁)C𝑁)))
90	89, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ ℕ)
91	90	adantrr 716	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ℕ)
92	91	nnred 12224	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ℝ)
93	88, 66	syldan 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℕ)
94	93	nnred 12224	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ)
95	94	adantrr 716	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ)
96	21	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (2 · 𝑁) ∈ ℝ)
97	91	nncnd 12225	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ℂ)
98	97	exp1d 14103	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑1) = 𝑘)
99	91	nnge1d 12257	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 1 ≤ 𝑘)
100		simprr 772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)
101		nnuz 12862	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ = (ℤ_≥‘1)
102	100, 101	eleqtrdi 2844	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ (ℤ_≥‘1))
103	92, 99, 102	leexp2ad 14214	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑1) ≤ (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))
104	98, 103	eqbrtrrd 5172	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))
105	3	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑁 ∈ ℕ)
106	88	elin2d 4199	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ ℙ)
107	106	adantrr 716	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ℙ)
108	105, 107, 72	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
109	92, 95, 96, 104, 108	letrd 11368	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ (2 · 𝑁))
110		elfzle2 13502	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...((2 · 𝑁)C𝑁)) → 𝑘 ≤ ((2 · 𝑁)C𝑁))
111	89, 110	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ≤ ((2 · 𝑁)C𝑁))
112	111	adantrr 716	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ ((2 · 𝑁)C𝑁))
113	49	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → ((2 · 𝑁)C𝑁) ∈ ℝ)
114		lemin 13168	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ ((2 · 𝑁)C𝑁) ∈ ℝ) → (𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ↔ (𝑘 ≤ (2 · 𝑁) ∧ 𝑘 ≤ ((2 · 𝑁)C𝑁))))
115	92, 96, 113, 114	syl3anc 1372	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ↔ (𝑘 ≤ (2 · 𝑁) ∧ 𝑘 ≤ ((2 · 𝑁)C𝑁))))
116	109, 112, 115	mpbir2and 712	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)))
117	116, 35	breqtrrdi 5190	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ 𝐾)
118	37	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝐾 ∈ ℕ)
119	118	nnzd 12582	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝐾 ∈ ℤ)
120		fznn 13566	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ ℤ → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ 𝐾)))
121	119, 120	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ 𝐾)))
122	91, 117, 121	mpbir2and 712	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ (1...𝐾))
123	122, 107	elind 4194	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ((1...𝐾) ∩ ℙ))
124	123	expr 458	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → ((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ → 𝑘 ∈ ((1...𝐾) ∩ ℙ)))
125	86, 124	mtod 197	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → ¬ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)
126	88, 65	syldan 592	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
127		elnn0 12471	. . . . . . . . . . . . 13 ⊢ ((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀ ↔ ((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ ∨ (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0))
128	126, 127	sylib 217	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → ((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ ∨ (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0))
129	128	ord 863	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (¬ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ → (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0))
130	125, 129	mpd 15	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0)
131	130	oveq2d 7422	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) = (𝑘↑0))
132	90	nncnd 12225	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ ℂ)
133	132	exp0d 14102	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑0) = 1)
134	131, 133	eqtrd 2773	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) = 1)
135	134	fveq2d 6893	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = (log‘1))
136		log1 26086	. . . . . . 7 ⊢ (log‘1) = 0
137	135, 136	eqtrdi 2789	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = 0)
138		fzfid 13935	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (1...((2 · 𝑁)C𝑁)) ∈ Fin)
139		inss1 4228	. . . . . . 7 ⊢ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ⊆ (1...((2 · 𝑁)C𝑁))
140		ssfi 9170	. . . . . . 7 ⊢ (((1...((2 · 𝑁)C𝑁)) ∈ Fin ∧ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ⊆ (1...((2 · 𝑁)C𝑁))) → ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∈ Fin)
141	138, 139, 140	sylancl 587	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∈ Fin)
142	57, 84, 137, 141	fsumss 15668	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))))
143	62	nnrpd 13011	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ℝ⁺)
144	65	nn0zd 12581	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ)
145		relogexp 26096	. . . . . . 7 ⊢ ((𝑘 ∈ ℝ⁺ ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = ((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘)))
146	143, 144, 145	syl2anc 585	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = ((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘)))
147	146	sumeq2dv 15646	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘)))
148		pclogsum 26708	. . . . . 6 ⊢ (((2 · 𝑁)C𝑁) ∈ ℕ → Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘)) = (log‘((2 · 𝑁)C𝑁)))
149	14, 148	syl 17	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘)) = (log‘((2 · 𝑁)C𝑁)))
150	142, 147, 149	3eqtrd 2777	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = (log‘((2 · 𝑁)C𝑁)))
151	29	recnd 11239	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘(2 · 𝑁)) ∈ ℂ)
152		fsumconst 15733	. . . . . 6 ⊢ ((((1...𝐾) ∩ ℙ) ∈ Fin ∧ (log‘(2 · 𝑁)) ∈ ℂ) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)) = ((♯‘((1...𝐾) ∩ ℙ)) · (log‘(2 · 𝑁))))
153	46, 151, 152	syl2anc 585	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)) = ((♯‘((1...𝐾) ∩ ℙ)) · (log‘(2 · 𝑁))))
154		2eluzge1 12875	. . . . . . 7 ⊢ 2 ∈ (ℤ_≥‘1)
155		ppival2g 26623	. . . . . . 7 ⊢ ((𝐾 ∈ ℤ ∧ 2 ∈ (ℤ_≥‘1)) → (π‘𝐾) = (♯‘((1...𝐾) ∩ ℙ)))
156	47, 154, 155	sylancl 587	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (π‘𝐾) = (♯‘((1...𝐾) ∩ ℙ)))
157	156	oveq1d 7421	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) = ((♯‘((1...𝐾) ∩ ℙ)) · (log‘(2 · 𝑁))))
158	153, 157	eqtr4d 2776	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)) = ((π‘𝐾) · (log‘(2 · 𝑁))))
159	82, 150, 158	3brtr3d 5179	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘((2 · 𝑁)C𝑁)) ≤ ((π‘𝐾) · (log‘(2 · 𝑁))))
160		min1 13165	. . . . . . 7 ⊢ (((2 · 𝑁) ∈ ℝ ∧ ((2 · 𝑁)C𝑁) ∈ ℝ) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ (2 · 𝑁))
161	21, 49, 160	syl2anc 585	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ (2 · 𝑁))
162	35, 161	eqbrtrid 5183	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝐾 ≤ (2 · 𝑁))
163		ppiwordi 26656	. . . . 5 ⊢ ((𝐾 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ 𝐾 ≤ (2 · 𝑁)) → (π‘𝐾) ≤ (π‘(2 · 𝑁)))
164	38, 21, 162, 163	syl3anc 1372	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (π‘𝐾) ≤ (π‘(2 · 𝑁)))
165		1red 11212	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 1 ∈ ℝ)
166		2re 12283	. . . . . . . 8 ⊢ 2 ∈ ℝ
167	166	a1i 11	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 2 ∈ ℝ)
168		1lt2 12380	. . . . . . . 8 ⊢ 1 < 2
169	168	a1i 11	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 1 < 2)
170		2t1e2 12372	. . . . . . . 8 ⊢ (2 · 1) = 2
171	3	nnge1d 12257	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 1 ≤ 𝑁)
172		eluzelre 12830	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝑁 ∈ ℝ)
173		2pos 12312	. . . . . . . . . . . 12 ⊢ 0 < 2
174	166, 173	pm3.2i 472	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ ∧ 0 < 2)
175	174	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (2 ∈ ℝ ∧ 0 < 2))
176		lemul2 12064	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
177	165, 172, 175, 176	syl3anc 1372	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
178	171, 177	mpbid 231	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (2 · 1) ≤ (2 · 𝑁))
179	170, 178	eqbrtrrid 5184	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 2 ≤ (2 · 𝑁))
180	165, 167, 21, 169, 179	ltletrd 11371	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 1 < (2 · 𝑁))
181	21, 180	rplogcld 26129	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘(2 · 𝑁)) ∈ ℝ⁺)
182	41, 24, 181	lemul1d 13056	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((π‘𝐾) ≤ (π‘(2 · 𝑁)) ↔ ((π‘𝐾) · (log‘(2 · 𝑁))) ≤ ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁)))))
183	164, 182	mpbid 231	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) ≤ ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁))))
184	16, 42, 30, 159, 183	letrd 11368	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘((2 · 𝑁)C𝑁)) ≤ ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁))))
185	10, 16, 30, 34, 184	ltletrd 11371	1 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘((4↑𝑁) / 𝑁)) < ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 = wceq 1542 ∈ wcel 2107 ∖ cdif 3945 ∩ cin 3947 ⊆ wss 3948 ifcif 4528 class class class wbr 5148 ‘cfv 6541 (class class class)co 7406 Fincfn 8936 ℂcc 11105 ℝcr 11106 0cc0 11107 1c1 11108 · cmul 11112 < clt 11245 ≤ cle 11246 / cdiv 11868 ℕcn 12209 2c2 12264 4c4 12266 ℕ₀cn0 12469 ℤcz 12555 ℤ_≥cuz 12819 ℝ⁺crp 12971 ...cfz 13481 ↑cexp 14024 Ccbc 14259 ♯chash 14287 Σcsu 15629 expce 16002 ℙcprime 16605 pCnt cpc 16766 logclog 26055 πcppi 26588

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-inf2 9633 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185 ax-addf 11186 ax-mulf 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-of 7667 df-om 7853 df-1st 7972 df-2nd 7973 df-supp 8144 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-2o 8464 df-oadd 8467 df-er 8700 df-map 8819 df-pm 8820 df-ixp 8889 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-fsupp 9359 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9502 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-xnn0 12542 df-z 12556 df-dec 12675 df-uz 12820 df-q 12930 df-rp 12972 df-xneg 13089 df-xadd 13090 df-xmul 13091 df-ioo 13325 df-ioc 13326 df-ico 13327 df-icc 13328 df-fz 13482 df-fzo 13625 df-fl 13754 df-mod 13832 df-seq 13964 df-exp 14025 df-fac 14231 df-bc 14260 df-hash 14288 df-shft 15011 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-limsup 15412 df-clim 15429 df-rlim 15430 df-sum 15630 df-ef 16008 df-sin 16010 df-cos 16011 df-pi 16013 df-dvds 16195 df-gcd 16433 df-prm 16606 df-pc 16767 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-mulr 17208 df-starv 17209 df-sca 17210 df-vsca 17211 df-ip 17212 df-tset 17213 df-ple 17214 df-ds 17216 df-unif 17217 df-hom 17218 df-cco 17219 df-rest 17365 df-topn 17366 df-0g 17384 df-gsum 17385 df-topgen 17386 df-pt 17387 df-prds 17390 df-xrs 17445 df-qtop 17450 df-imas 17451 df-xps 17453 df-mre 17527 df-mrc 17528 df-acs 17530 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-submnd 18669 df-mulg 18946 df-cntz 19176 df-cmn 19645 df-psmet 20929 df-xmet 20930 df-met 20931 df-bl 20932 df-mopn 20933 df-fbas 20934 df-fg 20935 df-cnfld 20938 df-top 22388 df-topon 22405 df-topsp 22427 df-bases 22441 df-cld 22515 df-ntr 22516 df-cls 22517 df-nei 22594 df-lp 22632 df-perf 22633 df-cn 22723 df-cnp 22724 df-haus 22811 df-tx 23058 df-hmeo 23251 df-fil 23342 df-fm 23434 df-flim 23435 df-flf 23436 df-xms 23818 df-ms 23819 df-tms 23820 df-cncf 24386 df-limc 25375 df-dv 25376 df-log 26057 df-ppi 26594

This theorem is referenced by: chebbnd1lem3 26964

W3C validator