Theorem chebbnd1lem1 27434

Description: Lemma for chebbnd1 27437: show a lower bound on π(𝑥) at even integers using similar techniques to those used to prove bpos 27258. (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 27249, 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 27245 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 12226	. . . . . 6 ⊢ 4 ∈ ℕ
2		eluznn 12829	. . . . . . . 8 ⊢ ((4 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘4)) → 𝑁 ∈ ℕ)
3	1, 2	mpan 690	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘4) → 𝑁 ∈ ℕ)
4	3	nnnn0d 12460	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘4) → 𝑁 ∈ ℕ0)
5		nnexpcl 13995	. . . . . 6 ⊢ ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (4↑𝑁) ∈ ℕ)
6	1, 4, 5	sylancr 587	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘4) → (4↑𝑁) ∈ ℕ)
7	6	nnrpd 12945	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘4) → (4↑𝑁) ∈ ℝ+)
8	3	nnrpd 12945	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘4) → 𝑁 ∈ ℝ+)
9	7, 8	rpdivcld 12964	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((4↑𝑁) / 𝑁) ∈ ℝ+)
10	9	relogcld 26586	. 2 ⊢ (𝑁 ∈ (ℤ≥‘4) → (log‘((4↑𝑁) / 𝑁)) ∈ ℝ)
11		fzctr 13554	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0...(2 · 𝑁)))
12	4, 11	syl 17	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘4) → 𝑁 ∈ (0...(2 · 𝑁)))
13		bccl2 14244	. . . . 5 ⊢ (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
14	12, 13	syl 17	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℕ)
15	14	nnrpd 12945	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℝ+)
16	15	relogcld 26586	. 2 ⊢ (𝑁 ∈ (ℤ≥‘4) → (log‘((2 · 𝑁)C𝑁)) ∈ ℝ)
17		2z 12521	. . . . . . 7 ⊢ 2 ∈ ℤ
18		eluzelz 12759	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘4) → 𝑁 ∈ ℤ)
19		zmulcl 12538	. . . . . . 7 ⊢ ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 · 𝑁) ∈ ℤ)
20	17, 18, 19	sylancr 587	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘4) → (2 · 𝑁) ∈ ℤ)
21	20	zred 12594	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘4) → (2 · 𝑁) ∈ ℝ)
22		ppicl 27095	. . . . 5 ⊢ ((2 · 𝑁) ∈ ℝ → (π‘(2 · 𝑁)) ∈ ℕ0)
23	21, 22	syl 17	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘4) → (π‘(2 · 𝑁)) ∈ ℕ0)
24	23	nn0red 12461	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘4) → (π‘(2 · 𝑁)) ∈ ℝ)
25		2nn 12216	. . . . . 6 ⊢ 2 ∈ ℕ
26		nnmulcl 12167	. . . . . 6 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
27	25, 3, 26	sylancr 587	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘4) → (2 · 𝑁) ∈ ℕ)
28	27	nnrpd 12945	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘4) → (2 · 𝑁) ∈ ℝ+)
29	28	relogcld 26586	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘4) → (log‘(2 · 𝑁)) ∈ ℝ)
30	24, 29	remulcld 11160	. 2 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁))) ∈ ℝ)
31		bclbnd 27245	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
32		logltb 26563	. . . 4 ⊢ ((((4↑𝑁) / 𝑁) ∈ ℝ+ ∧ ((2 · 𝑁)C𝑁) ∈ ℝ+) → (((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁) ↔ (log‘((4↑𝑁) / 𝑁)) < (log‘((2 · 𝑁)C𝑁))))
33	9, 15, 32	syl2anc 584	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘4) → (((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁) ↔ (log‘((4↑𝑁) / 𝑁)) < (log‘((2 · 𝑁)C𝑁))))
34	31, 33	mpbid 232	. 2 ⊢ (𝑁 ∈ (ℤ≥‘4) → (log‘((4↑𝑁) / 𝑁)) < (log‘((2 · 𝑁)C𝑁)))
35		chebbnd1lem1.1	. . . . . . . 8 ⊢ 𝐾 = if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁))
36	27, 14	ifcld 4524	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ≥‘4) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ∈ ℕ)
37	35, 36	eqeltrid 2838	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘4) → 𝐾 ∈ ℕ)
38	37	nnred 12158	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘4) → 𝐾 ∈ ℝ)
39		ppicl 27095	. . . . . 6 ⊢ (𝐾 ∈ ℝ → (π‘𝐾) ∈ ℕ0)
40	38, 39	syl 17	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘4) → (π‘𝐾) ∈ ℕ0)
41	40	nn0red 12461	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘4) → (π‘𝐾) ∈ ℝ)
42	41, 29	remulcld 11160	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) ∈ ℝ)
43		fzfid 13894	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘4) → (1...𝐾) ∈ Fin)
44		inss1 4187	. . . . . 6 ⊢ ((1...𝐾) ∩ ℙ) ⊆ (1...𝐾)
45		ssfi 9095	. . . . . 6 ⊢ (((1...𝐾) ∈ Fin ∧ ((1...𝐾) ∩ ℙ) ⊆ (1...𝐾)) → ((1...𝐾) ∩ ℙ) ∈ Fin)
46	43, 44, 45	sylancl 586	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((1...𝐾) ∩ ℙ) ∈ Fin)
47	37	nnzd 12512	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ≥‘4) → 𝐾 ∈ ℤ)
48	14	nnzd 12512	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℤ)
49	14	nnred 12158	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℝ)
50		min2 13103	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℝ ∧ ((2 · 𝑁)C𝑁) ∈ ℝ) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ ((2 · 𝑁)C𝑁))
51	21, 49, 50	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ≥‘4) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ ((2 · 𝑁)C𝑁))
52	35, 51	eqbrtrid 5131	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ≥‘4) → 𝐾 ≤ ((2 · 𝑁)C𝑁))
53		eluz2 12755	. . . . . . . . . 10 ⊢ (((2 · 𝑁)C𝑁) ∈ (ℤ≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ ((2 · 𝑁)C𝑁) ∈ ℤ ∧ 𝐾 ≤ ((2 · 𝑁)C𝑁)))
54	47, 48, 52, 53	syl3anbrc 1344	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈ (ℤ≥‘𝐾))
55		fzss2 13478	. . . . . . . . 9 ⊢ (((2 · 𝑁)C𝑁) ∈ (ℤ≥‘𝐾) → (1...𝐾) ⊆ (1...((2 · 𝑁)C𝑁)))
56	54, 55	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ≥‘4) → (1...𝐾) ⊆ (1...((2 · 𝑁)C𝑁)))
57	56	ssrind 4194	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((1...𝐾) ∩ ℙ) ⊆ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ))
58	57	sselda 3931	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ))
59		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ))
60	59	elin1d 4154	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ (1...((2 · 𝑁)C𝑁)))
61		elfznn 13467	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...((2 · 𝑁)C𝑁)) → 𝑘 ∈ ℕ)
62	60, 61	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ℕ)
63	59	elin2d 4155	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ℙ)
64	14	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
65	63, 64	pccld 16776	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
66	62, 65	nnexpcld 14166	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℕ)
67	66	nnrpd 12945	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ+)
68	67	relogcld 26586	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℝ)
69	58, 68	syldan 591	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℝ)
70	29	adantr 480	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(2 · 𝑁)) ∈ ℝ)
71		elinel2 4152	. . . . . . . 8 ⊢ (𝑘 ∈ ((1...𝐾) ∩ ℙ) → 𝑘 ∈ ℙ)
72		bposlem1 27249	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℙ) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
73	3, 71, 72	syl2an 596	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
74	58, 67	syldan 591	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ+)
75	74	reeflogd 26587	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) = (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))
76	28	adantr 480	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (2 · 𝑁) ∈ ℝ+)
77	76	reeflogd 26587	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (exp‘(log‘(2 · 𝑁))) = (2 · 𝑁))
78	73, 75, 77	3brtr4d 5128	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) ≤ (exp‘(log‘(2 · 𝑁))))
79		efle 16041	. . . . . . 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 584	. . . . . 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 15720	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)))
83	68	recnd 11158	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℂ)
84	58, 83	syldan 591	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℂ)
85		eldifn 4082	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) → ¬ 𝑘 ∈ ((1...𝐾) ∩ ℙ))
86	85	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → ¬ 𝑘 ∈ ((1...𝐾) ∩ ℙ))
87		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)))
88	87	eldifad 3911	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ))
89	88	elin1d 4154	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ (1...((2 · 𝑁)C𝑁)))
90	89, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ ℕ)
91	90	adantrr 717	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ℕ)
92	91	nnred 12158	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ℝ)
93	88, 66	syldan 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℕ)
94	93	nnred 12158	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ)
95	94	adantrr 717	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ)
96	21	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (2 · 𝑁) ∈ ℝ)
97	91	nncnd 12159	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ℂ)
98	97	exp1d 14062	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑1) = 𝑘)
99	91	nnge1d 12191	. . . . . . . . . . . . . . . . . . . 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 12788	. . . . . . . . . . . . . . . . . . . . 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 14175	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑1) ≤ (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))
104	98, 103	eqbrtrrd 5120	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))
105	3	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑁 ∈ ℕ)
106	88	elin2d 4155	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ ℙ)
107	106	adantrr 717	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ℙ)
108	105, 107, 72	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
109	92, 95, 96, 104, 108	letrd 11288	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ (2 · 𝑁))
110		elfzle2 13442	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...((2 · 𝑁)C𝑁)) → 𝑘 ≤ ((2 · 𝑁)C𝑁))
111	89, 110	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ≤ ((2 · 𝑁)C𝑁))
112	111	adantrr 717	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ ((2 · 𝑁)C𝑁))
113	49	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → ((2 · 𝑁)C𝑁) ∈ ℝ)
114		lemin 13105	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ ((2 · 𝑁)C𝑁) ∈ ℝ) → (𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ↔ (𝑘 ≤ (2 · 𝑁) ∧ 𝑘 ≤ ((2 · 𝑁)C𝑁))))
115	92, 96, 113, 114	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ↔ (𝑘 ≤ (2 · 𝑁) ∧ 𝑘 ≤ ((2 · 𝑁)C𝑁))))
116	109, 112, 115	mpbir2and 713	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)))
117	116, 35	breqtrrdi 5138	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ 𝐾)
118	37	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝐾 ∈ ℕ)
119	118	nnzd 12512	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝐾 ∈ ℤ)
120		fznn 13506	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ ℤ → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ 𝐾)))
121	119, 120	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ 𝐾)))
122	91, 117, 121	mpbir2and 713	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ (1...𝐾))
123	122, 107	elind 4150	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ((1...𝐾) ∩ ℙ))
124	123	expr 456	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → ((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ → 𝑘 ∈ ((1...𝐾) ∩ ℙ)))
125	86, 124	mtod 198	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → ¬ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)
126	88, 65	syldan 591	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0)
127		elnn0 12401	. . . . . . . . . . . . 13 ⊢ ((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0 ↔ ((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ ∨ (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0))
128	126, 127	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → ((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ ∨ (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0))
129	128	ord 864	. . . . . . . . . . 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 7372	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) = (𝑘↑0))
132	90	nncnd 12159	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ ℂ)
133	132	exp0d 14061	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑0) = 1)
134	131, 133	eqtrd 2769	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) = 1)
135	134	fveq2d 6836	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = (log‘1))
136		log1 26548	. . . . . . 7 ⊢ (log‘1) = 0
137	135, 136	eqtrdi 2785	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = 0)
138		fzfid 13894	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘4) → (1...((2 · 𝑁)C𝑁)) ∈ Fin)
139		inss1 4187	. . . . . . 7 ⊢ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ⊆ (1...((2 · 𝑁)C𝑁))
140		ssfi 9095	. . . . . . 7 ⊢ (((1...((2 · 𝑁)C𝑁)) ∈ Fin ∧ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ⊆ (1...((2 · 𝑁)C𝑁))) → ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∈ Fin)
141	138, 139, 140	sylancl 586	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∈ Fin)
142	57, 84, 137, 141	fsumss 15646	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))))
143	62	nnrpd 12945	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ℝ+)
144	65	nn0zd 12511	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ)
145		relogexp 26559	. . . . . . 7 ⊢ ((𝑘 ∈ ℝ+ ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = ((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘)))
146	143, 144, 145	syl2anc 584	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = ((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘)))
147	146	sumeq2dv 15623	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘4) → Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘)))
148		pclogsum 27180	. . . . . 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 2773	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = (log‘((2 · 𝑁)C𝑁)))
151	29	recnd 11158	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘4) → (log‘(2 · 𝑁)) ∈ ℂ)
152		fsumconst 15711	. . . . . 6 ⊢ ((((1...𝐾) ∩ ℙ) ∈ Fin ∧ (log‘(2 · 𝑁)) ∈ ℂ) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)) = ((♯‘((1...𝐾) ∩ ℙ)) · (log‘(2 · 𝑁))))
153	46, 151, 152	syl2anc 584	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)) = ((♯‘((1...𝐾) ∩ ℙ)) · (log‘(2 · 𝑁))))
154		2eluzge1 12793	. . . . . . 7 ⊢ 2 ∈ (ℤ≥‘1)
155		ppival2g 27093	. . . . . . 7 ⊢ ((𝐾 ∈ ℤ ∧ 2 ∈ (ℤ≥‘1)) → (π‘𝐾) = (♯‘((1...𝐾) ∩ ℙ)))
156	47, 154, 155	sylancl 586	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘4) → (π‘𝐾) = (♯‘((1...𝐾) ∩ ℙ)))
157	156	oveq1d 7371	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) = ((♯‘((1...𝐾) ∩ ℙ)) · (log‘(2 · 𝑁))))
158	153, 157	eqtr4d 2772	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)) = ((π‘𝐾) · (log‘(2 · 𝑁))))
159	82, 150, 158	3brtr3d 5127	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘4) → (log‘((2 · 𝑁)C𝑁)) ≤ ((π‘𝐾) · (log‘(2 · 𝑁))))
160		min1 13102	. . . . . . 7 ⊢ (((2 · 𝑁) ∈ ℝ ∧ ((2 · 𝑁)C𝑁) ∈ ℝ) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ (2 · 𝑁))
161	21, 49, 160	syl2anc 584	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘4) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ (2 · 𝑁))
162	35, 161	eqbrtrid 5131	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘4) → 𝐾 ≤ (2 · 𝑁))
163		ppiwordi 27126	. . . . 5 ⊢ ((𝐾 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ 𝐾 ≤ (2 · 𝑁)) → (π‘𝐾) ≤ (π‘(2 · 𝑁)))
164	38, 21, 162, 163	syl3anc 1373	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘4) → (π‘𝐾) ≤ (π‘(2 · 𝑁)))
165		1red 11131	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘4) → 1 ∈ ℝ)
166		2re 12217	. . . . . . . 8 ⊢ 2 ∈ ℝ
167	166	a1i 11	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘4) → 2 ∈ ℝ)
168		1lt2 12309	. . . . . . . 8 ⊢ 1 < 2
169	168	a1i 11	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘4) → 1 < 2)
170		2t1e2 12301	. . . . . . . 8 ⊢ (2 · 1) = 2
171	3	nnge1d 12191	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ≥‘4) → 1 ≤ 𝑁)
172		eluzelre 12760	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ≥‘4) → 𝑁 ∈ ℝ)
173		2pos 12246	. . . . . . . . . . . 12 ⊢ 0 < 2
174	166, 173	pm3.2i 470	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ ∧ 0 < 2)
175	174	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ≥‘4) → (2 ∈ ℝ ∧ 0 < 2))
176		lemul2 11992	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
177	165, 172, 175, 176	syl3anc 1373	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ≥‘4) → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
178	171, 177	mpbid 232	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ≥‘4) → (2 · 1) ≤ (2 · 𝑁))
179	170, 178	eqbrtrrid 5132	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘4) → 2 ≤ (2 · 𝑁))
180	165, 167, 21, 169, 179	ltletrd 11291	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘4) → 1 < (2 · 𝑁))
181	21, 180	rplogcld 26592	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘4) → (log‘(2 · 𝑁)) ∈ ℝ+)
182	41, 24, 181	lemul1d 12990	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((π‘𝐾) ≤ (π‘(2 · 𝑁)) ↔ ((π‘𝐾) · (log‘(2 · 𝑁))) ≤ ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁)))))
183	164, 182	mpbid 232	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) ≤ ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁))))
184	16, 42, 30, 159, 183	letrd 11288	. 2 ⊢ (𝑁 ∈ (ℤ≥‘4) → (log‘((2 · 𝑁)C𝑁)) ≤ ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁))))
185	10, 16, 30, 34, 184	ltletrd 11291	1 ⊢ (𝑁 ∈ (ℤ≥‘4) → (log‘((4↑𝑁) / 𝑁)) < ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113   ∖ cdif 3896   ∩ cin 3898   ⊆ wss 3899  ifcif 4477   class class class wbr 5096  ‘cfv 6490  (class class class)co 7356  Fincfn 8881  ℂcc 11022  ℝcr 11023  0cc0 11024  1c1 11025   · cmul 11029   < clt 11164   ≤ cle 11165   / cdiv 11792  ℕcn 12143  2c2 12198  4c4 12200  ℕ₀cn0 12399  ℤcz 12486  ℤ_≥cuz 12749  ℝ⁺crp 12903  ...cfz 13421  ↑cexp 13982  Ccbc 14223  ♯chash 14251  Σcsu 15607  expce 15982  ℙcprime 16596   pCnt cpc 16762  logclog 26517  πcppi 27058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-inf2 9548  ax-cnex 11080  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101  ax-pre-sup 11102  ax-addf 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-tp 4583  df-op 4585  df-uni 4862  df-int 4901  df-iun 4946  df-iin 4947  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-se 5576  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-isom 6499  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-of 7620  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-oadd 8399  df-er 8633  df-map 8763  df-pm 8764  df-ixp 8834  df-en 8882  df-dom 8883  df-sdom 8884  df-fin 8885  df-fsupp 9263  df-fi 9312  df-sup 9343  df-inf 9344  df-oi 9413  df-card 9849  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-div 11793  df-nn 12144  df-2 12206  df-3 12207  df-4 12208  df-5 12209  df-6 12210  df-7 12211  df-8 12212  df-9 12213  df-n0 12400  df-xnn0 12473  df-z 12487  df-dec 12606  df-uz 12750  df-q 12860  df-rp 12904  df-xneg 13024  df-xadd 13025  df-xmul 13026  df-ioo 13263  df-ioc 13264  df-ico 13265  df-icc 13266  df-fz 13422  df-fzo 13569  df-fl 13710  df-mod 13788  df-seq 13923  df-exp 13983  df-fac 14195  df-bc 14224  df-hash 14252  df-shft 14988  df-cj 15020  df-re 15021  df-im 15022  df-sqrt 15156  df-abs 15157  df-limsup 15392  df-clim 15409  df-rlim 15410  df-sum 15608  df-ef 15988  df-sin 15990  df-cos 15991  df-pi 15993  df-dvds 16178  df-gcd 16420  df-prm 16597  df-pc 16763  df-struct 17072  df-sets 17089  df-slot 17107  df-ndx 17119  df-base 17135  df-ress 17156  df-plusg 17188  df-mulr 17189  df-starv 17190  df-sca 17191  df-vsca 17192  df-ip 17193  df-tset 17194  df-ple 17195  df-ds 17197  df-unif 17198  df-hom 17199  df-cco 17200  df-rest 17340  df-topn 17341  df-0g 17359  df-gsum 17360  df-topgen 17361  df-pt 17362  df-prds 17365  df-xrs 17421  df-qtop 17426  df-imas 17427  df-xps 17429  df-mre 17503  df-mrc 17504  df-acs 17506  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-submnd 18707  df-mulg 18996  df-cntz 19244  df-cmn 19709  df-psmet 21299  df-xmet 21300  df-met 21301  df-bl 21302  df-mopn 21303  df-fbas 21304  df-fg 21305  df-cnfld 21308  df-top 22836  df-topon 22853  df-topsp 22875  df-bases 22888  df-cld 22961  df-ntr 22962  df-cls 22963  df-nei 23040  df-lp 23078  df-perf 23079  df-cn 23169  df-cnp 23170  df-haus 23257  df-tx 23504  df-hmeo 23697  df-fil 23788  df-fm 23880  df-flim 23881  df-flf 23882  df-xms 24262  df-ms 24263  df-tms 24264  df-cncf 24825  df-limc 25821  df-dv 25822  df-log 26519  df-ppi 27064

This theorem is referenced by:  chebbnd1lem3  27436