Theorem pntlemc

Description: Lemma for pnt . Closure for the constants used in the proof. For comparison with Equation 10.6.27 of Shapiro, p. 434, U is α, E is ε, and K isK. (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 ‘ ( 𝐵 / 𝐸 ) )
Assertion	pntlemc	⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )

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	1 2 3 4 5 6	pntlemd	⊢ ( 𝜑 → ( 𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ∧ 𝐹 ∈ ℝ+ ) )
12	11	simp2d	⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
13	7 12	rpdivcld	⊢ ( 𝜑 → ( 𝑈 / 𝐷 ) ∈ ℝ+ )
14	9 13	eqeltrid	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
15	3 14	rpdivcld	⊢ ( 𝜑 → ( 𝐵 / 𝐸 ) ∈ ℝ+ )
16	15	rpred	⊢ ( 𝜑 → ( 𝐵 / 𝐸 ) ∈ ℝ )
17	16	rpefcld	⊢ ( 𝜑 → ( exp ‘ ( 𝐵 / 𝐸 ) ) ∈ ℝ+ )
18	10 17	eqeltrid	⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
19	14	rpred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
20	14	rpgt0d	⊢ ( 𝜑 → 0 < 𝐸 )
21	7	rpred	⊢ ( 𝜑 → 𝑈 ∈ ℝ )
22	2	rpred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
23	12	rpred	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
24	22	ltp1d	⊢ ( 𝜑 → 𝐴 < ( 𝐴 + 1 ) )
25	24 5	breqtrrdi	⊢ ( 𝜑 → 𝐴 < 𝐷 )
26	21 22 23 8 25	lelttrd	⊢ ( 𝜑 → 𝑈 < 𝐷 )
27	12	rpcnd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
28	27	mulridd	⊢ ( 𝜑 → ( 𝐷 · 1 ) = 𝐷 )
29	26 28	breqtrrd	⊢ ( 𝜑 → 𝑈 < ( 𝐷 · 1 ) )
30		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
31	21 30 12	ltdivmuld	⊢ ( 𝜑 → ( ( 𝑈 / 𝐷 ) < 1 ↔ 𝑈 < ( 𝐷 · 1 ) ) )
32	29 31	mpbird	⊢ ( 𝜑 → ( 𝑈 / 𝐷 ) < 1 )
33	9 32	eqbrtrid	⊢ ( 𝜑 → 𝐸 < 1 )
34		0xr	⊢ 0 ∈ ℝ*
35		1xr	⊢ 1 ∈ ℝ*
36		elioo2	⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( 𝐸 ∈ ( 0 (,) 1 ) ↔ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ∧ 𝐸 < 1 ) ) )
37	34 35 36	mp2an	⊢ ( 𝐸 ∈ ( 0 (,) 1 ) ↔ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ∧ 𝐸 < 1 ) )
38	19 20 33 37	syl3anbrc	⊢ ( 𝜑 → 𝐸 ∈ ( 0 (,) 1 ) )
39		efgt1	⊢ ( ( 𝐵 / 𝐸 ) ∈ ℝ+ → 1 < ( exp ‘ ( 𝐵 / 𝐸 ) ) )
40	15 39	syl	⊢ ( 𝜑 → 1 < ( exp ‘ ( 𝐵 / 𝐸 ) ) )
41	40 10	breqtrrdi	⊢ ( 𝜑 → 1 < 𝐾 )
42		1re	⊢ 1 ∈ ℝ
43		ltaddrp	⊢ ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → 1 < ( 1 + 𝐴 ) )
44	42 2 43	sylancr	⊢ ( 𝜑 → 1 < ( 1 + 𝐴 ) )
45	7	rpcnne0d	⊢ ( 𝜑 → ( 𝑈 ∈ ℂ ∧ 𝑈 ≠ 0 ) )
46		divid	⊢ ( ( 𝑈 ∈ ℂ ∧ 𝑈 ≠ 0 ) → ( 𝑈 / 𝑈 ) = 1 )
47	45 46	syl	⊢ ( 𝜑 → ( 𝑈 / 𝑈 ) = 1 )
48	2	rpcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
49		ax-1cn	⊢ 1 ∈ ℂ
50		addcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 + 1 ) = ( 1 + 𝐴 ) )
51	48 49 50	sylancl	⊢ ( 𝜑 → ( 𝐴 + 1 ) = ( 1 + 𝐴 ) )
52	5 51	eqtrid	⊢ ( 𝜑 → 𝐷 = ( 1 + 𝐴 ) )
53	44 47 52	3brtr4d	⊢ ( 𝜑 → ( 𝑈 / 𝑈 ) < 𝐷 )
54	21 7 12 53	ltdiv23d	⊢ ( 𝜑 → ( 𝑈 / 𝐷 ) < 𝑈 )
55	9 54	eqbrtrid	⊢ ( 𝜑 → 𝐸 < 𝑈 )
56		difrp	⊢ ( ( 𝐸 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( 𝐸 < 𝑈 ↔ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
57	19 21 56	syl2anc	⊢ ( 𝜑 → ( 𝐸 < 𝑈 ↔ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
58	55 57	mpbid	⊢ ( 𝜑 → ( 𝑈 − 𝐸 ) ∈ ℝ+ )
59	38 41 58	3jca	⊢ ( 𝜑 → ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) )
60	14 18 59	3jca	⊢ ( 𝜑 → ( 𝐸 ∈ ℝ+ ∧ 𝐾 ∈ ℝ+ ∧ ( 𝐸 ∈ ( 0 (,) 1 ) ∧ 1 < 𝐾 ∧ ( 𝑈 − 𝐸 ) ∈ ℝ+ ) ) )