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	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	pntlem1.a	$⊢ φ \to A \in ℝ^{+}$
	pntlem1.b	$⊢ φ \to B \in ℝ^{+}$
	pntlem1.l	$⊢ φ \to L \in (0, 1)$
	pntlem1.d	$⊢ D = A + 1$
	pntlem1.f	$⊢ F = (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}})$
Assertion	pntlemd	$⊢ φ \to (L \in ℝ^{+} \land D \in ℝ^{+} \land F \in ℝ^{+})$

Proof

Step	Hyp	Ref	Expression
1		pntlem1.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		pntlem1.a	$⊢ φ \to A \in ℝ^{+}$
3		pntlem1.b	$⊢ φ \to B \in ℝ^{+}$
4		pntlem1.l	$⊢ φ \to L \in (0, 1)$
5		pntlem1.d	$⊢ D = A + 1$
6		pntlem1.f	$⊢ F = (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}})$
7		ioossre	$⊢ (0, 1) \subseteq ℝ$
8	7 4	sselid	$⊢ φ \to L \in ℝ$
9		eliooord	$⊢ L \in (0, 1) \to (0 < L \land L < 1)$
10	4 9	syl	$⊢ φ \to (0 < L \land L < 1)$
11	10	simpld	$⊢ φ \to 0 < L$
12	8 11	elrpd	$⊢ φ \to L \in ℝ^{+}$
13		1rp	$⊢ 1 \in ℝ^{+}$
14		rpaddcl	$⊢ (A \in ℝ^{+} \land 1 \in ℝ^{+}) \to A + 1 \in ℝ^{+}$
15	2 13 14	sylancl	$⊢ φ \to A + 1 \in ℝ^{+}$
16	5 15	eqeltrid	$⊢ φ \to D \in ℝ^{+}$
17		1re	$⊢ 1 \in ℝ$
18		ltaddrp	$⊢ (1 \in ℝ \land A \in ℝ^{+}) \to 1 < 1 + A$
19	17 2 18	sylancr	$⊢ φ \to 1 < 1 + A$
20	2	rpcnd	$⊢ φ \to A \in ℂ$
21		ax-1cn	$⊢ 1 \in ℂ$
22		addcom	$⊢ (A \in ℂ \land 1 \in ℂ) \to A + 1 = 1 + A$
23	20 21 22	sylancl	$⊢ φ \to A + 1 = 1 + A$
24	5 23	syl5eq	$⊢ φ \to D = 1 + A$
25	19 24	breqtrrd	$⊢ φ \to 1 < D$
26	16	recgt1d	$⊢ φ \to (1 < D \leftrightarrow \frac{1}{D} < 1)$
27	25 26	mpbid	$⊢ φ \to \frac{1}{D} < 1$
28	16	rprecred	$⊢ φ \to \frac{1}{D} \in ℝ$
29		difrp	$⊢ (\frac{1}{D} \in ℝ \land 1 \in ℝ) \to (\frac{1}{D} < 1 \leftrightarrow 1 - (\frac{1}{D}) \in ℝ^{+})$
30	28 17 29	sylancl	$⊢ φ \to (\frac{1}{D} < 1 \leftrightarrow 1 - (\frac{1}{D}) \in ℝ^{+})$
31	27 30	mpbid	$⊢ φ \to 1 - (\frac{1}{D}) \in ℝ^{+}$
32		3nn0	$⊢ 3 \in ℕ_{0}$
33		2nn	$⊢ 2 \in ℕ$
34	32 33	decnncl	$⊢ 32 \in ℕ$
35		nnrp	$⊢ 32 \in ℕ \to 32 \in ℝ^{+}$
36	34 35	ax-mp	$⊢ 32 \in ℝ^{+}$
37		rpmulcl	$⊢ (32 \in ℝ^{+} \land B \in ℝ^{+}) \to 32 B \in ℝ^{+}$
38	36 3 37	sylancr	$⊢ φ \to 32 B \in ℝ^{+}$
39	12 38	rpdivcld	$⊢ φ \to \frac{L}{32 B} \in ℝ^{+}$
40		2z	$⊢ 2 \in ℤ$
41		rpexpcl	$⊢ (D \in ℝ^{+} \land 2 \in ℤ) \to D^{2} \in ℝ^{+}$
42	16 40 41	sylancl	$⊢ φ \to D^{2} \in ℝ^{+}$
43	39 42	rpdivcld	$⊢ φ \to \frac{\frac{L}{32 B}}{D^{2}} \in ℝ^{+}$
44	31 43	rpmulcld	$⊢ φ \to (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}}) \in ℝ^{+}$
45	6 44	eqeltrid	$⊢ φ \to F \in ℝ^{+}$
46	12 16 45	3jca	$⊢ φ \to (L \in ℝ^{+} \land D \in ℝ^{+} \land F \in ℝ^{+})$

Metamath Proof Explorer

Theorem pntlemd

Proof