pntpbnd1a - Metamath Proof Explorer

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

Theorem pntpbnd1a 25730

Description: Lemma for pntpbnd 25733. (Contributed by Mario Carneiro, 11-Apr-2016.) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020.)

**Hypotheses**
Ref	Expression
pntpbnd.r	⊢ 𝑅 = (𝑎 ∈ ℝ⁺ ↦ ((ψ‘𝑎) − 𝑎))
pntpbnd1.e	⊢ (𝜑 → 𝐸 ∈ (0(,)1))
pntpbnd1.x	⊢ 𝑋 = (exp‘(2 / 𝐸))
pntpbnd1.y	⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞))
pntpbnd1a.1	⊢ (𝜑 → 𝑁 ∈ ℕ)
pntpbnd1a.2	⊢ (𝜑 → (𝑌 < 𝑁 ∧ 𝑁 ≤ (𝐾 · 𝑌)))
pntpbnd1a.3	⊢ (𝜑 → (abs‘(𝑅‘𝑁)) ≤ (abs‘((𝑅‘(𝑁 + 1)) − (𝑅‘𝑁))))

**Assertion**
Ref	Expression
pntpbnd1a	⊢ (𝜑 → (abs‘((𝑅‘𝑁) / 𝑁)) ≤ 𝐸)

Distinct variable group: 𝑁,𝑎 Allowed substitution hints: 𝜑(𝑎) 𝑅(𝑎) 𝐸(𝑎) 𝐾(𝑎) 𝑋(𝑎) 𝑌(𝑎)

