Metamath Proof Explorer


Theorem pntibnd

Description: Lemma for pnt . Establish smallness of R on an interval. Lemma 10.6.2 in Shapiro, p. 436. (Contributed by Mario Carneiro, 10-Apr-2016)

Ref Expression
Hypothesis pntlem1.r R=a+ψaa
Assertion pntibnd c+l01e01x+kece+∞yx+∞z+y<z1+lez<kyuz1+lezRuue

Proof

Step Hyp Ref Expression
1 pntlem1.r R=a+ψaa
2 1 pntrmax d+x+Rxxd
3 1 pntpbnd b+f01g+mebf+∞vg+∞nv<nnmvRnnf
4 reeanv d+b+x+Rxxdf01g+mebf+∞vg+∞nv<nnmvRnnfd+x+Rxxdb+f01g+mebf+∞vg+∞nv<nnmvRnnf
5 2rp 2+
6 rpmulcl 2+b+2b+
7 5 6 mpan b+2b+
8 2re 2
9 1lt2 1<2
10 rplogcl 21<2log2+
11 8 9 10 mp2an log2+
12 rpaddcl 2b+log2+2b+log2+
13 7 11 12 sylancl b+2b+log2+
14 13 ad2antlr d+b+x+Rxxdf01g+mebf+∞vg+∞nv<nnmvRnnf2b+log2+
15 id d+d+
16 eqid 14d+3=14d+3
17 1 15 16 pntibndlem1 d+14d+301
18 17 ad2antrr d+b+x+Rxxdf01g+mebf+∞vg+∞nv<nnmvRnnf14d+301
19 elioore e01e
20 eliooord e010<ee<1
21 20 simpld e010<e
22 19 21 elrpd e01e+
23 22 rphalfcld e01e2+
24 23 rpred e01e2
25 23 rpgt0d e010<e2
26 1red e011
27 rphalflt e+e2<e
28 22 27 syl e01e2<e
29 20 simprd e01e<1
30 24 19 26 28 29 lttrd e01e2<1
31 0xr 0*
32 1xr 1*
33 elioo2 0*1*e201e20<e2e2<1
34 31 32 33 mp2an e201e20<e2e2<1
35 24 25 30 34 syl3anbrc e01e201
36 35 adantl d+b+x+Rxxde01e201
37 oveq2 f=e2bf=be2
38 37 fveq2d f=e2ebf=ebe2
39 38 oveq1d f=e2ebf+∞=ebe2+∞
40 breq2 f=e2RnnfRnne2
41 40 anbi2d f=e2v<nnmvRnnfv<nnmvRnne2
42 41 rexbidv f=e2nv<nnmvRnnfnv<nnmvRnne2
43 42 ralbidv f=e2vg+∞nv<nnmvRnnfvg+∞nv<nnmvRnne2
44 39 43 raleqbidv f=e2mebf+∞vg+∞nv<nnmvRnnfmebe2+∞vg+∞nv<nnmvRnne2
45 44 rexbidv f=e2g+mebf+∞vg+∞nv<nnmvRnnfg+mebe2+∞vg+∞nv<nnmvRnne2
46 45 rspcv e201f01g+mebf+∞vg+∞nv<nnmvRnnfg+mebe2+∞vg+∞nv<nnmvRnne2
47 36 46 syl d+b+x+Rxxde01f01g+mebf+∞vg+∞nv<nnmvRnnfg+mebe2+∞vg+∞nv<nnmvRnne2
48 simp-4l d+b+x+Rxxde01g+mebe2+∞vg+∞nv<nnmvRnne2d+
49 simpllr d+b+x+Rxxde01g+mebe2+∞vg+∞nv<nnmvRnne2x+Rxxd
50 simplr d+b+x+Rxxdb+
51 50 ad2antrr d+b+x+Rxxde01g+mebe2+∞vg+∞nv<nnmvRnne2b+
52 eqid ebe2=ebe2
53 eqid 2b+log2=2b+log2
54 simplr d+b+x+Rxxde01g+mebe2+∞vg+∞nv<nnmvRnne2e01
55 simprl d+b+x+Rxxde01g+mebe2+∞vg+∞nv<nnmvRnne2g+
56 simprr d+b+x+Rxxde01g+mebe2+∞vg+∞nv<nnmvRnne2mebe2+∞vg+∞nv<nnmvRnne2
57 1 48 16 49 51 52 53 54 55 56 pntibndlem3 d+b+x+Rxxde01g+mebe2+∞vg+∞nv<nnmvRnne2x+ke2b+log2e+∞yx+∞z+y<z1+14d+3ez<kyuz1+14d+3ezRuue
58 57 rexlimdvaa d+b+x+Rxxde01g+mebe2+∞vg+∞nv<nnmvRnne2x+ke2b+log2e+∞yx+∞z+y<z1+14d+3ez<kyuz1+14d+3ezRuue
59 47 58 syld d+b+x+Rxxde01f01g+mebf+∞vg+∞nv<nnmvRnnfx+ke2b+log2e+∞yx+∞z+y<z1+14d+3ez<kyuz1+14d+3ezRuue
60 59 ralrimdva d+b+x+Rxxdf01g+mebf+∞vg+∞nv<nnmvRnnfe01x+ke2b+log2e+∞yx+∞z+y<z1+14d+3ez<kyuz1+14d+3ezRuue
61 60 impr d+b+x+Rxxdf01g+mebf+∞vg+∞nv<nnmvRnnfe01x+ke2b+log2e+∞yx+∞z+y<z1+14d+3ez<kyuz1+14d+3ezRuue
62 fvoveq1 c=2b+log2ece=e2b+log2e
63 62 oveq1d c=2b+log2ece+∞=e2b+log2e+∞
64 63 raleqdv c=2b+log2kece+∞yx+∞z+y<z1+lez<kyuz1+lezRuueke2b+log2e+∞yx+∞z+y<z1+lez<kyuz1+lezRuue
65 64 rexbidv c=2b+log2x+kece+∞yx+∞z+y<z1+lez<kyuz1+lezRuuex+ke2b+log2e+∞yx+∞z+y<z1+lez<kyuz1+lezRuue
66 65 ralbidv c=2b+log2e01x+kece+∞yx+∞z+y<z1+lez<kyuz1+lezRuuee01x+ke2b+log2e+∞yx+∞z+y<z1+lez<kyuz1+lezRuue
67 oveq1 l=14d+3le=14d+3e
68 67 oveq2d l=14d+31+le=1+14d+3e
69 68 oveq1d l=14d+31+lez=1+14d+3ez
70 69 breq1d l=14d+31+lez<ky1+14d+3ez<ky
71 70 anbi2d l=14d+3y<z1+lez<kyy<z1+14d+3ez<ky
72 69 oveq2d l=14d+3z1+lez=z1+14d+3ez
73 72 raleqdv l=14d+3uz1+lezRuueuz1+14d+3ezRuue
74 71 73 anbi12d l=14d+3y<z1+lez<kyuz1+lezRuuey<z1+14d+3ez<kyuz1+14d+3ezRuue
75 74 rexbidv l=14d+3z+y<z1+lez<kyuz1+lezRuuez+y<z1+14d+3ez<kyuz1+14d+3ezRuue
76 75 ralbidv l=14d+3yx+∞z+y<z1+lez<kyuz1+lezRuueyx+∞z+y<z1+14d+3ez<kyuz1+14d+3ezRuue
77 76 rexralbidv l=14d+3x+ke2b+log2e+∞yx+∞z+y<z1+lez<kyuz1+lezRuuex+ke2b+log2e+∞yx+∞z+y<z1+14d+3ez<kyuz1+14d+3ezRuue
78 77 ralbidv l=14d+3e01x+ke2b+log2e+∞yx+∞z+y<z1+lez<kyuz1+lezRuuee01x+ke2b+log2e+∞yx+∞z+y<z1+14d+3ez<kyuz1+14d+3ezRuue
79 66 78 rspc2ev 2b+log2+14d+301e01x+ke2b+log2e+∞yx+∞z+y<z1+14d+3ez<kyuz1+14d+3ezRuuec+l01e01x+kece+∞yx+∞z+y<z1+lez<kyuz1+lezRuue
80 14 18 61 79 syl3anc d+b+x+Rxxdf01g+mebf+∞vg+∞nv<nnmvRnnfc+l01e01x+kece+∞yx+∞z+y<z1+lez<kyuz1+lezRuue
81 80 ex d+b+x+Rxxdf01g+mebf+∞vg+∞nv<nnmvRnnfc+l01e01x+kece+∞yx+∞z+y<z1+lez<kyuz1+lezRuue
82 81 rexlimivv d+b+x+Rxxdf01g+mebf+∞vg+∞nv<nnmvRnnfc+l01e01x+kece+∞yx+∞z+y<z1+lez<kyuz1+lezRuue
83 4 82 sylbir d+x+Rxxdb+f01g+mebf+∞vg+∞nv<nnmvRnnfc+l01e01x+kece+∞yx+∞z+y<z1+lez<kyuz1+lezRuue
84 2 3 83 mp2an c+l01e01x+kece+∞yx+∞z+y<z1+lez<kyuz1+lezRuue