Step | Hyp | Ref
| Expression |
1 | | pntlem1.w |
. 2
โข ๐ = (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) |
2 | | pntlem1.y |
. . . . . 6
โข (๐ โ (๐ โ โ+ โง 1 โค
๐)) |
3 | 2 | simpld 496 |
. . . . 5
โข (๐ โ ๐ โ
โ+) |
4 | | 4nn 12243 |
. . . . . . 7
โข 4 โ
โ |
5 | | nnrp 12933 |
. . . . . . 7
โข (4 โ
โ โ 4 โ โ+) |
6 | 4, 5 | ax-mp 5 |
. . . . . 6
โข 4 โ
โ+ |
7 | | pntlem1.r |
. . . . . . . . 9
โข ๐
= (๐ โ โ+ โฆ
((ฯโ๐) โ
๐)) |
8 | | pntlem1.a |
. . . . . . . . 9
โข (๐ โ ๐ด โ
โ+) |
9 | | pntlem1.b |
. . . . . . . . 9
โข (๐ โ ๐ต โ
โ+) |
10 | | pntlem1.l |
. . . . . . . . 9
โข (๐ โ ๐ฟ โ (0(,)1)) |
11 | | pntlem1.d |
. . . . . . . . 9
โข ๐ท = (๐ด + 1) |
12 | | pntlem1.f |
. . . . . . . . 9
โข ๐น = ((1 โ (1 / ๐ท)) ยท ((๐ฟ / (;32 ยท ๐ต)) / (๐ทโ2))) |
13 | 7, 8, 9, 10, 11, 12 | pntlemd 26958 |
. . . . . . . 8
โข (๐ โ (๐ฟ โ โ+ โง ๐ท โ โ+
โง ๐น โ
โ+)) |
14 | 13 | simp1d 1143 |
. . . . . . 7
โข (๐ โ ๐ฟ โ
โ+) |
15 | | pntlem1.u |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ+) |
16 | | pntlem1.u2 |
. . . . . . . . 9
โข (๐ โ ๐ โค ๐ด) |
17 | | pntlem1.e |
. . . . . . . . 9
โข ๐ธ = (๐ / ๐ท) |
18 | | pntlem1.k |
. . . . . . . . 9
โข ๐พ = (expโ(๐ต / ๐ธ)) |
19 | 7, 8, 9, 10, 11, 12, 15, 16, 17, 18 | pntlemc 26959 |
. . . . . . . 8
โข (๐ โ (๐ธ โ โ+ โง ๐พ โ โ+
โง (๐ธ โ (0(,)1)
โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+))) |
20 | 19 | simp1d 1143 |
. . . . . . 7
โข (๐ โ ๐ธ โ
โ+) |
21 | 14, 20 | rpmulcld 12980 |
. . . . . 6
โข (๐ โ (๐ฟ ยท ๐ธ) โ
โ+) |
22 | | rpdivcl 12947 |
. . . . . 6
โข ((4
โ โ+ โง (๐ฟ ยท ๐ธ) โ โ+) โ (4 /
(๐ฟ ยท ๐ธ)) โ
โ+) |
23 | 6, 21, 22 | sylancr 588 |
. . . . 5
โข (๐ โ (4 / (๐ฟ ยท ๐ธ)) โ
โ+) |
24 | 3, 23 | rpaddcld 12979 |
. . . 4
โข (๐ โ (๐ + (4 / (๐ฟ ยท ๐ธ))) โ
โ+) |
25 | | 2z 12542 |
. . . 4
โข 2 โ
โค |
26 | | rpexpcl 13993 |
. . . 4
โข (((๐ + (4 / (๐ฟ ยท ๐ธ))) โ โ+ โง 2
โ โค) โ ((๐
+ (4 / (๐ฟ ยท ๐ธ)))โ2) โ
โ+) |
27 | 24, 25, 26 | sylancl 587 |
. . 3
โข (๐ โ ((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) โ
โ+) |
28 | | pntlem1.x |
. . . . . . 7
โข (๐ โ (๐ โ โ+ โง ๐ < ๐)) |
29 | 28 | simpld 496 |
. . . . . 6
โข (๐ โ ๐ โ
โ+) |
30 | 19 | simp2d 1144 |
. . . . . . 7
โข (๐ โ ๐พ โ
โ+) |
31 | | rpexpcl 13993 |
. . . . . . 7
โข ((๐พ โ โ+
โง 2 โ โค) โ (๐พโ2) โ
โ+) |
32 | 30, 25, 31 | sylancl 587 |
. . . . . 6
โข (๐ โ (๐พโ2) โ
โ+) |
33 | 29, 32 | rpmulcld 12980 |
. . . . 5
โข (๐ โ (๐ ยท (๐พโ2)) โ
โ+) |
34 | | 4z 12544 |
. . . . 5
โข 4 โ
โค |
35 | | rpexpcl 13993 |
. . . . 5
โข (((๐ ยท (๐พโ2)) โ โ+ โง 4
โ โค) โ ((๐
ยท (๐พโ2))โ4) โ
โ+) |
36 | 33, 34, 35 | sylancl 587 |
. . . 4
โข (๐ โ ((๐ ยท (๐พโ2))โ4) โ
โ+) |
37 | | 3nn0 12438 |
. . . . . . . . . . 11
โข 3 โ
โ0 |
38 | | 2nn 12233 |
. . . . . . . . . . 11
โข 2 โ
โ |
39 | 37, 38 | decnncl 12645 |
. . . . . . . . . 10
โข ;32 โ โ |
40 | | nnrp 12933 |
. . . . . . . . . 10
โข (;32 โ โ โ ;32 โ
โ+) |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . 9
โข ;32 โ
โ+ |
42 | | rpmulcl 12945 |
. . . . . . . . 9
โข ((;32 โ โ+ โง
๐ต โ
โ+) โ (;32
ยท ๐ต) โ
โ+) |
43 | 41, 9, 42 | sylancr 588 |
. . . . . . . 8
โข (๐ โ (;32 ยท ๐ต) โ
โ+) |
44 | 19 | simp3d 1145 |
. . . . . . . . . 10
โข (๐ โ (๐ธ โ (0(,)1) โง 1 < ๐พ โง (๐ โ ๐ธ) โ
โ+)) |
45 | 44 | simp3d 1145 |
. . . . . . . . 9
โข (๐ โ (๐ โ ๐ธ) โ
โ+) |
46 | | rpexpcl 13993 |
. . . . . . . . . . 11
โข ((๐ธ โ โ+
โง 2 โ โค) โ (๐ธโ2) โ
โ+) |
47 | 20, 25, 46 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ (๐ธโ2) โ
โ+) |
48 | 14, 47 | rpmulcld 12980 |
. . . . . . . . 9
โข (๐ โ (๐ฟ ยท (๐ธโ2)) โ
โ+) |
49 | 45, 48 | rpmulcld 12980 |
. . . . . . . 8
โข (๐ โ ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2))) โ
โ+) |
50 | 43, 49 | rpdivcld 12981 |
. . . . . . 7
โข (๐ โ ((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) โ
โ+) |
51 | | 3rp 12928 |
. . . . . . . . 9
โข 3 โ
โ+ |
52 | | rpmulcl 12945 |
. . . . . . . . 9
โข ((๐ โ โ+
โง 3 โ โ+) โ (๐ ยท 3) โ
โ+) |
53 | 15, 51, 52 | sylancl 587 |
. . . . . . . 8
โข (๐ โ (๐ ยท 3) โ
โ+) |
54 | | pntlem1.c |
. . . . . . . 8
โข (๐ โ ๐ถ โ
โ+) |
55 | 53, 54 | rpaddcld 12979 |
. . . . . . 7
โข (๐ โ ((๐ ยท 3) + ๐ถ) โ
โ+) |
56 | 50, 55 | rpmulcld 12980 |
. . . . . 6
โข (๐ โ (((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)) โ
โ+) |
57 | 56 | rpred 12964 |
. . . . 5
โข (๐ โ (((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)) โ โ) |
58 | 57 | rpefcld 15994 |
. . . 4
โข (๐ โ (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))) โ
โ+) |
59 | 36, 58 | rpaddcld 12979 |
. . 3
โข (๐ โ (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ)))) โ
โ+) |
60 | 27, 59 | rpaddcld 12979 |
. 2
โข (๐ โ (((๐ + (4 / (๐ฟ ยท ๐ธ)))โ2) + (((๐ ยท (๐พโ2))โ4) + (expโ(((;32 ยท ๐ต) / ((๐ โ ๐ธ) ยท (๐ฟ ยท (๐ธโ2)))) ยท ((๐ ยท 3) + ๐ถ))))) โ
โ+) |
61 | 1, 60 | eqeltrid 2842 |
1
โข (๐ โ ๐ โ
โ+) |