**Proof of Theorem pntpbnd1a**
Step	Hyp	Ref	Expression
1		pntpbnd1a.1	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ)
2	1	nnrpd 12183	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
3		pntpbnd.r	. . . . . . . 8 ⊢ 𝑅 = (𝑎 ∈ ℝ⁺ ↦ ((ψ‘𝑎) − 𝑎))
4	3	pntrf 25708	. . . . . . 7 ⊢ 𝑅:ℝ⁺⟶ℝ
5	4	ffvelrni 6624	. . . . . 6 ⊢ (𝑁 ∈ ℝ⁺ → (𝑅‘𝑁) ∈ ℝ)
6	2, 5	syl 17	. . . . 5 ⊢ (𝜑 → (𝑅‘𝑁) ∈ ℝ)
7	6, 2	rerpdivcld 12216	. . . 4 ⊢ (𝜑 → ((𝑅‘𝑁) / 𝑁) ∈ ℝ)
8	7	recnd 10407	. . 3 ⊢ (𝜑 → ((𝑅‘𝑁) / 𝑁) ∈ ℂ)
9	8	abscld 14587	. 2 ⊢ (𝜑 → (abs‘((𝑅‘𝑁) / 𝑁)) ∈ ℝ)
10	2	relogcld 24810	. . 3 ⊢ (𝜑 → (log‘𝑁) ∈ ℝ)
11	10, 2	rerpdivcld 12216	. 2 ⊢ (𝜑 → ((log‘𝑁) / 𝑁) ∈ ℝ)
12		ioossre 12551	. . 3 ⊢ (0(,)1) ⊆ ℝ
13		pntpbnd1.e	. . 3 ⊢ (𝜑 → 𝐸 ∈ (0(,)1))
14	12, 13	sseldi 3819	. 2 ⊢ (𝜑 → 𝐸 ∈ ℝ)
15	6	recnd 10407	. . . . 5 ⊢ (𝜑 → (𝑅‘𝑁) ∈ ℂ)
16	1	nnred 11395	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℝ)
17	16	recnd 10407	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℂ)
18	1	nnne0d 11429	. . . . 5 ⊢ (𝜑 → 𝑁 ≠ 0)
19	15, 17, 18	absdivd 14606	. . . 4 ⊢ (𝜑 → (abs‘((𝑅‘𝑁) / 𝑁)) = ((abs‘(𝑅‘𝑁)) / (abs‘𝑁)))
20	1	nnnn0d 11706	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
21	20	nn0ge0d 11709	. . . . . 6 ⊢ (𝜑 → 0 ≤ 𝑁)
22	16, 21	absidd 14573	. . . . 5 ⊢ (𝜑 → (abs‘𝑁) = 𝑁)
23	22	oveq2d 6940	. . . 4 ⊢ (𝜑 → ((abs‘(𝑅‘𝑁)) / (abs‘𝑁)) = ((abs‘(𝑅‘𝑁)) / 𝑁))
24	19, 23	eqtrd 2814	. . 3 ⊢ (𝜑 → (abs‘((𝑅‘𝑁) / 𝑁)) = ((abs‘(𝑅‘𝑁)) / 𝑁))
25	15	abscld 14587	. . . 4 ⊢ (𝜑 → (abs‘(𝑅‘𝑁)) ∈ ℝ)
26	1	peano2nnd 11397	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ)
27		vmacl 25300	. . . . . . . . 9 ⊢ ((𝑁 + 1) ∈ ℕ → (Λ‘(𝑁 + 1)) ∈ ℝ)
28	26, 27	syl 17	. . . . . . . 8 ⊢ (𝜑 → (Λ‘(𝑁 + 1)) ∈ ℝ)
29		peano2rem 10692	. . . . . . . 8 ⊢ ((Λ‘(𝑁 + 1)) ∈ ℝ → ((Λ‘(𝑁 + 1)) − 1) ∈ ℝ)
30	28, 29	syl 17	. . . . . . 7 ⊢ (𝜑 → ((Λ‘(𝑁 + 1)) − 1) ∈ ℝ)
31	30	recnd 10407	. . . . . 6 ⊢ (𝜑 → ((Λ‘(𝑁 + 1)) − 1) ∈ ℂ)
32	31	abscld 14587	. . . . 5 ⊢ (𝜑 → (abs‘((Λ‘(𝑁 + 1)) − 1)) ∈ ℝ)
33		pntpbnd1a.3	. . . . . 6 ⊢ (𝜑 → (abs‘(𝑅‘𝑁)) ≤ (abs‘((𝑅‘(𝑁 + 1)) − (𝑅‘𝑁))))
34	26	nnrpd 12183	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ⁺)
35	3	pntrval 25707	. . . . . . . . . 10 ⊢ ((𝑁 + 1) ∈ ℝ⁺ → (𝑅‘(𝑁 + 1)) = ((ψ‘(𝑁 + 1)) − (𝑁 + 1)))
36	34, 35	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑅‘(𝑁 + 1)) = ((ψ‘(𝑁 + 1)) − (𝑁 + 1)))
37	3	pntrval 25707	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℝ⁺ → (𝑅‘𝑁) = ((ψ‘𝑁) − 𝑁))
38	2, 37	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑅‘𝑁) = ((ψ‘𝑁) − 𝑁))
39	36, 38	oveq12d 6942	. . . . . . . 8 ⊢ (𝜑 → ((𝑅‘(𝑁 + 1)) − (𝑅‘𝑁)) = (((ψ‘(𝑁 + 1)) − (𝑁 + 1)) − ((ψ‘𝑁) − 𝑁)))
40		peano2re 10551	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
41	16, 40	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
42		chpcl 25306	. . . . . . . . . . 11 ⊢ ((𝑁 + 1) ∈ ℝ → (ψ‘(𝑁 + 1)) ∈ ℝ)
43	41, 42	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (ψ‘(𝑁 + 1)) ∈ ℝ)
44	43	recnd 10407	. . . . . . . . 9 ⊢ (𝜑 → (ψ‘(𝑁 + 1)) ∈ ℂ)
45	41	recnd 10407	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 + 1) ∈ ℂ)
46		chpcl 25306	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℝ → (ψ‘𝑁) ∈ ℝ)
47	16, 46	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (ψ‘𝑁) ∈ ℝ)
48	47	recnd 10407	. . . . . . . . 9 ⊢ (𝜑 → (ψ‘𝑁) ∈ ℂ)
49	44, 45, 48, 17	sub4d 10785	. . . . . . . 8 ⊢ (𝜑 → (((ψ‘(𝑁 + 1)) − (𝑁 + 1)) − ((ψ‘𝑁) − 𝑁)) = (((ψ‘(𝑁 + 1)) − (ψ‘𝑁)) − ((𝑁 + 1) − 𝑁)))
50	28	recnd 10407	. . . . . . . . . 10 ⊢ (𝜑 → (Λ‘(𝑁 + 1)) ∈ ℂ)
51		chpp1 25337	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (ψ‘(𝑁 + 1)) = ((ψ‘𝑁) + (Λ‘(𝑁 + 1))))
52	20, 51	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (ψ‘(𝑁 + 1)) = ((ψ‘𝑁) + (Λ‘(𝑁 + 1))))
53	48, 50, 52	mvrladdd 10790	. . . . . . . . 9 ⊢ (𝜑 → ((ψ‘(𝑁 + 1)) − (ψ‘𝑁)) = (Λ‘(𝑁 + 1)))
54		ax-1cn 10332	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
55		pncan2 10631	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 𝑁) = 1)
56	17, 54, 55	sylancl 580	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + 1) − 𝑁) = 1)
57	53, 56	oveq12d 6942	. . . . . . . 8 ⊢ (𝜑 → (((ψ‘(𝑁 + 1)) − (ψ‘𝑁)) − ((𝑁 + 1) − 𝑁)) = ((Λ‘(𝑁 + 1)) − 1))
58	39, 49, 57	3eqtrd 2818	. . . . . . 7 ⊢ (𝜑 → ((𝑅‘(𝑁 + 1)) − (𝑅‘𝑁)) = ((Λ‘(𝑁 + 1)) − 1))
59	58	fveq2d 6452	. . . . . 6 ⊢ (𝜑 → (abs‘((𝑅‘(𝑁 + 1)) − (𝑅‘𝑁))) = (abs‘((Λ‘(𝑁 + 1)) − 1)))
60	33, 59	breqtrd 4914	. . . . 5 ⊢ (𝜑 → (abs‘(𝑅‘𝑁)) ≤ (abs‘((Λ‘(𝑁 + 1)) − 1)))
61		1red 10379	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
62	61, 10	resubcld 10805	. . . . . . 7 ⊢ (𝜑 → (1 − (log‘𝑁)) ∈ ℝ)
63		0red 10382	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℝ)
64		2re 11453	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
65		eliooord 12549	. . . . . . . . . . . . . 14 ⊢ (𝐸 ∈ (0(,)1) → (0 < 𝐸 ∧ 𝐸 < 1))
66	13, 65	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1))
67	66	simpld 490	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 𝐸)
68	14, 67	elrpd 12182	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
69		rerpdivcl 12173	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 𝐸 ∈ ℝ⁺) → (2 / 𝐸) ∈ ℝ)
70	64, 68, 69	sylancr 581	. . . . . . . . . 10 ⊢ (𝜑 → (2 / 𝐸) ∈ ℝ)
71	64	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℝ)
72		1lt2 11557	. . . . . . . . . . . 12 ⊢ 1 < 2
73	72	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 1 < 2)
74		2cn 11454	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
75	74	div1i 11105	. . . . . . . . . . . 12 ⊢ (2 / 1) = 2
76	66	simprd 491	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 < 1)
77		0lt1 10899	. . . . . . . . . . . . . . 15 ⊢ 0 < 1
78	77	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 1)
79		2pos 11489	. . . . . . . . . . . . . . 15 ⊢ 0 < 2
80	79	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 2)
81		ltdiv2 11265	. . . . . . . . . . . . . 14 ⊢ (((𝐸 ∈ ℝ ∧ 0 < 𝐸) ∧ (1 ∈ ℝ ∧ 0 < 1) ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐸 < 1 ↔ (2 / 1) < (2 / 𝐸)))
82	14, 67, 61, 78, 71, 80, 81	syl222anc 1454	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 < 1 ↔ (2 / 1) < (2 / 𝐸)))
83	76, 82	mpbid 224	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 / 1) < (2 / 𝐸))
84	75, 83	syl5eqbrr 4924	. . . . . . . . . . 11 ⊢ (𝜑 → 2 < (2 / 𝐸))
85	61, 71, 70, 73, 84	lttrd 10539	. . . . . . . . . 10 ⊢ (𝜑 → 1 < (2 / 𝐸))
86		pntpbnd1.x	. . . . . . . . . . . . 13 ⊢ 𝑋 = (exp‘(2 / 𝐸))
87	70	rpefcld 15241	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (exp‘(2 / 𝐸)) ∈ ℝ⁺)
88	86, 87	syl5eqel 2863	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ ℝ⁺)
89	88	rpred 12185	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ∈ ℝ)
90		pntpbnd1.y	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞))
91	88	rpxrd 12186	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ ℝ^*)
92		elioopnf 12584	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ ℝ^* → (𝑌 ∈ (𝑋(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌)))
93	91, 92	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 ∈ (𝑋(,)+∞) ↔ (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌)))
94	90, 93	mpbid 224	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝑋 < 𝑌))
95	94	simpld 490	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ∈ ℝ)
96	94	simprd 491	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 < 𝑌)
97		pntpbnd1a.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑌 < 𝑁 ∧ 𝑁 ≤ (𝐾 · 𝑌)))
98	97	simpld 490	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 < 𝑁)
99	89, 95, 16, 96, 98	lttrd 10539	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 < 𝑁)
100	86, 99	syl5eqbrr 4924	. . . . . . . . . . . 12 ⊢ (𝜑 → (exp‘(2 / 𝐸)) < 𝑁)
101	2	reeflogd 24811	. . . . . . . . . . . 12 ⊢ (𝜑 → (exp‘(log‘𝑁)) = 𝑁)
102	100, 101	breqtrrd 4916	. . . . . . . . . . 11 ⊢ (𝜑 → (exp‘(2 / 𝐸)) < (exp‘(log‘𝑁)))
103		eflt 15253	. . . . . . . . . . . 12 ⊢ (((2 / 𝐸) ∈ ℝ ∧ (log‘𝑁) ∈ ℝ) → ((2 / 𝐸) < (log‘𝑁) ↔ (exp‘(2 / 𝐸)) < (exp‘(log‘𝑁))))
104	70, 10, 103	syl2anc 579	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 / 𝐸) < (log‘𝑁) ↔ (exp‘(2 / 𝐸)) < (exp‘(log‘𝑁))))
105	102, 104	mpbird 249	. . . . . . . . . 10 ⊢ (𝜑 → (2 / 𝐸) < (log‘𝑁))
106	61, 70, 10, 85, 105	lttrd 10539	. . . . . . . . 9 ⊢ (𝜑 → 1 < (log‘𝑁))
107	61, 10, 106	ltled 10526	. . . . . . . 8 ⊢ (𝜑 → 1 ≤ (log‘𝑁))
108		1re 10378	. . . . . . . . 9 ⊢ 1 ∈ ℝ
109		suble0 10891	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ (log‘𝑁) ∈ ℝ) → ((1 − (log‘𝑁)) ≤ 0 ↔ 1 ≤ (log‘𝑁)))
110	108, 10, 109	sylancr 581	. . . . . . . 8 ⊢ (𝜑 → ((1 − (log‘𝑁)) ≤ 0 ↔ 1 ≤ (log‘𝑁)))
111	107, 110	mpbird 249	. . . . . . 7 ⊢ (𝜑 → (1 − (log‘𝑁)) ≤ 0)
112		vmage0 25303	. . . . . . . 8 ⊢ ((𝑁 + 1) ∈ ℕ → 0 ≤ (Λ‘(𝑁 + 1)))
113	26, 112	syl 17	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (Λ‘(𝑁 + 1)))
114	62, 63, 28, 111, 113	letrd 10535	. . . . . 6 ⊢ (𝜑 → (1 − (log‘𝑁)) ≤ (Λ‘(𝑁 + 1)))
115	34	relogcld 24810	. . . . . . 7 ⊢ (𝜑 → (log‘(𝑁 + 1)) ∈ ℝ)
116		readdcl 10357	. . . . . . . 8 ⊢ ((1 ∈ ℝ ∧ (log‘𝑁) ∈ ℝ) → (1 + (log‘𝑁)) ∈ ℝ)
117	108, 10, 116	sylancr 581	. . . . . . 7 ⊢ (𝜑 → (1 + (log‘𝑁)) ∈ ℝ)
118		vmalelog 25386	. . . . . . . 8 ⊢ ((𝑁 + 1) ∈ ℕ → (Λ‘(𝑁 + 1)) ≤ (log‘(𝑁 + 1)))
119	26, 118	syl 17	. . . . . . 7 ⊢ (𝜑 → (Λ‘(𝑁 + 1)) ≤ (log‘(𝑁 + 1)))
120	71, 16	remulcld 10409	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ)
121		epr 15344	. . . . . . . . . . . 12 ⊢ e ∈ ℝ⁺
122		rpmulcl 12166	. . . . . . . . . . . 12 ⊢ ((e ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → (e · 𝑁) ∈ ℝ⁺)
123	121, 2, 122	sylancr 581	. . . . . . . . . . 11 ⊢ (𝜑 → (e · 𝑁) ∈ ℝ⁺)
124	123	rpred 12185	. . . . . . . . . 10 ⊢ (𝜑 → (e · 𝑁) ∈ ℝ)
125	1	nnge1d 11427	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ≤ 𝑁)
126	61, 16, 16, 125	leadd2dd 10992	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + 1) ≤ (𝑁 + 𝑁))
127	17	2timesd 11629	. . . . . . . . . . 11 ⊢ (𝜑 → (2 · 𝑁) = (𝑁 + 𝑁))
128	126, 127	breqtrrd 4916	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 1) ≤ (2 · 𝑁))
129		ere 15225	. . . . . . . . . . . . 13 ⊢ e ∈ ℝ
130		egt2lt3 15342	. . . . . . . . . . . . . 14 ⊢ (2 < e ∧ e < 3)
131	130	simpli 478	. . . . . . . . . . . . 13 ⊢ 2 < e
132	64, 129, 131	ltleii 10501	. . . . . . . . . . . 12 ⊢ 2 ≤ e
133	132	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ≤ e)
134	129	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → e ∈ ℝ)
135	1	nngt0d 11428	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < 𝑁)
136		lemul1 11231	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ ∧ e ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (2 ≤ e ↔ (2 · 𝑁) ≤ (e · 𝑁)))
137	71, 134, 16, 135, 136	syl112anc 1442	. . . . . . . . . . 11 ⊢ (𝜑 → (2 ≤ e ↔ (2 · 𝑁) ≤ (e · 𝑁)))
138	133, 137	mpbid 224	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑁) ≤ (e · 𝑁))
139	41, 120, 124, 128, 138	letrd 10535	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 + 1) ≤ (e · 𝑁))
140	34, 123	logled 24814	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + 1) ≤ (e · 𝑁) ↔ (log‘(𝑁 + 1)) ≤ (log‘(e · 𝑁))))
141	139, 140	mpbid 224	. . . . . . . 8 ⊢ (𝜑 → (log‘(𝑁 + 1)) ≤ (log‘(e · 𝑁)))
142		relogmul 24779	. . . . . . . . . 10 ⊢ ((e ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → (log‘(e · 𝑁)) = ((log‘e) + (log‘𝑁)))
143	121, 2, 142	sylancr 581	. . . . . . . . 9 ⊢ (𝜑 → (log‘(e · 𝑁)) = ((log‘e) + (log‘𝑁)))
144		loge 24774	. . . . . . . . . 10 ⊢ (log‘e) = 1
145	144	oveq1i 6934	. . . . . . . . 9 ⊢ ((log‘e) + (log‘𝑁)) = (1 + (log‘𝑁))
146	143, 145	syl6eq 2830	. . . . . . . 8 ⊢ (𝜑 → (log‘(e · 𝑁)) = (1 + (log‘𝑁)))
147	141, 146	breqtrd 4914	. . . . . . 7 ⊢ (𝜑 → (log‘(𝑁 + 1)) ≤ (1 + (log‘𝑁)))
148	28, 115, 117, 119, 147	letrd 10535	. . . . . 6 ⊢ (𝜑 → (Λ‘(𝑁 + 1)) ≤ (1 + (log‘𝑁)))
149	28, 61, 10	absdifled 14585	. . . . . 6 ⊢ (𝜑 → ((abs‘((Λ‘(𝑁 + 1)) − 1)) ≤ (log‘𝑁) ↔ ((1 − (log‘𝑁)) ≤ (Λ‘(𝑁 + 1)) ∧ (Λ‘(𝑁 + 1)) ≤ (1 + (log‘𝑁)))))
150	114, 148, 149	mpbir2and 703	. . . . 5 ⊢ (𝜑 → (abs‘((Λ‘(𝑁 + 1)) − 1)) ≤ (log‘𝑁))
151	25, 32, 10, 60, 150	letrd 10535	. . . 4 ⊢ (𝜑 → (abs‘(𝑅‘𝑁)) ≤ (log‘𝑁))
152	25, 10, 2, 151	lediv1dd 12243	. . 3 ⊢ (𝜑 → ((abs‘(𝑅‘𝑁)) / 𝑁) ≤ ((log‘𝑁) / 𝑁))
153	24, 152	eqbrtrd 4910	. 2 ⊢ (𝜑 → (abs‘((𝑅‘𝑁) / 𝑁)) ≤ ((log‘𝑁) / 𝑁))
154	88	relogcld 24810	. . . . 5 ⊢ (𝜑 → (log‘𝑋) ∈ ℝ)
155	154, 88	rerpdivcld 12216	. . . 4 ⊢ (𝜑 → ((log‘𝑋) / 𝑋) ∈ ℝ)
156	61, 70, 85	ltled 10526	. . . . . . . 8 ⊢ (𝜑 → 1 ≤ (2 / 𝐸))
157		efle 15254	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ (2 / 𝐸) ∈ ℝ) → (1 ≤ (2 / 𝐸) ↔ (exp‘1) ≤ (exp‘(2 / 𝐸))))
158	108, 70, 157	sylancr 581	. . . . . . . 8 ⊢ (𝜑 → (1 ≤ (2 / 𝐸) ↔ (exp‘1) ≤ (exp‘(2 / 𝐸))))
159	156, 158	mpbid 224	. . . . . . 7 ⊢ (𝜑 → (exp‘1) ≤ (exp‘(2 / 𝐸)))
160		df-e 15205	. . . . . . 7 ⊢ e = (exp‘1)
161	159, 160, 86	3brtr4g 4922	. . . . . 6 ⊢ (𝜑 → e ≤ 𝑋)
162	144, 107	syl5eqbr 4923	. . . . . . 7 ⊢ (𝜑 → (log‘e) ≤ (log‘𝑁))
163		logleb 24790	. . . . . . . 8 ⊢ ((e ∈ ℝ⁺ ∧ 𝑁 ∈ ℝ⁺) → (e ≤ 𝑁 ↔ (log‘e) ≤ (log‘𝑁)))
164	121, 2, 163	sylancr 581	. . . . . . 7 ⊢ (𝜑 → (e ≤ 𝑁 ↔ (log‘e) ≤ (log‘𝑁)))
165	162, 164	mpbird 249	. . . . . 6 ⊢ (𝜑 → e ≤ 𝑁)
166		logdivlt 24808	. . . . . 6 ⊢ (((𝑋 ∈ ℝ ∧ e ≤ 𝑋) ∧ (𝑁 ∈ ℝ ∧ e ≤ 𝑁)) → (𝑋 < 𝑁 ↔ ((log‘𝑁) / 𝑁) < ((log‘𝑋) / 𝑋)))
167	89, 161, 16, 165, 166	syl22anc 829	. . . . 5 ⊢ (𝜑 → (𝑋 < 𝑁 ↔ ((log‘𝑁) / 𝑁) < ((log‘𝑋) / 𝑋)))
168	99, 167	mpbid 224	. . . 4 ⊢ (𝜑 → ((log‘𝑁) / 𝑁) < ((log‘𝑋) / 𝑋))
169	86	fveq2i 6451	. . . . . . 7 ⊢ (log‘𝑋) = (log‘(exp‘(2 / 𝐸)))
170	70	relogefd 24815	. . . . . . 7 ⊢ (𝜑 → (log‘(exp‘(2 / 𝐸))) = (2 / 𝐸))
171	169, 170	syl5eq 2826	. . . . . 6 ⊢ (𝜑 → (log‘𝑋) = (2 / 𝐸))
172	171	oveq1d 6939	. . . . 5 ⊢ (𝜑 → ((log‘𝑋) / 𝑋) = ((2 / 𝐸) / 𝑋))
173		2rp 12146	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ⁺
174		rpdivcl 12168	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ⁺ ∧ 𝐸 ∈ ℝ⁺) → (2 / 𝐸) ∈ ℝ⁺)
175	173, 68, 174	sylancr 581	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 / 𝐸) ∈ ℝ⁺)
176	175	rpcnd 12187	. . . . . . . . . . 11 ⊢ (𝜑 → (2 / 𝐸) ∈ ℂ)
177	176	sqvald 13328	. . . . . . . . . 10 ⊢ (𝜑 → ((2 / 𝐸)↑2) = ((2 / 𝐸) · (2 / 𝐸)))
178		2cnd 11457	. . . . . . . . . . 11 ⊢ (𝜑 → 2 ∈ ℂ)
179	68	rpcnne0d 12194	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0))
180		div12 11057	. . . . . . . . . . 11 ⊢ (((2 / 𝐸) ∈ ℂ ∧ 2 ∈ ℂ ∧ (𝐸 ∈ ℂ ∧ 𝐸 ≠ 0)) → ((2 / 𝐸) · (2 / 𝐸)) = (2 · ((2 / 𝐸) / 𝐸)))
181	176, 178, 179, 180	syl3anc 1439	. . . . . . . . . 10 ⊢ (𝜑 → ((2 / 𝐸) · (2 / 𝐸)) = (2 · ((2 / 𝐸) / 𝐸)))
182	177, 181	eqtrd 2814	. . . . . . . . 9 ⊢ (𝜑 → ((2 / 𝐸)↑2) = (2 · ((2 / 𝐸) / 𝐸)))
183	182	oveq1d 6939	. . . . . . . 8 ⊢ (𝜑 → (((2 / 𝐸)↑2) / 2) = ((2 · ((2 / 𝐸) / 𝐸)) / 2))
184	175, 68	rpdivcld 12202	. . . . . . . . . 10 ⊢ (𝜑 → ((2 / 𝐸) / 𝐸) ∈ ℝ⁺)
185	184	rpcnd 12187	. . . . . . . . 9 ⊢ (𝜑 → ((2 / 𝐸) / 𝐸) ∈ ℂ)
186		2ne0 11490	. . . . . . . . . 10 ⊢ 2 ≠ 0
187	186	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 2 ≠ 0)
188	185, 178, 187	divcan3d 11158	. . . . . . . 8 ⊢ (𝜑 → ((2 · ((2 / 𝐸) / 𝐸)) / 2) = ((2 / 𝐸) / 𝐸))
189	183, 188	eqtrd 2814	. . . . . . 7 ⊢ (𝜑 → (((2 / 𝐸)↑2) / 2) = ((2 / 𝐸) / 𝐸))
190	70	resqcld 13360	. . . . . . . . 9 ⊢ (𝜑 → ((2 / 𝐸)↑2) ∈ ℝ)
191	190	rehalfcld 11633	. . . . . . . 8 ⊢ (𝜑 → (((2 / 𝐸)↑2) / 2) ∈ ℝ)
192		1rp 12145	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ⁺
193		rpaddcl 12165	. . . . . . . . . . 11 ⊢ ((1 ∈ ℝ⁺ ∧ (2 / 𝐸) ∈ ℝ⁺) → (1 + (2 / 𝐸)) ∈ ℝ⁺)
194	192, 175, 193	sylancr 581	. . . . . . . . . 10 ⊢ (𝜑 → (1 + (2 / 𝐸)) ∈ ℝ⁺)
195	194	rpred 12185	. . . . . . . . 9 ⊢ (𝜑 → (1 + (2 / 𝐸)) ∈ ℝ)
196	195, 191	readdcld 10408	. . . . . . . 8 ⊢ (𝜑 → ((1 + (2 / 𝐸)) + (((2 / 𝐸)↑2) / 2)) ∈ ℝ)
197	191, 194	ltaddrp2d 12219	. . . . . . . 8 ⊢ (𝜑 → (((2 / 𝐸)↑2) / 2) < ((1 + (2 / 𝐸)) + (((2 / 𝐸)↑2) / 2)))
198		efgt1p2 15250	. . . . . . . . . 10 ⊢ ((2 / 𝐸) ∈ ℝ⁺ → ((1 + (2 / 𝐸)) + (((2 / 𝐸)↑2) / 2)) < (exp‘(2 / 𝐸)))
199	175, 198	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((1 + (2 / 𝐸)) + (((2 / 𝐸)↑2) / 2)) < (exp‘(2 / 𝐸)))
200	199, 86	syl6breqr 4930	. . . . . . . 8 ⊢ (𝜑 → ((1 + (2 / 𝐸)) + (((2 / 𝐸)↑2) / 2)) < 𝑋)
201	191, 196, 89, 197, 200	lttrd 10539	. . . . . . 7 ⊢ (𝜑 → (((2 / 𝐸)↑2) / 2) < 𝑋)
202	189, 201	eqbrtrrd 4912	. . . . . 6 ⊢ (𝜑 → ((2 / 𝐸) / 𝐸) < 𝑋)
203	70, 68, 88, 202	ltdiv23d 12252	. . . . 5 ⊢ (𝜑 → ((2 / 𝐸) / 𝑋) < 𝐸)
204	172, 203	eqbrtrd 4910	. . . 4 ⊢ (𝜑 → ((log‘𝑋) / 𝑋) < 𝐸)
205	11, 155, 14, 168, 204	lttrd 10539	. . 3 ⊢ (𝜑 → ((log‘𝑁) / 𝑁) < 𝐸)
206	11, 14, 205	ltled 10526	. 2 ⊢ (𝜑 → ((log‘𝑁) / 𝑁) ≤ 𝐸)
207	9, 11, 14, 153, 206	letrd 10535	1 ⊢ (𝜑 → (abs‘((𝑅‘𝑁) / 𝑁)) ≤ 𝐸)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1601 ∈ wcel 2107 ≠ wne 2969 class class class wbr 4888 ↦ cmpt 4967 ‘cfv 6137 (class class class)co 6924 ℂcc 10272 ℝcr 10273 0cc0 10274 1c1 10275 + caddc 10277 · cmul 10279 +∞cpnf 10410 ℝ^*cxr 10412 < clt 10413 ≤ cle 10414 − cmin 10608 / cdiv 11034 ℕcn 11378 2c2 11434 3c3 11435 ℕ₀cn0 11646 ℝ⁺crp 12141 (,)cioo 12491 ↑cexp 13182 abscabs 14385 expce 15198 eceu 15199 logclog 24742 Λcvma 25274 ψcchp 25275

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-rep 5008 ax-sep 5019 ax-nul 5027 ax-pow 5079 ax-pr 5140 ax-un 7228 ax-inf2 8837 ax-cnex 10330 ax-resscn 10331 ax-1cn 10332 ax-icn 10333 ax-addcl 10334 ax-addrcl 10335 ax-mulcl 10336 ax-mulrcl 10337 ax-mulcom 10338 ax-addass 10339 ax-mulass 10340 ax-distr 10341 ax-i2m1 10342 ax-1ne0 10343 ax-1rid 10344 ax-rnegex 10345 ax-rrecex 10346 ax-cnre 10347 ax-pre-lttri 10348 ax-pre-lttrn 10349 ax-pre-ltadd 10350 ax-pre-mulgt0 10351 ax-pre-sup 10352 ax-addf 10353 ax-mulf 10354

