Theorem pntibndlem1

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

	Ref	Expression
Hypotheses	pntibnd.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
	pntibndlem1.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	pntibndlem1.l	⊢ 𝐿 = ( ( 1 / 4 ) / ( 𝐴 + 3 ) )
Assertion	pntibndlem1	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )

Proof

Step	Hyp	Ref	Expression
1		pntibnd.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		pntibndlem1.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3		pntibndlem1.l	⊢ 𝐿 = ( ( 1 / 4 ) / ( 𝐴 + 3 ) )
4		4nn	⊢ 4 ∈ ℕ
5		nnrp	⊢ ( 4 ∈ ℕ → 4 ∈ ℝ+ )
6		rpreccl	⊢ ( 4 ∈ ℝ+ → ( 1 / 4 ) ∈ ℝ+ )
7	4 5 6	mp2b	⊢ ( 1 / 4 ) ∈ ℝ+
8		3rp	⊢ 3 ∈ ℝ+
9		rpaddcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 3 ∈ ℝ+ ) → ( 𝐴 + 3 ) ∈ ℝ+ )
10	2 8 9	sylancl	⊢ ( 𝜑 → ( 𝐴 + 3 ) ∈ ℝ+ )
11		rpdivcl	⊢ ( ( ( 1 / 4 ) ∈ ℝ+ ∧ ( 𝐴 + 3 ) ∈ ℝ+ ) → ( ( 1 / 4 ) / ( 𝐴 + 3 ) ) ∈ ℝ+ )
12	7 10 11	sylancr	⊢ ( 𝜑 → ( ( 1 / 4 ) / ( 𝐴 + 3 ) ) ∈ ℝ+ )
13	3 12	eqeltrid	⊢ ( 𝜑 → 𝐿 ∈ ℝ+ )
14	13	rpred	⊢ ( 𝜑 → 𝐿 ∈ ℝ )
15	13	rpgt0d	⊢ ( 𝜑 → 0 < 𝐿 )
16		rpcn	⊢ ( ( 1 / 4 ) ∈ ℝ+ → ( 1 / 4 ) ∈ ℂ )
17	7 16	ax-mp	⊢ ( 1 / 4 ) ∈ ℂ
18	17	div1i	⊢ ( ( 1 / 4 ) / 1 ) = ( 1 / 4 )
19		rpre	⊢ ( ( 1 / 4 ) ∈ ℝ+ → ( 1 / 4 ) ∈ ℝ )
20	7 19	mp1i	⊢ ( 𝜑 → ( 1 / 4 ) ∈ ℝ )
21		3re	⊢ 3 ∈ ℝ
22	21	a1i	⊢ ( 𝜑 → 3 ∈ ℝ )
23	10	rpred	⊢ ( 𝜑 → ( 𝐴 + 3 ) ∈ ℝ )
24		1lt4	⊢ 1 < 4
25		4re	⊢ 4 ∈ ℝ
26		4pos	⊢ 0 < 4
27		recgt1	⊢ ( ( 4 ∈ ℝ ∧ 0 < 4 ) → ( 1 < 4 ↔ ( 1 / 4 ) < 1 ) )
28	25 26 27	mp2an	⊢ ( 1 < 4 ↔ ( 1 / 4 ) < 1 )
29	24 28	mpbi	⊢ ( 1 / 4 ) < 1
30		1lt3	⊢ 1 < 3
31	7 19	ax-mp	⊢ ( 1 / 4 ) ∈ ℝ
32		1re	⊢ 1 ∈ ℝ
33	31 32 21	lttri	⊢ ( ( ( 1 / 4 ) < 1 ∧ 1 < 3 ) → ( 1 / 4 ) < 3 )
34	29 30 33	mp2an	⊢ ( 1 / 4 ) < 3
35	34	a1i	⊢ ( 𝜑 → ( 1 / 4 ) < 3 )
36		ltaddrp	⊢ ( ( 3 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → 3 < ( 3 + 𝐴 ) )
37	21 2 36	sylancr	⊢ ( 𝜑 → 3 < ( 3 + 𝐴 ) )
38		3cn	⊢ 3 ∈ ℂ
39	2	rpcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
40		addcom	⊢ ( ( 3 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 3 + 𝐴 ) = ( 𝐴 + 3 ) )
41	38 39 40	sylancr	⊢ ( 𝜑 → ( 3 + 𝐴 ) = ( 𝐴 + 3 ) )
42	37 41	breqtrd	⊢ ( 𝜑 → 3 < ( 𝐴 + 3 ) )
43	20 22 23 35 42	lttrd	⊢ ( 𝜑 → ( 1 / 4 ) < ( 𝐴 + 3 ) )
44	18 43	eqbrtrid	⊢ ( 𝜑 → ( ( 1 / 4 ) / 1 ) < ( 𝐴 + 3 ) )
45	32	a1i	⊢ ( 𝜑 → 1 ∈ ℝ )
46		0lt1	⊢ 0 < 1
47	46	a1i	⊢ ( 𝜑 → 0 < 1 )
48	10	rpregt0d	⊢ ( 𝜑 → ( ( 𝐴 + 3 ) ∈ ℝ ∧ 0 < ( 𝐴 + 3 ) ) )
49		ltdiv23	⊢ ( ( ( 1 / 4 ) ∈ ℝ ∧ ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( ( 𝐴 + 3 ) ∈ ℝ ∧ 0 < ( 𝐴 + 3 ) ) ) → ( ( ( 1 / 4 ) / 1 ) < ( 𝐴 + 3 ) ↔ ( ( 1 / 4 ) / ( 𝐴 + 3 ) ) < 1 ) )
50	20 45 47 48 49	syl121anc	⊢ ( 𝜑 → ( ( ( 1 / 4 ) / 1 ) < ( 𝐴 + 3 ) ↔ ( ( 1 / 4 ) / ( 𝐴 + 3 ) ) < 1 ) )
51	44 50	mpbid	⊢ ( 𝜑 → ( ( 1 / 4 ) / ( 𝐴 + 3 ) ) < 1 )
52	3 51	eqbrtrid	⊢ ( 𝜑 → 𝐿 < 1 )
53		0xr	⊢ 0 ∈ ℝ*
54		1xr	⊢ 1 ∈ ℝ*
55		elioo2	⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( 𝐿 ∈ ( 0 (,) 1 ) ↔ ( 𝐿 ∈ ℝ ∧ 0 < 𝐿 ∧ 𝐿 < 1 ) ) )
56	53 54 55	mp2an	⊢ ( 𝐿 ∈ ( 0 (,) 1 ) ↔ ( 𝐿 ∈ ℝ ∧ 0 < 𝐿 ∧ 𝐿 < 1 ) )
57	14 15 52 56	syl3anbrc	⊢ ( 𝜑 → 𝐿 ∈ ( 0 (,) 1 ) )