Step | Hyp | Ref
| Expression |
1 | | nn0uz 12810 |
. 2
โข
โ0 = (โคโฅโ0) |
2 | | eqid 2733 |
. 2
โข
(โคโฅโ(โโ(2 ยท
(absโ๐ด)))) =
(โคโฅโ(โโ(2 ยท (absโ๐ด)))) |
3 | | halfre 12372 |
. . 3
โข (1 / 2)
โ โ |
4 | 3 | a1i 11 |
. 2
โข (๐ด โ โ โ (1 / 2)
โ โ) |
5 | | halflt1 12376 |
. . 3
โข (1 / 2)
< 1 |
6 | 5 | a1i 11 |
. 2
โข (๐ด โ โ โ (1 / 2)
< 1) |
7 | | 2re 12232 |
. . . 4
โข 2 โ
โ |
8 | | abscl 15169 |
. . . 4
โข (๐ด โ โ โ
(absโ๐ด) โ
โ) |
9 | | remulcl 11141 |
. . . 4
โข ((2
โ โ โง (absโ๐ด) โ โ) โ (2 ยท
(absโ๐ด)) โ
โ) |
10 | 7, 8, 9 | sylancr 588 |
. . 3
โข (๐ด โ โ โ (2
ยท (absโ๐ด))
โ โ) |
11 | 7 | a1i 11 |
. . . 4
โข (๐ด โ โ โ 2 โ
โ) |
12 | | 0le2 12260 |
. . . . 5
โข 0 โค
2 |
13 | 12 | a1i 11 |
. . . 4
โข (๐ด โ โ โ 0 โค
2) |
14 | | absge0 15178 |
. . . 4
โข (๐ด โ โ โ 0 โค
(absโ๐ด)) |
15 | 11, 8, 13, 14 | mulge0d 11737 |
. . 3
โข (๐ด โ โ โ 0 โค (2
ยท (absโ๐ด))) |
16 | | flge0nn0 13731 |
. . 3
โข (((2
ยท (absโ๐ด))
โ โ โง 0 โค (2 ยท (absโ๐ด))) โ (โโ(2 ยท
(absโ๐ด))) โ
โ0) |
17 | 10, 15, 16 | syl2anc 585 |
. 2
โข (๐ด โ โ โ
(โโ(2 ยท (absโ๐ด))) โ
โ0) |
18 | | eftval.1 |
. . . . 5
โข ๐น = (๐ โ โ0 โฆ ((๐ดโ๐) / (!โ๐))) |
19 | 18 | eftval 15964 |
. . . 4
โข (๐ โ โ0
โ (๐นโ๐) = ((๐ดโ๐) / (!โ๐))) |
20 | 19 | adantl 483 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐นโ๐) = ((๐ดโ๐) / (!โ๐))) |
21 | | eftcl 15961 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐ดโ๐) / (!โ๐)) โ โ) |
22 | 20, 21 | eqeltrd 2834 |
. 2
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐นโ๐) โ
โ) |
23 | 8 | adantr 482 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ๐ด) โ
โ) |
24 | | eluznn0 12847 |
. . . . . . 7
โข
(((โโ(2 ยท (absโ๐ด))) โ โ0 โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ๐ โ โ0) |
25 | 17, 24 | sylan 581 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ๐ โ โ0) |
26 | | nn0p1nn 12457 |
. . . . . 6
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
27 | 25, 26 | syl 17 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (๐ + 1) โ โ) |
28 | 23, 27 | nndivred 12212 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((absโ๐ด) / (๐ + 1)) โ โ) |
29 | 3 | a1i 11 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (1 / 2) โ
โ) |
30 | 23, 25 | reexpcld 14074 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((absโ๐ด)โ๐) โ โ) |
31 | 25 | faccld 14190 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (!โ๐) โ
โ) |
32 | 30, 31 | nndivred 12212 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (((absโ๐ด)โ๐) / (!โ๐)) โ โ) |
33 | | expcl 13991 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
34 | 25, 33 | syldan 592 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (๐ดโ๐) โ โ) |
35 | 34 | absge0d 15335 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ 0 โค
(absโ(๐ดโ๐))) |
36 | | absexp 15195 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) |
37 | 25, 36 | syldan 592 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) |
38 | 35, 37 | breqtrd 5132 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ 0 โค
((absโ๐ด)โ๐)) |
39 | 31 | nnred 12173 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (!โ๐) โ
โ) |
40 | 31 | nngt0d 12207 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ 0 <
(!โ๐)) |
41 | | divge0 12029 |
. . . . 5
โข
(((((absโ๐ด)โ๐) โ โ โง 0 โค
((absโ๐ด)โ๐)) โง ((!โ๐) โ โ โง 0 <
(!โ๐))) โ 0 โค
(((absโ๐ด)โ๐) / (!โ๐))) |
42 | 30, 38, 39, 40, 41 | syl22anc 838 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ 0 โค
(((absโ๐ด)โ๐) / (!โ๐))) |
43 | 10 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (2 ยท
(absโ๐ด)) โ
โ) |
44 | | peano2nn0 12458 |
. . . . . . . . . . 11
โข
((โโ(2 ยท (absโ๐ด))) โ โ0 โ
((โโ(2 ยท (absโ๐ด))) + 1) โ
โ0) |
45 | 17, 44 | syl 17 |
. . . . . . . . . 10
โข (๐ด โ โ โ
((โโ(2 ยท (absโ๐ด))) + 1) โ
โ0) |
46 | 45 | nn0red 12479 |
. . . . . . . . 9
โข (๐ด โ โ โ
((โโ(2 ยท (absโ๐ด))) + 1) โ โ) |
47 | 46 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((โโ(2
ยท (absโ๐ด))) +
1) โ โ) |
48 | 27 | nnred 12173 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (๐ + 1) โ โ) |
49 | | flltp1 13711 |
. . . . . . . . 9
โข ((2
ยท (absโ๐ด))
โ โ โ (2 ยท (absโ๐ด)) < ((โโ(2 ยท
(absโ๐ด))) +
1)) |
50 | 43, 49 | syl 17 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (2 ยท
(absโ๐ด)) <
((โโ(2 ยท (absโ๐ด))) + 1)) |
51 | | eluzp1p1 12796 |
. . . . . . . . . 10
โข (๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด)))) โ (๐ + 1) โ
(โคโฅโ((โโ(2 ยท (absโ๐ด))) + 1))) |
52 | 51 | adantl 483 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (๐ + 1) โ
(โคโฅโ((โโ(2 ยท (absโ๐ด))) + 1))) |
53 | | eluzle 12781 |
. . . . . . . . 9
โข ((๐ + 1) โ
(โคโฅโ((โโ(2 ยท (absโ๐ด))) + 1)) โ
((โโ(2 ยท (absโ๐ด))) + 1) โค (๐ + 1)) |
54 | 52, 53 | syl 17 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((โโ(2
ยท (absโ๐ด))) +
1) โค (๐ +
1)) |
55 | 43, 47, 48, 50, 54 | ltletrd 11320 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (2 ยท
(absโ๐ด)) < (๐ + 1)) |
56 | 23 | recnd 11188 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ๐ด) โ
โ) |
57 | | 2cn 12233 |
. . . . . . . 8
โข 2 โ
โ |
58 | | mulcom 11142 |
. . . . . . . 8
โข
(((absโ๐ด)
โ โ โง 2 โ โ) โ ((absโ๐ด) ยท 2) = (2 ยท (absโ๐ด))) |
59 | 56, 57, 58 | sylancl 587 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((absโ๐ด) ยท 2) = (2 ยท
(absโ๐ด))) |
60 | 27 | nncnd 12174 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (๐ + 1) โ โ) |
61 | 60 | mulid2d 11178 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (1 ยท (๐ + 1)) = (๐ + 1)) |
62 | 55, 59, 61 | 3brtr4d 5138 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((absโ๐ด) ยท 2) < (1 ยท
(๐ + 1))) |
63 | | 2rp 12925 |
. . . . . . . 8
โข 2 โ
โ+ |
64 | 63 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ 2 โ
โ+) |
65 | | 1red 11161 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ 1 โ
โ) |
66 | 27 | nnrpd 12960 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (๐ + 1) โ
โ+) |
67 | 23, 64, 65, 66 | lt2mul2divd 13031 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (((absโ๐ด) ยท 2) < (1 ยท
(๐ + 1)) โ
((absโ๐ด) / (๐ + 1)) < (1 /
2))) |
68 | 62, 67 | mpbid 231 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((absโ๐ด) / (๐ + 1)) < (1 / 2)) |
69 | | ltle 11248 |
. . . . . 6
โข
((((absโ๐ด) /
(๐ + 1)) โ โ
โง (1 / 2) โ โ) โ (((absโ๐ด) / (๐ + 1)) < (1 / 2) โ ((absโ๐ด) / (๐ + 1)) โค (1 / 2))) |
70 | 28, 3, 69 | sylancl 587 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (((absโ๐ด) / (๐ + 1)) < (1 / 2) โ ((absโ๐ด) / (๐ + 1)) โค (1 / 2))) |
71 | 68, 70 | mpd 15 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((absโ๐ด) / (๐ + 1)) โค (1 / 2)) |
72 | 28, 29, 32, 42, 71 | lemul2ad 12100 |
. . 3
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((absโ๐ด) / (๐ + 1))) โค ((((absโ๐ด)โ๐) / (!โ๐)) ยท (1 / 2))) |
73 | | peano2nn0 12458 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
74 | 25, 73 | syl 17 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (๐ + 1) โ
โ0) |
75 | 18 | eftval 15964 |
. . . . . 6
โข ((๐ + 1) โ โ0
โ (๐นโ(๐ + 1)) = ((๐ดโ(๐ + 1)) / (!โ(๐ + 1)))) |
76 | 74, 75 | syl 17 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (๐นโ(๐ + 1)) = ((๐ดโ(๐ + 1)) / (!โ(๐ + 1)))) |
77 | 76 | fveq2d 6847 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ(๐นโ(๐ + 1))) = (absโ((๐ดโ(๐ + 1)) / (!โ(๐ + 1))))) |
78 | | absexp 15195 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ + 1) โ
โ0) โ (absโ(๐ดโ(๐ + 1))) = ((absโ๐ด)โ(๐ + 1))) |
79 | 74, 78 | syldan 592 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ(๐ดโ(๐ + 1))) = ((absโ๐ด)โ(๐ + 1))) |
80 | 56, 25 | expp1d 14058 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((absโ๐ด)โ(๐ + 1)) = (((absโ๐ด)โ๐) ยท (absโ๐ด))) |
81 | 79, 80 | eqtrd 2773 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ(๐ดโ(๐ + 1))) = (((absโ๐ด)โ๐) ยท (absโ๐ด))) |
82 | 74 | faccld 14190 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (!โ(๐ + 1)) โ
โ) |
83 | 82 | nnred 12173 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (!โ(๐ + 1)) โ
โ) |
84 | 82 | nnnn0d 12478 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (!โ(๐ + 1)) โ
โ0) |
85 | 84 | nn0ge0d 12481 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ 0 โค
(!โ(๐ +
1))) |
86 | 83, 85 | absidd 15313 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ
(absโ(!โ(๐ +
1))) = (!โ(๐ +
1))) |
87 | | facp1 14184 |
. . . . . . . 8
โข (๐ โ โ0
โ (!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
88 | 25, 87 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (!โ(๐ + 1)) = ((!โ๐) ยท (๐ + 1))) |
89 | 86, 88 | eqtrd 2773 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ
(absโ(!โ(๐ +
1))) = ((!โ๐)
ยท (๐ +
1))) |
90 | 81, 89 | oveq12d 7376 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((absโ(๐ดโ(๐ + 1))) / (absโ(!โ(๐ + 1)))) = ((((absโ๐ด)โ๐) ยท (absโ๐ด)) / ((!โ๐) ยท (๐ + 1)))) |
91 | | expcl 13991 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ + 1) โ
โ0) โ (๐ดโ(๐ + 1)) โ โ) |
92 | 74, 91 | syldan 592 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (๐ดโ(๐ + 1)) โ โ) |
93 | 82 | nncnd 12174 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (!โ(๐ + 1)) โ
โ) |
94 | 82 | nnne0d 12208 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (!โ(๐ + 1)) โ 0) |
95 | 92, 93, 94 | absdivd 15346 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ((๐ดโ(๐ + 1)) / (!โ(๐ + 1)))) = ((absโ(๐ดโ(๐ + 1))) / (absโ(!โ(๐ + 1))))) |
96 | 30 | recnd 11188 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((absโ๐ด)โ๐) โ โ) |
97 | 31 | nncnd 12174 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (!โ๐) โ
โ) |
98 | 31 | nnne0d 12208 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (!โ๐) โ 0) |
99 | 27 | nnne0d 12208 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (๐ + 1) โ 0) |
100 | 96, 97, 56, 60, 98, 99 | divmuldivd 11977 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((absโ๐ด) / (๐ + 1))) = ((((absโ๐ด)โ๐) ยท (absโ๐ด)) / ((!โ๐) ยท (๐ + 1)))) |
101 | 90, 95, 100 | 3eqtr4d 2783 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ((๐ดโ(๐ + 1)) / (!โ(๐ + 1)))) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((absโ๐ด) / (๐ + 1)))) |
102 | 77, 101 | eqtrd 2773 |
. . 3
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ(๐นโ(๐ + 1))) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((absโ๐ด) / (๐ + 1)))) |
103 | | halfcn 12373 |
. . . . 5
โข (1 / 2)
โ โ |
104 | 25, 22 | syldan 592 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (๐นโ๐) โ โ) |
105 | 104 | abscld 15327 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ(๐นโ๐)) โ โ) |
106 | 105 | recnd 11188 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ(๐นโ๐)) โ โ) |
107 | | mulcom 11142 |
. . . . 5
โข (((1 / 2)
โ โ โง (absโ(๐นโ๐)) โ โ) โ ((1 / 2) ยท
(absโ(๐นโ๐))) = ((absโ(๐นโ๐)) ยท (1 / 2))) |
108 | 103, 106,
107 | sylancr 588 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((1 / 2) ยท
(absโ(๐นโ๐))) = ((absโ(๐นโ๐)) ยท (1 / 2))) |
109 | 25, 19 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (๐นโ๐) = ((๐ดโ๐) / (!โ๐))) |
110 | 109 | fveq2d 6847 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ(๐นโ๐)) = (absโ((๐ดโ๐) / (!โ๐)))) |
111 | | eftabs 15963 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ (absโ((๐ดโ๐) / (!โ๐))) = (((absโ๐ด)โ๐) / (!โ๐))) |
112 | 25, 111 | syldan 592 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ((๐ดโ๐) / (!โ๐))) = (((absโ๐ด)โ๐) / (!โ๐))) |
113 | 110, 112 | eqtrd 2773 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ(๐นโ๐)) = (((absโ๐ด)โ๐) / (!โ๐))) |
114 | 113 | oveq1d 7373 |
. . . 4
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((absโ(๐นโ๐)) ยท (1 / 2)) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท (1 / 2))) |
115 | 108, 114 | eqtrd 2773 |
. . 3
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ ((1 / 2) ยท
(absโ(๐นโ๐))) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท (1 / 2))) |
116 | 72, 102, 115 | 3brtr4d 5138 |
. 2
โข ((๐ด โ โ โง ๐ โ
(โคโฅโ(โโ(2 ยท (absโ๐ด))))) โ (absโ(๐นโ(๐ + 1))) โค ((1 / 2) ยท
(absโ(๐นโ๐)))) |
117 | 1, 2, 4, 6, 17, 22, 116 | cvgrat 15773 |
1
โข (๐ด โ โ โ seq0( + ,
๐น) โ dom โ
) |