Theorem pntibndlem1

Description: Lemma for pntibnd . (Contributed by Mario Carneiro, 10-Apr-2016)

	Ref	Expression
Hypotheses	pntibnd.r	$$⊢R=\left(a\in {ℝ}^{+}⟼\psi \left(a\right)-a\right)$$
	pntibndlem1.1	$$⊢\phi \to A\in {ℝ}^{+}$$
	pntibndlem1.l	$$⊢L=\frac{\frac{1}{4}}{A+3}$$
Assertion	pntibndlem1	$$⊢\phi \to L\in \left(0,1\right)$$

Proof

Step	Hyp	Ref	Expression
1		pntibnd.r	$$⊢R=\left(a\in {ℝ}^{+}⟼\psi \left(a\right)-a\right)$$
2		pntibndlem1.1	$$⊢\phi \to A\in {ℝ}^{+}$$
3		pntibndlem1.l	$$⊢L=\frac{\frac{1}{4}}{A+3}$$
4		4nn	$$⊢4\in \mathbb{N}$$
5		nnrp	$$⊢4\in \mathbb{N}\to 4\in {ℝ}^{+}$$
6		rpreccl	$$⊢4\in {ℝ}^{+}\to \frac{1}{4}\in {ℝ}^{+}$$
7	4 5 6	mp2b	$$⊢\frac{1}{4}\in {ℝ}^{+}$$
8		3rp	$$⊢3\in {ℝ}^{+}$$
9		rpaddcl	$$⊢\left(A\in {ℝ}^{+}\wedge 3\in {ℝ}^{+}\right)\to A+3\in {ℝ}^{+}$$
10	2 8 9	sylancl	$$⊢\phi \to A+3\in {ℝ}^{+}$$
11		rpdivcl	$$⊢\left(\frac{1}{4}\in {ℝ}^{+}\wedge A+3\in {ℝ}^{+}\right)\to \frac{\frac{1}{4}}{A+3}\in {ℝ}^{+}$$
12	7 10 11	sylancr	$$⊢\phi \to \frac{\frac{1}{4}}{A+3}\in {ℝ}^{+}$$
13	3 12	eqeltrid	$$⊢\phi \to L\in {ℝ}^{+}$$
14	13	rpred	$$⊢\phi \to L\in ℝ$$
15	13	rpgt0d	$$⊢\phi \to 0<L$$
16		rpcn	$$⊢\frac{1}{4}\in {ℝ}^{+}\to \frac{1}{4}\in ℂ$$
17	7 16	ax-mp	$$⊢\frac{1}{4}\in ℂ$$
18	17	div1i	$$⊢\frac{\frac{1}{4}}{1}=\frac{1}{4}$$
19		rpre	$$⊢\frac{1}{4}\in {ℝ}^{+}\to \frac{1}{4}\in ℝ$$
20	7 19	mp1i	$$⊢\phi \to \frac{1}{4}\in ℝ$$
21		3re	$$⊢3\in ℝ$$
22	21	a1i	$$⊢\phi \to 3\in ℝ$$
23	10	rpred	$$⊢\phi \to A+3\in ℝ$$
24		1lt4	$$⊢1<4$$
25		4re	$$⊢4\in ℝ$$
26		4pos	$$⊢0<4$$
27		recgt1	$$⊢\left(4\in ℝ\wedge 0<4\right)\to \left(1<4\leftrightarrow \frac{1}{4}<1\right)$$
28	25 26 27	mp2an	$$⊢1<4\leftrightarrow \frac{1}{4}<1$$
29	24 28	mpbi	$$⊢\frac{1}{4}<1$$
30		1lt3	$$⊢1<3$$
31	7 19	ax-mp	$$⊢\frac{1}{4}\in ℝ$$
32		1re	$$⊢1\in ℝ$$
33	31 32 21	lttri	$$⊢\left(\frac{1}{4}<1\wedge 1<3\right)\to \frac{1}{4}<3$$
34	29 30 33	mp2an	$$⊢\frac{1}{4}<3$$
35	34	a1i	$$⊢\phi \to \frac{1}{4}<3$$
36		ltaddrp	$$⊢\left(3\in ℝ\wedge A\in {ℝ}^{+}\right)\to 3<3+A$$
37	21 2 36	sylancr	$$⊢\phi \to 3<3+A$$
38		3cn	$$⊢3\in ℂ$$
39	2	rpcnd	$$⊢\phi \to A\in ℂ$$
40		addcom	$$⊢\left(3\in ℂ\wedge A\in ℂ\right)\to 3+A=A+3$$
41	38 39 40	sylancr	$$⊢\phi \to 3+A=A+3$$
42	37 41	breqtrd	$$⊢\phi \to 3<A+3$$
43	20 22 23 35 42	lttrd	$$⊢\phi \to \frac{1}{4}<A+3$$
44	18 43	eqbrtrid	$$⊢\phi \to \frac{\frac{1}{4}}{1}<A+3$$
45	32	a1i	$$⊢\phi \to 1\in ℝ$$
46		0lt1	$$⊢0<1$$
47	46	a1i	$$⊢\phi \to 0<1$$
48	10	rpregt0d	$$⊢\phi \to \left(A+3\in ℝ\wedge 0<A+3\right)$$
49		ltdiv23	$$⊢\left(\frac{1}{4}\in ℝ\wedge \left(1\in ℝ\wedge 0<1\right)\wedge \left(A+3\in ℝ\wedge 0<A+3\right)\right)\to \left(\frac{\frac{1}{4}}{1}<A+3\leftrightarrow \frac{\frac{1}{4}}{A+3}<1\right)$$
50	20 45 47 48 49	syl121anc	$$⊢\phi \to \left(\frac{\frac{1}{4}}{1}<A+3\leftrightarrow \frac{\frac{1}{4}}{A+3}<1\right)$$
51	44 50	mpbid	$$⊢\phi \to \frac{\frac{1}{4}}{A+3}<1$$
52	3 51	eqbrtrid	$$⊢\phi \to L<1$$
53		0xr	$$⊢0\in {ℝ}^{*}$$
54		1xr	$$⊢1\in {ℝ}^{*}$$
55		elioo2	$$⊢\left(0\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\right)\to \left(L\in \left(0,1\right)\leftrightarrow \left(L\in ℝ\wedge 0<L\wedge L<1\right)\right)$$
56	53 54 55	mp2an	$$⊢L\in \left(0,1\right)\leftrightarrow \left(L\in ℝ\wedge 0<L\wedge L<1\right)$$
57	14 15 52 56	syl3anbrc	$$⊢\phi \to L\in \left(0,1\right)$$