Theorem chebbnd1lem2

Description: Lemma for chebbnd1 : Show that log ( N ) / N does not change too much between N and M = |_ ( N / 2 ) . (Contributed by Mario Carneiro, 22-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		chebbnd1lem2.1	⊢ 𝑀 = ( ⌊ ‘ ( 𝑁 / 2 ) )
2		2rp	⊢ 2 ∈ ℝ+
3		4nn	⊢ 4 ∈ ℕ
4		4z	⊢ 4 ∈ ℤ
5	4	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ∈ ℤ )
6		rehalfcl	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 / 2 ) ∈ ℝ )
7	6	adantr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑁 / 2 ) ∈ ℝ )
8	7	flcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
9	1 8	eqeltrid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℤ )
10		4t2e8	⊢ ( 4 · 2 ) = 8
11		simpr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 8 ≤ 𝑁 )
12	10 11	eqbrtrid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 4 · 2 ) ≤ 𝑁 )
13		4re	⊢ 4 ∈ ℝ
14	13	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ∈ ℝ )
15		simpl	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
16		2re	⊢ 2 ∈ ℝ
17	16	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ∈ ℝ )
18		2pos	⊢ 0 < 2
19	18	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 < 2 )
20		lemuldiv	⊢ ( ( 4 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 4 · 2 ) ≤ 𝑁 ↔ 4 ≤ ( 𝑁 / 2 ) ) )
21	14 15 17 19 20	syl112anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 4 · 2 ) ≤ 𝑁 ↔ 4 ≤ ( 𝑁 / 2 ) ) )
22	12 21	mpbid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ≤ ( 𝑁 / 2 ) )
23		flge	⊢ ( ( ( 𝑁 / 2 ) ∈ ℝ ∧ 4 ∈ ℤ ) → ( 4 ≤ ( 𝑁 / 2 ) ↔ 4 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
24	7 4 23	sylancl	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 4 ≤ ( 𝑁 / 2 ) ↔ 4 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
25	22 24	mpbid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) )
26	25 1	breqtrrdi	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ≤ 𝑀 )
27		eluz2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 4 ) ↔ ( 4 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 4 ≤ 𝑀 ) )
28	5 9 26 27	syl3anbrc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ( ℤ≥ ‘ 4 ) )
29		eluznn	⊢ ( ( 4 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 4 ) ) → 𝑀 ∈ ℕ )
30	3 28 29	sylancr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℕ )
31	30	nnrpd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℝ+ )
32		rpmulcl	⊢ ( ( 2 ∈ ℝ+ ∧ 𝑀 ∈ ℝ+ ) → ( 2 · 𝑀 ) ∈ ℝ+ )
33	2 31 32	sylancr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ∈ ℝ+ )
34	33	relogcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 2 · 𝑀 ) ) ∈ ℝ )
35	34 33	rerpdivcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ∈ ℝ )
36		0red	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 ∈ ℝ )
37		8re	⊢ 8 ∈ ℝ
38	37	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 8 ∈ ℝ )
39		8pos	⊢ 0 < 8
40	39	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 < 8 )
41	36 38 15 40 11	ltletrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 < 𝑁 )
42	15 41	elrpd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑁 ∈ ℝ+ )
43	42	rphalfcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑁 / 2 ) ∈ ℝ+ )
44	43	relogcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 𝑁 / 2 ) ) ∈ ℝ )
45	44 43	rerpdivcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) ∈ ℝ )
46	42	relogcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ 𝑁 ) ∈ ℝ )
47	46 42	rerpdivcld	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑁 ) / 𝑁 ) ∈ ℝ )
48		remulcl	⊢ ( ( 2 ∈ ℝ ∧ ( ( log ‘ 𝑁 ) / 𝑁 ) ∈ ℝ ) → ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ )
49	16 47 48	sylancr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ )
50	9	zred	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℝ )
51		peano2re	⊢ ( 𝑀 ∈ ℝ → ( 𝑀 + 1 ) ∈ ℝ )
52	50 51	syl	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑀 + 1 ) ∈ ℝ )
53		remulcl	⊢ ( ( 2 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 2 · 𝑀 ) ∈ ℝ )
54	16 50 53	sylancr	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ∈ ℝ )
55		flltp1	⊢ ( ( 𝑁 / 2 ) ∈ ℝ → ( 𝑁 / 2 ) < ( ( ⌊ ‘ ( 𝑁 / 2 ) ) + 1 ) )
56	7 55	syl	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑁 / 2 ) < ( ( ⌊ ‘ ( 𝑁 / 2 ) ) + 1 ) )
57	1	oveq1i	⊢ ( 𝑀 + 1 ) = ( ( ⌊ ‘ ( 𝑁 / 2 ) ) + 1 )
58	56 57	breqtrrdi	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑁 / 2 ) < ( 𝑀 + 1 ) )
59		1red	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 1 ∈ ℝ )
60	30	nnge1d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 1 ≤ 𝑀 )
61	59 50 50 60	leadd2dd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑀 + 1 ) ≤ ( 𝑀 + 𝑀 ) )
62	50	recnd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℂ )
63	62	2timesd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) = ( 𝑀 + 𝑀 ) )
64	61 63	breqtrrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑀 + 1 ) ≤ ( 2 · 𝑀 ) )
65	7 52 54 58 64	ltletrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑁 / 2 ) < ( 2 · 𝑀 ) )
66		ere	⊢ e ∈ ℝ
67	66	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e ∈ ℝ )
68		egt2lt3	⊢ ( 2 < e ∧ e < 3 )
69	68	simpri	⊢ e < 3
70		3lt4	⊢ 3 < 4
71		3re	⊢ 3 ∈ ℝ
72	66 71 13	lttri	⊢ ( ( e < 3 ∧ 3 < 4 ) → e < 4 )
73	69 70 72	mp2an	⊢ e < 4
74	73	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e < 4 )
75	67 14 7 74 22	ltletrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e < ( 𝑁 / 2 ) )
76	67 7 75	ltled	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e ≤ ( 𝑁 / 2 ) )
77	67 7 54 75 65	lttrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e < ( 2 · 𝑀 ) )
78	67 54 77	ltled	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e ≤ ( 2 · 𝑀 ) )
79		logdivlt	⊢ ( ( ( ( 𝑁 / 2 ) ∈ ℝ ∧ e ≤ ( 𝑁 / 2 ) ) ∧ ( ( 2 · 𝑀 ) ∈ ℝ ∧ e ≤ ( 2 · 𝑀 ) ) ) → ( ( 𝑁 / 2 ) < ( 2 · 𝑀 ) ↔ ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) < ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) ) )
80	7 76 54 78 79	syl22anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 𝑁 / 2 ) < ( 2 · 𝑀 ) ↔ ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) < ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) ) )
81	65 80	mpbid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) < ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) )
82		rphalflt	⊢ ( 𝑁 ∈ ℝ+ → ( 𝑁 / 2 ) < 𝑁 )
83	42 82	syl	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑁 / 2 ) < 𝑁 )
84		logltb	⊢ ( ( ( 𝑁 / 2 ) ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝑁 / 2 ) < 𝑁 ↔ ( log ‘ ( 𝑁 / 2 ) ) < ( log ‘ 𝑁 ) ) )
85	43 42 84	syl2anc	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 𝑁 / 2 ) < 𝑁 ↔ ( log ‘ ( 𝑁 / 2 ) ) < ( log ‘ 𝑁 ) ) )
86	83 85	mpbid	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 𝑁 / 2 ) ) < ( log ‘ 𝑁 ) )
87	44 46 43 86	ltdiv1dd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) < ( ( log ‘ 𝑁 ) / ( 𝑁 / 2 ) ) )
88	46	recnd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ 𝑁 ) ∈ ℂ )
89	15	recnd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑁 ∈ ℂ )
90	17	recnd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ∈ ℂ )
91	42	rpne0d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑁 ≠ 0 )
92		2ne0	⊢ 2 ≠ 0
93	92	a1i	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ≠ 0 )
94	88 89 90 91 93	divdiv2d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑁 ) / ( 𝑁 / 2 ) ) = ( ( ( log ‘ 𝑁 ) · 2 ) / 𝑁 ) )
95	88 90	mulcomd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑁 ) · 2 ) = ( 2 · ( log ‘ 𝑁 ) ) )
96	95	oveq1d	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 𝑁 ) · 2 ) / 𝑁 ) = ( ( 2 · ( log ‘ 𝑁 ) ) / 𝑁 ) )
97	90 88 89 91	divassd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 2 · ( log ‘ 𝑁 ) ) / 𝑁 ) = ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) )
98	94 96 97	3eqtrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑁 ) / ( 𝑁 / 2 ) ) = ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) )
99	87 98	breqtrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 𝑁 / 2 ) ) / ( 𝑁 / 2 ) ) < ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) )
100	35 45 49 81 99	lttrd	⊢ ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) < ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) )