Theorem lgamgulmlem5

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

	Ref	Expression
Hypotheses	lgamgulm.r	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
	lgamgulm.u	⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
	lgamgulm.g	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
	lgamgulm.t	⊢ 𝑇 = ( 𝑚 ∈ ℕ ↦ if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) )
Assertion	lgamgulmlem5	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑦 ) ) ≤ ( 𝑇 ‘ 𝑛 ) )

Proof

Step	Hyp	Ref	Expression
1		lgamgulm.r	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
2		lgamgulm.u	⊢ 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
3		lgamgulm.g	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
4		lgamgulm.t	⊢ 𝑇 = ( 𝑚 ∈ ℕ ↦ if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) )
5		breq2	⊢ ( ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) = if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) → ( ( abs ‘ ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ≤ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) ↔ ( abs ‘ ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ≤ if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) ) )
6		breq2	⊢ ( ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) = if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) → ( ( abs ‘ ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ≤ ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ↔ ( abs ‘ ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ≤ if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) ) )
7	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑅 ∈ ℕ )
8	7	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 2 · 𝑅 ) ≤ 𝑛 ) → 𝑅 ∈ ℕ )
9		fveq2	⊢ ( 𝑥 = 𝑡 → ( abs ‘ 𝑥 ) = ( abs ‘ 𝑡 ) )
10	9	breq1d	⊢ ( 𝑥 = 𝑡 → ( ( abs ‘ 𝑥 ) ≤ 𝑅 ↔ ( abs ‘ 𝑡 ) ≤ 𝑅 ) )
11		fvoveq1	⊢ ( 𝑥 = 𝑡 → ( abs ‘ ( 𝑥 + 𝑘 ) ) = ( abs ‘ ( 𝑡 + 𝑘 ) ) )
12	11	breq2d	⊢ ( 𝑥 = 𝑡 → ( ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ↔ ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑡 + 𝑘 ) ) ) )
13	12	ralbidv	⊢ ( 𝑥 = 𝑡 → ( ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ↔ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑡 + 𝑘 ) ) ) )
14	10 13	anbi12d	⊢ ( 𝑥 = 𝑡 → ( ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ↔ ( ( abs ‘ 𝑡 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑡 + 𝑘 ) ) ) ) )
15	14	cbvrabv	⊢ { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) } = { 𝑡 ∈ ℂ ∣ ( ( abs ‘ 𝑡 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑡 + 𝑘 ) ) ) }
16	2 15	eqtri	⊢ 𝑈 = { 𝑡 ∈ ℂ ∣ ( ( abs ‘ 𝑡 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑡 + 𝑘 ) ) ) }
17		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 2 · 𝑅 ) ≤ 𝑛 ) → 𝑛 ∈ ℕ )
18		simprr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑈 )
19	18	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 2 · 𝑅 ) ≤ 𝑛 ) → 𝑦 ∈ 𝑈 )
20		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 2 · 𝑅 ) ≤ 𝑛 ) → ( 2 · 𝑅 ) ≤ 𝑛 )
21	8 16 17 19 20	lgamgulmlem3	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) ∧ ( 2 · 𝑅 ) ≤ 𝑛 ) → ( abs ‘ ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ≤ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) )
22	1 2	lgamgulmlem1	⊢ ( 𝜑 → 𝑈 ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
23	22	adantr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑈 ⊆ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
24	23 18	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
25	24	eldifad	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ ℂ )
26		simprl	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑛 ∈ ℕ )
27	26	peano2nnd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑛 + 1 ) ∈ ℕ )
28	27	nnrpd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑛 + 1 ) ∈ ℝ+ )
29	26	nnrpd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑛 ∈ ℝ+ )
30	28 29	rpdivcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑛 + 1 ) / 𝑛 ) ∈ ℝ+ )
31	30	relogcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ∈ ℝ )
32	31	recnd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ∈ ℂ )
33	25 32	mulcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ∈ ℂ )
34	26	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑛 ∈ ℂ )
35	26	nnne0d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑛 ≠ 0 )
36	25 34 35	divcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑦 / 𝑛 ) ∈ ℂ )
37		1cnd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 1 ∈ ℂ )
38	36 37	addcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑦 / 𝑛 ) + 1 ) ∈ ℂ )
39	24 26	dmgmdivn0	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑦 / 𝑛 ) + 1 ) ≠ 0 )
40	38 39	logcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ∈ ℂ )
41	33 40	subcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ∈ ℂ )
42	41	abscld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ∈ ℝ )
43	33	abscld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) ∈ ℝ )
44	40	abscld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ∈ ℝ )
45	43 44	readdcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) + ( abs ‘ ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ∈ ℝ )
46	7	nnred	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑅 ∈ ℝ )
47	46 31	remulcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ∈ ℝ )
48	7	peano2nnd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑅 + 1 ) ∈ ℕ )
49	48	nnrpd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑅 + 1 ) ∈ ℝ+ )
50	49 29	rpmulcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑅 + 1 ) · 𝑛 ) ∈ ℝ+ )
51	50	relogcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) ∈ ℝ )
52		pire	⊢ π ∈ ℝ
53	52	a1i	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → π ∈ ℝ )
54	51 53	readdcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ∈ ℝ )
55	47 54	readdcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ∈ ℝ )
56	33 40	abs2dif2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ≤ ( ( abs ‘ ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) + ( abs ‘ ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) )
57	25 32	absmuld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) = ( ( abs ‘ 𝑦 ) · ( abs ‘ ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) )
58	30	rpred	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑛 + 1 ) / 𝑛 ) ∈ ℝ )
59	34	mullidd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 1 · 𝑛 ) = 𝑛 )
60	26	nnred	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑛 ∈ ℝ )
61	60	lep1d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑛 ≤ ( 𝑛 + 1 ) )
62	59 61	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 1 · 𝑛 ) ≤ ( 𝑛 + 1 ) )
63		1red	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 1 ∈ ℝ )
64	60 63	readdcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑛 + 1 ) ∈ ℝ )
65	63 64 29	lemuldivd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 1 · 𝑛 ) ≤ ( 𝑛 + 1 ) ↔ 1 ≤ ( ( 𝑛 + 1 ) / 𝑛 ) ) )
66	62 65	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 1 ≤ ( ( 𝑛 + 1 ) / 𝑛 ) )
67	58 66	logge0d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 0 ≤ ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) )
68	31 67	absidd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) = ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) )
69	68	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ 𝑦 ) · ( abs ‘ ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) = ( ( abs ‘ 𝑦 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) )
70	57 69	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) = ( ( abs ‘ 𝑦 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) )
71	25	abscld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ 𝑦 ) ∈ ℝ )
72		fveq2	⊢ ( 𝑥 = 𝑦 → ( abs ‘ 𝑥 ) = ( abs ‘ 𝑦 ) )
73	72	breq1d	⊢ ( 𝑥 = 𝑦 → ( ( abs ‘ 𝑥 ) ≤ 𝑅 ↔ ( abs ‘ 𝑦 ) ≤ 𝑅 ) )
74		fvoveq1	⊢ ( 𝑥 = 𝑦 → ( abs ‘ ( 𝑥 + 𝑘 ) ) = ( abs ‘ ( 𝑦 + 𝑘 ) ) )
75	74	breq2d	⊢ ( 𝑥 = 𝑦 → ( ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ↔ ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑦 + 𝑘 ) ) ) )
76	75	ralbidv	⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ↔ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑦 + 𝑘 ) ) ) )
77	73 76	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) ↔ ( ( abs ‘ 𝑦 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑦 + 𝑘 ) ) ) ) )
78	77 2	elrab2	⊢ ( 𝑦 ∈ 𝑈 ↔ ( 𝑦 ∈ ℂ ∧ ( ( abs ‘ 𝑦 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑦 + 𝑘 ) ) ) ) )
79	78	simprbi	⊢ ( 𝑦 ∈ 𝑈 → ( ( abs ‘ 𝑦 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑦 + 𝑘 ) ) ) )
80	79	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ 𝑦 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑦 + 𝑘 ) ) ) )
81	80	simpld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ 𝑦 ) ≤ 𝑅 )
82	71 46 31 67 81	lemul1ad	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ 𝑦 ) · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ≤ ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) )
83	70 82	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) ≤ ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) )
84	38 39	absrpcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ∈ ℝ+ )
85	84	relogcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ∈ ℝ )
86	85	recnd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ∈ ℂ )
87	86	abscld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ∈ ℝ )
88	87 53	readdcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) + π ) ∈ ℝ )
89		abslogle	⊢ ( ( ( ( 𝑦 / 𝑛 ) + 1 ) ∈ ℂ ∧ ( ( 𝑦 / 𝑛 ) + 1 ) ≠ 0 ) → ( abs ‘ ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ≤ ( ( abs ‘ ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) + π ) )
90	38 39 89	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ≤ ( ( abs ‘ ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) + π ) )
91		1rp	⊢ 1 ∈ ℝ+
92		relogdiv	⊢ ( ( 1 ∈ ℝ+ ∧ ( ( 𝑅 + 1 ) · 𝑛 ) ∈ ℝ+ ) → ( log ‘ ( 1 / ( ( 𝑅 + 1 ) · 𝑛 ) ) ) = ( ( log ‘ 1 ) − ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) ) )
93	91 50 92	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( log ‘ ( 1 / ( ( 𝑅 + 1 ) · 𝑛 ) ) ) = ( ( log ‘ 1 ) − ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) ) )
94		log1	⊢ ( log ‘ 1 ) = 0
95	94	oveq1i	⊢ ( ( log ‘ 1 ) − ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) ) = ( 0 − ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) )
96		df-neg	⊢ - ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) = ( 0 − ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) )
97	95 96	eqtr4i	⊢ ( ( log ‘ 1 ) − ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) ) = - ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) )
98	93 97	eqtr2di	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → - ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) = ( log ‘ ( 1 / ( ( 𝑅 + 1 ) · 𝑛 ) ) ) )
99	48	nnrecred	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 1 / ( 𝑅 + 1 ) ) ∈ ℝ )
100	25 34	addcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑦 + 𝑛 ) ∈ ℂ )
101	100	abscld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( 𝑦 + 𝑛 ) ) ∈ ℝ )
102	7	nnrecred	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 1 / 𝑅 ) ∈ ℝ )
103	7	nnrpd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑅 ∈ ℝ+ )
104		0le1	⊢ 0 ≤ 1
105	104	a1i	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 0 ≤ 1 )
106	46	lep1d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑅 ≤ ( 𝑅 + 1 ) )
107	103 49 63 105 106	lediv2ad	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 1 / ( 𝑅 + 1 ) ) ≤ ( 1 / 𝑅 ) )
108		oveq2	⊢ ( 𝑘 = 𝑛 → ( 𝑦 + 𝑘 ) = ( 𝑦 + 𝑛 ) )
109	108	fveq2d	⊢ ( 𝑘 = 𝑛 → ( abs ‘ ( 𝑦 + 𝑘 ) ) = ( abs ‘ ( 𝑦 + 𝑛 ) ) )
110	109	breq2d	⊢ ( 𝑘 = 𝑛 → ( ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑦 + 𝑘 ) ) ↔ ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑦 + 𝑛 ) ) ) )
111	80	simprd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑦 + 𝑘 ) ) )
112	26	nnnn0d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑛 ∈ ℕ0 )
113	110 111 112	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑦 + 𝑛 ) ) )
114	99 102 101 107 113	letrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 1 / ( 𝑅 + 1 ) ) ≤ ( abs ‘ ( 𝑦 + 𝑛 ) ) )
115	99 101 29 114	lediv1dd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 1 / ( 𝑅 + 1 ) ) / 𝑛 ) ≤ ( ( abs ‘ ( 𝑦 + 𝑛 ) ) / 𝑛 ) )
116	48	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑅 + 1 ) ∈ ℂ )
117	48	nnne0d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑅 + 1 ) ≠ 0 )
118	116 34 117 35	recdiv2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 1 / ( 𝑅 + 1 ) ) / 𝑛 ) = ( 1 / ( ( 𝑅 + 1 ) · 𝑛 ) ) )
119	25 34 34 35	divdird	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑦 + 𝑛 ) / 𝑛 ) = ( ( 𝑦 / 𝑛 ) + ( 𝑛 / 𝑛 ) ) )
120	34 35	dividd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑛 / 𝑛 ) = 1 )
121	120	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑦 / 𝑛 ) + ( 𝑛 / 𝑛 ) ) = ( ( 𝑦 / 𝑛 ) + 1 ) )
122	119 121	eqtr2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑦 / 𝑛 ) + 1 ) = ( ( 𝑦 + 𝑛 ) / 𝑛 ) )
123	122	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) = ( abs ‘ ( ( 𝑦 + 𝑛 ) / 𝑛 ) ) )
124	100 34 35	absdivd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝑦 + 𝑛 ) / 𝑛 ) ) = ( ( abs ‘ ( 𝑦 + 𝑛 ) ) / ( abs ‘ 𝑛 ) ) )
125	29	rpge0d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 0 ≤ 𝑛 )
126	60 125	absidd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ 𝑛 ) = 𝑛 )
127	126	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ ( 𝑦 + 𝑛 ) ) / ( abs ‘ 𝑛 ) ) = ( ( abs ‘ ( 𝑦 + 𝑛 ) ) / 𝑛 ) )
128	123 124 127	3eqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ ( 𝑦 + 𝑛 ) ) / 𝑛 ) = ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) )
129	115 118 128	3brtr3d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 1 / ( ( 𝑅 + 1 ) · 𝑛 ) ) ≤ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) )
130	50	rpreccld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 1 / ( ( 𝑅 + 1 ) · 𝑛 ) ) ∈ ℝ+ )
131	130 84	logled	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 1 / ( ( 𝑅 + 1 ) · 𝑛 ) ) ≤ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ↔ ( log ‘ ( 1 / ( ( 𝑅 + 1 ) · 𝑛 ) ) ) ≤ ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) )
132	129 131	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( log ‘ ( 1 / ( ( 𝑅 + 1 ) · 𝑛 ) ) ) ≤ ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) )
133	98 132	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → - ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) ≤ ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) )
134	38	abscld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ∈ ℝ )
135	46 63	readdcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑅 + 1 ) ∈ ℝ )
136	50	rpred	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑅 + 1 ) · 𝑛 ) ∈ ℝ )
137	36	abscld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( 𝑦 / 𝑛 ) ) ∈ ℝ )
138	137 63	readdcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ ( 𝑦 / 𝑛 ) ) + 1 ) ∈ ℝ )
139	36 37	abstrid	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ≤ ( ( abs ‘ ( 𝑦 / 𝑛 ) ) + ( abs ‘ 1 ) ) )
140		abs1	⊢ ( abs ‘ 1 ) = 1
141	140	oveq2i	⊢ ( ( abs ‘ ( 𝑦 / 𝑛 ) ) + ( abs ‘ 1 ) ) = ( ( abs ‘ ( 𝑦 / 𝑛 ) ) + 1 )
142	139 141	breqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ≤ ( ( abs ‘ ( 𝑦 / 𝑛 ) ) + 1 ) )
143	91	a1i	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 1 ∈ ℝ+ )
144	25	absge0d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 0 ≤ ( abs ‘ 𝑦 ) )
145	26	nnge1d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 1 ≤ 𝑛 )
146	71 46 143 60 144 81 145	lediv12ad	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ 𝑦 ) / 𝑛 ) ≤ ( 𝑅 / 1 ) )
147	25 34 35	absdivd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( 𝑦 / 𝑛 ) ) = ( ( abs ‘ 𝑦 ) / ( abs ‘ 𝑛 ) ) )
148	126	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ 𝑦 ) / ( abs ‘ 𝑛 ) ) = ( ( abs ‘ 𝑦 ) / 𝑛 ) )
149	147 148	eqtr2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ 𝑦 ) / 𝑛 ) = ( abs ‘ ( 𝑦 / 𝑛 ) ) )
150	7	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 𝑅 ∈ ℂ )
151	150	div1d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑅 / 1 ) = 𝑅 )
152	146 149 151	3brtr3d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( 𝑦 / 𝑛 ) ) ≤ 𝑅 )
153	137 46 63 152	leadd1dd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ ( 𝑦 / 𝑛 ) ) + 1 ) ≤ ( 𝑅 + 1 ) )
154	134 138 135 142 153	letrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ≤ ( 𝑅 + 1 ) )
155	49	rpge0d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → 0 ≤ ( 𝑅 + 1 ) )
156	135 60 155 145	lemulge11d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑅 + 1 ) ≤ ( ( 𝑅 + 1 ) · 𝑛 ) )
157	134 135 136 154 156	letrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ≤ ( ( 𝑅 + 1 ) · 𝑛 ) )
158	84 50	logled	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ≤ ( ( 𝑅 + 1 ) · 𝑛 ) ↔ ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ≤ ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) ) )
159	157 158	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ≤ ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) )
160	85 51	absled	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ≤ ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) ↔ ( - ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) ≤ ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ∧ ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ≤ ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) ) ) )
161	133 159 160	mpbir2and	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ≤ ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) )
162	87 51 53 161	leadd1dd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ ( log ‘ ( abs ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) + π ) ≤ ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) )
163	44 88 54 90 162	letrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ≤ ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) )
164	43 44 47 54 83 163	le2addd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( abs ‘ ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ) + ( abs ‘ ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ≤ ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) )
165	42 45 55 56 164	letrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ≤ ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) )
166	165	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) ∧ ¬ ( 2 · 𝑅 ) ≤ 𝑛 ) → ( abs ‘ ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ≤ ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) )
167	5 6 21 166	ifbothda	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) ≤ if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) )
168		oveq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 + 1 ) = ( 𝑛 + 1 ) )
169		id	⊢ ( 𝑚 = 𝑛 → 𝑚 = 𝑛 )
170	168 169	oveq12d	⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 + 1 ) / 𝑚 ) = ( ( 𝑛 + 1 ) / 𝑛 ) )
171	170	fveq2d	⊢ ( 𝑚 = 𝑛 → ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) = ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) )
172	171	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) = ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) )
173		oveq2	⊢ ( 𝑚 = 𝑛 → ( 𝑧 / 𝑚 ) = ( 𝑧 / 𝑛 ) )
174	173	fvoveq1d	⊢ ( 𝑚 = 𝑛 → ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) = ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) )
175	172 174	oveq12d	⊢ ( 𝑚 = 𝑛 → ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) = ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) )
176	175	mpteq2dv	⊢ ( 𝑚 = 𝑛 → ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) = ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) ) )
177		cnex	⊢ ℂ ∈ V
178	2 177	rabex2	⊢ 𝑈 ∈ V
179	178	mptex	⊢ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) ) ∈ V
180	176 3 179	fvmpt	⊢ ( 𝑛 ∈ ℕ → ( 𝐺 ‘ 𝑛 ) = ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) ) )
181	180	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝐺 ‘ 𝑛 ) = ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) ) )
182	181	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑦 ) = ( ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) ) ‘ 𝑦 ) )
183		oveq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) = ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) )
184		oveq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 / 𝑛 ) = ( 𝑦 / 𝑛 ) )
185	184	fvoveq1d	⊢ ( 𝑧 = 𝑦 → ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) = ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) )
186	183 185	oveq12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) = ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) )
187		eqid	⊢ ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) ) = ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) )
188		ovex	⊢ ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ∈ V
189	186 187 188	fvmpt	⊢ ( 𝑦 ∈ 𝑈 → ( ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) )
190	189	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝑧 ∈ 𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑛 ) + 1 ) ) ) ) ‘ 𝑦 ) = ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) )
191	182 190	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑦 ) = ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) )
192	191	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑦 ) ) = ( abs ‘ ( ( 𝑦 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) − ( log ‘ ( ( 𝑦 / 𝑛 ) + 1 ) ) ) ) )
193		breq2	⊢ ( 𝑚 = 𝑛 → ( ( 2 · 𝑅 ) ≤ 𝑚 ↔ ( 2 · 𝑅 ) ≤ 𝑛 ) )
194		oveq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 ↑ 2 ) = ( 𝑛 ↑ 2 ) )
195	194	oveq2d	⊢ ( 𝑚 = 𝑛 → ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) = ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) )
196	195	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) = ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) )
197	171	oveq2d	⊢ ( 𝑚 = 𝑛 → ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) = ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) )
198		oveq2	⊢ ( 𝑚 = 𝑛 → ( ( 𝑅 + 1 ) · 𝑚 ) = ( ( 𝑅 + 1 ) · 𝑛 ) )
199	198	fveq2d	⊢ ( 𝑚 = 𝑛 → ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) = ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) )
200	199	oveq1d	⊢ ( 𝑚 = 𝑛 → ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) = ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) )
201	197 200	oveq12d	⊢ ( 𝑚 = 𝑛 → ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) = ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) )
202	193 196 201	ifbieq12d	⊢ ( 𝑚 = 𝑛 → if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) = if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) )
203		ovex	⊢ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) ∈ V
204		ovex	⊢ ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ∈ V
205	203 204	ifex	⊢ if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) ∈ V
206	202 4 205	fvmpt	⊢ ( 𝑛 ∈ ℕ → ( 𝑇 ‘ 𝑛 ) = if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) )
207	206	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑇 ‘ 𝑛 ) = if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) )
208	167 192 207	3brtr4d	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑦 ) ) ≤ ( 𝑇 ‘ 𝑛 ) )