Step | Hyp | Ref
| Expression |
1 | | cjcl 14996 |
. . 3
β’ (π΄ β β β
(ββπ΄) β
β) |
2 | | eqid 2733 |
. . . 4
β’ (π β β0
β¦ (((ββπ΄)βπ) / (!βπ))) = (π β β0 β¦
(((ββπ΄)βπ) / (!βπ))) |
3 | 2 | efcvg 15972 |
. . 3
β’
((ββπ΄)
β β β seq0( + , (π β β0 β¦
(((ββπ΄)βπ) / (!βπ)))) β (expβ(ββπ΄))) |
4 | 1, 3 | syl 17 |
. 2
β’ (π΄ β β β seq0( + ,
(π β
β0 β¦ (((ββπ΄)βπ) / (!βπ)))) β (expβ(ββπ΄))) |
5 | | nn0uz 12810 |
. . 3
β’
β0 = (β€β₯β0) |
6 | | eqid 2733 |
. . . 4
β’ (π β β0
β¦ ((π΄βπ) / (!βπ))) = (π β β0 β¦ ((π΄βπ) / (!βπ))) |
7 | 6 | efcvg 15972 |
. . 3
β’ (π΄ β β β seq0( + ,
(π β
β0 β¦ ((π΄βπ) / (!βπ)))) β (expβπ΄)) |
8 | | seqex 13914 |
. . . 4
β’ seq0( + ,
(π β
β0 β¦ (((ββπ΄)βπ) / (!βπ)))) β V |
9 | 8 | a1i 11 |
. . 3
β’ (π΄ β β β seq0( + ,
(π β
β0 β¦ (((ββπ΄)βπ) / (!βπ)))) β V) |
10 | | 0zd 12516 |
. . 3
β’ (π΄ β β β 0 β
β€) |
11 | 6 | eftval 15964 |
. . . . . . 7
β’ (π β β0
β ((π β
β0 β¦ ((π΄βπ) / (!βπ)))βπ) = ((π΄βπ) / (!βπ))) |
12 | 11 | adantl 483 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β ((π β
β0 β¦ ((π΄βπ) / (!βπ)))βπ) = ((π΄βπ) / (!βπ))) |
13 | | eftcl 15961 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β ((π΄βπ) / (!βπ)) β β) |
14 | 12, 13 | eqeltrd 2834 |
. . . . 5
β’ ((π΄ β β β§ π β β0)
β ((π β
β0 β¦ ((π΄βπ) / (!βπ)))βπ) β β) |
15 | 5, 10, 14 | serf 13942 |
. . . 4
β’ (π΄ β β β seq0( + ,
(π β
β0 β¦ ((π΄βπ) / (!βπ)))):β0βΆβ) |
16 | 15 | ffvelcdmda 7036 |
. . 3
β’ ((π΄ β β β§ π β β0)
β (seq0( + , (π β
β0 β¦ ((π΄βπ) / (!βπ))))βπ) β β) |
17 | | addcl 11138 |
. . . . . 6
β’ ((π β β β§ π β β) β (π + π) β β) |
18 | 17 | adantl 483 |
. . . . 5
β’ (((π΄ β β β§ π β β0)
β§ (π β β
β§ π β β))
β (π + π) β
β) |
19 | | simpl 484 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β π΄ β
β) |
20 | | elfznn0 13540 |
. . . . . 6
β’ (π β (0...π) β π β β0) |
21 | 19, 20, 14 | syl2an 597 |
. . . . 5
β’ (((π΄ β β β§ π β β0)
β§ π β (0...π)) β ((π β β0 β¦ ((π΄βπ) / (!βπ)))βπ) β β) |
22 | | simpr 486 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β π β
β0) |
23 | 22, 5 | eleqtrdi 2844 |
. . . . 5
β’ ((π΄ β β β§ π β β0)
β π β
(β€β₯β0)) |
24 | | cjadd 15032 |
. . . . . 6
β’ ((π β β β§ π β β) β
(ββ(π + π)) = ((ββπ) + (ββπ))) |
25 | 24 | adantl 483 |
. . . . 5
β’ (((π΄ β β β§ π β β0)
β§ (π β β
β§ π β β))
β (ββ(π +
π)) =
((ββπ) +
(ββπ))) |
26 | | expcl 13991 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β β0)
β (π΄βπ) β
β) |
27 | | faccl 14189 |
. . . . . . . . . . 11
β’ (π β β0
β (!βπ) β
β) |
28 | 27 | adantl 483 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π β β0)
β (!βπ) β
β) |
29 | 28 | nncnd 12174 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β β0)
β (!βπ) β
β) |
30 | 28 | nnne0d 12208 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β β0)
β (!βπ) β
0) |
31 | 26, 29, 30 | cjdivd 15114 |
. . . . . . . 8
β’ ((π΄ β β β§ π β β0)
β (ββ((π΄βπ) / (!βπ))) = ((ββ(π΄βπ)) / (ββ(!βπ)))) |
32 | | cjexp 15041 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β β0)
β (ββ(π΄βπ)) = ((ββπ΄)βπ)) |
33 | 28 | nnred 12173 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π β β0)
β (!βπ) β
β) |
34 | 33 | cjred 15117 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β β0)
β (ββ(!βπ)) = (!βπ)) |
35 | 32, 34 | oveq12d 7376 |
. . . . . . . 8
β’ ((π΄ β β β§ π β β0)
β ((ββ(π΄βπ)) / (ββ(!βπ))) = (((ββπ΄)βπ) / (!βπ))) |
36 | 31, 35 | eqtrd 2773 |
. . . . . . 7
β’ ((π΄ β β β§ π β β0)
β (ββ((π΄βπ) / (!βπ))) = (((ββπ΄)βπ) / (!βπ))) |
37 | 12 | fveq2d 6847 |
. . . . . . 7
β’ ((π΄ β β β§ π β β0)
β (ββ((π
β β0 β¦ ((π΄βπ) / (!βπ)))βπ)) = (ββ((π΄βπ) / (!βπ)))) |
38 | 2 | eftval 15964 |
. . . . . . . 8
β’ (π β β0
β ((π β
β0 β¦ (((ββπ΄)βπ) / (!βπ)))βπ) = (((ββπ΄)βπ) / (!βπ))) |
39 | 38 | adantl 483 |
. . . . . . 7
β’ ((π΄ β β β§ π β β0)
β ((π β
β0 β¦ (((ββπ΄)βπ) / (!βπ)))βπ) = (((ββπ΄)βπ) / (!βπ))) |
40 | 36, 37, 39 | 3eqtr4d 2783 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β (ββ((π
β β0 β¦ ((π΄βπ) / (!βπ)))βπ)) = ((π β β0 β¦
(((ββπ΄)βπ) / (!βπ)))βπ)) |
41 | 19, 20, 40 | syl2an 597 |
. . . . 5
β’ (((π΄ β β β§ π β β0)
β§ π β (0...π)) β
(ββ((π β
β0 β¦ ((π΄βπ) / (!βπ)))βπ)) = ((π β β0 β¦
(((ββπ΄)βπ) / (!βπ)))βπ)) |
42 | 18, 21, 23, 25, 41 | seqhomo 13961 |
. . . 4
β’ ((π΄ β β β§ π β β0)
β (ββ(seq0( + , (π β β0 β¦ ((π΄βπ) / (!βπ))))βπ)) = (seq0( + , (π β β0 β¦
(((ββπ΄)βπ) / (!βπ))))βπ)) |
43 | 42 | eqcomd 2739 |
. . 3
β’ ((π΄ β β β§ π β β0)
β (seq0( + , (π β
β0 β¦ (((ββπ΄)βπ) / (!βπ))))βπ) = (ββ(seq0( + , (π β β0
β¦ ((π΄βπ) / (!βπ))))βπ))) |
44 | 5, 7, 9, 10, 16, 43 | climcj 15493 |
. 2
β’ (π΄ β β β seq0( + ,
(π β
β0 β¦ (((ββπ΄)βπ) / (!βπ)))) β (ββ(expβπ΄))) |
45 | | climuni 15440 |
. 2
β’ ((seq0( +
, (π β
β0 β¦ (((ββπ΄)βπ) / (!βπ)))) β (expβ(ββπ΄)) β§ seq0( + , (π β β0
β¦ (((ββπ΄)βπ) / (!βπ)))) β (ββ(expβπ΄))) β
(expβ(ββπ΄)) = (ββ(expβπ΄))) |
46 | 4, 44, 45 | syl2anc 585 |
1
β’ (π΄ β β β
(expβ(ββπ΄)) = (ββ(expβπ΄))) |