Theorem pntlema

Description: Lemma for pnt . Closure for the constants used in the proof. The mammoth expression W is a number large enough to satisfy all the lower bounds needed for Z . For comparison with Equation 10.6.27 of Shapiro, p. 434, Y is x_2, X is x_1, C is the big-O constant in Equation 10.6.29 of Shapiro, p. 435, and W is the unnamed lower bound of "for sufficiently large x" in Equation 10.6.34 of Shapiro, p. 436. (Contributed by Mario Carneiro, 13-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 ) + 𝐶 ) ) ) ) )
Assertion	pntlema	⊢ ( 𝜑 → 𝑊 ∈ ℝ+ )

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	11	simpld	⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
16		4nn	⊢ 4 ∈ ℕ
17		nnrp	⊢ ( 4 ∈ ℕ → 4 ∈ ℝ+ )
18	16 17	ax-mp	⊢ 4 ∈ ℝ+
19	1 2 3 4 5 6	pntlemd	⊢ ( 𝜑 → ( 𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ∧ 𝐹 ∈ ℝ+ ) )
20	19	simp1d	⊢ ( 𝜑 → 𝐿 ∈ ℝ+ )
21	1 2 3 4 5 6 7 8 9 10	pntlemc	⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )
22	21	simp1d	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
23	20 22	rpmulcld	⊢ ( 𝜑 → ( 𝐿 · 𝐸 ) ∈ ℝ+ )
24		rpdivcl	⊢ ( ( 4 ∈ ℝ+ ∧ ( 𝐿 · 𝐸 ) ∈ ℝ+ ) → ( 4 / ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
25	18 23 24	sylancr	⊢ ( 𝜑 → ( 4 / ( 𝐿 · 𝐸 ) ) ∈ ℝ+ )
26	15 25	rpaddcld	⊢ ( 𝜑 → ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ∈ ℝ+ )
27		2z	⊢ 2 ∈ ℤ
28		rpexpcl	⊢ ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) ∈ ℝ+ )
29	26 27 28	sylancl	⊢ ( 𝜑 → ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) ∈ ℝ+ )
30	12	simpld	⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
31	21	simp2d	⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
32		rpexpcl	⊢ ( ( 𝐾 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝐾 ↑ 2 ) ∈ ℝ+ )
33	31 27 32	sylancl	⊢ ( 𝜑 → ( 𝐾 ↑ 2 ) ∈ ℝ+ )
34	30 33	rpmulcld	⊢ ( 𝜑 → ( 𝑋 · ( 𝐾 ↑ 2 ) ) ∈ ℝ+ )
35		4z	⊢ 4 ∈ ℤ
36		rpexpcl	⊢ ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ∈ ℝ+ ∧ 4 ∈ ℤ ) → ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) ∈ ℝ+ )
37	34 35 36	sylancl	⊢ ( 𝜑 → ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) ∈ ℝ+ )
38		3nn0	⊢ 3 ∈ ℕ0
39		2nn	⊢ 2 ∈ ℕ
40	38 39	decnncl	⊢ ; 3 2 ∈ ℕ
41		nnrp	⊢ ( ; 3 2 ∈ ℕ → ; 3 2 ∈ ℝ+ )
42	40 41	ax-mp	⊢ ; 3 2 ∈ ℝ+
43		rpmulcl	⊢ ( ( ; 3 2 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ; 3 2 · 𝐵 ) ∈ ℝ+ )
44	42 3 43	sylancr	⊢ ( 𝜑 → ( ; 3 2 · 𝐵 ) ∈ ℝ+ )
45	21	simp3d	⊢ ( 𝜑 → ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
46	45	simp3d	⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) ∈ ℝ+ )
47		rpexpcl	⊢ ( ( 𝐸 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝐸 ↑ 2 ) ∈ ℝ+ )
48	22 27 47	sylancl	⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℝ+ )
49	20 48	rpmulcld	⊢ ( 𝜑 → ( 𝐿 · ( 𝐸 ↑ 2 ) ) ∈ ℝ+ )
50	46 49	rpmulcld	⊢ ( 𝜑 → ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ∈ ℝ+ )
51	44 50	rpdivcld	⊢ ( 𝜑 → ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) ∈ ℝ+ )
52		3rp	⊢ 3 ∈ ℝ+
53		rpmulcl	⊢ ( ( 𝑈 ∈ ℝ+ ∧ 3 ∈ ℝ+ ) → ( 𝑈 · 3 ) ∈ ℝ+ )
54	7 52 53	sylancl	⊢ ( 𝜑 → ( 𝑈 · 3 ) ∈ ℝ+ )
55	54 13	rpaddcld	⊢ ( 𝜑 → ( ( 𝑈 · 3 ) + 𝐶 ) ∈ ℝ+ )
56	51 55	rpmulcld	⊢ ( 𝜑 → ( ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ∈ ℝ+ )
57	56	rpred	⊢ ( 𝜑 → ( ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ∈ ℝ )
58	57	rpefcld	⊢ ( 𝜑 → ( exp ‘ ( ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ∈ ℝ+ )
59	37 58	rpaddcld	⊢ ( 𝜑 → ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) ∈ ℝ+ )
60	29 59	rpaddcld	⊢ ( 𝜑 → ( ( ( 𝑌 + ( 4 / ( 𝐿 · 𝐸 ) ) ) ↑ 2 ) + ( ( ( 𝑋 · ( 𝐾 ↑ 2 ) ) ↑ 4 ) + ( exp ‘ ( ( ( ; 3 2 · 𝐵 ) / ( ( 𝑈 − 𝐸 ) · ( 𝐿 · ( 𝐸 ↑ 2 ) ) ) ) · ( ( 𝑈 · 3 ) + 𝐶 ) ) ) ) ) ∈ ℝ+ )
61	14 60	eqeltrid	⊢ ( 𝜑 → 𝑊 ∈ ℝ+ )