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 e. RR+ \|-> ( ( psi ` a ) - a ) )
	pntlem1.a	\|- ( ph -> A e. RR+ )
	pntlem1.b	\|- ( ph -> B e. RR+ )
	pntlem1.l	\|- ( ph -> L e. ( 0 (,) 1 ) )
	pntlem1.d	\|- D = ( A + 1 )
	pntlem1.f	\|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
Assertion	pntlemd	\|- ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )

Proof

Step	Hyp	Ref	Expression
1		pntlem1.r	\|- R = ( a e. RR+ \|-> ( ( psi ` a ) - a ) )
2		pntlem1.a	\|- ( ph -> A e. RR+ )
3		pntlem1.b	\|- ( ph -> B e. RR+ )
4		pntlem1.l	\|- ( ph -> L e. ( 0 (,) 1 ) )
5		pntlem1.d	\|- D = ( A + 1 )
6		pntlem1.f	\|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
7		ioossre	\|- ( 0 (,) 1 ) C_ RR
8	7 4	sselid	\|- ( ph -> L e. RR )
9		eliooord	\|- ( L e. ( 0 (,) 1 ) -> ( 0 < L /\ L < 1 ) )
10	4 9	syl	\|- ( ph -> ( 0 < L /\ L < 1 ) )
11	10	simpld	\|- ( ph -> 0 < L )
12	8 11	elrpd	\|- ( ph -> L e. RR+ )
13		1rp	\|- 1 e. RR+
14		rpaddcl	\|- ( ( A e. RR+ /\ 1 e. RR+ ) -> ( A + 1 ) e. RR+ )
15	2 13 14	sylancl	\|- ( ph -> ( A + 1 ) e. RR+ )
16	5 15	eqeltrid	\|- ( ph -> D e. RR+ )
17		1re	\|- 1 e. RR
18		ltaddrp	\|- ( ( 1 e. RR /\ A e. RR+ ) -> 1 < ( 1 + A ) )
19	17 2 18	sylancr	\|- ( ph -> 1 < ( 1 + A ) )
20	2	rpcnd	\|- ( ph -> A e. CC )
21		ax-1cn	\|- 1 e. CC
22		addcom	\|- ( ( A e. CC /\ 1 e. CC ) -> ( A + 1 ) = ( 1 + A ) )
23	20 21 22	sylancl	\|- ( ph -> ( A + 1 ) = ( 1 + A ) )
24	5 23	eqtrid	\|- ( ph -> D = ( 1 + A ) )
25	19 24	breqtrrd	\|- ( ph -> 1 < D )
26	16	recgt1d	\|- ( ph -> ( 1 < D <-> ( 1 / D ) < 1 ) )
27	25 26	mpbid	\|- ( ph -> ( 1 / D ) < 1 )
28	16	rprecred	\|- ( ph -> ( 1 / D ) e. RR )
29		difrp	\|- ( ( ( 1 / D ) e. RR /\ 1 e. RR ) -> ( ( 1 / D ) < 1 <-> ( 1 - ( 1 / D ) ) e. RR+ ) )
30	28 17 29	sylancl	\|- ( ph -> ( ( 1 / D ) < 1 <-> ( 1 - ( 1 / D ) ) e. RR+ ) )
31	27 30	mpbid	\|- ( ph -> ( 1 - ( 1 / D ) ) e. RR+ )
32		3nn0	\|- 3 e. NN0
33		2nn	\|- 2 e. NN
34	32 33	decnncl	\|- ; 3 2 e. NN
35		nnrp	\|- ( ; 3 2 e. NN -> ; 3 2 e. RR+ )
36	34 35	ax-mp	\|- ; 3 2 e. RR+
37		rpmulcl	\|- ( ( ; 3 2 e. RR+ /\ B e. RR+ ) -> ( ; 3 2 x. B ) e. RR+ )
38	36 3 37	sylancr	\|- ( ph -> ( ; 3 2 x. B ) e. RR+ )
39	12 38	rpdivcld	\|- ( ph -> ( L / ( ; 3 2 x. B ) ) e. RR+ )
40		2z	\|- 2 e. ZZ
41		rpexpcl	\|- ( ( D e. RR+ /\ 2 e. ZZ ) -> ( D ^ 2 ) e. RR+ )
42	16 40 41	sylancl	\|- ( ph -> ( D ^ 2 ) e. RR+ )
43	39 42	rpdivcld	\|- ( ph -> ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) e. RR+ )
44	31 43	rpmulcld	\|- ( ph -> ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) ) e. RR+ )
45	6 44	eqeltrid	\|- ( ph -> F e. RR+ )
46	12 16 45	3jca	\|- ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )

Metamath Proof Explorer

Theorem pntlemd

Proof