Theorem chebbnd1lem3

Description: Lemma for chebbnd1 : get a lower bound on ppi ( N ) / ( N / log ( N ) ) that is independent of N . (Contributed by Mario Carneiro, 21-Sep-2014)

	Ref	Expression
Hypothesis	chebbnd1lem2.1	⊢ 𝑀 = ( ⌊ ‘ ( 𝑁 / 2 ) )
Assertion	chebbnd1lem3	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) < ( ( π ‘ 𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		chebbnd1lem2.1	⊢ 𝑀 = ( ⌊ ‘ ( 𝑁 / 2 ) )
2		2rp	⊢ 2 ∈ ℝ+
3		relogcl	⊢ ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
4	2 3	ax-mp	⊢ ( log ‘ 2 ) ∈ ℝ
5		1re	⊢ 1 ∈ ℝ
6		2re	⊢ 2 ∈ ℝ
7		ere	⊢ e ∈ ℝ
8	6 7	remulcli	⊢ ( 2 · e ) ∈ ℝ
9		2pos	⊢ 0 < 2
10		epos	⊢ 0 < e
11	6 7 9 10	mulgt0ii	⊢ 0 < ( 2 · e )
12	8 11	gt0ne0ii	⊢ ( 2 · e ) ≠ 0
13	5 8 12	redivcli	⊢ ( 1 / ( 2 · e ) ) ∈ ℝ
14	4 13	resubcli	⊢ ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ∈ ℝ
15		2ne0	⊢ 2 ≠ 0
16	14 6 15	redivcli	⊢ ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) ∈ ℝ
17	16	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) ∈ ℝ )
18	6	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ∈ ℝ )
19		8re	⊢ 8 ∈ ℝ
20	19	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 8 ∈ ℝ )
21		simpl	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
22		2lt8	⊢ 2 < 8
23	6 19 22	ltleii	⊢ 2 ≤ 8
24	23	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ≤ 8 )
25		simpr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 8 ≤ 𝑁 )
26	18 20 21 24 25	letrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ≤ 𝑁 )
27		ppinncl	⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → ( π ‘ 𝑁 ) ∈ ℕ )
28	26 27	syldan	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π ‘ 𝑁 ) ∈ ℕ )
29	28	nnred	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π ‘ 𝑁 ) ∈ ℝ )
30		rehalfcl	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 / 2 ) ∈ ℝ )
31	30	adantr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑁 / 2 ) ∈ ℝ )
32	31	flcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
33	1 32	eqeltrid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℤ )
34	33	zred	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℝ )
35		remulcl	⊢ ( ( 2 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 2 · 𝑀 ) ∈ ℝ )
36	6 34 35	sylancr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ∈ ℝ )
37	5	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 1 ∈ ℝ )
38		1lt2	⊢ 1 < 2
39	38	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 1 < 2 )
40		2t1e2	⊢ ( 2 · 1 ) = 2
41		4nn	⊢ 4 ∈ ℕ
42		4z	⊢ 4 ∈ ℤ
43	42	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ∈ ℤ )
44		4t2e8	⊢ ( 4 · 2 ) = 8
45	44 25	eqbrtrid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 4 · 2 ) ≤ 𝑁 )
46		4re	⊢ 4 ∈ ℝ
47	46	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ∈ ℝ )
48	9	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 < 2 )
49		lemuldiv	⊢ ( ( 4 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 4 · 2 ) ≤ 𝑁 ↔ 4 ≤ ( 𝑁 / 2 ) ) )
50	47 21 18 48 49	syl112anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 4 · 2 ) ≤ 𝑁 ↔ 4 ≤ ( 𝑁 / 2 ) ) )
51	45 50	mpbid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ≤ ( 𝑁 / 2 ) )
52		flge	⊢ ( ( ( 𝑁 / 2 ) ∈ ℝ ∧ 4 ∈ ℤ ) → ( 4 ≤ ( 𝑁 / 2 ) ↔ 4 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
53	31 42 52	sylancl	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 4 ≤ ( 𝑁 / 2 ) ↔ 4 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
54	51 53	mpbid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) )
55	54 1	breqtrrdi	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ≤ 𝑀 )
56		eluz2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 4 ) ↔ ( 4 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 4 ≤ 𝑀 ) )
57	43 33 55 56	syl3anbrc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ( ℤ≥ ‘ 4 ) )
58		eluznn	⊢ ( ( 4 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 4 ) ) → 𝑀 ∈ ℕ )
59	41 57 58	sylancr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℕ )
60	59	nnge1d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 1 ≤ 𝑀 )
61		lemul2	⊢ ( ( 1 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 1 ≤ 𝑀 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑀 ) ) )
62	37 34 18 48 61	syl112anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 1 ≤ 𝑀 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑀 ) ) )
63	60 62	mpbid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 1 ) ≤ ( 2 · 𝑀 ) )
64	40 63	eqbrtrrid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ≤ ( 2 · 𝑀 ) )
65	37 18 36 39 64	ltletrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 1 < ( 2 · 𝑀 ) )
66	36 65	rplogcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 2 · 𝑀 ) ) ∈ ℝ+ )
67	66	rpred	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 2 · 𝑀 ) ) ∈ ℝ )
68		2nn	⊢ 2 ∈ ℕ
69		nnmulcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 2 · 𝑀 ) ∈ ℕ )
70	68 59 69	sylancr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ∈ ℕ )
71	67 70	nndivred	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ∈ ℝ )
72	29 71	remulcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ∈ ℝ )
73		rehalfcl	⊢ ( ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ∈ ℝ → ( ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) ∈ ℝ )
74	72 73	syl	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) ∈ ℝ )
75		0red	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 ∈ ℝ )
76		8pos	⊢ 0 < 8
77	76	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 < 8 )
78	75 20 21 77 25	ltletrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 < 𝑁 )
79	21 78	elrpd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑁 ∈ ℝ+ )
80	79	relogcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ 𝑁 ) ∈ ℝ )
81	80 79	rerpdivcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑁 ) / 𝑁 ) ∈ ℝ )
82	29 81	remulcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π ‘ 𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ )
83	14	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ∈ ℝ )
84		ppinncl	⊢ ( ( ( 2 · 𝑀 ) ∈ ℝ ∧ 2 ≤ ( 2 · 𝑀 ) ) → ( π ‘ ( 2 · 𝑀 ) ) ∈ ℕ )
85	36 64 84	syl2anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π ‘ ( 2 · 𝑀 ) ) ∈ ℕ )
86	85	nnred	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π ‘ ( 2 · 𝑀 ) ) ∈ ℝ )
87	86 71	remulcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π ‘ ( 2 · 𝑀 ) ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ∈ ℝ )
88		remulcl	⊢ ( ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ∈ ℝ ∧ ( 2 · 𝑀 ) ∈ ℝ ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) ∈ ℝ )
89	14 36 88	sylancr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) ∈ ℝ )
90		4pos	⊢ 0 < 4
91	46 90	elrpii	⊢ 4 ∈ ℝ+
92		rpexpcl	⊢ ( ( 4 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ) → ( 4 ↑ 𝑀 ) ∈ ℝ+ )
93	91 33 92	sylancr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 4 ↑ 𝑀 ) ∈ ℝ+ )
94	59	nnrpd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℝ+ )
95	93 94	rpdivcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 4 ↑ 𝑀 ) / 𝑀 ) ∈ ℝ+ )
96	95	relogcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( ( 4 ↑ 𝑀 ) / 𝑀 ) ) ∈ ℝ )
97	86 67	remulcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) ∈ ℝ )
98	94	relogcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ 𝑀 ) ∈ ℝ )
99		epr	⊢ e ∈ ℝ+
100		rerpdivcl	⊢ ( ( 𝑀 ∈ ℝ ∧ e ∈ ℝ+ ) → ( 𝑀 / e ) ∈ ℝ )
101	34 99 100	sylancl	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑀 / e ) ∈ ℝ )
102	93	relogcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 4 ↑ 𝑀 ) ) ∈ ℝ )
103	7	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e ∈ ℝ )
104		egt2lt3	⊢ ( 2 < e ∧ e < 3 )
105	104	simpri	⊢ e < 3
106		3lt4	⊢ 3 < 4
107		3re	⊢ 3 ∈ ℝ
108	7 107 46	lttri	⊢ ( ( e < 3 ∧ 3 < 4 ) → e < 4 )
109	105 106 108	mp2an	⊢ e < 4
110	109	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e < 4 )
111	103 47 34 110 55	ltletrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e < 𝑀 )
112	103 34 111	ltled	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e ≤ 𝑀 )
113	7	leidi	⊢ e ≤ e
114		logdivlt	⊢ ( ( ( e ∈ ℝ ∧ e ≤ e ) ∧ ( 𝑀 ∈ ℝ ∧ e ≤ 𝑀 ) ) → ( e < 𝑀 ↔ ( ( log ‘ 𝑀 ) / 𝑀 ) < ( ( log ‘ e ) / e ) ) )
115	7 113 114	mpanl12	⊢ ( ( 𝑀 ∈ ℝ ∧ e ≤ 𝑀 ) → ( e < 𝑀 ↔ ( ( log ‘ 𝑀 ) / 𝑀 ) < ( ( log ‘ e ) / e ) ) )
116	34 112 115	syl2anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( e < 𝑀 ↔ ( ( log ‘ 𝑀 ) / 𝑀 ) < ( ( log ‘ e ) / e ) ) )
117	111 116	mpbid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑀 ) / 𝑀 ) < ( ( log ‘ e ) / e ) )
118		loge	⊢ ( log ‘ e ) = 1
119	118	oveq1i	⊢ ( ( log ‘ e ) / e ) = ( 1 / e )
120	117 119	breqtrdi	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑀 ) / 𝑀 ) < ( 1 / e ) )
121	7 10	pm3.2i	⊢ ( e ∈ ℝ ∧ 0 < e )
122	121	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( e ∈ ℝ ∧ 0 < e ) )
123	59	nngt0d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 < 𝑀 )
124	34 123	jca	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) )
125		lt2mul2div	⊢ ( ( ( ( log ‘ 𝑀 ) ∈ ℝ ∧ ( e ∈ ℝ ∧ 0 < e ) ) ∧ ( 1 ∈ ℝ ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ) ) → ( ( ( log ‘ 𝑀 ) · e ) < ( 1 · 𝑀 ) ↔ ( ( log ‘ 𝑀 ) / 𝑀 ) < ( 1 / e ) ) )
126	98 122 37 124 125	syl22anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 𝑀 ) · e ) < ( 1 · 𝑀 ) ↔ ( ( log ‘ 𝑀 ) / 𝑀 ) < ( 1 / e ) ) )
127	120 126	mpbird	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑀 ) · e ) < ( 1 · 𝑀 ) )
128	34	recnd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℂ )
129	128	mullidd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 1 · 𝑀 ) = 𝑀 )
130	127 129	breqtrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑀 ) · e ) < 𝑀 )
131		ltmuldiv	⊢ ( ( ( log ‘ 𝑀 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( e ∈ ℝ ∧ 0 < e ) ) → ( ( ( log ‘ 𝑀 ) · e ) < 𝑀 ↔ ( log ‘ 𝑀 ) < ( 𝑀 / e ) ) )
132	98 34 122 131	syl3anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 𝑀 ) · e ) < 𝑀 ↔ ( log ‘ 𝑀 ) < ( 𝑀 / e ) ) )
133	130 132	mpbid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ 𝑀 ) < ( 𝑀 / e ) )
134	98 101 102 133	ltsub2dd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 4 ↑ 𝑀 ) ) − ( 𝑀 / e ) ) < ( ( log ‘ ( 4 ↑ 𝑀 ) ) − ( log ‘ 𝑀 ) ) )
135	4	recni	⊢ ( log ‘ 2 ) ∈ ℂ
136	135	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ 2 ) ∈ ℂ )
137	13	recni	⊢ ( 1 / ( 2 · e ) ) ∈ ℂ
138	137	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 1 / ( 2 · e ) ) ∈ ℂ )
139	70	nnrpd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ∈ ℝ+ )
140	139	rpcnd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ∈ ℂ )
141	136 138 140	subdird	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) = ( ( ( log ‘ 2 ) · ( 2 · 𝑀 ) ) − ( ( 1 / ( 2 · e ) ) · ( 2 · 𝑀 ) ) ) )
142	136 140	mulcomd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 2 ) · ( 2 · 𝑀 ) ) = ( ( 2 · 𝑀 ) · ( log ‘ 2 ) ) )
143		2z	⊢ 2 ∈ ℤ
144		zmulcl	⊢ ( ( 2 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 2 · 𝑀 ) ∈ ℤ )
145	143 33 144	sylancr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ∈ ℤ )
146		relogexp	⊢ ( ( 2 ∈ ℝ+ ∧ ( 2 · 𝑀 ) ∈ ℤ ) → ( log ‘ ( 2 ↑ ( 2 · 𝑀 ) ) ) = ( ( 2 · 𝑀 ) · ( log ‘ 2 ) ) )
147	2 145 146	sylancr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 2 ↑ ( 2 · 𝑀 ) ) ) = ( ( 2 · 𝑀 ) · ( log ‘ 2 ) ) )
148		2cnd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ∈ ℂ )
149	59	nnnn0d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℕ0 )
150		2nn0	⊢ 2 ∈ ℕ0
151	150	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ∈ ℕ0 )
152	148 149 151	expmuld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 ↑ ( 2 · 𝑀 ) ) = ( ( 2 ↑ 2 ) ↑ 𝑀 ) )
153		sq2	⊢ ( 2 ↑ 2 ) = 4
154	153	oveq1i	⊢ ( ( 2 ↑ 2 ) ↑ 𝑀 ) = ( 4 ↑ 𝑀 )
155	152 154	eqtrdi	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 ↑ ( 2 · 𝑀 ) ) = ( 4 ↑ 𝑀 ) )
156	155	fveq2d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 2 ↑ ( 2 · 𝑀 ) ) ) = ( log ‘ ( 4 ↑ 𝑀 ) ) )
157	142 147 156	3eqtr2d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 2 ) · ( 2 · 𝑀 ) ) = ( log ‘ ( 4 ↑ 𝑀 ) ) )
158	8	recni	⊢ ( 2 · e ) ∈ ℂ
159	158	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · e ) ∈ ℂ )
160	12	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · e ) ≠ 0 )
161	140 159 160	divrec2d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 2 · 𝑀 ) / ( 2 · e ) ) = ( ( 1 / ( 2 · e ) ) · ( 2 · 𝑀 ) ) )
162	7	recni	⊢ e ∈ ℂ
163	162	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e ∈ ℂ )
164	7 10	gt0ne0ii	⊢ e ≠ 0
165	164	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e ≠ 0 )
166	15	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ≠ 0 )
167	128 163 148 165 166	divcan5d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 2 · 𝑀 ) / ( 2 · e ) ) = ( 𝑀 / e ) )
168	161 167	eqtr3d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 1 / ( 2 · e ) ) · ( 2 · 𝑀 ) ) = ( 𝑀 / e ) )
169	157 168	oveq12d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) · ( 2 · 𝑀 ) ) − ( ( 1 / ( 2 · e ) ) · ( 2 · 𝑀 ) ) ) = ( ( log ‘ ( 4 ↑ 𝑀 ) ) − ( 𝑀 / e ) ) )
170	141 169	eqtrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) = ( ( log ‘ ( 4 ↑ 𝑀 ) ) − ( 𝑀 / e ) ) )
171	93 94	relogdivd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( ( 4 ↑ 𝑀 ) / 𝑀 ) ) = ( ( log ‘ ( 4 ↑ 𝑀 ) ) − ( log ‘ 𝑀 ) ) )
172	134 170 171	3brtr4d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) < ( log ‘ ( ( 4 ↑ 𝑀 ) / 𝑀 ) ) )
173		eqid	⊢ if ( ( 2 · 𝑀 ) ≤ ( ( 2 · 𝑀 ) C 𝑀 ) , ( 2 · 𝑀 ) , ( ( 2 · 𝑀 ) C 𝑀 ) ) = if ( ( 2 · 𝑀 ) ≤ ( ( 2 · 𝑀 ) C 𝑀 ) , ( 2 · 𝑀 ) , ( ( 2 · 𝑀 ) C 𝑀 ) )
174	173	chebbnd1lem1	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 4 ) → ( log ‘ ( ( 4 ↑ 𝑀 ) / 𝑀 ) ) < ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) )
175	57 174	syl	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( ( 4 ↑ 𝑀 ) / 𝑀 ) ) < ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) )
176	89 96 97 172 175	lttrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) < ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) )
177	83 97 139	ltmuldivd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) < ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) ↔ ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) < ( ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) / ( 2 · 𝑀 ) ) ) )
178	176 177	mpbid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) < ( ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) / ( 2 · 𝑀 ) ) )
179	86	recnd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π ‘ ( 2 · 𝑀 ) ) ∈ ℂ )
180	66	rpcnd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 2 · 𝑀 ) ) ∈ ℂ )
181	139	rpcnne0d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 2 · 𝑀 ) ∈ ℂ ∧ ( 2 · 𝑀 ) ≠ 0 ) )
182		divass	⊢ ( ( ( π ‘ ( 2 · 𝑀 ) ) ∈ ℂ ∧ ( log ‘ ( 2 · 𝑀 ) ) ∈ ℂ ∧ ( ( 2 · 𝑀 ) ∈ ℂ ∧ ( 2 · 𝑀 ) ≠ 0 ) ) → ( ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) / ( 2 · 𝑀 ) ) = ( ( π ‘ ( 2 · 𝑀 ) ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) )
183	179 180 181 182	syl3anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) / ( 2 · 𝑀 ) ) = ( ( π ‘ ( 2 · 𝑀 ) ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) )
184	178 183	breqtrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) < ( ( π ‘ ( 2 · 𝑀 ) ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) )
185		flle	⊢ ( ( 𝑁 / 2 ) ∈ ℝ → ( ⌊ ‘ ( 𝑁 / 2 ) ) ≤ ( 𝑁 / 2 ) )
186	31 185	syl	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) ≤ ( 𝑁 / 2 ) )
187	1 186	eqbrtrid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ≤ ( 𝑁 / 2 ) )
188		lemuldiv2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑀 ) ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑁 / 2 ) ) )
189	34 21 18 48 188	syl112anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 2 · 𝑀 ) ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑁 / 2 ) ) )
190	187 189	mpbird	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ≤ 𝑁 )
191		ppiwordi	⊢ ( ( ( 2 · 𝑀 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 · 𝑀 ) ≤ 𝑁 ) → ( π ‘ ( 2 · 𝑀 ) ) ≤ ( π ‘ 𝑁 ) )
192	36 21 190 191	syl3anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π ‘ ( 2 · 𝑀 ) ) ≤ ( π ‘ 𝑁 ) )
193	66 139	rpdivcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ∈ ℝ+ )
194	86 29 193	lemul1d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π ‘ ( 2 · 𝑀 ) ) ≤ ( π ‘ 𝑁 ) ↔ ( ( π ‘ ( 2 · 𝑀 ) ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ≤ ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ) )
195	192 194	mpbid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π ‘ ( 2 · 𝑀 ) ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ≤ ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) )
196	83 87 72 184 195	ltletrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) < ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) )
197		ltdiv1	⊢ ( ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ∈ ℝ ∧ ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) < ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ↔ ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) < ( ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) ) )
198	83 72 18 48 197	syl112anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) < ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ↔ ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) < ( ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) ) )
199	196 198	mpbid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) < ( ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) )
200	1	chebbnd1lem2	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) < ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) )
201		remulcl	⊢ ( ( 2 ∈ ℝ ∧ ( ( log ‘ 𝑁 ) / 𝑁 ) ∈ ℝ ) → ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ )
202	6 81 201	sylancr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ )
203	28	nngt0d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 < ( π ‘ 𝑁 ) )
204		ltmul2	⊢ ( ( ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ∈ ℝ ∧ ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ ∧ ( ( π ‘ 𝑁 ) ∈ ℝ ∧ 0 < ( π ‘ 𝑁 ) ) ) → ( ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) < ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ↔ ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) < ( ( π ‘ 𝑁 ) · ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) ) )
205	71 202 29 203 204	syl112anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) < ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ↔ ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) < ( ( π ‘ 𝑁 ) · ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) ) )
206	200 205	mpbid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) < ( ( π ‘ 𝑁 ) · ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) )
207	29	recnd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π ‘ 𝑁 ) ∈ ℂ )
208	81	recnd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑁 ) / 𝑁 ) ∈ ℂ )
209	207 148 208	mul12d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π ‘ 𝑁 ) · ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) = ( 2 · ( ( π ‘ 𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) )
210	206 209	breqtrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) < ( 2 · ( ( π ‘ 𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) )
211		ltdivmul	⊢ ( ( ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ∈ ℝ ∧ ( ( π ‘ 𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) < ( ( π ‘ 𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ↔ ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) < ( 2 · ( ( π ‘ 𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) ) )
212	72 82 18 48 211	syl112anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) < ( ( π ‘ 𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ↔ ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) < ( 2 · ( ( π ‘ 𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) ) )
213	210 212	mpbird	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( π ‘ 𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) < ( ( π ‘ 𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) )
214	17 74 82 199 213	lttrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) < ( ( π ‘ 𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) )