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	$⊢ 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}})$
	pntlem1.u	$⊢ φ \to U \in ℝ^{+}$
	pntlem1.u2	$⊢ φ \to U \leq A$
	pntlem1.e	$⊢ E = \frac{U}{D}$
	pntlem1.k	$⊢ K = e^{\frac{B}{E}}$
Assertion	pntlemc	$⊢ φ \to (E \in ℝ^{+} \land K \in ℝ^{+} \land (E \in (0, 1) \land 1 < K \land U - E \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		pntlem1.u	$⊢ φ \to U \in ℝ^{+}$
8		pntlem1.u2	$⊢ φ \to U \leq A$
9		pntlem1.e	$⊢ E = \frac{U}{D}$
10		pntlem1.k	$⊢ K = e^{\frac{B}{E}}$
11	1 2 3 4 5 6	pntlemd	$⊢ φ \to (L \in ℝ^{+} \land D \in ℝ^{+} \land F \in ℝ^{+})$
12	11	simp2d	$⊢ φ \to D \in ℝ^{+}$
13	7 12	rpdivcld	$⊢ φ \to \frac{U}{D} \in ℝ^{+}$
14	9 13	eqeltrid	$⊢ φ \to E \in ℝ^{+}$
15	3 14	rpdivcld	$⊢ φ \to \frac{B}{E} \in ℝ^{+}$
16	15	rpred	$⊢ φ \to \frac{B}{E} \in ℝ$
17	16	rpefcld	$⊢ φ \to e^{\frac{B}{E}} \in ℝ^{+}$
18	10 17	eqeltrid	$⊢ φ \to K \in ℝ^{+}$
19	14	rpred	$⊢ φ \to E \in ℝ$
20	14	rpgt0d	$⊢ φ \to 0 < E$
21	7	rpred	$⊢ φ \to U \in ℝ$
22	2	rpred	$⊢ φ \to A \in ℝ$
23	12	rpred	$⊢ φ \to D \in ℝ$
24	22	ltp1d	$⊢ φ \to A < A + 1$
25	24 5	breqtrrdi	$⊢ φ \to A < D$
26	21 22 23 8 25	lelttrd	$⊢ φ \to U < D$
27	12	rpcnd	$⊢ φ \to D \in ℂ$
28	27	mulid1d	$⊢ φ \to D \cdot 1 = D$
29	26 28	breqtrrd	$⊢ φ \to U < D \cdot 1$
30		1red	$⊢ φ \to 1 \in ℝ$
31	21 30 12	ltdivmuld	$⊢ φ \to (\frac{U}{D} < 1 \leftrightarrow U < D \cdot 1)$
32	29 31	mpbird	$⊢ φ \to \frac{U}{D} < 1$
33	9 32	eqbrtrid	$⊢ φ \to E < 1$
34		0xr	$⊢ 0 \in ℝ^{*}$
35		1xr	$⊢ 1 \in ℝ^{*}$
36		elioo2	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{}) \to (E \in (0, 1) \leftrightarrow (E \in ℝ \land 0 < E \land E < 1))$
37	34 35 36	mp2an	$⊢ E \in (0, 1) \leftrightarrow (E \in ℝ \land 0 < E \land E < 1)$
38	19 20 33 37	syl3anbrc	$⊢ φ \to E \in (0, 1)$
39		efgt1	$⊢ \frac{B}{E} \in ℝ^{+} \to 1 < e^{\frac{B}{E}}$
40	15 39	syl	$⊢ φ \to 1 < e^{\frac{B}{E}}$
41	40 10	breqtrrdi	$⊢ φ \to 1 < K$
42		1re	$⊢ 1 \in ℝ$
43		ltaddrp	$⊢ (1 \in ℝ \land A \in ℝ^{+}) \to 1 < 1 + A$
44	42 2 43	sylancr	$⊢ φ \to 1 < 1 + A$
45	7	rpcnne0d	$⊢ φ \to (U \in ℂ \land U \neq 0)$
46		divid	$⊢ (U \in ℂ \land U \neq 0) \to \frac{U}{U} = 1$
47	45 46	syl	$⊢ φ \to \frac{U}{U} = 1$
48	2	rpcnd	$⊢ φ \to A \in ℂ$
49		ax-1cn	$⊢ 1 \in ℂ$
50		addcom	$⊢ (A \in ℂ \land 1 \in ℂ) \to A + 1 = 1 + A$
51	48 49 50	sylancl	$⊢ φ \to A + 1 = 1 + A$
52	5 51	syl5eq	$⊢ φ \to D = 1 + A$
53	44 47 52	3brtr4d	$⊢ φ \to \frac{U}{U} < D$
54	21 7 12 53	ltdiv23d	$⊢ φ \to \frac{U}{D} < U$
55	9 54	eqbrtrid	$⊢ φ \to E < U$
56		difrp	$⊢ (E \in ℝ \land U \in ℝ) \to (E < U \leftrightarrow U - E \in ℝ^{+})$
57	19 21 56	syl2anc	$⊢ φ \to (E < U \leftrightarrow U - E \in ℝ^{+})$
58	55 57	mpbid	$⊢ φ \to U - E \in ℝ^{+}$
59	38 41 58	3jca	$⊢ φ \to (E \in (0, 1) \land 1 < K \land U - E \in ℝ^{+})$
60	14 18 59	3jca	$⊢ φ \to (E \in ℝ^{+} \land K \in ℝ^{+} \land (E \in (0, 1) \land 1 < K \land U - E \in ℝ^{+}))$

Metamath Proof Explorer

Theorem pntlemc

Proof