This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-fal 1615 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-nel 3076 df-ral 3095 df-rex 3096 df-reu 3097 df-rmo 3098 df-rab 3099 df-v 3400 df-sbc 3653 df-csb 3752 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-pss 3808 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4674 df-int 4713 df-iun 4757 df-iin 4758 df-br 4889 df-opab 4951 df-mpt 4968 df-tr 4990 df-id 5263 df-eprel 5268 df-po 5276 df-so 5277 df-fr 5316 df-se 5317 df-we 5318 df-xp 5363 df-rel 5364 df-cnv 5365 df-co 5366 df-dm 5367 df-rn 5368 df-res 5369 df-ima 5370 df-pred 5935 df-ord 5981 df-on 5982 df-lim 5983 df-suc 5984 df-iota 6101 df-fun 6139 df-fn 6140 df-f 6141 df-f1 6142 df-fo 6143 df-f1o 6144 df-fv 6145 df-isom 6146 df-riota 6885 df-ov 6927 df-oprab 6928 df-mpt2 6929 df-of 7176 df-om 7346 df-1st 7447 df-2nd 7448 df-supp 7579 df-wrecs 7691 df-recs 7753 df-rdg 7791 df-1o 7845 df-2o 7846 df-oadd 7849 df-er 8028 df-map 8144 df-pm 8145 df-ixp 8197 df-en 8244 df-dom 8245 df-sdom 8246 df-fin 8247 df-fsupp 8566 df-fi 8607 df-sup 8638 df-inf 8639 df-oi 8706 df-card 9100 df-cda 9327 df-pnf 10415 df-mnf 10416 df-xr 10417 df-ltxr 10418 df-le 10419 df-sub 10610 df-neg 10611 df-div 11035 df-nn 11379 df-2 11442 df-3 11443 df-4 11444 df-5 11445 df-6 11446 df-7 11447 df-8 11448 df-9 11449 df-n0 11647 df-z 11733 df-dec 11850 df-uz 11997 df-q 12100 df-rp 12142 df-xneg 12261 df-xadd 12262 df-xmul 12263 df-ioo 12495 df-ioc 12496 df-ico 12497 df-icc 12498 df-fz 12648 df-fzo 12789 df-fl 12916 df-mod 12992 df-seq 13124 df-exp 13183 df-fac 13383 df-bc 13412 df-hash 13440 df-shft 14218 df-cj 14250 df-re 14251 df-im 14252 df-sqrt 14386 df-abs 14387 df-limsup 14614 df-clim 14631 df-rlim 14632 df-sum 14829 df-ef 15204 df-e 15205 df-sin 15206 df-cos 15207 df-pi 15209 df-dvds 15392 df-gcd 15627 df-prm 15795 df-pc 15950 df-struct 16261 df-ndx 16262 df-slot 16263 df-base 16265 df-sets 16266 df-ress 16267 df-plusg 16355 df-mulr 16356 df-starv 16357 df-sca 16358 df-vsca 16359 df-ip 16360 df-tset 16361 df-ple 16362 df-ds 16364 df-unif 16365 df-hom 16366 df-cco 16367 df-rest 16473 df-topn 16474 df-0g 16492 df-gsum 16493 df-topgen 16494 df-pt 16495 df-prds 16498 df-xrs 16552 df-qtop 16557 df-imas 16558 df-xps 16560 df-mre 16636 df-mrc 16637 df-acs 16639 df-mgm 17632 df-sgrp 17674 df-mnd 17685 df-submnd 17726 df-mulg 17932 df-cntz 18137 df-cmn 18585 df-psmet 20138 df-xmet 20139 df-met 20140 df-bl 20141 df-mopn 20142 df-fbas 20143 df-fg 20144 df-cnfld 20147 df-top 21110 df-topon 21127 df-topsp 21149 df-bases 21162 df-cld 21235 df-ntr 21236 df-cls 21237 df-nei 21314 df-lp 21352 df-perf 21353 df-cn 21443 df-cnp 21444 df-haus 21531 df-tx 21778 df-hmeo 21971 df-fil 22062 df-fm 22154 df-flim 22155 df-flf 22156 df-xms 22537 df-ms 22538 df-tms 22539 df-cncf 23093 df-limc 24071 df-dv 24072 df-log 24744 df-vma 25280 df-chp 25281

This theorem is referenced by: pntpbnd1 25731

W3C validator