Step | Hyp | Ref
| Expression |
1 | | eftl.5 |
. . . 4
โข (๐ โ ๐ด โ โ) |
2 | | eftl.4 |
. . . . 5
โข (๐ โ ๐ โ โ) |
3 | 2 | nnnn0d 12480 |
. . . 4
โข (๐ โ ๐ โ
โ0) |
4 | | eftl.1 |
. . . . 5
โข ๐น = (๐ โ โ0 โฆ ((๐ดโ๐) / (!โ๐))) |
5 | 4 | eftlcl 15996 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ0)
โ ฮฃ๐ โ
(โคโฅโ๐)(๐นโ๐) โ โ) |
6 | 1, 3, 5 | syl2anc 585 |
. . 3
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)(๐นโ๐) โ โ) |
7 | 6 | abscld 15328 |
. 2
โข (๐ โ (absโฮฃ๐ โ
(โคโฅโ๐)(๐นโ๐)) โ โ) |
8 | 1 | abscld 15328 |
. . 3
โข (๐ โ (absโ๐ด) โ
โ) |
9 | | eftl.2 |
. . . 4
โข ๐บ = (๐ โ โ0 โฆ
(((absโ๐ด)โ๐) / (!โ๐))) |
10 | 9 | reeftlcl 15997 |
. . 3
โข
(((absโ๐ด)
โ โ โง ๐
โ โ0) โ ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐) โ โ) |
11 | 8, 3, 10 | syl2anc 585 |
. 2
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐) โ โ) |
12 | 8, 3 | reexpcld 14075 |
. . 3
โข (๐ โ ((absโ๐ด)โ๐) โ โ) |
13 | | peano2nn0 12460 |
. . . . . 6
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
14 | 3, 13 | syl 17 |
. . . . 5
โข (๐ โ (๐ + 1) โ
โ0) |
15 | 14 | nn0red 12481 |
. . . 4
โข (๐ โ (๐ + 1) โ โ) |
16 | 3 | faccld 14191 |
. . . . 5
โข (๐ โ (!โ๐) โ โ) |
17 | 16, 2 | nnmulcld 12213 |
. . . 4
โข (๐ โ ((!โ๐) ยท ๐) โ โ) |
18 | 15, 17 | nndivred 12214 |
. . 3
โข (๐ โ ((๐ + 1) / ((!โ๐) ยท ๐)) โ โ) |
19 | 12, 18 | remulcld 11192 |
. 2
โข (๐ โ (((absโ๐ด)โ๐) ยท ((๐ + 1) / ((!โ๐) ยท ๐))) โ โ) |
20 | | eqid 2737 |
. . 3
โข
(โคโฅโ๐) = (โคโฅโ๐) |
21 | 2 | nnzd 12533 |
. . . 4
โข (๐ โ ๐ โ โค) |
22 | | eqidd 2738 |
. . . 4
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐) = (๐นโ๐)) |
23 | | eluznn0 12849 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ0) |
24 | 3, 23 | sylan 581 |
. . . . 5
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ0) |
25 | 4 | eftval 15966 |
. . . . . . 7
โข (๐ โ โ0
โ (๐นโ๐) = ((๐ดโ๐) / (!โ๐))) |
26 | 25 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) = ((๐ดโ๐) / (!โ๐))) |
27 | | eftcl 15963 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐ดโ๐) / (!โ๐)) โ โ) |
28 | 1, 27 | sylan 581 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ((๐ดโ๐) / (!โ๐)) โ โ) |
29 | 26, 28 | eqeltrd 2838 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) โ โ) |
30 | 24, 29 | syldan 592 |
. . . 4
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐) โ โ) |
31 | 4 | eftlcvg 15995 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ seq๐( + , ๐น) โ dom โ
) |
32 | 1, 3, 31 | syl2anc 585 |
. . . 4
โข (๐ โ seq๐( + , ๐น) โ dom โ ) |
33 | 20, 21, 22, 30, 32 | isumclim2 15650 |
. . 3
โข (๐ โ seq๐( + , ๐น) โ ฮฃ๐ โ (โคโฅโ๐)(๐นโ๐)) |
34 | | eqidd 2738 |
. . . 4
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐บโ๐) = (๐บโ๐)) |
35 | 9 | eftval 15966 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐บโ๐) = (((absโ๐ด)โ๐) / (!โ๐))) |
36 | 35 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ (๐บโ๐) = (((absโ๐ด)โ๐) / (!โ๐))) |
37 | | reeftcl 15964 |
. . . . . . . 8
โข
(((absโ๐ด)
โ โ โง ๐
โ โ0) โ (((absโ๐ด)โ๐) / (!โ๐)) โ โ) |
38 | 8, 37 | sylan 581 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
(((absโ๐ด)โ๐) / (!โ๐)) โ โ) |
39 | 36, 38 | eqeltrd 2838 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ (๐บโ๐) โ โ) |
40 | 24, 39 | syldan 592 |
. . . . 5
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐บโ๐) โ โ) |
41 | 40 | recnd 11190 |
. . . 4
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐บโ๐) โ โ) |
42 | 8 | recnd 11190 |
. . . . 5
โข (๐ โ (absโ๐ด) โ
โ) |
43 | 9 | eftlcvg 15995 |
. . . . 5
โข
(((absโ๐ด)
โ โ โง ๐
โ โ0) โ seq๐( + , ๐บ) โ dom โ ) |
44 | 42, 3, 43 | syl2anc 585 |
. . . 4
โข (๐ โ seq๐( + , ๐บ) โ dom โ ) |
45 | 20, 21, 34, 41, 44 | isumclim2 15650 |
. . 3
โข (๐ โ seq๐( + , ๐บ) โ ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐)) |
46 | | eftabs 15965 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ (absโ((๐ดโ๐) / (!โ๐))) = (((absโ๐ด)โ๐) / (!โ๐))) |
47 | 1, 46 | sylan 581 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
(absโ((๐ดโ๐) / (!โ๐))) = (((absโ๐ด)โ๐) / (!โ๐))) |
48 | 26 | fveq2d 6851 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
(absโ(๐นโ๐)) = (absโ((๐ดโ๐) / (!โ๐)))) |
49 | 47, 48, 36 | 3eqtr4rd 2788 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ (๐บโ๐) = (absโ(๐นโ๐))) |
50 | 24, 49 | syldan 592 |
. . 3
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐บโ๐) = (absโ(๐นโ๐))) |
51 | 20, 33, 45, 21, 30, 50 | iserabs 15707 |
. 2
โข (๐ โ (absโฮฃ๐ โ
(โคโฅโ๐)(๐นโ๐)) โค ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐)) |
52 | | nn0uz 12812 |
. . . 4
โข
โ0 = (โคโฅโ0) |
53 | | 0zd 12518 |
. . . 4
โข (๐ โ 0 โ
โค) |
54 | 2 | nncnd 12176 |
. . . . 5
โข (๐ โ ๐ โ โ) |
55 | | nn0cn 12430 |
. . . . 5
โข (๐ โ โ0
โ ๐ โ
โ) |
56 | | nn0ex 12426 |
. . . . . . . 8
โข
โ0 โ V |
57 | 56 | mptex 7178 |
. . . . . . 7
โข (๐ โ โ0
โฆ (((absโ๐ด)โ๐) / (!โ๐))) โ V |
58 | 9, 57 | eqeltri 2834 |
. . . . . 6
โข ๐บ โ V |
59 | 58 | shftval4 14969 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ) โ ((๐บ shift -๐)โ๐) = (๐บโ(๐ + ๐))) |
60 | 54, 55, 59 | syl2an 597 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ ((๐บ shift -๐)โ๐) = (๐บโ(๐ + ๐))) |
61 | | nn0addcl 12455 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + ๐) โ
โ0) |
62 | 3, 61 | sylan 581 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ (๐ + ๐) โ
โ0) |
63 | 9 | eftval 15966 |
. . . . . 6
โข ((๐ + ๐) โ โ0 โ (๐บโ(๐ + ๐)) = (((absโ๐ด)โ(๐ + ๐)) / (!โ(๐ + ๐)))) |
64 | 62, 63 | syl 17 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ (๐บโ(๐ + ๐)) = (((absโ๐ด)โ(๐ + ๐)) / (!โ(๐ + ๐)))) |
65 | 8 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
(absโ๐ด) โ
โ) |
66 | | reeftcl 15964 |
. . . . . 6
โข
(((absโ๐ด)
โ โ โง (๐ +
๐) โ
โ0) โ (((absโ๐ด)โ(๐ + ๐)) / (!โ(๐ + ๐))) โ โ) |
67 | 65, 62, 66 | syl2anc 585 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
(((absโ๐ด)โ(๐ + ๐)) / (!โ(๐ + ๐))) โ โ) |
68 | 64, 67 | eqeltrd 2838 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ (๐บโ(๐ + ๐)) โ โ) |
69 | | oveq2 7370 |
. . . . . . 7
โข (๐ = ๐ โ ((1 / (๐ + 1))โ๐) = ((1 / (๐ + 1))โ๐)) |
70 | 69 | oveq2d 7378 |
. . . . . 6
โข (๐ = ๐ โ ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐)) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐))) |
71 | | eftl.3 |
. . . . . 6
โข ๐ป = (๐ โ โ0 โฆ
((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐))) |
72 | | ovex 7395 |
. . . . . 6
โข
((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐)) โ V |
73 | 70, 71, 72 | fvmpt 6953 |
. . . . 5
โข (๐ โ โ0
โ (๐ปโ๐) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐))) |
74 | 73 | adantl 483 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ (๐ปโ๐) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐))) |
75 | 12, 16 | nndivred 12214 |
. . . . . 6
โข (๐ โ (((absโ๐ด)โ๐) / (!โ๐)) โ โ) |
76 | 75 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
(((absโ๐ด)โ๐) / (!โ๐)) โ โ) |
77 | 2 | peano2nnd 12177 |
. . . . . . 7
โข (๐ โ (๐ + 1) โ โ) |
78 | 77 | nnrecred 12211 |
. . . . . 6
โข (๐ โ (1 / (๐ + 1)) โ โ) |
79 | | reexpcl 13991 |
. . . . . 6
โข (((1 /
(๐ + 1)) โ โ
โง ๐ โ
โ0) โ ((1 / (๐ + 1))โ๐) โ โ) |
80 | 78, 79 | sylan 581 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ((1 /
(๐ + 1))โ๐) โ
โ) |
81 | 76, 80 | remulcld 11192 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ
((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐)) โ โ) |
82 | 65, 62 | reexpcld 14075 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
((absโ๐ด)โ(๐ + ๐)) โ โ) |
83 | 12 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
((absโ๐ด)โ๐) โ
โ) |
84 | 62 | faccld 14191 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ
(!โ(๐ + ๐)) โ
โ) |
85 | 84 | nnred 12175 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
(!โ(๐ + ๐)) โ
โ) |
86 | 85, 81 | remulcld 11192 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
((!โ(๐ + ๐)) ยท ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐))) โ โ) |
87 | 3 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ0) |
88 | | uzid 12785 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
(โคโฅโ๐)) |
89 | 21, 88 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐ โ (โคโฅโ๐)) |
90 | | uzaddcl 12836 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ๐) โง ๐ โ โ0) โ (๐ + ๐) โ (โคโฅโ๐)) |
91 | 89, 90 | sylan 581 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ (๐ + ๐) โ (โคโฅโ๐)) |
92 | 1 | absge0d 15336 |
. . . . . . . . 9
โข (๐ โ 0 โค (absโ๐ด)) |
93 | 92 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ 0 โค
(absโ๐ด)) |
94 | | eftl.6 |
. . . . . . . . 9
โข (๐ โ (absโ๐ด) โค 1) |
95 | 94 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
(absโ๐ด) โค
1) |
96 | 65, 87, 91, 93, 95 | leexp2rd 14165 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
((absโ๐ด)โ(๐ + ๐)) โค ((absโ๐ด)โ๐)) |
97 | 16 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ0) โ
(!โ๐) โ
โ) |
98 | | nnexpcl 13987 |
. . . . . . . . . . . . 13
โข (((๐ + 1) โ โ โง ๐ โ โ0)
โ ((๐ + 1)โ๐) โ
โ) |
99 | 77, 98 | sylan 581 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ0) โ ((๐ + 1)โ๐) โ โ) |
100 | 97, 99 | nnmulcld 12213 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ0) โ
((!โ๐) ยท
((๐ + 1)โ๐)) โ
โ) |
101 | 100 | nnred 12175 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ
((!โ๐) ยท
((๐ + 1)โ๐)) โ
โ) |
102 | 8, 3, 92 | expge0d 14076 |
. . . . . . . . . . . 12
โข (๐ โ 0 โค ((absโ๐ด)โ๐)) |
103 | 12, 102 | jca 513 |
. . . . . . . . . . 11
โข (๐ โ (((absโ๐ด)โ๐) โ โ โง 0 โค
((absโ๐ด)โ๐))) |
104 | 103 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ
(((absโ๐ด)โ๐) โ โ โง 0 โค
((absโ๐ด)โ๐))) |
105 | | faclbnd6 14206 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐))) |
106 | 3, 105 | sylan 581 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ
((!โ๐) ยท
((๐ + 1)โ๐)) โค (!โ(๐ + ๐))) |
107 | | lemul1a 12016 |
. . . . . . . . . 10
โข
(((((!โ๐)
ยท ((๐ +
1)โ๐)) โ โ
โง (!โ(๐ + ๐)) โ โ โง
(((absโ๐ด)โ๐) โ โ โง 0 โค
((absโ๐ด)โ๐))) โง ((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐))) โ (((!โ๐) ยท ((๐ + 1)โ๐)) ยท ((absโ๐ด)โ๐)) โค ((!โ(๐ + ๐)) ยท ((absโ๐ด)โ๐))) |
108 | 101, 85, 104, 106, 107 | syl31anc 1374 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ
(((!โ๐) ยท
((๐ + 1)โ๐)) ยท ((absโ๐ด)โ๐)) โค ((!โ(๐ + ๐)) ยท ((absโ๐ด)โ๐))) |
109 | 85, 83 | remulcld 11192 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ
((!โ(๐ + ๐)) ยท ((absโ๐ด)โ๐)) โ โ) |
110 | 100 | nnrpd 12962 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ
((!โ๐) ยท
((๐ + 1)โ๐)) โ
โ+) |
111 | 83, 109, 110 | lemuldiv2d 13014 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ
((((!โ๐) ยท
((๐ + 1)โ๐)) ยท ((absโ๐ด)โ๐)) โค ((!โ(๐ + ๐)) ยท ((absโ๐ด)โ๐)) โ ((absโ๐ด)โ๐) โค (((!โ(๐ + ๐)) ยท ((absโ๐ด)โ๐)) / ((!โ๐) ยท ((๐ + 1)โ๐))))) |
112 | 108, 111 | mpbid 231 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
((absโ๐ด)โ๐) โค (((!โ(๐ + ๐)) ยท ((absโ๐ด)โ๐)) / ((!โ๐) ยท ((๐ + 1)โ๐)))) |
113 | 84 | nncnd 12176 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ
(!โ(๐ + ๐)) โ
โ) |
114 | 12 | recnd 11190 |
. . . . . . . . . . 11
โข (๐ โ ((absโ๐ด)โ๐) โ โ) |
115 | 114 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ
((absโ๐ด)โ๐) โ
โ) |
116 | 100 | nncnd 12176 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ
((!โ๐) ยท
((๐ + 1)โ๐)) โ
โ) |
117 | 100 | nnne0d 12210 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ
((!โ๐) ยท
((๐ + 1)โ๐)) โ 0) |
118 | 113, 115,
116, 117 | divassd 11973 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ
(((!โ(๐ + ๐)) ยท ((absโ๐ด)โ๐)) / ((!โ๐) ยท ((๐ + 1)โ๐))) = ((!โ(๐ + ๐)) ยท (((absโ๐ด)โ๐) / ((!โ๐) ยท ((๐ + 1)โ๐))))) |
119 | 77 | nncnd 12176 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ + 1) โ โ) |
120 | 119 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ โ0) โ (๐ + 1) โ
โ) |
121 | 77 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ โ0) โ (๐ + 1) โ
โ) |
122 | 121 | nnne0d 12210 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ โ0) โ (๐ + 1) โ 0) |
123 | | nn0z 12531 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ ๐ โ
โค) |
124 | 123 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โค) |
125 | 120, 122,
124 | exprecd 14066 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ0) โ ((1 /
(๐ + 1))โ๐) = (1 / ((๐ + 1)โ๐))) |
126 | 125 | oveq2d 7378 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ0) โ
((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐)) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท (1 / ((๐ + 1)โ๐)))) |
127 | 75 | recnd 11190 |
. . . . . . . . . . . . 13
โข (๐ โ (((absโ๐ด)โ๐) / (!โ๐)) โ โ) |
128 | 127 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ0) โ
(((absโ๐ด)โ๐) / (!โ๐)) โ โ) |
129 | 99 | nncnd 12176 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ0) โ ((๐ + 1)โ๐) โ โ) |
130 | 99 | nnne0d 12210 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ0) โ ((๐ + 1)โ๐) โ 0) |
131 | 128, 129,
130 | divrecd 11941 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ0) โ
((((absโ๐ด)โ๐) / (!โ๐)) / ((๐ + 1)โ๐)) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท (1 / ((๐ + 1)โ๐)))) |
132 | 16 | nncnd 12176 |
. . . . . . . . . . . . 13
โข (๐ โ (!โ๐) โ โ) |
133 | 132 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ0) โ
(!โ๐) โ
โ) |
134 | | facne0 14193 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (!โ๐) โ
0) |
135 | 3, 134 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (!โ๐) โ 0) |
136 | 135 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ0) โ
(!โ๐) โ
0) |
137 | 115, 133,
129, 136, 130 | divdiv1d 11969 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ0) โ
((((absโ๐ด)โ๐) / (!โ๐)) / ((๐ + 1)โ๐)) = (((absโ๐ด)โ๐) / ((!โ๐) ยท ((๐ + 1)โ๐)))) |
138 | 126, 131,
137 | 3eqtr2rd 2784 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ0) โ
(((absโ๐ด)โ๐) / ((!โ๐) ยท ((๐ + 1)โ๐))) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐))) |
139 | 138 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ
((!โ(๐ + ๐)) ยท (((absโ๐ด)โ๐) / ((!โ๐) ยท ((๐ + 1)โ๐)))) = ((!โ(๐ + ๐)) ยท ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐)))) |
140 | 118, 139 | eqtrd 2777 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
(((!โ(๐ + ๐)) ยท ((absโ๐ด)โ๐)) / ((!โ๐) ยท ((๐ + 1)โ๐))) = ((!โ(๐ + ๐)) ยท ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐)))) |
141 | 112, 140 | breqtrd 5136 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
((absโ๐ด)โ๐) โค ((!โ(๐ + ๐)) ยท ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐)))) |
142 | 82, 83, 86, 96, 141 | letrd 11319 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
((absโ๐ด)โ(๐ + ๐)) โค ((!โ(๐ + ๐)) ยท ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐)))) |
143 | 84 | nngt0d 12209 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ 0 <
(!โ(๐ + ๐))) |
144 | | ledivmul 12038 |
. . . . . . 7
โข
((((absโ๐ด)โ(๐ + ๐)) โ โ โง ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐)) โ โ โง ((!โ(๐ + ๐)) โ โ โง 0 <
(!โ(๐ + ๐)))) โ ((((absโ๐ด)โ(๐ + ๐)) / (!โ(๐ + ๐))) โค ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐)) โ ((absโ๐ด)โ(๐ + ๐)) โค ((!โ(๐ + ๐)) ยท ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐))))) |
145 | 82, 81, 85, 143, 144 | syl112anc 1375 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
((((absโ๐ด)โ(๐ + ๐)) / (!โ(๐ + ๐))) โค ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐)) โ ((absโ๐ด)โ(๐ + ๐)) โค ((!โ(๐ + ๐)) ยท ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐))))) |
146 | 142, 145 | mpbird 257 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
(((absโ๐ด)โ(๐ + ๐)) / (!โ(๐ + ๐))) โค ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐))) |
147 | 64, 146 | eqbrtrd 5132 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ (๐บโ(๐ + ๐)) โค ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐))) |
148 | | 0z 12517 |
. . . . . 6
โข 0 โ
โค |
149 | 21 | znegcld 12616 |
. . . . . 6
โข (๐ โ -๐ โ โค) |
150 | 58 | seqshft 14977 |
. . . . . 6
โข ((0
โ โค โง -๐
โ โค) โ seq0( + , (๐บ shift -๐)) = (seq(0 โ -๐)( + , ๐บ) shift -๐)) |
151 | 148, 149,
150 | sylancr 588 |
. . . . 5
โข (๐ โ seq0( + , (๐บ shift -๐)) = (seq(0 โ -๐)( + , ๐บ) shift -๐)) |
152 | | 0cn 11154 |
. . . . . . . . . . . 12
โข 0 โ
โ |
153 | | subneg 11457 |
. . . . . . . . . . . 12
โข ((0
โ โ โง ๐
โ โ) โ (0 โ -๐) = (0 + ๐)) |
154 | 152, 153 | mpan 689 |
. . . . . . . . . . 11
โข (๐ โ โ โ (0
โ -๐) = (0 + ๐)) |
155 | | addid2 11345 |
. . . . . . . . . . 11
โข (๐ โ โ โ (0 +
๐) = ๐) |
156 | 154, 155 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ โ โ (0
โ -๐) = ๐) |
157 | 54, 156 | syl 17 |
. . . . . . . . 9
โข (๐ โ (0 โ -๐) = ๐) |
158 | 157 | seqeq1d 13919 |
. . . . . . . 8
โข (๐ โ seq(0 โ -๐)( + , ๐บ) = seq๐( + , ๐บ)) |
159 | 158, 45 | eqbrtrd 5132 |
. . . . . . 7
โข (๐ โ seq(0 โ -๐)( + , ๐บ) โ ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐)) |
160 | | seqex 13915 |
. . . . . . . 8
โข seq(0
โ -๐)( + , ๐บ) โ V |
161 | | climshft 15465 |
. . . . . . . 8
โข ((-๐ โ โค โง seq(0
โ -๐)( + , ๐บ) โ V) โ ((seq(0
โ -๐)( + , ๐บ) shift -๐) โ ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐) โ seq(0 โ -๐)( + , ๐บ) โ ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐))) |
162 | 149, 160,
161 | sylancl 587 |
. . . . . . 7
โข (๐ โ ((seq(0 โ -๐)( + , ๐บ) shift -๐) โ ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐) โ seq(0 โ -๐)( + , ๐บ) โ ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐))) |
163 | 159, 162 | mpbird 257 |
. . . . . 6
โข (๐ โ (seq(0 โ -๐)( + , ๐บ) shift -๐) โ ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐)) |
164 | | ovex 7395 |
. . . . . . 7
โข (seq(0
โ -๐)( + , ๐บ) shift -๐) โ V |
165 | | sumex 15579 |
. . . . . . 7
โข
ฮฃ๐ โ
(โคโฅโ๐)(๐บโ๐) โ V |
166 | 164, 165 | breldm 5869 |
. . . . . 6
โข ((seq(0
โ -๐)( + , ๐บ) shift -๐) โ ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐) โ (seq(0 โ -๐)( + , ๐บ) shift -๐) โ dom โ ) |
167 | 163, 166 | syl 17 |
. . . . 5
โข (๐ โ (seq(0 โ -๐)( + , ๐บ) shift -๐) โ dom โ ) |
168 | 151, 167 | eqeltrd 2838 |
. . . 4
โข (๐ โ seq0( + , (๐บ shift -๐)) โ dom โ ) |
169 | 2 | nnge1d 12208 |
. . . . . . . . . 10
โข (๐ โ 1 โค ๐) |
170 | | 1nn 12171 |
. . . . . . . . . . 11
โข 1 โ
โ |
171 | | nnleltp1 12565 |
. . . . . . . . . . 11
โข ((1
โ โ โง ๐
โ โ) โ (1 โค ๐ โ 1 < (๐ + 1))) |
172 | 170, 2, 171 | sylancr 588 |
. . . . . . . . . 10
โข (๐ โ (1 โค ๐ โ 1 < (๐ + 1))) |
173 | 169, 172 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ 1 < (๐ + 1)) |
174 | 14 | nn0ge0d 12483 |
. . . . . . . . . 10
โข (๐ โ 0 โค (๐ + 1)) |
175 | 15, 174 | absidd 15314 |
. . . . . . . . 9
โข (๐ โ (absโ(๐ + 1)) = (๐ + 1)) |
176 | 173, 175 | breqtrrd 5138 |
. . . . . . . 8
โข (๐ โ 1 < (absโ(๐ + 1))) |
177 | | eqid 2737 |
. . . . . . . . . 10
โข (๐ โ โ0
โฆ ((1 / (๐ +
1))โ๐)) = (๐ โ โ0
โฆ ((1 / (๐ +
1))โ๐)) |
178 | | ovex 7395 |
. . . . . . . . . 10
โข ((1 /
(๐ + 1))โ๐) โ V |
179 | 69, 177, 178 | fvmpt 6953 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ ((1 / (๐ + 1))โ๐))โ๐) = ((1 / (๐ + 1))โ๐)) |
180 | 179 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ ((1 / (๐ +
1))โ๐))โ๐) = ((1 / (๐ + 1))โ๐)) |
181 | 119, 176,
180 | georeclim 15764 |
. . . . . . 7
โข (๐ โ seq0( + , (๐ โ โ0
โฆ ((1 / (๐ +
1))โ๐))) โ
((๐ + 1) / ((๐ + 1) โ
1))) |
182 | 80 | recnd 11190 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ ((1 /
(๐ + 1))โ๐) โ
โ) |
183 | 180, 182 | eqeltrd 2838 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ ((1 / (๐ +
1))โ๐))โ๐) โ
โ) |
184 | 180 | oveq2d 7378 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
((((absโ๐ด)โ๐) / (!โ๐)) ยท ((๐ โ โ0 โฆ ((1 /
(๐ + 1))โ๐))โ๐)) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐))) |
185 | 74, 184 | eqtr4d 2780 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ (๐ปโ๐) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((๐ โ โ0 โฆ ((1 /
(๐ + 1))โ๐))โ๐))) |
186 | 52, 53, 127, 181, 183, 185 | isermulc2 15549 |
. . . . . 6
โข (๐ โ seq0( + , ๐ป) โ ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((๐ + 1) / ((๐ + 1) โ 1)))) |
187 | | ax-1cn 11116 |
. . . . . . . . . . 11
โข 1 โ
โ |
188 | | pncan 11414 |
. . . . . . . . . . 11
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ + 1)
โ 1) = ๐) |
189 | 54, 187, 188 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ ((๐ + 1) โ 1) = ๐) |
190 | 189 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1) / ((๐ + 1) โ 1)) = ((๐ + 1) / ๐)) |
191 | 190 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((๐ + 1) / ((๐ + 1) โ 1))) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((๐ + 1) / ๐))) |
192 | 15, 2 | nndivred 12214 |
. . . . . . . . . 10
โข (๐ โ ((๐ + 1) / ๐) โ โ) |
193 | 192 | recnd 11190 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1) / ๐) โ โ) |
194 | 114, 193,
132, 135 | div23d 11975 |
. . . . . . . 8
โข (๐ โ ((((absโ๐ด)โ๐) ยท ((๐ + 1) / ๐)) / (!โ๐)) = ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((๐ + 1) / ๐))) |
195 | 191, 194 | eqtr4d 2780 |
. . . . . . 7
โข (๐ โ ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((๐ + 1) / ((๐ + 1) โ 1))) = ((((absโ๐ด)โ๐) ยท ((๐ + 1) / ๐)) / (!โ๐))) |
196 | 114, 193,
132, 135 | divassd 11973 |
. . . . . . 7
โข (๐ โ ((((absโ๐ด)โ๐) ยท ((๐ + 1) / ๐)) / (!โ๐)) = (((absโ๐ด)โ๐) ยท (((๐ + 1) / ๐) / (!โ๐)))) |
197 | 2 | nnne0d 12210 |
. . . . . . . . . 10
โข (๐ โ ๐ โ 0) |
198 | 119, 54, 132, 197, 135 | divdiv1d 11969 |
. . . . . . . . 9
โข (๐ โ (((๐ + 1) / ๐) / (!โ๐)) = ((๐ + 1) / (๐ ยท (!โ๐)))) |
199 | 54, 132 | mulcomd 11183 |
. . . . . . . . . 10
โข (๐ โ (๐ ยท (!โ๐)) = ((!โ๐) ยท ๐)) |
200 | 199 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ ((๐ + 1) / (๐ ยท (!โ๐))) = ((๐ + 1) / ((!โ๐) ยท ๐))) |
201 | 198, 200 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (((๐ + 1) / ๐) / (!โ๐)) = ((๐ + 1) / ((!โ๐) ยท ๐))) |
202 | 201 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ (((absโ๐ด)โ๐) ยท (((๐ + 1) / ๐) / (!โ๐))) = (((absโ๐ด)โ๐) ยท ((๐ + 1) / ((!โ๐) ยท ๐)))) |
203 | 195, 196,
202 | 3eqtrd 2781 |
. . . . . 6
โข (๐ โ ((((absโ๐ด)โ๐) / (!โ๐)) ยท ((๐ + 1) / ((๐ + 1) โ 1))) = (((absโ๐ด)โ๐) ยท ((๐ + 1) / ((!โ๐) ยท ๐)))) |
204 | 186, 203 | breqtrd 5136 |
. . . . 5
โข (๐ โ seq0( + , ๐ป) โ (((absโ๐ด)โ๐) ยท ((๐ + 1) / ((!โ๐) ยท ๐)))) |
205 | | seqex 13915 |
. . . . . 6
โข seq0( + ,
๐ป) โ
V |
206 | | ovex 7395 |
. . . . . 6
โข
(((absโ๐ด)โ๐) ยท ((๐ + 1) / ((!โ๐) ยท ๐))) โ V |
207 | 205, 206 | breldm 5869 |
. . . . 5
โข (seq0( +
, ๐ป) โ
(((absโ๐ด)โ๐) ยท ((๐ + 1) / ((!โ๐) ยท ๐))) โ seq0( + , ๐ป) โ dom โ ) |
208 | 204, 207 | syl 17 |
. . . 4
โข (๐ โ seq0( + , ๐ป) โ dom โ
) |
209 | 52, 53, 60, 68, 74, 81, 147, 168, 208 | isumle 15736 |
. . 3
โข (๐ โ ฮฃ๐ โ โ0 (๐บโ(๐ + ๐)) โค ฮฃ๐ โ โ0
((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐))) |
210 | | eqid 2737 |
. . . . 5
โข
(โคโฅโ(0 + ๐)) = (โคโฅโ(0 +
๐)) |
211 | | fveq2 6847 |
. . . . 5
โข (๐ = (๐ + ๐) โ (๐บโ๐) = (๐บโ(๐ + ๐))) |
212 | 54 | addid2d 11363 |
. . . . . . . . 9
โข (๐ โ (0 + ๐) = ๐) |
213 | 212 | fveq2d 6851 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ(0 + ๐)) = (โคโฅโ๐)) |
214 | 213 | eleq2d 2824 |
. . . . . . 7
โข (๐ โ (๐ โ (โคโฅโ(0 +
๐)) โ ๐ โ
(โคโฅโ๐))) |
215 | 214 | biimpa 478 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ(0 +
๐))) โ ๐ โ
(โคโฅโ๐)) |
216 | 215, 41 | syldan 592 |
. . . . 5
โข ((๐ โง ๐ โ (โคโฅโ(0 +
๐))) โ (๐บโ๐) โ โ) |
217 | 52, 210, 211, 21, 53, 216 | isumshft 15731 |
. . . 4
โข (๐ โ ฮฃ๐ โ (โคโฅโ(0 +
๐))(๐บโ๐) = ฮฃ๐ โ โ0 (๐บโ(๐ + ๐))) |
218 | 213 | sumeq1d 15593 |
. . . 4
โข (๐ โ ฮฃ๐ โ (โคโฅโ(0 +
๐))(๐บโ๐) = ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐)) |
219 | 217, 218 | eqtr3d 2779 |
. . 3
โข (๐ โ ฮฃ๐ โ โ0 (๐บโ(๐ + ๐)) = ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐)) |
220 | 81 | recnd 11190 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ
((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐)) โ โ) |
221 | 52, 53, 74, 220, 204 | isumclim 15649 |
. . 3
โข (๐ โ ฮฃ๐ โ โ0
((((absโ๐ด)โ๐) / (!โ๐)) ยท ((1 / (๐ + 1))โ๐)) = (((absโ๐ด)โ๐) ยท ((๐ + 1) / ((!โ๐) ยท ๐)))) |
222 | 209, 219,
221 | 3brtr3d 5141 |
. 2
โข (๐ โ ฮฃ๐ โ (โคโฅโ๐)(๐บโ๐) โค (((absโ๐ด)โ๐) ยท ((๐ + 1) / ((!โ๐) ยท ๐)))) |
223 | 7, 11, 19, 51, 222 | letrd 11319 |
1
โข (๐ โ (absโฮฃ๐ โ
(โคโฅโ๐)(๐นโ๐)) โค (((absโ๐ด)โ๐) ยท ((๐ + 1) / ((!โ๐) ยท ๐)))) |