Step | Hyp | Ref
| Expression |
1 | | 2rp 12785 |
. . . . . 6
โข 2 โ
โ+ |
2 | | rpdivcl 12805 |
. . . . . 6
โข ((2
โ โ+ โง ๐ต โ โ+) โ (2 /
๐ต) โ
โ+) |
3 | 1, 2 | mpan 688 |
. . . . 5
โข (๐ต โ โ+
โ (2 / ๐ต) โ
โ+) |
4 | 3 | rpred 12822 |
. . . 4
โข (๐ต โ โ+
โ (2 / ๐ต) โ
โ) |
5 | | 2re 12097 |
. . . . 5
โข 2 โ
โ |
6 | | 1lt2 12194 |
. . . . 5
โข 1 <
2 |
7 | | expnbnd 13997 |
. . . . 5
โข (((2 /
๐ต) โ โ โง 2
โ โ โง 1 < 2) โ โ๐ โ โ (2 / ๐ต) < (2โ๐)) |
8 | 5, 6, 7 | mp3an23 1453 |
. . . 4
โข ((2 /
๐ต) โ โ โ
โ๐ โ โ (2
/ ๐ต) < (2โ๐)) |
9 | 4, 8 | syl 17 |
. . 3
โข (๐ต โ โ+
โ โ๐ โ
โ (2 / ๐ต) <
(2โ๐)) |
10 | 9 | adantl 483 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ+)
โ โ๐ โ
โ (2 / ๐ต) <
(2โ๐)) |
11 | | simprl 769 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ๐ โ
โ) |
12 | | simpll 765 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ๐ด โ
โ) |
13 | | nnaddm1cl 12427 |
. . . 4
โข ((๐ โ โ โง ๐ด โ โ) โ ((๐ + ๐ด) โ 1) โ
โ) |
14 | 11, 12, 13 | syl2anc 585 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ((๐ + ๐ด) โ 1) โ
โ) |
15 | | simplr 767 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ๐ต โ
โ+) |
16 | | rerpdivcl 12810 |
. . . . . . . . . 10
โข ((2
โ โ โง ๐ต
โ โ+) โ (2 / ๐ต) โ โ) |
17 | 5, 15, 16 | sylancr 588 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (2 /
๐ต) โ
โ) |
18 | 11 | nnnn0d 12343 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ๐ โ
โ0) |
19 | | reexpcl 13849 |
. . . . . . . . . 10
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
20 | 5, 18, 19 | sylancr 588 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(2โ๐) โ
โ) |
21 | 11, 12 | nnaddcld 12075 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (๐ + ๐ด) โ โ) |
22 | | nnm1nn0 12324 |
. . . . . . . . . . . . . . . 16
โข ((๐ + ๐ด) โ โ โ ((๐ + ๐ด) โ 1) โ
โ0) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ((๐ + ๐ด) โ 1) โ
โ0) |
24 | | peano2nn0 12323 |
. . . . . . . . . . . . . . 15
โข (((๐ + ๐ด) โ 1) โ โ0
โ (((๐ + ๐ด) โ 1) + 1) โ
โ0) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(((๐ + ๐ด) โ 1) + 1) โ
โ0) |
26 | 25 | faccld 14048 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(!โ(((๐ + ๐ด) โ 1) + 1)) โ
โ) |
27 | 26 | nnzd 12475 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(!โ(((๐ + ๐ด) โ 1) + 1)) โ
โค) |
28 | 23 | faccld 14048 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(!โ((๐ + ๐ด) โ 1)) โ
โ) |
29 | 28 | nnzd 12475 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(!โ((๐ + ๐ด) โ 1)) โ
โค) |
30 | 12 | nnzd 12475 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ๐ด โ
โค) |
31 | 29, 30 | zmulcld 12482 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด) โ
โค) |
32 | 27, 31 | zsubcld 12481 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((!โ(((๐ + ๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด)) โ
โค) |
33 | | rpexpcl 13851 |
. . . . . . . . . . 11
โข ((2
โ โ+ โง ((!โ(((๐ + ๐ด) โ 1) + 1)) โ ((!โ((๐ + ๐ด) โ 1)) ยท ๐ด)) โ โค) โ
(2โ((!โ(((๐ +
๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด))) โ
โ+) |
34 | 1, 32, 33 | sylancr 588 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(2โ((!โ(((๐ +
๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด))) โ
โ+) |
35 | 34 | rpred 12822 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(2โ((!โ(((๐ +
๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด))) โ
โ) |
36 | | simprr 771 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (2 /
๐ต) < (2โ๐)) |
37 | 17, 20, 36 | ltled 11173 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (2 /
๐ต) โค (2โ๐)) |
38 | 5 | a1i 11 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ 2
โ โ) |
39 | | 1le2 12232 |
. . . . . . . . . . 11
โข 1 โค
2 |
40 | 39 | a1i 11 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ 1 โค
2) |
41 | 11 | nnred 12038 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ๐ โ
โ) |
42 | 28 | nnred 12038 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(!โ((๐ + ๐ด) โ 1)) โ
โ) |
43 | 18 | nn0ge0d 12346 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ 0 โค
๐) |
44 | 28 | nnge1d 12071 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ 1 โค
(!โ((๐ + ๐ด) โ 1))) |
45 | 41, 42, 43, 44 | lemulge12d 11963 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ๐ โค ((!โ((๐ + ๐ด) โ 1)) ยท ๐)) |
46 | | facp1 14042 |
. . . . . . . . . . . . . . 15
โข (((๐ + ๐ด) โ 1) โ โ0
โ (!โ(((๐ +
๐ด) โ 1) + 1)) =
((!โ((๐ + ๐ด) โ 1)) ยท (((๐ + ๐ด) โ 1) + 1))) |
47 | 23, 46 | syl 17 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(!โ(((๐ + ๐ด) โ 1) + 1)) =
((!โ((๐ + ๐ด) โ 1)) ยท (((๐ + ๐ด) โ 1) + 1))) |
48 | 47 | oveq1d 7322 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((!โ(((๐ + ๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด)) = (((!โ((๐ + ๐ด) โ 1)) ยท (((๐ + ๐ด) โ 1) + 1)) โ ((!โ((๐ + ๐ด) โ 1)) ยท ๐ด))) |
49 | 28 | nncnd 12039 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(!โ((๐ + ๐ด) โ 1)) โ
โ) |
50 | 25 | nn0cnd 12345 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(((๐ + ๐ด) โ 1) + 1) โ
โ) |
51 | 12 | nncnd 12039 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ๐ด โ
โ) |
52 | 49, 50, 51 | subdid 11481 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((!โ((๐ + ๐ด) โ 1)) ยท ((((๐ + ๐ด) โ 1) + 1) โ ๐ด)) = (((!โ((๐ + ๐ด) โ 1)) ยท (((๐ + ๐ด) โ 1) + 1)) โ ((!โ((๐ + ๐ด) โ 1)) ยท ๐ด))) |
53 | 11 | nncnd 12039 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ๐ โ
โ) |
54 | 21 | nncnd 12039 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (๐ + ๐ด) โ โ) |
55 | | 1cnd 11020 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ 1
โ โ) |
56 | 54, 55 | npcand 11386 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(((๐ + ๐ด) โ 1) + 1) = (๐ + ๐ด)) |
57 | 53, 51, 56 | mvrraddd 11437 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((((๐ + ๐ด) โ 1) + 1) โ ๐ด) = ๐) |
58 | 57 | oveq2d 7323 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((!โ((๐ + ๐ด) โ 1)) ยท ((((๐ + ๐ด) โ 1) + 1) โ ๐ด)) = ((!โ((๐ + ๐ด) โ 1)) ยท ๐)) |
59 | 48, 52, 58 | 3eqtr2d 2782 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((!โ(((๐ + ๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด)) = ((!โ((๐ + ๐ด) โ 1)) ยท ๐)) |
60 | 45, 59 | breqtrrd 5109 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ๐ โค ((!โ(((๐ + ๐ด) โ 1) + 1)) โ ((!โ((๐ + ๐ด) โ 1)) ยท ๐ด))) |
61 | 11 | nnzd 12475 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ๐ โ
โค) |
62 | | eluz 12646 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง
((!โ(((๐ + ๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด)) โ โค) โ
(((!โ(((๐ + ๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด)) โ
(โคโฅโ๐) โ ๐ โค ((!โ(((๐ + ๐ด) โ 1) + 1)) โ ((!โ((๐ + ๐ด) โ 1)) ยท ๐ด)))) |
63 | 61, 32, 62 | syl2anc 585 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(((!โ(((๐ + ๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด)) โ
(โคโฅโ๐) โ ๐ โค ((!โ(((๐ + ๐ด) โ 1) + 1)) โ ((!โ((๐ + ๐ด) โ 1)) ยท ๐ด)))) |
64 | 60, 63 | mpbird 257 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((!โ(((๐ + ๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด)) โ
(โคโฅโ๐)) |
65 | 38, 40, 64 | leexp2ad 14021 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(2โ๐) โค
(2โ((!โ(((๐ +
๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด)))) |
66 | 17, 20, 35, 37, 65 | letrd 11182 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (2 /
๐ต) โค
(2โ((!โ(((๐ +
๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด)))) |
67 | | rpcnne0 12798 |
. . . . . . . . . . 11
โข (2 โ
โ+ โ (2 โ โ โง 2 โ 0)) |
68 | 1, 67 | mp1i 13 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (2
โ โ โง 2 โ 0)) |
69 | | expsub 13881 |
. . . . . . . . . 10
โข (((2
โ โ โง 2 โ 0) โง ((!โ(((๐ + ๐ด) โ 1) + 1)) โ โค โง
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด) โ โค)) โ
(2โ((!โ(((๐ +
๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด))) = ((2โ(!โ(((๐ + ๐ด) โ 1) + 1))) /
(2โ((!โ((๐ +
๐ด) โ 1)) ยท
๐ด)))) |
70 | 68, 27, 31, 69 | syl12anc 835 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(2โ((!โ(((๐ +
๐ด) โ 1) + 1)) โ
((!โ((๐ + ๐ด) โ 1)) ยท ๐ด))) = ((2โ(!โ(((๐ + ๐ด) โ 1) + 1))) /
(2โ((!โ((๐ +
๐ด) โ 1)) ยท
๐ด)))) |
71 | | 2cn 12098 |
. . . . . . . . . . . 12
โข 2 โ
โ |
72 | 71 | a1i 11 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ 2
โ โ) |
73 | 12 | nnnn0d 12343 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ๐ด โ
โ0) |
74 | 28 | nnnn0d 12343 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(!โ((๐ + ๐ด) โ 1)) โ
โ0) |
75 | 72, 73, 74 | expmuld 13917 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(2โ((!โ((๐ +
๐ด) โ 1)) ยท
๐ด)) =
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด)) |
76 | 75 | oveq2d 7323 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((2โ(!โ(((๐ +
๐ด) โ 1) + 1))) /
(2โ((!โ((๐ +
๐ด) โ 1)) ยท
๐ด))) =
((2โ(!โ(((๐ +
๐ด) โ 1) + 1))) /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด))) |
77 | | rpexpcl 13851 |
. . . . . . . . . . . 12
โข ((2
โ โ+ โง (!โ(((๐ + ๐ด) โ 1) + 1)) โ โค) โ
(2โ(!โ(((๐ +
๐ด) โ 1) + 1))) โ
โ+) |
78 | 1, 27, 77 | sylancr 588 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(2โ(!โ(((๐ +
๐ด) โ 1) + 1))) โ
โ+) |
79 | 78 | rpcnd 12824 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(2โ(!โ(((๐ +
๐ด) โ 1) + 1))) โ
โ) |
80 | | rpexpcl 13851 |
. . . . . . . . . . . . 13
โข ((2
โ โ+ โง (!โ((๐ + ๐ด) โ 1)) โ โค) โ
(2โ(!โ((๐ +
๐ด) โ 1))) โ
โ+) |
81 | 1, 29, 80 | sylancr 588 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(2โ(!โ((๐ +
๐ด) โ 1))) โ
โ+) |
82 | 81, 30 | rpexpcld 14012 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด) โ
โ+) |
83 | 82 | rpcnd 12824 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด) โ
โ) |
84 | 82 | rpne0d 12827 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด) โ 0) |
85 | 79, 83, 84 | divrecd 11804 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((2โ(!โ(((๐ +
๐ด) โ 1) + 1))) /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด)) = ((2โ(!โ(((๐ + ๐ด) โ 1) + 1))) ยท (1 /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด)))) |
86 | 70, 76, 85 | 3eqtrrd 2781 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((2โ(!โ(((๐ +
๐ด) โ 1) + 1)))
ยท (1 / ((2โ(!โ((๐ + ๐ด) โ 1)))โ๐ด))) = (2โ((!โ(((๐ + ๐ด) โ 1) + 1)) โ ((!โ((๐ + ๐ด) โ 1)) ยท ๐ด)))) |
87 | 66, 86 | breqtrrd 5109 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (2 /
๐ต) โค
((2โ(!โ(((๐ +
๐ด) โ 1) + 1)))
ยท (1 / ((2โ(!โ((๐ + ๐ด) โ 1)))โ๐ด)))) |
88 | 82 | rpreccld 12832 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (1 /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด)) โ
โ+) |
89 | 78, 88 | rpmulcld 12838 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((2โ(!โ(((๐ +
๐ด) โ 1) + 1)))
ยท (1 / ((2โ(!โ((๐ + ๐ด) โ 1)))โ๐ด))) โ
โ+) |
90 | 89 | rpred 12822 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
((2โ(!โ(((๐ +
๐ด) โ 1) + 1)))
ยท (1 / ((2โ(!โ((๐ + ๐ด) โ 1)))โ๐ด))) โ โ) |
91 | 38, 90, 15 | ledivmuld 12875 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ((2 /
๐ต) โค
((2โ(!โ(((๐ +
๐ด) โ 1) + 1)))
ยท (1 / ((2โ(!โ((๐ + ๐ด) โ 1)))โ๐ด))) โ 2 โค (๐ต ยท ((2โ(!โ(((๐ + ๐ด) โ 1) + 1))) ยท (1 /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด)))))) |
92 | 87, 91 | mpbid 231 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ 2 โค
(๐ต ยท
((2โ(!โ(((๐ +
๐ด) โ 1) + 1)))
ยท (1 / ((2โ(!โ((๐ + ๐ด) โ 1)))โ๐ด))))) |
93 | 15 | rpcnd 12824 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ๐ต โ
โ) |
94 | 88 | rpcnd 12824 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (1 /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด)) โ
โ) |
95 | 93, 79, 94 | mul12d 11234 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (๐ต ยท
((2โ(!โ(((๐ +
๐ด) โ 1) + 1)))
ยท (1 / ((2โ(!โ((๐ + ๐ด) โ 1)))โ๐ด)))) = ((2โ(!โ(((๐ + ๐ด) โ 1) + 1))) ยท (๐ต ยท (1 /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด))))) |
96 | 92, 95 | breqtrd 5107 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ 2 โค
((2โ(!โ(((๐ +
๐ด) โ 1) + 1)))
ยท (๐ต ยท (1 /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด))))) |
97 | 15, 88 | rpmulcld 12838 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (๐ต ยท (1 /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด))) โ
โ+) |
98 | 97 | rpred 12822 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (๐ต ยท (1 /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด))) โ
โ) |
99 | 38, 98, 78 | ledivmuld 12875 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ ((2 /
(2โ(!โ(((๐ +
๐ด) โ 1) + 1)))) โค
(๐ต ยท (1 /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด))) โ 2 โค
((2โ(!โ(((๐ +
๐ด) โ 1) + 1)))
ยท (๐ต ยท (1 /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด)))))) |
100 | 96, 99 | mpbird 257 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (2 /
(2โ(!โ(((๐ +
๐ด) โ 1) + 1)))) โค
(๐ต ยท (1 /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด)))) |
101 | 26 | nnnn0d 12343 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(!โ(((๐ + ๐ด) โ 1) + 1)) โ
โ0) |
102 | | expneg 13840 |
. . . . . . 7
โข ((2
โ โ โง (!โ(((๐ + ๐ด) โ 1) + 1)) โ
โ0) โ (2โ-(!โ(((๐ + ๐ด) โ 1) + 1))) = (1 /
(2โ(!โ(((๐ +
๐ด) โ 1) +
1))))) |
103 | 71, 101, 102 | sylancr 588 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(2โ-(!โ(((๐ +
๐ด) โ 1) + 1))) = (1 /
(2โ(!โ(((๐ +
๐ด) โ 1) +
1))))) |
104 | 103 | oveq2d 7323 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (2
ยท (2โ-(!โ(((๐ + ๐ด) โ 1) + 1)))) = (2 ยท (1 /
(2โ(!โ(((๐ +
๐ด) โ 1) +
1)))))) |
105 | 78 | rpne0d 12827 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
(2โ(!โ(((๐ +
๐ด) โ 1) + 1))) โ
0) |
106 | 72, 79, 105 | divrecd 11804 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (2 /
(2โ(!โ(((๐ +
๐ด) โ 1) + 1)))) = (2
ยท (1 / (2โ(!โ(((๐ + ๐ด) โ 1) + 1)))))) |
107 | 104, 106 | eqtr4d 2779 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (2
ยท (2โ-(!โ(((๐ + ๐ด) โ 1) + 1)))) = (2 /
(2โ(!โ(((๐ +
๐ด) โ 1) +
1))))) |
108 | 93, 83, 84 | divrecd 11804 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (๐ต / ((2โ(!โ((๐ + ๐ด) โ 1)))โ๐ด)) = (๐ต ยท (1 / ((2โ(!โ((๐ + ๐ด) โ 1)))โ๐ด)))) |
109 | 100, 107,
108 | 3brtr4d 5113 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ (2
ยท (2โ-(!โ(((๐ + ๐ด) โ 1) + 1)))) โค (๐ต / ((2โ(!โ((๐ + ๐ด) โ 1)))โ๐ด))) |
110 | | fvoveq1 7330 |
. . . . . . . 8
โข (๐ฅ = ((๐ + ๐ด) โ 1) โ (!โ(๐ฅ + 1)) = (!โ(((๐ + ๐ด) โ 1) + 1))) |
111 | 110 | negeqd 11265 |
. . . . . . 7
โข (๐ฅ = ((๐ + ๐ด) โ 1) โ -(!โ(๐ฅ + 1)) = -(!โ(((๐ + ๐ด) โ 1) + 1))) |
112 | 111 | oveq2d 7323 |
. . . . . 6
โข (๐ฅ = ((๐ + ๐ด) โ 1) โ (2โ-(!โ(๐ฅ + 1))) =
(2โ-(!โ(((๐ +
๐ด) โ 1) +
1)))) |
113 | 112 | oveq2d 7323 |
. . . . 5
โข (๐ฅ = ((๐ + ๐ด) โ 1) โ (2 ยท
(2โ-(!โ(๐ฅ +
1)))) = (2 ยท (2โ-(!โ(((๐ + ๐ด) โ 1) + 1))))) |
114 | | fveq2 6804 |
. . . . . . . 8
โข (๐ฅ = ((๐ + ๐ด) โ 1) โ (!โ๐ฅ) = (!โ((๐ + ๐ด) โ 1))) |
115 | 114 | oveq2d 7323 |
. . . . . . 7
โข (๐ฅ = ((๐ + ๐ด) โ 1) โ (2โ(!โ๐ฅ)) = (2โ(!โ((๐ + ๐ด) โ 1)))) |
116 | 115 | oveq1d 7322 |
. . . . . 6
โข (๐ฅ = ((๐ + ๐ด) โ 1) โ ((2โ(!โ๐ฅ))โ๐ด) = ((2โ(!โ((๐ + ๐ด) โ 1)))โ๐ด)) |
117 | 116 | oveq2d 7323 |
. . . . 5
โข (๐ฅ = ((๐ + ๐ด) โ 1) โ (๐ต / ((2โ(!โ๐ฅ))โ๐ด)) = (๐ต / ((2โ(!โ((๐ + ๐ด) โ 1)))โ๐ด))) |
118 | 113, 117 | breq12d 5094 |
. . . 4
โข (๐ฅ = ((๐ + ๐ด) โ 1) โ ((2 ยท
(2โ-(!โ(๐ฅ +
1)))) โค (๐ต /
((2โ(!โ๐ฅ))โ๐ด)) โ (2 ยท
(2โ-(!โ(((๐ +
๐ด) โ 1) + 1)))) โค
(๐ต /
((2โ(!โ((๐ +
๐ด) โ 1)))โ๐ด)))) |
119 | 118 | rspcev 3566 |
. . 3
โข ((((๐ + ๐ด) โ 1) โ โ โง (2
ยท (2โ-(!โ(((๐ + ๐ด) โ 1) + 1)))) โค (๐ต / ((2โ(!โ((๐ + ๐ด) โ 1)))โ๐ด))) โ โ๐ฅ โ โ (2 ยท
(2โ-(!โ(๐ฅ +
1)))) โค (๐ต /
((2โ(!โ๐ฅ))โ๐ด))) |
120 | 14, 109, 119 | syl2anc 585 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ+)
โง (๐ โ โ
โง (2 / ๐ต) <
(2โ๐))) โ
โ๐ฅ โ โ (2
ยท (2โ-(!โ(๐ฅ + 1)))) โค (๐ต / ((2โ(!โ๐ฅ))โ๐ด))) |
121 | 10, 120 | rexlimddv 3155 |
1
โข ((๐ด โ โ โง ๐ต โ โ+)
โ โ๐ฅ โ
โ (2 ยท (2โ-(!โ(๐ฅ + 1)))) โค (๐ต / ((2โ(!โ๐ฅ))โ๐ด))) |