pntlemd

Description: Lemma for pnt . Closure for the constants used in the proof. For comparison with Equation 10.6.27 of Shapiro, p. 434, A is C^*, B is c_1, L is λ, D is c_2, and F is c_3. (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 ) ) )
Assertion	pntlemd	⊢ ( 𝜑 → ( 𝐿 ∈ ℝ⁺ ∧ 𝐷 ∈ ℝ⁺ ∧ 𝐹 ∈ ℝ⁺ ) )

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		ioossre	⊢ ( 0 (,) 1 ) ⊆ ℝ
8	7 4	sselid	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
9		eliooord	⊢ ( 𝐿 ∈ ( 0 (,) 1 ) → ( 0 < 𝐿 ∧ 𝐿 < 1 ) )
10	4 9	syl	⊢ ( 𝜑 → ( 0 < 𝐿 ∧ 𝐿 < 1 ) )
11	10	simpld	⊢ ( 𝜑 → 0 < 𝐿 )
12	8 11	elrpd	⊢ ( 𝜑 → 𝐿 ∈ ℝ⁺ )
13		1rp	⊢ 1 ∈ ℝ⁺
14		rpaddcl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 1 ∈ ℝ⁺ ) → ( 𝐴 + 1 ) ∈ ℝ⁺ )
15	2 13 14	sylancl	⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℝ⁺ )
16	5 15	eqeltrid	⊢ ( 𝜑 → 𝐷 ∈ ℝ⁺ )
17		1re	⊢ 1 ∈ ℝ
18		ltaddrp	⊢ ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ⁺ ) → 1 < ( 1 + 𝐴 ) )
19	17 2 18	sylancr	⊢ ( 𝜑 → 1 < ( 1 + 𝐴 ) )
20	2	rpcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
21		ax-1cn	⊢ 1 ∈ ℂ
22		addcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 + 1 ) = ( 1 + 𝐴 ) )
23	20 21 22	sylancl	⊢ ( 𝜑 → ( 𝐴 + 1 ) = ( 1 + 𝐴 ) )
24	5 23	eqtrid	⊢ ( 𝜑 → 𝐷 = ( 1 + 𝐴 ) )
25	19 24	breqtrrd	⊢ ( 𝜑 → 1 < 𝐷 )
26	16	recgt1d	⊢ ( 𝜑 → ( 1 < 𝐷 ↔ ( 1 / 𝐷 ) < 1 ) )
27	25 26	mpbid	⊢ ( 𝜑 → ( 1 / 𝐷 ) < 1 )
28	16	rprecred	⊢ ( 𝜑 → ( 1 / 𝐷 ) ∈ ℝ )
29		difrp	⊢ ( ( ( 1 / 𝐷 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 / 𝐷 ) < 1 ↔ ( 1 − ( 1 / 𝐷 ) ) ∈ ℝ⁺ ) )
30	28 17 29	sylancl	⊢ ( 𝜑 → ( ( 1 / 𝐷 ) < 1 ↔ ( 1 − ( 1 / 𝐷 ) ) ∈ ℝ⁺ ) )
31	27 30	mpbid	⊢ ( 𝜑 → ( 1 − ( 1 / 𝐷 ) ) ∈ ℝ⁺ )
32		3nn0	⊢ 3 ∈ ℕ₀
33		2nn	⊢ 2 ∈ ℕ
34	32 33	decnncl	⊢ ; 3 2 ∈ ℕ
35		nnrp	⊢ ( ; 3 2 ∈ ℕ → ; 3 2 ∈ ℝ⁺ )
36	34 35	ax-mp	⊢ ; 3 2 ∈ ℝ⁺
37		rpmulcl	⊢ ( ( ; 3 2 ∈ ℝ⁺ ∧ 𝐵 ∈ ℝ⁺ ) → ( ; 3 2 · 𝐵 ) ∈ ℝ⁺ )
38	36 3 37	sylancr	⊢ ( 𝜑 → ( ; 3 2 · 𝐵 ) ∈ ℝ⁺ )
39	12 38	rpdivcld	⊢ ( 𝜑 → ( 𝐿 / ( ; 3 2 · 𝐵 ) ) ∈ ℝ⁺ )
40		2z	⊢ 2 ∈ ℤ
41		rpexpcl	⊢ ( ( 𝐷 ∈ ℝ⁺ ∧ 2 ∈ ℤ ) → ( 𝐷 ↑ 2 ) ∈ ℝ⁺ )
42	16 40 41	sylancl	⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℝ⁺ )
43	39 42	rpdivcld	⊢ ( 𝜑 → ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) ∈ ℝ⁺ )
44	31 43	rpmulcld	⊢ ( 𝜑 → ( ( 1 − ( 1 / 𝐷 ) ) · ( ( 𝐿 / ( ; 3 2 · 𝐵 ) ) / ( 𝐷 ↑ 2 ) ) ) ∈ ℝ⁺ )
45	6 44	eqeltrid	⊢ ( 𝜑 → 𝐹 ∈ ℝ⁺ )
46	12 16 45	3jca	⊢ ( 𝜑 → ( 𝐿 ∈ ℝ⁺ ∧ 𝐷 ∈ ℝ⁺ ∧ 𝐹 ∈ ℝ⁺ ) )

Metamath Proof Explorer

Theorem pntlemd

Proof