pntleme

Description: Lemma for pnt . Package up pntlemo in quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016)

	Ref	Expression
Hypotheses	pntlem1.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ⁺ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
	pntlem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ⁺ )
	pntlem1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ⁺ )
	pntlem1.l	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
	pntlem1.d	⊢ 𝐷 = ( 𝐴 + 1 )
	pntlem1.f	⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
	pntlem1.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ⁺ )
	pntlem1.u2	⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
	pntlem1.e	⊢ 𝐸 = ( 𝑈 / 𝐷 )
	pntlem1.k	⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
	pntlem1.y	⊢ ( 𝜑 → ( 𝑌 ∈ ℝ⁺ ∧ 1 ≤ 𝑌 ) )
	pntlem1.x	⊢ ( 𝜑 → ( 𝑋 ∈ ℝ⁺ ∧ 𝑌 < 𝑋 ) )
	pntlem1.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ⁺ )
	pntlem1.w	⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
	pntleme.U	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
	pntleme.K	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ⁺ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
	pntleme.C	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) ) · ( log ‘ 𝑖 ) ) ) ) / 𝑧 ) ≤ 𝐶 )
Assertion	pntleme	⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pntlem1.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ⁺ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		pntlem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ⁺ )
3		pntlem1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ⁺ )
4		pntlem1.l	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )
5		pntlem1.d	⊢ 𝐷 = ( 𝐴 + 1 )
6		pntlem1.f	⊢ 𝐹 = ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) )
7		pntlem1.u	⊢ ( 𝜑 → 𝑈 ∈ ℝ⁺ )
8		pntlem1.u2	⊢ ( 𝜑 → 𝑈 ≤ 𝐴 )
9		pntlem1.e	⊢ 𝐸 = ( 𝑈 / 𝐷 )
10		pntlem1.k	⊢ 𝐾 = ( exp ‘ ( 𝐵 / 𝐸 ) )
11		pntlem1.y	⊢ ( 𝜑 → ( 𝑌 ∈ ℝ⁺ ∧ 1 ≤ 𝑌 ) )
12		pntlem1.x	⊢ ( 𝜑 → ( 𝑋 ∈ ℝ⁺ ∧ 𝑌 < 𝑋 ) )
13		pntlem1.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ⁺ )
14		pntlem1.w	⊢ 𝑊 = ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) )
15		pntleme.U	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
16		pntleme.K	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝐾 [,) +∞ ) ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ⁺ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
17		pntleme.C	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) ) · ( log ‘ 𝑖 ) ) ) ) / 𝑧 ) ≤ 𝐶 )
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14	pntlema	⊢ ( 𝜑 → 𝑊 ∈ ℝ⁺ )
19	2	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑊 [,) +∞ ) ) → 𝐴 ∈ ℝ⁺ )
20	3	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑊 [,) +∞ ) ) → 𝐵 ∈ ℝ⁺ )
21	4	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑊 [,) +∞ ) ) → 𝐿 ∈ ( 0 (,) 1 ) )
22	7	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑊 [,) +∞ ) ) → 𝑈 ∈ ℝ⁺ )
23	8	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑊 [,) +∞ ) ) → 𝑈 ≤ 𝐴 )
24	11	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑊 [,) +∞ ) ) → ( 𝑌 ∈ ℝ⁺ ∧ 1 ≤ 𝑌 ) )
25	12	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑊 [,) +∞ ) ) → ( 𝑋 ∈ ℝ⁺ ∧ 𝑌 < 𝑋 ) )
26	13	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑊 [,) +∞ ) ) → 𝐶 ∈ ℝ⁺ )
27		simpr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑊 [,) +∞ ) ) → 𝑣 ∈ ( 𝑊 [,) +∞ ) )
28		eqid	⊢ ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 ) = ( ( ⌊ ‘ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐾 ) ) ) + 1 )
29		eqid	⊢ ( ⌊ ‘ ( ( ( log ‘ 𝑣 ) / ( log ‘ 𝐾 ) ) / 2 ) ) = ( ⌊ ‘ ( ( ( log ‘ 𝑣 ) / ( log ‘ 𝐾 ) ) / 2 ) )
30	15	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑊 [,) +∞ ) ) → ∀ 𝑧 ∈ ( 𝑌 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑧 ) / 𝑧 ) ) ≤ 𝑈 )
31		oveq1	⊢ ( 𝑘 = 𝐾 → ( 𝑘 · 𝑦 ) = ( 𝐾 · 𝑦 ) )
32	31	breq2d	⊢ ( 𝑘 = 𝐾 → ( ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ↔ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) )
33	32	anbi2d	⊢ ( 𝑘 = 𝐾 → ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ↔ ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ) )
34	33	anbi1d	⊢ ( 𝑘 = 𝐾 → ( ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
35	34	rexbidv	⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑧 ∈ ℝ⁺ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ∃ 𝑧 ∈ ℝ⁺ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
36	35	ralbidv	⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ⁺ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝑘 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ↔ ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ⁺ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) ) )
37	1 2 3 4 5 6 7 8 9 10	pntlemc	⊢ ( 𝜑 → ( 𝐸 ∈ ℝ⁺ ∧ 𝐾 ∈ ℝ⁺ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ⁺ ) ) )
38	37	simp2d	⊢ ( 𝜑 → 𝐾 ∈ ℝ⁺ )
39	38	rpxrd	⊢ ( 𝜑 → 𝐾 ∈ ℝ^* )
40		pnfxr	⊢ +∞ ∈ ℝ^*
41	40	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ^* )
42	38	rpred	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
43	42	ltpnfd	⊢ ( 𝜑 → 𝐾 < +∞ )
44		lbico1	⊢ ( ( 𝐾 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝐾 < +∞ ) → 𝐾 ∈ ( 𝐾 [,) +∞ ) )
45	39 41 43 44	syl3anc	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐾 [,) +∞ ) )
46	36 16 45	rspcdva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ⁺ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
47	46	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑊 [,) +∞ ) ) → ∀ 𝑦 ∈ ( 𝑋 (,) +∞ ) ∃ 𝑧 ∈ ℝ⁺ ( ( 𝑦 < 𝑧 ∧ ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) < ( 𝐾 · 𝑦 ) ) ∧ ∀ 𝑢 ∈ ( 𝑧 [,] ( ( 1 + ( 𝐿 · 𝐸 ) ) · 𝑧 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑢 ) / 𝑢 ) ) ≤ 𝐸 ) )
48	17	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑊 [,) +∞ ) ) → ∀ 𝑧 ∈ ( 1 (,) +∞ ) ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑧 ) ) · ( log ‘ 𝑧 ) ) − ( ( 2 / ( log ‘ 𝑧 ) ) · Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ ( 𝑧 / 𝑌 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑧 / 𝑖 ) ) ) · ( log ‘ 𝑖 ) ) ) ) / 𝑧 ) ≤ 𝐶 )
49	1 19 20 21 5 6 22 23 9 10 24 25 26 14 27 28 29 30 47 48	pntlemo	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝑊 [,) +∞ ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )
50	49	ralrimiva	⊢ ( 𝜑 → ∀ 𝑣 ∈ ( 𝑊 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )
51		oveq1	⊢ ( 𝑤 = 𝑊 → ( 𝑤 [,) +∞ ) = ( 𝑊 [,) +∞ ) )
52	51	raleqdv	⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) ↔ ∀ 𝑣 ∈ ( 𝑊 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) ) )
53	52	rspcev	⊢ ( ( 𝑊 ∈ ℝ⁺ ∧ ∀ 𝑣 ∈ ( 𝑊 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) ) → ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )
54	18 50 53	syl2anc	⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑣 ∈ ( 𝑤 [,) +∞ ) ( abs ‘ ( ( 𝑅 ‘ 𝑣 ) / 𝑣 ) ) ≤ ( 𝑈 − ( 𝐹 · ( 𝑈 ↑ 3 ) ) ) )

Metamath Proof Explorer

Theorem pntleme

Proof