Step | Hyp | Ref
| Expression |
1 | | aaliou3lem8 25849 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โ+)
โ โ๐ โ
โ (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐))) |
2 | | aaliou3lem.c |
. . . . . . . . 9
โข ๐น = (๐ โ โ โฆ
(2โ-(!โ๐))) |
3 | | aaliou3lem.d |
. . . . . . . . 9
โข ๐ฟ = ฮฃ๐ โ โ (๐นโ๐) |
4 | | aaliou3lem.e |
. . . . . . . . 9
โข ๐ป = (๐ โ โ โฆ ฮฃ๐ โ (1...๐)(๐นโ๐)) |
5 | 2, 3, 4 | aaliou3lem6 25852 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ปโ๐) ยท (2โ(!โ๐))) โ
โค) |
6 | 5 | ad2antrl 726 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ ((๐ปโ๐) ยท (2โ(!โ๐))) โ
โค) |
7 | | 2nn 12281 |
. . . . . . . 8
โข 2 โ
โ |
8 | | nnnn0 12475 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ0) |
9 | 8 | ad2antrl 726 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ ๐ โ โ0) |
10 | | faccl 14239 |
. . . . . . . . 9
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
11 | | nnnn0 12475 |
. . . . . . . . 9
โข
((!โ๐) โ
โ โ (!โ๐)
โ โ0) |
12 | 9, 10, 11 | 3syl 18 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (!โ๐) โ
โ0) |
13 | | nnexpcl 14036 |
. . . . . . . 8
โข ((2
โ โ โง (!โ๐) โ โ0) โ
(2โ(!โ๐)) โ
โ) |
14 | 7, 12, 13 | sylancr 587 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (2โ(!โ๐)) โ
โ) |
15 | 2, 3, 4 | aaliou3lem5 25851 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ปโ๐) โ โ) |
16 | 15 | ad2antrl 726 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (๐ปโ๐) โ โ) |
17 | 16 | recnd 11238 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (๐ปโ๐) โ โ) |
18 | 14 | nncnd 12224 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (2โ(!โ๐)) โ
โ) |
19 | 14 | nnne0d 12258 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (2โ(!โ๐)) โ 0) |
20 | 17, 18, 19 | divcan4d 11992 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))) = (๐ปโ๐)) |
21 | 2, 3, 4 | aaliou3lem7 25853 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((๐ปโ๐) โ ๐ฟ โง (absโ(๐ฟ โ (๐ปโ๐))) โค (2 ยท (2โ-(!โ(๐ + 1)))))) |
22 | 21 | simpld 495 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ปโ๐) โ ๐ฟ) |
23 | 22 | ad2antrl 726 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (๐ปโ๐) โ ๐ฟ) |
24 | 20, 23 | eqnetrd 3008 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))) โ ๐ฟ) |
25 | 24 | necomd 2996 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ ๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐)))) |
26 | 25 | neneqd 2945 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ ยฌ ๐ฟ = (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐)))) |
27 | 2, 3, 4 | aaliou3lem4 25850 |
. . . . . . . . . . 11
โข ๐ฟ โ โ |
28 | 14 | nnred 12223 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (2โ(!โ๐)) โ
โ) |
29 | 16, 28 | remulcld 11240 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ ((๐ปโ๐) ยท (2โ(!โ๐))) โ
โ) |
30 | 29, 14 | nndivred 12262 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))) โ
โ) |
31 | | resubcl 11520 |
. . . . . . . . . . 11
โข ((๐ฟ โ โ โง (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))) โ โ) โ
(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐)))) โ
โ) |
32 | 27, 30, 31 | sylancr 587 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐)))) โ
โ) |
33 | 32 | recnd 11238 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐)))) โ
โ) |
34 | 33 | abscld 15379 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))))) โ
โ) |
35 | | simplr 767 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ ๐ โ โ+) |
36 | | nnnn0 12475 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ0) |
37 | 36 | ad2antrr 724 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ ๐ โ โ0) |
38 | 14, 37 | nnexpcld 14204 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ ((2โ(!โ๐))โ๐) โ โ) |
39 | 38 | nnrpd 13010 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ ((2โ(!โ๐))โ๐) โ
โ+) |
40 | 35, 39 | rpdivcld 13029 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (๐ / ((2โ(!โ๐))โ๐)) โ
โ+) |
41 | 40 | rpred 13012 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (๐ / ((2โ(!โ๐))โ๐)) โ โ) |
42 | | 2rp 12975 |
. . . . . . . . . . 11
โข 2 โ
โ+ |
43 | | peano2nn0 12508 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
44 | | faccl 14239 |
. . . . . . . . . . . . . 14
โข ((๐ + 1) โ โ0
โ (!โ(๐ + 1))
โ โ) |
45 | 9, 43, 44 | 3syl 18 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (!โ(๐ + 1)) โ โ) |
46 | | nnz 12575 |
. . . . . . . . . . . . 13
โข
((!โ(๐ + 1))
โ โ โ (!โ(๐ + 1)) โ โค) |
47 | | znegcl 12593 |
. . . . . . . . . . . . 13
โข
((!โ(๐ + 1))
โ โค โ -(!โ(๐ + 1)) โ โค) |
48 | 45, 46, 47 | 3syl 18 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ -(!โ(๐ + 1)) โ โค) |
49 | | rpexpcl 14042 |
. . . . . . . . . . . 12
โข ((2
โ โ+ โง -(!โ(๐ + 1)) โ โค) โ
(2โ-(!โ(๐ + 1)))
โ โ+) |
50 | 42, 48, 49 | sylancr 587 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (2โ-(!โ(๐ + 1))) โ
โ+) |
51 | | rpmulcl 12993 |
. . . . . . . . . . 11
โข ((2
โ โ+ โง (2โ-(!โ(๐ + 1))) โ โ+) โ (2
ยท (2โ-(!โ(๐ + 1)))) โ
โ+) |
52 | 42, 50, 51 | sylancr 587 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (2 ยท
(2โ-(!โ(๐ +
1)))) โ โ+) |
53 | 52 | rpred 13012 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (2 ยท
(2โ-(!โ(๐ +
1)))) โ โ) |
54 | 20 | oveq2d 7421 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐)))) = (๐ฟ โ (๐ปโ๐))) |
55 | 54 | fveq2d 6892 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))))) = (absโ(๐ฟ โ (๐ปโ๐)))) |
56 | 21 | simprd 496 |
. . . . . . . . . . 11
โข (๐ โ โ โ
(absโ(๐ฟ โ
(๐ปโ๐))) โค (2 ยท (2โ-(!โ(๐ + 1))))) |
57 | 56 | ad2antrl 726 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (absโ(๐ฟ โ (๐ปโ๐))) โค (2 ยท (2โ-(!โ(๐ + 1))))) |
58 | 55, 57 | eqbrtrd 5169 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))))) โค (2 ยท
(2โ-(!โ(๐ +
1))))) |
59 | | simprr 771 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (2 ยท
(2โ-(!โ(๐ +
1)))) โค (๐ /
((2โ(!โ๐))โ๐))) |
60 | 34, 53, 41, 58, 59 | letrd 11367 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))))) โค (๐ / ((2โ(!โ๐))โ๐))) |
61 | 34, 41, 60 | lensymd 11361 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ ยฌ (๐ / ((2โ(!โ๐))โ๐)) < (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐)))))) |
62 | | oveq1 7412 |
. . . . . . . . . . 11
โข (๐ = ((๐ปโ๐) ยท (2โ(!โ๐))) โ (๐ / ๐) = (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐)) |
63 | 62 | eqeq2d 2743 |
. . . . . . . . . 10
โข (๐ = ((๐ปโ๐) ยท (2โ(!โ๐))) โ (๐ฟ = (๐ / ๐) โ ๐ฟ = (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐))) |
64 | 63 | notbid 317 |
. . . . . . . . 9
โข (๐ = ((๐ปโ๐) ยท (2โ(!โ๐))) โ (ยฌ ๐ฟ = (๐ / ๐) โ ยฌ ๐ฟ = (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐))) |
65 | 62 | oveq2d 7421 |
. . . . . . . . . . . 12
โข (๐ = ((๐ปโ๐) ยท (2โ(!โ๐))) โ (๐ฟ โ (๐ / ๐)) = (๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐))) |
66 | 65 | fveq2d 6892 |
. . . . . . . . . . 11
โข (๐ = ((๐ปโ๐) ยท (2โ(!โ๐))) โ (absโ(๐ฟ โ (๐ / ๐))) = (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐)))) |
67 | 66 | breq2d 5159 |
. . . . . . . . . 10
โข (๐ = ((๐ปโ๐) ยท (2โ(!โ๐))) โ ((๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))) โ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐))))) |
68 | 67 | notbid 317 |
. . . . . . . . 9
โข (๐ = ((๐ปโ๐) ยท (2โ(!โ๐))) โ (ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))) โ ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐))))) |
69 | 64, 68 | anbi12d 631 |
. . . . . . . 8
โข (๐ = ((๐ปโ๐) ยท (2โ(!โ๐))) โ ((ยฌ ๐ฟ = (๐ / ๐) โง ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐)))) โ (ยฌ ๐ฟ = (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐) โง ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐)))))) |
70 | | oveq2 7413 |
. . . . . . . . . . 11
โข (๐ = (2โ(!โ๐)) โ (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐) = (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐)))) |
71 | 70 | eqeq2d 2743 |
. . . . . . . . . 10
โข (๐ = (2โ(!โ๐)) โ (๐ฟ = (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐) โ ๐ฟ = (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))))) |
72 | 71 | notbid 317 |
. . . . . . . . 9
โข (๐ = (2โ(!โ๐)) โ (ยฌ ๐ฟ = (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐) โ ยฌ ๐ฟ = (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))))) |
73 | | oveq1 7412 |
. . . . . . . . . . . 12
โข (๐ = (2โ(!โ๐)) โ (๐โ๐) = ((2โ(!โ๐))โ๐)) |
74 | 73 | oveq2d 7421 |
. . . . . . . . . . 11
โข (๐ = (2โ(!โ๐)) โ (๐ / (๐โ๐)) = (๐ / ((2โ(!โ๐))โ๐))) |
75 | 70 | oveq2d 7421 |
. . . . . . . . . . . 12
โข (๐ = (2โ(!โ๐)) โ (๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐)) = (๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))))) |
76 | 75 | fveq2d 6892 |
. . . . . . . . . . 11
โข (๐ = (2โ(!โ๐)) โ (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐))) = (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐)))))) |
77 | 74, 76 | breq12d 5160 |
. . . . . . . . . 10
โข (๐ = (2โ(!โ๐)) โ ((๐ / (๐โ๐)) < (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐))) โ (๐ / ((2โ(!โ๐))โ๐)) < (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))))))) |
78 | 77 | notbid 317 |
. . . . . . . . 9
โข (๐ = (2โ(!โ๐)) โ (ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐))) โ ยฌ (๐ / ((2โ(!โ๐))โ๐)) < (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))))))) |
79 | 72, 78 | anbi12d 631 |
. . . . . . . 8
โข (๐ = (2โ(!โ๐)) โ ((ยฌ ๐ฟ = (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐) โง ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / ๐)))) โ (ยฌ ๐ฟ = (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))) โง ยฌ (๐ / ((2โ(!โ๐))โ๐)) < (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐)))))))) |
80 | 69, 79 | rspc2ev 3623 |
. . . . . . 7
โข ((((๐ปโ๐) ยท (2โ(!โ๐))) โ โค โง
(2โ(!โ๐)) โ
โ โง (ยฌ ๐ฟ =
(((๐ปโ๐) ยท
(2โ(!โ๐))) /
(2โ(!โ๐))) โง
ยฌ (๐ /
((2โ(!โ๐))โ๐)) < (absโ(๐ฟ โ (((๐ปโ๐) ยท (2โ(!โ๐))) / (2โ(!โ๐))))))) โ โ๐ โ โค โ๐ โ โ (ยฌ ๐ฟ = (๐ / ๐) โง ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))))) |
81 | 6, 14, 26, 61, 80 | syl112anc 1374 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ+)
โง (๐ โ โ
โง (2 ยท (2โ-(!โ(๐ + 1)))) โค (๐ / ((2โ(!โ๐))โ๐)))) โ โ๐ โ โค โ๐ โ โ (ยฌ ๐ฟ = (๐ / ๐) โง ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))))) |
82 | 1, 81 | rexlimddv 3161 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ+)
โ โ๐ โ
โค โ๐ โ
โ (ยฌ ๐ฟ = (๐ / ๐) โง ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))))) |
83 | | pm4.56 987 |
. . . . . . . . 9
โข ((ยฌ
๐ฟ = (๐ / ๐) โง ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐)))) โ ยฌ (๐ฟ = (๐ / ๐) โจ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))))) |
84 | 83 | rexbii 3094 |
. . . . . . . 8
โข
(โ๐ โ
โ (ยฌ ๐ฟ = (๐ / ๐) โง ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐)))) โ โ๐ โ โ ยฌ (๐ฟ = (๐ / ๐) โจ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))))) |
85 | | rexnal 3100 |
. . . . . . . 8
โข
(โ๐ โ
โ ยฌ (๐ฟ = (๐ / ๐) โจ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐)))) โ ยฌ โ๐ โ โ (๐ฟ = (๐ / ๐) โจ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))))) |
86 | 84, 85 | bitri 274 |
. . . . . . 7
โข
(โ๐ โ
โ (ยฌ ๐ฟ = (๐ / ๐) โง ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐)))) โ ยฌ โ๐ โ โ (๐ฟ = (๐ / ๐) โจ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))))) |
87 | 86 | rexbii 3094 |
. . . . . 6
โข
(โ๐ โ
โค โ๐ โ
โ (ยฌ ๐ฟ = (๐ / ๐) โง ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐)))) โ โ๐ โ โค ยฌ โ๐ โ โ (๐ฟ = (๐ / ๐) โจ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))))) |
88 | | rexnal 3100 |
. . . . . 6
โข
(โ๐ โ
โค ยฌ โ๐
โ โ (๐ฟ = (๐ / ๐) โจ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐)))) โ ยฌ โ๐ โ โค โ๐ โ โ (๐ฟ = (๐ / ๐) โจ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))))) |
89 | 87, 88 | bitri 274 |
. . . . 5
โข
(โ๐ โ
โค โ๐ โ
โ (ยฌ ๐ฟ = (๐ / ๐) โง ยฌ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐)))) โ ยฌ โ๐ โ โค โ๐ โ โ (๐ฟ = (๐ / ๐) โจ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))))) |
90 | 82, 89 | sylib 217 |
. . . 4
โข ((๐ โ โ โง ๐ โ โ+)
โ ยฌ โ๐
โ โค โ๐
โ โ (๐ฟ = (๐ / ๐) โจ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))))) |
91 | 90 | nrexdv 3149 |
. . 3
โข (๐ โ โ โ ยฌ
โ๐ โ
โ+ โ๐ โ โค โ๐ โ โ (๐ฟ = (๐ / ๐) โจ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))))) |
92 | 91 | nrex 3074 |
. 2
โข ยฌ
โ๐ โ โ
โ๐ โ
โ+ โ๐ โ โค โ๐ โ โ (๐ฟ = (๐ / ๐) โจ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐)))) |
93 | | aaliou2b 25845 |
. 2
โข (๐ฟ โ ๐ธ โ
โ๐ โ โ
โ๐ โ
โ+ โ๐ โ โค โ๐ โ โ (๐ฟ = (๐ / ๐) โจ (๐ / (๐โ๐)) < (absโ(๐ฟ โ (๐ / ๐))))) |
94 | 92, 93 | mto 196 |
1
โข ยฌ
๐ฟ โ
๐ธ |