Step | Hyp | Ref
| Expression |
1 | | efadd.4 |
. . . 4
โข (๐ โ ๐ด โ โ) |
2 | | efadd.5 |
. . . 4
โข (๐ โ ๐ต โ โ) |
3 | 1, 2 | addcld 11179 |
. . 3
โข (๐ โ (๐ด + ๐ต) โ โ) |
4 | | efadd.3 |
. . . 4
โข ๐ป = (๐ โ โ0 โฆ (((๐ด + ๐ต)โ๐) / (!โ๐))) |
5 | 4 | efcvg 15972 |
. . 3
โข ((๐ด + ๐ต) โ โ โ seq0( + , ๐ป) โ (expโ(๐ด + ๐ต))) |
6 | 3, 5 | syl 17 |
. 2
โข (๐ โ seq0( + , ๐ป) โ (expโ(๐ด + ๐ต))) |
7 | | efadd.1 |
. . . . . 6
โข ๐น = (๐ โ โ0 โฆ ((๐ดโ๐) / (!โ๐))) |
8 | 7 | eftval 15964 |
. . . . 5
โข (๐ โ โ0
โ (๐นโ๐) = ((๐ดโ๐) / (!โ๐))) |
9 | 8 | adantl 483 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ (๐นโ๐) = ((๐ดโ๐) / (!โ๐))) |
10 | | absexp 15195 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) |
11 | 1, 10 | sylan 581 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
(absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) |
12 | | faccl 14189 |
. . . . . . . 8
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
13 | 12 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
(!โ๐) โ
โ) |
14 | | nnre 12165 |
. . . . . . . 8
โข
((!โ๐) โ
โ โ (!โ๐)
โ โ) |
15 | | nnnn0 12425 |
. . . . . . . . 9
โข
((!โ๐) โ
โ โ (!โ๐)
โ โ0) |
16 | 15 | nn0ge0d 12481 |
. . . . . . . 8
โข
((!โ๐) โ
โ โ 0 โค (!โ๐)) |
17 | 14, 16 | absidd 15313 |
. . . . . . 7
โข
((!โ๐) โ
โ โ (absโ(!โ๐)) = (!โ๐)) |
18 | 13, 17 | syl 17 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
(absโ(!โ๐)) =
(!โ๐)) |
19 | 11, 18 | oveq12d 7376 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
((absโ(๐ดโ๐)) / (absโ(!โ๐))) = (((absโ๐ด)โ๐) / (!โ๐))) |
20 | | expcl 13991 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
21 | 1, 20 | sylan 581 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ (๐ดโ๐) โ โ) |
22 | 13 | nncnd 12174 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
(!โ๐) โ
โ) |
23 | 13 | nnne0d 12208 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
(!โ๐) โ
0) |
24 | 21, 22, 23 | absdivd 15346 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
(absโ((๐ดโ๐) / (!โ๐))) = ((absโ(๐ดโ๐)) / (absโ(!โ๐)))) |
25 | | eqid 2733 |
. . . . . . 7
โข (๐ โ โ0
โฆ (((absโ๐ด)โ๐) / (!โ๐))) = (๐ โ โ0 โฆ
(((absโ๐ด)โ๐) / (!โ๐))) |
26 | 25 | eftval 15964 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ (((absโ๐ด)โ๐) / (!โ๐)))โ๐) = (((absโ๐ด)โ๐) / (!โ๐))) |
27 | 26 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ (((absโ๐ด)โ๐) / (!โ๐)))โ๐) = (((absโ๐ด)โ๐) / (!โ๐))) |
28 | 19, 24, 27 | 3eqtr4rd 2784 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ ((๐ โ โ0
โฆ (((absโ๐ด)โ๐) / (!โ๐)))โ๐) = (absโ((๐ดโ๐) / (!โ๐)))) |
29 | | eftcl 15961 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐ดโ๐) / (!โ๐)) โ โ) |
30 | 1, 29 | sylan 581 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ ((๐ดโ๐) / (!โ๐)) โ โ) |
31 | | efadd.2 |
. . . . . 6
โข ๐บ = (๐ โ โ0 โฆ ((๐ตโ๐) / (!โ๐))) |
32 | 31 | eftval 15964 |
. . . . 5
โข (๐ โ โ0
โ (๐บโ๐) = ((๐ตโ๐) / (!โ๐))) |
33 | 32 | adantl 483 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ (๐บโ๐) = ((๐ตโ๐) / (!โ๐))) |
34 | | eftcl 15961 |
. . . . 5
โข ((๐ต โ โ โง ๐ โ โ0)
โ ((๐ตโ๐) / (!โ๐)) โ โ) |
35 | 2, 34 | sylan 581 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ ((๐ตโ๐) / (!โ๐)) โ โ) |
36 | 4 | eftval 15964 |
. . . . . 6
โข (๐ โ โ0
โ (๐ปโ๐) = (((๐ด + ๐ต)โ๐) / (!โ๐))) |
37 | 36 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ (๐ปโ๐) = (((๐ด + ๐ต)โ๐) / (!โ๐))) |
38 | 1 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ ๐ด โ
โ) |
39 | 2 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ ๐ต โ
โ) |
40 | | simpr 486 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ0) |
41 | | binom 15720 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ โ โ0)
โ ((๐ด + ๐ต)โ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐)))) |
42 | 38, 39, 40, 41 | syl3anc 1372 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ ((๐ด + ๐ต)โ๐) = ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐)))) |
43 | 42 | oveq1d 7373 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ (((๐ด + ๐ต)โ๐) / (!โ๐)) = (ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐))) / (!โ๐))) |
44 | | fzfid 13884 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
(0...๐) โ
Fin) |
45 | | faccl 14189 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
46 | 45 | adantl 483 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ
(!โ๐) โ
โ) |
47 | 46 | nncnd 12174 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
(!โ๐) โ
โ) |
48 | | bccl2 14229 |
. . . . . . . . . . 11
โข (๐ โ (0...๐) โ (๐C๐) โ โ) |
49 | 48 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐C๐) โ โ) |
50 | 49 | nncnd 12174 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐C๐) โ โ) |
51 | 1 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ๐ด โ โ) |
52 | | fznn0sub 13479 |
. . . . . . . . . . . 12
โข (๐ โ (0...๐) โ (๐ โ ๐) โ
โ0) |
53 | 52 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ โ ๐) โ
โ0) |
54 | 51, 53 | expcld 14057 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ดโ(๐ โ ๐)) โ โ) |
55 | 2 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ๐ต โ โ) |
56 | | elfznn0 13540 |
. . . . . . . . . . . 12
โข (๐ โ (0...๐) โ ๐ โ โ0) |
57 | 56 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ๐ โ โ0) |
58 | 55, 57 | expcld 14057 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ตโ๐) โ โ) |
59 | 54, 58 | mulcld 11180 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐)) โ โ) |
60 | 50, 59 | mulcld 11180 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((๐C๐) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐))) โ โ) |
61 | 46 | nnne0d 12208 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
(!โ๐) โ
0) |
62 | 44, 47, 60, 61 | fsumdivc 15676 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
(ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐))) / (!โ๐)) = ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐))) / (!โ๐))) |
63 | 51, 57 | expcld 14057 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ดโ๐) โ โ) |
64 | 57, 12 | syl 17 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (!โ๐) โ โ) |
65 | 64 | nncnd 12174 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (!โ๐) โ โ) |
66 | 64 | nnne0d 12208 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (!โ๐) โ 0) |
67 | 63, 65, 66 | divcld 11936 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((๐ดโ๐) / (!โ๐)) โ โ) |
68 | 31 | eftval 15964 |
. . . . . . . . . . . 12
โข ((๐ โ ๐) โ โ0 โ (๐บโ(๐ โ ๐)) = ((๐ตโ(๐ โ ๐)) / (!โ(๐ โ ๐)))) |
69 | 53, 68 | syl 17 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐บโ(๐ โ ๐)) = ((๐ตโ(๐ โ ๐)) / (!โ(๐ โ ๐)))) |
70 | 55, 53 | expcld 14057 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ตโ(๐ โ ๐)) โ โ) |
71 | | faccl 14189 |
. . . . . . . . . . . . . 14
โข ((๐ โ ๐) โ โ0 โ
(!โ(๐ โ ๐)) โ
โ) |
72 | 53, 71 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (!โ(๐ โ ๐)) โ โ) |
73 | 72 | nncnd 12174 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (!โ(๐ โ ๐)) โ โ) |
74 | 72 | nnne0d 12208 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (!โ(๐ โ ๐)) โ 0) |
75 | 70, 73, 74 | divcld 11936 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((๐ตโ(๐ โ ๐)) / (!โ(๐ โ ๐))) โ โ) |
76 | 69, 75 | eqeltrd 2834 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐บโ(๐ โ ๐)) โ โ) |
77 | 67, 76 | mulcld 11180 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (((๐ดโ๐) / (!โ๐)) ยท (๐บโ(๐ โ ๐))) โ โ) |
78 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = ((0 + ๐) โ ๐) โ (๐ดโ๐) = (๐ดโ((0 + ๐) โ ๐))) |
79 | | fveq2 6843 |
. . . . . . . . . . 11
โข (๐ = ((0 + ๐) โ ๐) โ (!โ๐) = (!โ((0 + ๐) โ ๐))) |
80 | 78, 79 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = ((0 + ๐) โ ๐) โ ((๐ดโ๐) / (!โ๐)) = ((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐)))) |
81 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = ((0 + ๐) โ ๐) โ (๐ โ ๐) = (๐ โ ((0 + ๐) โ ๐))) |
82 | 81 | fveq2d 6847 |
. . . . . . . . . 10
โข (๐ = ((0 + ๐) โ ๐) โ (๐บโ(๐ โ ๐)) = (๐บโ(๐ โ ((0 + ๐) โ ๐)))) |
83 | 80, 82 | oveq12d 7376 |
. . . . . . . . 9
โข (๐ = ((0 + ๐) โ ๐) โ (((๐ดโ๐) / (!โ๐)) ยท (๐บโ(๐ โ ๐))) = (((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐))) ยท (๐บโ(๐ โ ((0 + ๐) โ ๐))))) |
84 | 77, 83 | fsumrev2 15672 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
ฮฃ๐ โ (0...๐)(((๐ดโ๐) / (!โ๐)) ยท (๐บโ(๐ โ ๐))) = ฮฃ๐ โ (0...๐)(((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐))) ยท (๐บโ(๐ โ ((0 + ๐) โ ๐))))) |
85 | 31 | eftval 15964 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (๐บโ๐) = ((๐ตโ๐) / (!โ๐))) |
86 | 57, 85 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐บโ๐) = ((๐ตโ๐) / (!โ๐))) |
87 | 86 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (((๐ดโ(๐ โ ๐)) / (!โ(๐ โ ๐))) ยท (๐บโ๐)) = (((๐ดโ(๐ โ ๐)) / (!โ(๐ โ ๐))) ยท ((๐ตโ๐) / (!โ๐)))) |
88 | 72, 64 | nnmulcld 12211 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((!โ(๐ โ ๐)) ยท (!โ๐)) โ โ) |
89 | 88 | nncnd 12174 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((!โ(๐ โ ๐)) ยท (!โ๐)) โ โ) |
90 | 88 | nnne0d 12208 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((!โ(๐ โ ๐)) ยท (!โ๐)) โ 0) |
91 | 59, 89, 90 | divrec2d 11940 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐)) / ((!โ(๐ โ ๐)) ยท (!โ๐))) = ((1 / ((!โ(๐ โ ๐)) ยท (!โ๐))) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐)))) |
92 | 54, 73, 58, 65, 74, 66 | divmuldivd 11977 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (((๐ดโ(๐ โ ๐)) / (!โ(๐ โ ๐))) ยท ((๐ตโ๐) / (!โ๐))) = (((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐)) / ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
93 | | bcval2 14211 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (0...๐) โ (๐C๐) = ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
94 | 93 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐C๐) = ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
95 | 94 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((๐C๐) / (!โ๐)) = (((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))) / (!โ๐))) |
96 | 47 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (!โ๐) โ โ) |
97 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (!โ๐) โ 0) |
98 | 96, 89, 96, 90, 97 | divdiv32d 11961 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))) / (!โ๐)) = (((!โ๐) / (!โ๐)) / ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
99 | 96, 97 | dividd 11934 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((!โ๐) / (!โ๐)) = 1) |
100 | 99 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (((!โ๐) / (!โ๐)) / ((!โ(๐ โ ๐)) ยท (!โ๐))) = (1 / ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
101 | 98, 100 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))) / (!โ๐)) = (1 / ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
102 | 95, 101 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((๐C๐) / (!โ๐)) = (1 / ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
103 | 102 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (((๐C๐) / (!โ๐)) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐))) = ((1 / ((!โ(๐ โ ๐)) ยท (!โ๐))) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐)))) |
104 | 91, 92, 103 | 3eqtr4rd 2784 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (((๐C๐) / (!โ๐)) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐))) = (((๐ดโ(๐ โ ๐)) / (!โ(๐ โ ๐))) ยท ((๐ตโ๐) / (!โ๐)))) |
105 | 87, 104 | eqtr4d 2776 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (((๐ดโ(๐ โ ๐)) / (!โ(๐ โ ๐))) ยท (๐บโ๐)) = (((๐C๐) / (!โ๐)) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐)))) |
106 | | nn0cn 12428 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ0
โ ๐ โ
โ) |
107 | 106 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ๐ โ โ) |
108 | 107 | addid2d 11361 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (0 + ๐) = ๐) |
109 | 108 | oveq1d 7373 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((0 + ๐) โ ๐) = (๐ โ ๐)) |
110 | 109 | oveq2d 7374 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ดโ((0 + ๐) โ ๐)) = (๐ดโ(๐ โ ๐))) |
111 | 109 | fveq2d 6847 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (!โ((0 + ๐) โ ๐)) = (!โ(๐ โ ๐))) |
112 | 110, 111 | oveq12d 7376 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐))) = ((๐ดโ(๐ โ ๐)) / (!โ(๐ โ ๐)))) |
113 | 109 | oveq2d 7374 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ โ ((0 + ๐) โ ๐)) = (๐ โ (๐ โ ๐))) |
114 | | nn0cn 12428 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ0
โ ๐ โ
โ) |
115 | 57, 114 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ ๐ โ โ) |
116 | 107, 115 | nncand 11522 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ โ (๐ โ ๐)) = ๐) |
117 | 113, 116 | eqtrd 2773 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐ โ ((0 + ๐) โ ๐)) = ๐) |
118 | 117 | fveq2d 6847 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (๐บโ(๐ โ ((0 + ๐) โ ๐))) = (๐บโ๐)) |
119 | 112, 118 | oveq12d 7376 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐))) ยท (๐บโ(๐ โ ((0 + ๐) โ ๐)))) = (((๐ดโ(๐ โ ๐)) / (!โ(๐ โ ๐))) ยท (๐บโ๐))) |
120 | 50, 59, 96, 97 | div23d 11973 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (((๐C๐) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐))) / (!โ๐)) = (((๐C๐) / (!โ๐)) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐)))) |
121 | 105, 119,
120 | 3eqtr4rd 2784 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โ0) โง ๐ โ (0...๐)) โ (((๐C๐) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐))) / (!โ๐)) = (((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐))) ยท (๐บโ(๐ โ ((0 + ๐) โ ๐))))) |
122 | 121 | sumeq2dv 15593 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ0) โ
ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐))) / (!โ๐)) = ฮฃ๐ โ (0...๐)(((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐))) ยท (๐บโ(๐ โ ((0 + ๐) โ ๐))))) |
123 | | oveq2 7366 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ ((0 + ๐) โ ๐) = ((0 + ๐) โ ๐)) |
124 | 123 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ดโ((0 + ๐) โ ๐)) = (๐ดโ((0 + ๐) โ ๐))) |
125 | 123 | fveq2d 6847 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (!โ((0 + ๐) โ ๐)) = (!โ((0 + ๐) โ ๐))) |
126 | 124, 125 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐))) = ((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐)))) |
127 | 123 | oveq2d 7374 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ โ ((0 + ๐) โ ๐)) = (๐ โ ((0 + ๐) โ ๐))) |
128 | 127 | fveq2d 6847 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (๐บโ(๐ โ ((0 + ๐) โ ๐))) = (๐บโ(๐ โ ((0 + ๐) โ ๐)))) |
129 | 126, 128 | oveq12d 7376 |
. . . . . . . . . 10
โข (๐ = ๐ โ (((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐))) ยท (๐บโ(๐ โ ((0 + ๐) โ ๐)))) = (((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐))) ยท (๐บโ(๐ โ ((0 + ๐) โ ๐))))) |
130 | 129 | cbvsumv 15586 |
. . . . . . . . 9
โข
ฮฃ๐ โ
(0...๐)(((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐))) ยท (๐บโ(๐ โ ((0 + ๐) โ ๐)))) = ฮฃ๐ โ (0...๐)(((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐))) ยท (๐บโ(๐ โ ((0 + ๐) โ ๐)))) |
131 | 122, 130 | eqtrdi 2789 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ0) โ
ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐))) / (!โ๐)) = ฮฃ๐ โ (0...๐)(((๐ดโ((0 + ๐) โ ๐)) / (!โ((0 + ๐) โ ๐))) ยท (๐บโ(๐ โ ((0 + ๐) โ ๐))))) |
132 | 84, 131 | eqtr4d 2776 |
. . . . . . 7
โข ((๐ โง ๐ โ โ0) โ
ฮฃ๐ โ (0...๐)(((๐ดโ๐) / (!โ๐)) ยท (๐บโ(๐ โ ๐))) = ฮฃ๐ โ (0...๐)(((๐C๐) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐))) / (!โ๐))) |
133 | 62, 132 | eqtr4d 2776 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
(ฮฃ๐ โ (0...๐)((๐C๐) ยท ((๐ดโ(๐ โ ๐)) ยท (๐ตโ๐))) / (!โ๐)) = ฮฃ๐ โ (0...๐)(((๐ดโ๐) / (!โ๐)) ยท (๐บโ(๐ โ ๐)))) |
134 | 43, 133 | eqtrd 2773 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ (((๐ด + ๐ต)โ๐) / (!โ๐)) = ฮฃ๐ โ (0...๐)(((๐ดโ๐) / (!โ๐)) ยท (๐บโ(๐ โ ๐)))) |
135 | 37, 134 | eqtrd 2773 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ (๐ปโ๐) = ฮฃ๐ โ (0...๐)(((๐ดโ๐) / (!โ๐)) ยท (๐บโ(๐ โ ๐)))) |
136 | 1 | abscld 15327 |
. . . . . 6
โข (๐ โ (absโ๐ด) โ
โ) |
137 | 136 | recnd 11188 |
. . . . 5
โข (๐ โ (absโ๐ด) โ
โ) |
138 | 25 | efcllem 15965 |
. . . . 5
โข
((absโ๐ด)
โ โ โ seq0( + , (๐ โ โ0 โฆ
(((absโ๐ด)โ๐) / (!โ๐)))) โ dom โ ) |
139 | 137, 138 | syl 17 |
. . . 4
โข (๐ โ seq0( + , (๐ โ โ0
โฆ (((absโ๐ด)โ๐) / (!โ๐)))) โ dom โ ) |
140 | 31 | efcllem 15965 |
. . . . 5
โข (๐ต โ โ โ seq0( + ,
๐บ) โ dom โ
) |
141 | 2, 140 | syl 17 |
. . . 4
โข (๐ โ seq0( + , ๐บ) โ dom โ
) |
142 | 9, 28, 30, 33, 35, 135, 139, 141 | mertens 15776 |
. . 3
โข (๐ โ seq0( + , ๐ป) โ (ฮฃ๐ โ โ0
((๐ดโ๐) / (!โ๐)) ยท ฮฃ๐ โ โ0 ((๐ตโ๐) / (!โ๐)))) |
143 | | efval 15967 |
. . . . 5
โข (๐ด โ โ โ
(expโ๐ด) =
ฮฃ๐ โ
โ0 ((๐ดโ๐) / (!โ๐))) |
144 | 1, 143 | syl 17 |
. . . 4
โข (๐ โ (expโ๐ด) = ฮฃ๐ โ โ0 ((๐ดโ๐) / (!โ๐))) |
145 | | efval 15967 |
. . . . 5
โข (๐ต โ โ โ
(expโ๐ต) =
ฮฃ๐ โ
โ0 ((๐ตโ๐) / (!โ๐))) |
146 | 2, 145 | syl 17 |
. . . 4
โข (๐ โ (expโ๐ต) = ฮฃ๐ โ โ0 ((๐ตโ๐) / (!โ๐))) |
147 | 144, 146 | oveq12d 7376 |
. . 3
โข (๐ โ ((expโ๐ด) ยท (expโ๐ต)) = (ฮฃ๐ โ โ0 ((๐ดโ๐) / (!โ๐)) ยท ฮฃ๐ โ โ0 ((๐ตโ๐) / (!โ๐)))) |
148 | 142, 147 | breqtrrd 5134 |
. 2
โข (๐ โ seq0( + , ๐ป) โ ((expโ๐ด) ยท (expโ๐ต))) |
149 | | climuni 15440 |
. 2
โข ((seq0( +
, ๐ป) โ
(expโ(๐ด + ๐ต)) โง seq0( + , ๐ป) โ ((expโ๐ด) ยท (expโ๐ต))) โ (expโ(๐ด + ๐ต)) = ((expโ๐ด) ยท (expโ๐ต))) |
150 | 6, 148, 149 | syl2anc 585 |
1
โข (๐ โ (expโ(๐ด + ๐ต)) = ((expโ๐ด) ยท (expโ๐ต))) |