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 26979

Description: Lemma for chebbnd1 26982: show a lower bound on π(𝑥) at even integers using similar techniques to those used to prove bpos 26803. (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 26794, 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 26790 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 12297	. . . . . 6 ⊢ 4 ∈ ℕ
2		eluznn 12904	. . . . . . . 8 ⊢ ((4 ∈ ℕ ∧ 𝑁 ∈ (ℤ_≥‘4)) → 𝑁 ∈ ℕ)
3	1, 2	mpan 688	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝑁 ∈ ℕ)
4	3	nnnn0d 12534	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝑁 ∈ ℕ₀)
5		nnexpcl 14042	. . . . . 6 ⊢ ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (4↑𝑁) ∈ ℕ)
6	1, 4, 5	sylancr 587	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (4↑𝑁) ∈ ℕ)
7	6	nnrpd 13016	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (4↑𝑁) ∈ ℝ⁺)
8	3	nnrpd 13016	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝑁 ∈ ℝ⁺)
9	7, 8	rpdivcld 13035	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((4↑𝑁) / 𝑁) ∈ ℝ⁺)
10	9	relogcld 26138	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘((4↑𝑁) / 𝑁)) ∈ ℝ)
11		fzctr 13615	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ (0...(2 · 𝑁)))
12	4, 11	syl 17	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝑁 ∈ (0...(2 · 𝑁)))
13		bccl2 14285	. . . . 5 ⊢ (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
14	12, 13	syl 17	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℕ)
15	14	nnrpd 13016	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℝ⁺)
16	15	relogcld 26138	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘((2 · 𝑁)C𝑁)) ∈ ℝ)
17		2z 12596	. . . . . . 7 ⊢ 2 ∈ ℤ
18		eluzelz 12834	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝑁 ∈ ℤ)
19		zmulcl 12613	. . . . . . 7 ⊢ ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 · 𝑁) ∈ ℤ)
20	17, 18, 19	sylancr 587	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (2 · 𝑁) ∈ ℤ)
21	20	zred 12668	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (2 · 𝑁) ∈ ℝ)
22		ppicl 26642	. . . . 5 ⊢ ((2 · 𝑁) ∈ ℝ → (π‘(2 · 𝑁)) ∈ ℕ₀)
23	21, 22	syl 17	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (π‘(2 · 𝑁)) ∈ ℕ₀)
24	23	nn0red 12535	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (π‘(2 · 𝑁)) ∈ ℝ)
25		2nn 12287	. . . . . 6 ⊢ 2 ∈ ℕ
26		nnmulcl 12238	. . . . . 6 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
27	25, 3, 26	sylancr 587	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (2 · 𝑁) ∈ ℕ)
28	27	nnrpd 13016	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (2 · 𝑁) ∈ ℝ⁺)
29	28	relogcld 26138	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘(2 · 𝑁)) ∈ ℝ)
30	24, 29	remulcld 11246	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁))) ∈ ℝ)
31		bclbnd 26790	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
32		logltb 26115	. . . 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 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 2837	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝐾 ∈ ℕ)
38	37	nnred 12229	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝐾 ∈ ℝ)
39		ppicl 26642	. . . . . 6 ⊢ (𝐾 ∈ ℝ → (π‘𝐾) ∈ ℕ₀)
40	38, 39	syl 17	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (π‘𝐾) ∈ ℕ₀)
41	40	nn0red 12535	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (π‘𝐾) ∈ ℝ)
42	41, 29	remulcld 11246	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) ∈ ℝ)
43		fzfid 13940	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (1...𝐾) ∈ Fin)
44		inss1 4228	. . . . . 6 ⊢ ((1...𝐾) ∩ ℙ) ⊆ (1...𝐾)
45		ssfi 9175	. . . . . 6 ⊢ (((1...𝐾) ∈ Fin ∧ ((1...𝐾) ∩ ℙ) ⊆ (1...𝐾)) → ((1...𝐾) ∩ ℙ) ∈ Fin)
46	43, 44, 45	sylancl 586	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((1...𝐾) ∩ ℙ) ∈ Fin)
47	37	nnzd 12587	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝐾 ∈ ℤ)
48	14	nnzd 12587	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℤ)
49	14	nnred 12229	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℝ)
50		min2 13171	. . . . . . . . . . . 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 5183	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝐾 ≤ ((2 · 𝑁)C𝑁))
53		eluz2 12830	. . . . . . . . . 10 ⊢ (((2 · 𝑁)C𝑁) ∈ (ℤ_≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ ((2 · 𝑁)C𝑁) ∈ ℤ ∧ 𝐾 ≤ ((2 · 𝑁)C𝑁)))
54	47, 48, 52, 53	syl3anbrc 1343	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((2 · 𝑁)C𝑁) ∈ (ℤ_≥‘𝐾))
55		fzss2 13543	. . . . . . . . 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 485	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ))
60	59	elin1d 4198	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ (1...((2 · 𝑁)C𝑁)))
61		elfznn 13532	. . . . . . . . . 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 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
65	63, 64	pccld 16785	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
66	62, 65	nnexpcld 14210	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℕ)
67	66	nnrpd 13016	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ⁺)
68	67	relogcld 26138	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℝ)
69	58, 68	syldan 591	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℝ)
70	29	adantr 481	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(2 · 𝑁)) ∈ ℝ)
71		elinel2 4196	. . . . . . . 8 ⊢ (𝑘 ∈ ((1...𝐾) ∩ ℙ) → 𝑘 ∈ ℙ)
72		bposlem1 26794	. . . . . . . 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 26139	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) = (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))
76	28	adantr 481	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (2 · 𝑁) ∈ ℝ⁺)
77	76	reeflogd 26139	. . . . . . 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 16063	. . . . . . 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 256	. . . . 5 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ (log‘(2 · 𝑁)))
82	46, 69, 70, 81	fsumle 15747	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)))
83	68	recnd 11244	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℂ)
84	58, 83	syldan 591	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℂ)
85		eldifn 4127	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) → ¬ 𝑘 ∈ ((1...𝐾) ∩ ℙ))
86	85	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → ¬ 𝑘 ∈ ((1...𝐾) ∩ ℙ))
87		simpr 485	. . . . . . . . . . . . . . . . . . 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 715	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ℕ)
92	91	nnred 12229	. . . . . . . . . . . . . . . . . 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 12229	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ)
95	94	adantrr 715	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ)
96	21	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (2 · 𝑁) ∈ ℝ)
97	91	nncnd 12230	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ℂ)
98	97	exp1d 14108	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑1) = 𝑘)
99	91	nnge1d 12262	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 1 ≤ 𝑘)
100		simprr 771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)
101		nnuz 12867	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ = (ℤ_≥‘1)
102	100, 101	eleqtrdi 2843	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ (ℤ_≥‘1))
103	92, 99, 102	leexp2ad 14219	. . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑁 ∈ ℕ)
106	88	elin2d 4199	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ ℙ)
107	106	adantrr 715	. . . . . . . . . . . . . . . . . . 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 11373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ (2 · 𝑁))
110		elfzle2 13507	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...((2 · 𝑁)C𝑁)) → 𝑘 ≤ ((2 · 𝑁)C𝑁))
111	89, 110	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ≤ ((2 · 𝑁)C𝑁))
112	111	adantrr 715	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ ((2 · 𝑁)C𝑁))
113	49	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → ((2 · 𝑁)C𝑁) ∈ ℝ)
114		lemin 13173	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ ((2 · 𝑁)C𝑁) ∈ ℝ) → (𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ↔ (𝑘 ≤ (2 · 𝑁) ∧ 𝑘 ≤ ((2 · 𝑁)C𝑁))))
115	92, 96, 113, 114	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ↔ (𝑘 ≤ (2 · 𝑁) ∧ 𝑘 ≤ ((2 · 𝑁)C𝑁))))
116	109, 112, 115	mpbir2and 711	. . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝐾 ∈ ℕ)
119	118	nnzd 12587	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝐾 ∈ ℤ)
120		fznn 13571	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ ℤ → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ 𝐾)))
121	119, 120	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ 𝐾)))
122	91, 117, 121	mpbir2and 711	. . . . . . . . . . . . . 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 457	. . . . . . . . . . . 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 591	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
127		elnn0 12476	. . . . . . . . . . . . 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 862	. . . . . . . . . . 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 7427	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) = (𝑘↑0))
132	90	nncnd 12230	. . . . . . . . . 10 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ ℂ)
133	132	exp0d 14107	. . . . . . . . 9 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑0) = 1)
134	131, 133	eqtrd 2772	. . . . . . . 8 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) = 1)
135	134	fveq2d 6895	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = (log‘1))
136		log1 26101	. . . . . . 7 ⊢ (log‘1) = 0
137	135, 136	eqtrdi 2788	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = 0)
138		fzfid 13940	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (1...((2 · 𝑁)C𝑁)) ∈ Fin)
139		inss1 4228	. . . . . . 7 ⊢ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ⊆ (1...((2 · 𝑁)C𝑁))
140		ssfi 9175	. . . . . . 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 15673	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))))
143	62	nnrpd 13016	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ℝ⁺)
144	65	nn0zd 12586	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ_≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ)
145		relogexp 26111	. . . . . . 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 15651	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘)))
148		pclogsum 26725	. . . . . 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 2776	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = (log‘((2 · 𝑁)C𝑁)))
151	29	recnd 11244	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘(2 · 𝑁)) ∈ ℂ)
152		fsumconst 15738	. . . . . 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 12880	. . . . . . 7 ⊢ 2 ∈ (ℤ_≥‘1)
155		ppival2g 26640	. . . . . . 7 ⊢ ((𝐾 ∈ ℤ ∧ 2 ∈ (ℤ_≥‘1)) → (π‘𝐾) = (♯‘((1...𝐾) ∩ ℙ)))
156	47, 154, 155	sylancl 586	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (π‘𝐾) = (♯‘((1...𝐾) ∩ ℙ)))
157	156	oveq1d 7426	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) = ((♯‘((1...𝐾) ∩ ℙ)) · (log‘(2 · 𝑁))))
158	153, 157	eqtr4d 2775	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)) = ((π‘𝐾) · (log‘(2 · 𝑁))))
159	82, 150, 158	3brtr3d 5179	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘((2 · 𝑁)C𝑁)) ≤ ((π‘𝐾) · (log‘(2 · 𝑁))))
160		min1 13170	. . . . . . 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 5183	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝐾 ≤ (2 · 𝑁))
163		ppiwordi 26673	. . . . 5 ⊢ ((𝐾 ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ 𝐾 ≤ (2 · 𝑁)) → (π‘𝐾) ≤ (π‘(2 · 𝑁)))
164	38, 21, 162, 163	syl3anc 1371	. . . 4 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (π‘𝐾) ≤ (π‘(2 · 𝑁)))
165		1red 11217	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 1 ∈ ℝ)
166		2re 12288	. . . . . . . 8 ⊢ 2 ∈ ℝ
167	166	a1i 11	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 2 ∈ ℝ)
168		1lt2 12385	. . . . . . . 8 ⊢ 1 < 2
169	168	a1i 11	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 1 < 2)
170		2t1e2 12377	. . . . . . . 8 ⊢ (2 · 1) = 2
171	3	nnge1d 12262	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 1 ≤ 𝑁)
172		eluzelre 12835	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 𝑁 ∈ ℝ)
173		2pos 12317	. . . . . . . . . . . 12 ⊢ 0 < 2
174	166, 173	pm3.2i 471	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ ∧ 0 < 2)
175	174	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (2 ∈ ℝ ∧ 0 < 2))
176		lemul2 12069	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 · 𝑁)))
177	165, 172, 175, 176	syl3anc 1371	. . . . . . . . 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 11376	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘4) → 1 < (2 · 𝑁))
181	21, 180	rplogcld 26144	. . . . 5 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘(2 · 𝑁)) ∈ ℝ⁺)
182	41, 24, 181	lemul1d 13061	. . . 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 11373	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘((2 · 𝑁)C𝑁)) ≤ ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁))))
185	10, 16, 30, 34, 184	ltletrd 11376	1 ⊢ (𝑁 ∈ (ℤ_≥‘4) → (log‘((4↑𝑁) / 𝑁)) < ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 = wceq 1541 ∈ wcel 2106 ∖ cdif 3945 ∩ cin 3947 ⊆ wss 3948 ifcif 4528 class class class wbr 5148 ‘cfv 6543 (class class class)co 7411 Fincfn 8941 ℂcc 11110 ℝcr 11111 0cc0 11112 1c1 11113 · cmul 11117 < clt 11250 ≤ cle 11251 / cdiv 11873 ℕcn 12214 2c2 12269 4c4 12271 ℕ₀cn0 12474 ℤcz 12560 ℤ_≥cuz 12824 ℝ⁺crp 12976 ...cfz 13486 ↑cexp 14029 Ccbc 14264 ♯chash 14292 Σcsu 15634 expce 16007 ℙcprime 16610 pCnt cpc 16771 logclog 26070 πcppi 26605

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7727 ax-inf2 9638 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190 ax-addf 11191 ax-mulf 11192

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 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 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7672 df-om 7858 df-1st 7977 df-2nd 7978 df-supp 8149 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-2o 8469 df-oadd 8472 df-er 8705 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-fi 9408 df-sup 9439 df-inf 9440 df-oi 9507 df-card 9936 df-pnf 11252 df-mnf 11253 df-xr 11254 df-ltxr 11255 df-le 11256 df-sub 11448 df-neg 11449 df-div 11874 df-nn 12215 df-2 12277 df-3 12278 df-4 12279 df-5 12280 df-6 12281 df-7 12282 df-8 12283 df-9 12284 df-n0 12475 df-xnn0 12547 df-z 12561 df-dec 12680 df-uz 12825 df-q 12935 df-rp 12977 df-xneg 13094 df-xadd 13095 df-xmul 13096 df-ioo 13330 df-ioc 13331 df-ico 13332 df-icc 13333 df-fz 13487 df-fzo 13630 df-fl 13759 df-mod 13837 df-seq 13969 df-exp 14030 df-fac 14236 df-bc 14265 df-hash 14293 df-shft 15016 df-cj 15048 df-re 15049 df-im 15050 df-sqrt 15184 df-abs 15185 df-limsup 15417 df-clim 15434 df-rlim 15435 df-sum 15635 df-ef 16013 df-sin 16015 df-cos 16016 df-pi 16018 df-dvds 16200 df-gcd 16438 df-prm 16611 df-pc 16772 df-struct 17082 df-sets 17099 df-slot 17117 df-ndx 17129 df-base 17147 df-ress 17176 df-plusg 17212 df-mulr 17213 df-starv 17214 df-sca 17215 df-vsca 17216 df-ip 17217 df-tset 17218 df-ple 17219 df-ds 17221 df-unif 17222 df-hom 17223 df-cco 17224 df-rest 17370 df-topn 17371 df-0g 17389 df-gsum 17390 df-topgen 17391 df-pt 17392 df-prds 17395 df-xrs 17450 df-qtop 17455 df-imas 17456 df-xps 17458 df-mre 17532 df-mrc 17533 df-acs 17535 df-mgm 18563 df-sgrp 18612 df-mnd 18628 df-submnd 18674 df-mulg 18953 df-cntz 19183 df-cmn 19652 df-psmet 20942 df-xmet 20943 df-met 20944 df-bl 20945 df-mopn 20946 df-fbas 20947 df-fg 20948 df-cnfld 20951 df-top 22403 df-topon 22420 df-topsp 22442 df-bases 22456 df-cld 22530 df-ntr 22531 df-cls 22532 df-nei 22609 df-lp 22647 df-perf 22648 df-cn 22738 df-cnp 22739 df-haus 22826 df-tx 23073 df-hmeo 23266 df-fil 23357 df-fm 23449 df-flim 23450 df-flf 23451 df-xms 23833 df-ms 23834 df-tms 23835 df-cncf 24401 df-limc 25390 df-dv 25391 df-log 26072 df-ppi 26611

This theorem is referenced by: chebbnd1lem3 26981

W3C validator