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
|
syl5eq |
|- ( 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+ ) ) |