lgamgulmlem3 - Metamath Proof Explorer

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

Theorem lgamgulmlem3 26189

Description: Lemma for lgamgulm 26193. (Contributed by Mario Carneiro, 3-Jul-2017.)

**Hypotheses**
Ref	Expression
lgamgulm.r	⊢ (𝜑 → 𝑅 ∈ ℕ)
lgamgulm.u	⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}
lgamgulm.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
lgamgulm.a	⊢ (𝜑 → 𝐴 ∈ 𝑈)
lgamgulm.l	⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁)

**Assertion**
Ref	Expression
lgamgulmlem3	⊢ (𝜑 → (abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑁↑2))))

Distinct variable groups: 𝑥,𝑁 𝑥,𝑘,𝑅 𝐴,𝑘,𝑥 𝜑,𝑥 Allowed substitution hints: 𝜑(𝑘) 𝑈(𝑥,𝑘) 𝑁(𝑘)

**Proof of Theorem lgamgulmlem3**
Step	Hyp	Ref	Expression
1		lgamgulm.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ ℕ)
2		lgamgulm.u	. . . . . . . 8 ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}
3	1, 2	lgamgulmlem1 26187	. . . . . . 7 ⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
4		lgamgulm.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
5	3, 4	sseldd 3923	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
6	5	eldifad 3900	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ ℂ)
7		lgamgulm.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ)
8	7	peano2nnd 11999	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ)
9	8	nnrpd 12779	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ⁺)
10	7	nnrpd 12779	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
11	9, 10	rpdivcld 12798	. . . . . . 7 ⊢ (𝜑 → ((𝑁 + 1) / 𝑁) ∈ ℝ⁺)
12	11	relogcld 25787	. . . . . 6 ⊢ (𝜑 → (log‘((𝑁 + 1) / 𝑁)) ∈ ℝ)
13	12	recnd 11012	. . . . 5 ⊢ (𝜑 → (log‘((𝑁 + 1) / 𝑁)) ∈ ℂ)
14	6, 13	mulcld 11004	. . . 4 ⊢ (𝜑 → (𝐴 · (log‘((𝑁 + 1) / 𝑁))) ∈ ℂ)
15	7	nncnd 11998	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℂ)
16	7	nnne0d 12032	. . . . . . 7 ⊢ (𝜑 → 𝑁 ≠ 0)
17	6, 15, 16	divcld 11760	. . . . . 6 ⊢ (𝜑 → (𝐴 / 𝑁) ∈ ℂ)
18		1cnd 10979	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℂ)
19	17, 18	addcld 11003	. . . . 5 ⊢ (𝜑 → ((𝐴 / 𝑁) + 1) ∈ ℂ)
20	5, 7	dmgmdivn0 26186	. . . . 5 ⊢ (𝜑 → ((𝐴 / 𝑁) + 1) ≠ 0)
21	19, 20	logcld 25735	. . . 4 ⊢ (𝜑 → (log‘((𝐴 / 𝑁) + 1)) ∈ ℂ)
22	14, 21	subcld 11341	. . 3 ⊢ (𝜑 → ((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (log‘((𝐴 / 𝑁) + 1))) ∈ ℂ)
23	22	abscld 15157	. 2 ⊢ (𝜑 → (abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (log‘((𝐴 / 𝑁) + 1)))) ∈ ℝ)
24	14, 17	subcld 11341	. . . 4 ⊢ (𝜑 → ((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (𝐴 / 𝑁)) ∈ ℂ)
25	24	abscld 15157	. . 3 ⊢ (𝜑 → (abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (𝐴 / 𝑁))) ∈ ℝ)
26	17, 21	subcld 11341	. . . 4 ⊢ (𝜑 → ((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))) ∈ ℂ)
27	26	abscld 15157	. . 3 ⊢ (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) ∈ ℝ)
28	25, 27	readdcld 11013	. 2 ⊢ (𝜑 → ((abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (𝐴 / 𝑁))) + (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))))) ∈ ℝ)
29	1	nnred 11997	. . 3 ⊢ (𝜑 → 𝑅 ∈ ℝ)
30		2re 12056	. . . . . 6 ⊢ 2 ∈ ℝ
31	30	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℝ)
32		1red 10985	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
33	29, 32	readdcld 11013	. . . . 5 ⊢ (𝜑 → (𝑅 + 1) ∈ ℝ)
34	31, 33	remulcld 11014	. . . 4 ⊢ (𝜑 → (2 · (𝑅 + 1)) ∈ ℝ)
35	7	nnsqcld 13968	. . . 4 ⊢ (𝜑 → (𝑁↑2) ∈ ℕ)
36	34, 35	nndivred 12036	. . 3 ⊢ (𝜑 → ((2 · (𝑅 + 1)) / (𝑁↑2)) ∈ ℝ)
37	29, 36	remulcld 11014	. 2 ⊢ (𝜑 → (𝑅 · ((2 · (𝑅 + 1)) / (𝑁↑2))) ∈ ℝ)
38	14, 21, 17	abs3difd 15181	. 2 ⊢ (𝜑 → (abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (log‘((𝐴 / 𝑁) + 1)))) ≤ ((abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (𝐴 / 𝑁))) + (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))))))
39	7	nnrecred 12033	. . . . . 6 ⊢ (𝜑 → (1 / 𝑁) ∈ ℝ)
40	8	nnrecred 12033	. . . . . 6 ⊢ (𝜑 → (1 / (𝑁 + 1)) ∈ ℝ)
41	39, 40	resubcld 11412	. . . . 5 ⊢ (𝜑 → ((1 / 𝑁) − (1 / (𝑁 + 1))) ∈ ℝ)
42	29, 41	remulcld 11014	. . . 4 ⊢ (𝜑 → (𝑅 · ((1 / 𝑁) − (1 / (𝑁 + 1)))) ∈ ℝ)
43	31, 29	remulcld 11014	. . . . . . . . 9 ⊢ (𝜑 → (2 · 𝑅) ∈ ℝ)
44	7	nnred 11997	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℝ)
45	1	nnrpd 12779	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℝ⁺)
46	29, 45	ltaddrpd 12814	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 < (𝑅 + 𝑅))
47	1	nncnd 11998	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ ℂ)
48	47	2timesd 12225	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑅) = (𝑅 + 𝑅))
49	46, 48	breqtrrd 5103	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 < (2 · 𝑅))
50		lgamgulm.l	. . . . . . . . 9 ⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁)
51	29, 43, 44, 49, 50	ltletrd 11144	. . . . . . . 8 ⊢ (𝜑 → 𝑅 < 𝑁)
52		difrp 12777	. . . . . . . . 9 ⊢ ((𝑅 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑅 < 𝑁 ↔ (𝑁 − 𝑅) ∈ ℝ⁺))
53	29, 44, 52	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝑅 < 𝑁 ↔ (𝑁 − 𝑅) ∈ ℝ⁺))
54	51, 53	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (𝑁 − 𝑅) ∈ ℝ⁺)
55	54	rprecred 12792	. . . . . 6 ⊢ (𝜑 → (1 / (𝑁 − 𝑅)) ∈ ℝ)
56	55, 39	resubcld 11412	. . . . 5 ⊢ (𝜑 → ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)) ∈ ℝ)
57	29, 56	remulcld 11014	. . . 4 ⊢ (𝜑 → (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) ∈ ℝ)
58	42, 57	readdcld 11013	. . 3 ⊢ (𝜑 → ((𝑅 · ((1 / 𝑁) − (1 / (𝑁 + 1)))) + (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) ∈ ℝ)
59	6, 15, 16	divrecd 11763	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 / 𝑁) = (𝐴 · (1 / 𝑁)))
60	59	oveq2d 7300	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (𝐴 / 𝑁)) = ((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (𝐴 · (1 / 𝑁))))
61	39	recnd 11012	. . . . . . . . 9 ⊢ (𝜑 → (1 / 𝑁) ∈ ℂ)
62	6, 13, 61	subdid 11440	. . . . . . . 8 ⊢ (𝜑 → (𝐴 · ((log‘((𝑁 + 1) / 𝑁)) − (1 / 𝑁))) = ((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (𝐴 · (1 / 𝑁))))
63	60, 62	eqtr4d 2782	. . . . . . 7 ⊢ (𝜑 → ((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (𝐴 / 𝑁)) = (𝐴 · ((log‘((𝑁 + 1) / 𝑁)) − (1 / 𝑁))))
64	63	fveq2d 6787	. . . . . 6 ⊢ (𝜑 → (abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (𝐴 / 𝑁))) = (abs‘(𝐴 · ((log‘((𝑁 + 1) / 𝑁)) − (1 / 𝑁)))))
65	13, 61	subcld 11341	. . . . . . 7 ⊢ (𝜑 → ((log‘((𝑁 + 1) / 𝑁)) − (1 / 𝑁)) ∈ ℂ)
66	6, 65	absmuld 15175	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐴 · ((log‘((𝑁 + 1) / 𝑁)) − (1 / 𝑁)))) = ((abs‘𝐴) · (abs‘((log‘((𝑁 + 1) / 𝑁)) − (1 / 𝑁)))))
67	64, 66	eqtrd 2779	. . . . 5 ⊢ (𝜑 → (abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (𝐴 / 𝑁))) = ((abs‘𝐴) · (abs‘((log‘((𝑁 + 1) / 𝑁)) − (1 / 𝑁)))))
68	6	abscld 15157	. . . . . 6 ⊢ (𝜑 → (abs‘𝐴) ∈ ℝ)
69	65	abscld 15157	. . . . . 6 ⊢ (𝜑 → (abs‘((log‘((𝑁 + 1) / 𝑁)) − (1 / 𝑁))) ∈ ℝ)
70	6	absge0d 15165	. . . . . 6 ⊢ (𝜑 → 0 ≤ (abs‘𝐴))
71	65	absge0d 15165	. . . . . 6 ⊢ (𝜑 → 0 ≤ (abs‘((log‘((𝑁 + 1) / 𝑁)) − (1 / 𝑁))))
72		fveq2 6783	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐴 → (abs‘𝑥) = (abs‘𝐴))
73	72	breq1d 5085	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐴 → ((abs‘𝑥) ≤ 𝑅 ↔ (abs‘𝐴) ≤ 𝑅))
74		fvoveq1 7307	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝐴 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝐴 + 𝑘)))
75	74	breq2d 5087	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝐴 → ((1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
76	75	ralbidv 3113	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐴 → (∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
77	73, 76	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘)))))
78	77, 2	elrab2 3628	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝑈 ↔ (𝐴 ∈ ℂ ∧ ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘)))))
79	78	simprbi 497	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑈 → ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
80	4, 79	syl 17	. . . . . . 7 ⊢ (𝜑 → ((abs‘𝐴) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝐴 + 𝑘))))
81	80	simpld 495	. . . . . 6 ⊢ (𝜑 → (abs‘𝐴) ≤ 𝑅)
82	9, 10	relogdivd 25790	. . . . . . . . 9 ⊢ (𝜑 → (log‘((𝑁 + 1) / 𝑁)) = ((log‘(𝑁 + 1)) − (log‘𝑁)))
83		logdifbnd 26152	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℝ⁺ → ((log‘(𝑁 + 1)) − (log‘𝑁)) ≤ (1 / 𝑁))
84	10, 83	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((log‘(𝑁 + 1)) − (log‘𝑁)) ≤ (1 / 𝑁))
85	82, 84	eqbrtrd 5097	. . . . . . . 8 ⊢ (𝜑 → (log‘((𝑁 + 1) / 𝑁)) ≤ (1 / 𝑁))
86	12, 39, 85	abssuble0d 15153	. . . . . . 7 ⊢ (𝜑 → (abs‘((log‘((𝑁 + 1) / 𝑁)) − (1 / 𝑁))) = ((1 / 𝑁) − (log‘((𝑁 + 1) / 𝑁))))
87		logdiflbnd 26153	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℝ⁺ → (1 / (𝑁 + 1)) ≤ ((log‘(𝑁 + 1)) − (log‘𝑁)))
88	10, 87	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (1 / (𝑁 + 1)) ≤ ((log‘(𝑁 + 1)) − (log‘𝑁)))
89	88, 82	breqtrrd 5103	. . . . . . . 8 ⊢ (𝜑 → (1 / (𝑁 + 1)) ≤ (log‘((𝑁 + 1) / 𝑁)))
90	40, 12, 39, 89	lesub2dd 11601	. . . . . . 7 ⊢ (𝜑 → ((1 / 𝑁) − (log‘((𝑁 + 1) / 𝑁))) ≤ ((1 / 𝑁) − (1 / (𝑁 + 1))))
91	86, 90	eqbrtrd 5097	. . . . . 6 ⊢ (𝜑 → (abs‘((log‘((𝑁 + 1) / 𝑁)) − (1 / 𝑁))) ≤ ((1 / 𝑁) − (1 / (𝑁 + 1))))
92	68, 29, 69, 41, 70, 71, 81, 91	lemul12ad 11926	. . . . 5 ⊢ (𝜑 → ((abs‘𝐴) · (abs‘((log‘((𝑁 + 1) / 𝑁)) − (1 / 𝑁)))) ≤ (𝑅 · ((1 / 𝑁) − (1 / (𝑁 + 1)))))
93	67, 92	eqbrtrd 5097	. . . 4 ⊢ (𝜑 → (abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (𝐴 / 𝑁))) ≤ (𝑅 · ((1 / 𝑁) − (1 / (𝑁 + 1)))))
94	1, 2, 7, 4, 50	lgamgulmlem2 26188	. . . 4 ⊢ (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))
95	25, 27, 42, 57, 93, 94	le2addd 11603	. . 3 ⊢ (𝜑 → ((abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (𝐴 / 𝑁))) + (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))))) ≤ ((𝑅 · ((1 / 𝑁) − (1 / (𝑁 + 1)))) + (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))))
96	15, 47	subcld 11341	. . . . . . . 8 ⊢ (𝜑 → (𝑁 − 𝑅) ∈ ℂ)
97	15, 18	addcld 11003	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ∈ ℂ)
98	29, 51	gtned 11119	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ≠ 𝑅)
99	15, 47, 98	subne0d 11350	. . . . . . . 8 ⊢ (𝜑 → (𝑁 − 𝑅) ≠ 0)
100	8	nnne0d 12032	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ≠ 0)
101	96, 97, 99, 100	subrecd 11815	. . . . . . 7 ⊢ (𝜑 → ((1 / (𝑁 − 𝑅)) − (1 / (𝑁 + 1))) = (((𝑁 + 1) − (𝑁 − 𝑅)) / ((𝑁 − 𝑅) · (𝑁 + 1))))
102	15, 18, 47	pnncand 11380	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + 1) − (𝑁 − 𝑅)) = (1 + 𝑅))
103	18, 47, 102	comraddd 11198	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 + 1) − (𝑁 − 𝑅)) = (𝑅 + 1))
104	103	oveq1d 7299	. . . . . . 7 ⊢ (𝜑 → (((𝑁 + 1) − (𝑁 − 𝑅)) / ((𝑁 − 𝑅) · (𝑁 + 1))) = ((𝑅 + 1) / ((𝑁 − 𝑅) · (𝑁 + 1))))
105	101, 104	eqtr2d 2780	. . . . . 6 ⊢ (𝜑 → ((𝑅 + 1) / ((𝑁 − 𝑅) · (𝑁 + 1))) = ((1 / (𝑁 − 𝑅)) − (1 / (𝑁 + 1))))
106	105	oveq2d 7300	. . . . 5 ⊢ (𝜑 → (𝑅 · ((𝑅 + 1) / ((𝑁 − 𝑅) · (𝑁 + 1)))) = (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / (𝑁 + 1)))))
107	97, 100	reccld 11753	. . . . . . . 8 ⊢ (𝜑 → (1 / (𝑁 + 1)) ∈ ℂ)
108	96, 99	reccld 11753	. . . . . . . 8 ⊢ (𝜑 → (1 / (𝑁 − 𝑅)) ∈ ℂ)
109	61, 107, 108	npncan3d 11377	. . . . . . 7 ⊢ (𝜑 → (((1 / 𝑁) − (1 / (𝑁 + 1))) + ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))) = ((1 / (𝑁 − 𝑅)) − (1 / (𝑁 + 1))))
110	109	eqcomd 2745	. . . . . 6 ⊢ (𝜑 → ((1 / (𝑁 − 𝑅)) − (1 / (𝑁 + 1))) = (((1 / 𝑁) − (1 / (𝑁 + 1))) + ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))
111	110	oveq2d 7300	. . . . 5 ⊢ (𝜑 → (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / (𝑁 + 1)))) = (𝑅 · (((1 / 𝑁) − (1 / (𝑁 + 1))) + ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))))
112	41	recnd 11012	. . . . . 6 ⊢ (𝜑 → ((1 / 𝑁) − (1 / (𝑁 + 1))) ∈ ℂ)
113	56	recnd 11012	. . . . . 6 ⊢ (𝜑 → ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)) ∈ ℂ)
114	47, 112, 113	adddid 11008	. . . . 5 ⊢ (𝜑 → (𝑅 · (((1 / 𝑁) − (1 / (𝑁 + 1))) + ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) = ((𝑅 · ((1 / 𝑁) − (1 / (𝑁 + 1)))) + (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))))
115	106, 111, 114	3eqtrd 2783	. . . 4 ⊢ (𝜑 → (𝑅 · ((𝑅 + 1) / ((𝑁 − 𝑅) · (𝑁 + 1)))) = ((𝑅 · ((1 / 𝑁) − (1 / (𝑁 + 1)))) + (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))))
116	54, 9	rpmulcld 12797	. . . . . 6 ⊢ (𝜑 → ((𝑁 − 𝑅) · (𝑁 + 1)) ∈ ℝ⁺)
117	33, 116	rerpdivcld 12812	. . . . 5 ⊢ (𝜑 → ((𝑅 + 1) / ((𝑁 − 𝑅) · (𝑁 + 1))) ∈ ℝ)
118	45	rpge0d 12785	. . . . 5 ⊢ (𝜑 → 0 ≤ 𝑅)
119		2z 12361	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
120	119	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 2 ∈ ℤ)
121	10, 120	rpexpcld 13971	. . . . . . . 8 ⊢ (𝜑 → (𝑁↑2) ∈ ℝ⁺)
122	121	rphalfcld 12793	. . . . . . 7 ⊢ (𝜑 → ((𝑁↑2) / 2) ∈ ℝ⁺)
123		0le1 11507	. . . . . . . . 9 ⊢ 0 ≤ 1
124	123	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 1)
125	29, 32, 118, 124	addge0d 11560	. . . . . . 7 ⊢ (𝜑 → 0 ≤ (𝑅 + 1))
126	15	sqvald 13870	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁↑2) = (𝑁 · 𝑁))
127	126	oveq1d 7299	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁↑2) / 2) = ((𝑁 · 𝑁) / 2))
128	31	recnd 11012	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℂ)
129		2ne0 12086	. . . . . . . . . . 11 ⊢ 2 ≠ 0
130	129	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ≠ 0)
131	15, 15, 128, 130	div23d 11797	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 · 𝑁) / 2) = ((𝑁 / 2) · 𝑁))
132	127, 131	eqtrd 2779	. . . . . . . 8 ⊢ (𝜑 → ((𝑁↑2) / 2) = ((𝑁 / 2) · 𝑁))
133	44	rehalfcld 12229	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 / 2) ∈ ℝ)
134	44, 29	resubcld 11412	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 − 𝑅) ∈ ℝ)
135	44, 32	readdcld 11013	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
136		2rp 12744	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ⁺
137	136	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 2 ∈ ℝ⁺)
138	10	rpge0d 12785	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 𝑁)
139	44, 137, 138	divge0d 12821	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝑁 / 2))
140	29, 44, 137	lemuldiv2d 12831	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 𝑅) ≤ 𝑁 ↔ 𝑅 ≤ (𝑁 / 2)))
141	50, 140	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ≤ (𝑁 / 2))
142	15	2halvesd 12228	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = 𝑁)
143	133	recnd 11012	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 / 2) ∈ ℂ)
144	15, 143, 143	subaddd 11359	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 − (𝑁 / 2)) = (𝑁 / 2) ↔ ((𝑁 / 2) + (𝑁 / 2)) = 𝑁))
145	142, 144	mpbird 256	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − (𝑁 / 2)) = (𝑁 / 2))
146	141, 145	breqtrrd 5103	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ≤ (𝑁 − (𝑁 / 2)))
147	29, 44, 133, 146	lesubd 11588	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 / 2) ≤ (𝑁 − 𝑅))
148	44	lep1d 11915	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1))
149	133, 134, 44, 135, 139, 138, 147, 148	lemul12ad 11926	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 / 2) · 𝑁) ≤ ((𝑁 − 𝑅) · (𝑁 + 1)))
150	132, 149	eqbrtrd 5097	. . . . . . 7 ⊢ (𝜑 → ((𝑁↑2) / 2) ≤ ((𝑁 − 𝑅) · (𝑁 + 1)))
151	122, 116, 33, 125, 150	lediv2ad 12803	. . . . . 6 ⊢ (𝜑 → ((𝑅 + 1) / ((𝑁 − 𝑅) · (𝑁 + 1))) ≤ ((𝑅 + 1) / ((𝑁↑2) / 2)))
152	1	peano2nnd 11999	. . . . . . . . 9 ⊢ (𝜑 → (𝑅 + 1) ∈ ℕ)
153	152	nncnd 11998	. . . . . . . 8 ⊢ (𝜑 → (𝑅 + 1) ∈ ℂ)
154	35	nncnd 11998	. . . . . . . 8 ⊢ (𝜑 → (𝑁↑2) ∈ ℂ)
155	35	nnne0d 12032	. . . . . . . 8 ⊢ (𝜑 → (𝑁↑2) ≠ 0)
156	153, 154, 128, 155, 130	divdiv2d 11792	. . . . . . 7 ⊢ (𝜑 → ((𝑅 + 1) / ((𝑁↑2) / 2)) = (((𝑅 + 1) · 2) / (𝑁↑2)))
157	153, 128	mulcomd 11005	. . . . . . . 8 ⊢ (𝜑 → ((𝑅 + 1) · 2) = (2 · (𝑅 + 1)))
158	157	oveq1d 7299	. . . . . . 7 ⊢ (𝜑 → (((𝑅 + 1) · 2) / (𝑁↑2)) = ((2 · (𝑅 + 1)) / (𝑁↑2)))
159	156, 158	eqtr2d 2780	. . . . . 6 ⊢ (𝜑 → ((2 · (𝑅 + 1)) / (𝑁↑2)) = ((𝑅 + 1) / ((𝑁↑2) / 2)))
160	151, 159	breqtrrd 5103	. . . . 5 ⊢ (𝜑 → ((𝑅 + 1) / ((𝑁 − 𝑅) · (𝑁 + 1))) ≤ ((2 · (𝑅 + 1)) / (𝑁↑2)))
161	117, 36, 29, 118, 160	lemul2ad 11924	. . . 4 ⊢ (𝜑 → (𝑅 · ((𝑅 + 1) / ((𝑁 − 𝑅) · (𝑁 + 1)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑁↑2))))
162	115, 161	eqbrtrrd 5099	. . 3 ⊢ (𝜑 → ((𝑅 · ((1 / 𝑁) − (1 / (𝑁 + 1)))) + (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑁↑2))))
163	28, 58, 37, 95, 162	letrd 11141	. 2 ⊢ (𝜑 → ((abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (𝐴 / 𝑁))) + (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1))))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑁↑2))))
164	23, 28, 37, 38, 163	letrd 11141	1 ⊢ (𝜑 → (abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑁↑2))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2107 ≠ wne 2944 ∀wral 3065 {crab 3069 ∖ cdif 3885 class class class wbr 5075 ‘cfv 6437 (class class class)co 7284 ℂcc 10878 ℝcr 10879 0cc0 10880 1c1 10881 + caddc 10883 · cmul 10885 < clt 11018 ≤ cle 11019 − cmin 11214 / cdiv 11641 ℕcn 11982 2c2 12037 ℕ₀cn0 12242 ℤcz 12328 ℝ⁺crp 12739 ↑cexp 13791 abscabs 14954 logclog 25719

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-rep 5210 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-inf2 9408 ax-cnex 10936 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957 ax-pre-sup 10958 ax-addf 10959 ax-mulf 10960

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-rmo 3072 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4841 df-int 4881 df-iun 4927 df-iin 4928 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-se 5546 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-isom 6446 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-of 7542 df-om 7722 df-1st 7840 df-2nd 7841 df-supp 7987 df-frecs 8106 df-wrecs 8137 df-recs 8211 df-rdg 8250 df-1o 8306 df-2o 8307 df-er 8507 df-map 8626 df-pm 8627 df-ixp 8695 df-en 8743 df-dom 8744 df-sdom 8745 df-fin 8746 df-fsupp 9138 df-fi 9179 df-sup 9210 df-inf 9211 df-oi 9278 df-card 9706 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-div 11642 df-nn 11983 df-2 12045 df-3 12046 df-4 12047 df-5 12048 df-6 12049 df-7 12050 df-8 12051 df-9 12052 df-n0 12243 df-z 12329 df-dec 12447 df-uz 12592 df-q 12698 df-rp 12740 df-xneg 12857 df-xadd 12858 df-xmul 12859 df-ioo 13092 df-ioc 13093 df-ico 13094 df-icc 13095 df-fz 13249 df-fzo 13392 df-fl 13521 df-mod 13599 df-seq 13731 df-exp 13792 df-fac 13997 df-bc 14026 df-hash 14054 df-shft 14787 df-cj 14819 df-re 14820 df-im 14821 df-sqrt 14955 df-abs 14956 df-limsup 15189 df-clim 15206 df-rlim 15207 df-sum 15407 df-ef 15786 df-sin 15788 df-cos 15789 df-tan 15790 df-pi 15791 df-struct 16857 df-sets 16874 df-slot 16892 df-ndx 16904 df-base 16922 df-ress 16951 df-plusg 16984 df-mulr 16985 df-starv 16986 df-sca 16987 df-vsca 16988 df-ip 16989 df-tset 16990 df-ple 16991 df-ds 16993 df-unif 16994 df-hom 16995 df-cco 16996 df-rest 17142 df-topn 17143 df-0g 17161 df-gsum 17162 df-topgen 17163 df-pt 17164 df-prds 17167 df-xrs 17222 df-qtop 17227 df-imas 17228 df-xps 17230 df-mre 17304 df-mrc 17305 df-acs 17307 df-mgm 18335 df-sgrp 18384 df-mnd 18395 df-submnd 18440 df-mulg 18710 df-cntz 18932 df-cmn 19397 df-psmet 20598 df-xmet 20599 df-met 20600 df-bl 20601 df-mopn 20602 df-fbas 20603 df-fg 20604 df-cnfld 20607 df-top 22052 df-topon 22069 df-topsp 22091 df-bases 22105 df-cld 22179 df-ntr 22180 df-cls 22181 df-nei 22258 df-lp 22296 df-perf 22297 df-cn 22387 df-cnp 22388 df-haus 22475 df-cmp 22547 df-tx 22722 df-hmeo 22915 df-fil 23006 df-fm 23098 df-flim 23099 df-flf 23100 df-xms 23482 df-ms 23483 df-tms 23484 df-cncf 24050 df-limc 25039 df-dv 25040 df-log 25721

This theorem is referenced by: lgamgulmlem5 26191

W3C validator