Step | Hyp | Ref
| Expression |
1 | | cjcl 10856 |
. . 3
β’ (π΄ β β β
(ββπ΄) β
β) |
2 | | eqid 2177 |
. . . 4
β’ (π β β0
β¦ (((ββπ΄)βπ) / (!βπ))) = (π β β0 β¦
(((ββπ΄)βπ) / (!βπ))) |
3 | 2 | efcvg 11673 |
. . 3
β’
((ββπ΄)
β β β seq0( + , (π β β0 β¦
(((ββπ΄)βπ) / (!βπ)))) β (expβ(ββπ΄))) |
4 | 1, 3 | syl 14 |
. 2
β’ (π΄ β β β seq0( + ,
(π β
β0 β¦ (((ββπ΄)βπ) / (!βπ)))) β (expβ(ββπ΄))) |
5 | | nn0uz 9561 |
. . 3
β’
β0 = (β€β₯β0) |
6 | | eqid 2177 |
. . . 4
β’ (π β β0
β¦ ((π΄βπ) / (!βπ))) = (π β β0 β¦ ((π΄βπ) / (!βπ))) |
7 | 6 | efcvg 11673 |
. . 3
β’ (π΄ β β β seq0( + ,
(π β
β0 β¦ ((π΄βπ) / (!βπ)))) β (expβπ΄)) |
8 | | seqex 10446 |
. . . 4
β’ seq0( + ,
(π β
β0 β¦ (((ββπ΄)βπ) / (!βπ)))) β V |
9 | 8 | a1i 9 |
. . 3
β’ (π΄ β β β seq0( + ,
(π β
β0 β¦ (((ββπ΄)βπ) / (!βπ)))) β V) |
10 | | 0zd 9264 |
. . 3
β’ (π΄ β β β 0 β
β€) |
11 | 6 | eftvalcn 11664 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β ((π β
β0 β¦ ((π΄βπ) / (!βπ)))βπ) = ((π΄βπ) / (!βπ))) |
12 | | eftcl 11661 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β ((π΄βπ) / (!βπ)) β β) |
13 | 11, 12 | eqeltrd 2254 |
. . . . 5
β’ ((π΄ β β β§ π β β0)
β ((π β
β0 β¦ ((π΄βπ) / (!βπ)))βπ) β β) |
14 | 5, 10, 13 | serf 10473 |
. . . 4
β’ (π΄ β β β seq0( + ,
(π β
β0 β¦ ((π΄βπ) / (!βπ)))):β0βΆβ) |
15 | 14 | ffvelcdmda 5651 |
. . 3
β’ ((π΄ β β β§ π β β0)
β (seq0( + , (π β
β0 β¦ ((π΄βπ) / (!βπ))))βπ) β β) |
16 | | addcl 7935 |
. . . . . 6
β’ ((π β β β§ π β β) β (π + π) β β) |
17 | 16 | adantl 277 |
. . . . 5
β’ (((π΄ β β β§ π β β0)
β§ (π β β
β§ π β β))
β (π + π) β
β) |
18 | | simpl 109 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β π΄ β
β) |
19 | | elnn0uz 9564 |
. . . . . . 7
β’ (π β β0
β π β
(β€β₯β0)) |
20 | 19 | biimpri 133 |
. . . . . 6
β’ (π β
(β€β₯β0) β π β β0) |
21 | 18, 20, 13 | syl2an 289 |
. . . . 5
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β ((π β β0 β¦ ((π΄βπ) / (!βπ)))βπ) β β) |
22 | | simpr 110 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β π β
β0) |
23 | 22, 5 | eleqtrdi 2270 |
. . . . 5
β’ ((π΄ β β β§ π β β0)
β π β
(β€β₯β0)) |
24 | | cjadd 10892 |
. . . . . 6
β’ ((π β β β§ π β β) β
(ββ(π + π)) = ((ββπ) + (ββπ))) |
25 | 24 | adantl 277 |
. . . . 5
β’ (((π΄ β β β§ π β β0)
β§ (π β β
β§ π β β))
β (ββ(π +
π)) =
((ββπ) +
(ββπ))) |
26 | | expcl 10537 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β β0)
β (π΄βπ) β
β) |
27 | | faccl 10714 |
. . . . . . . . . . 11
β’ (π β β0
β (!βπ) β
β) |
28 | 27 | adantl 277 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π β β0)
β (!βπ) β
β) |
29 | 28 | nncnd 8932 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β β0)
β (!βπ) β
β) |
30 | 28 | nnap0d 8964 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β β0)
β (!βπ) #
0) |
31 | 26, 29, 30 | cjdivapd 10976 |
. . . . . . . 8
β’ ((π΄ β β β§ π β β0)
β (ββ((π΄βπ) / (!βπ))) = ((ββ(π΄βπ)) / (ββ(!βπ)))) |
32 | | cjexp 10901 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β β0)
β (ββ(π΄βπ)) = ((ββπ΄)βπ)) |
33 | 28 | nnred 8931 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π β β0)
β (!βπ) β
β) |
34 | 33 | cjred 10979 |
. . . . . . . . 9
β’ ((π΄ β β β§ π β β0)
β (ββ(!βπ)) = (!βπ)) |
35 | 32, 34 | oveq12d 5892 |
. . . . . . . 8
β’ ((π΄ β β β§ π β β0)
β ((ββ(π΄βπ)) / (ββ(!βπ))) = (((ββπ΄)βπ) / (!βπ))) |
36 | 31, 35 | eqtrd 2210 |
. . . . . . 7
β’ ((π΄ β β β§ π β β0)
β (ββ((π΄βπ) / (!βπ))) = (((ββπ΄)βπ) / (!βπ))) |
37 | 11 | fveq2d 5519 |
. . . . . . 7
β’ ((π΄ β β β§ π β β0)
β (ββ((π
β β0 β¦ ((π΄βπ) / (!βπ)))βπ)) = (ββ((π΄βπ) / (!βπ)))) |
38 | 2 | eftvalcn 11664 |
. . . . . . . 8
β’
(((ββπ΄)
β β β§ π
β β0) β ((π β β0 β¦
(((ββπ΄)βπ) / (!βπ)))βπ) = (((ββπ΄)βπ) / (!βπ))) |
39 | 1, 38 | sylan 283 |
. . . . . . 7
β’ ((π΄ β β β§ π β β0)
β ((π β
β0 β¦ (((ββπ΄)βπ) / (!βπ)))βπ) = (((ββπ΄)βπ) / (!βπ))) |
40 | 36, 37, 39 | 3eqtr4d 2220 |
. . . . . 6
β’ ((π΄ β β β§ π β β0)
β (ββ((π
β β0 β¦ ((π΄βπ) / (!βπ)))βπ)) = ((π β β0 β¦
(((ββπ΄)βπ) / (!βπ)))βπ)) |
41 | 18, 20, 40 | syl2an 289 |
. . . . 5
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β (ββ((π β β0 β¦ ((π΄βπ) / (!βπ)))βπ)) = ((π β β0 β¦
(((ββπ΄)βπ) / (!βπ)))βπ)) |
42 | 20 | adantl 277 |
. . . . . . 7
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β π β β0) |
43 | 1 | ad2antrr 488 |
. . . . . . . . 9
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β (ββπ΄) β β) |
44 | 43, 42 | expcld 10653 |
. . . . . . . 8
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β ((ββπ΄)βπ) β β) |
45 | 18, 20, 29 | syl2an 289 |
. . . . . . . 8
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β (!βπ) β β) |
46 | 18, 20, 30 | syl2an 289 |
. . . . . . . 8
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β (!βπ) # 0) |
47 | 44, 45, 46 | divclapd 8746 |
. . . . . . 7
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β (((ββπ΄)βπ) / (!βπ)) β β) |
48 | | oveq2 5882 |
. . . . . . . . 9
β’ (π = π β ((ββπ΄)βπ) = ((ββπ΄)βπ)) |
49 | | fveq2 5515 |
. . . . . . . . 9
β’ (π = π β (!βπ) = (!βπ)) |
50 | 48, 49 | oveq12d 5892 |
. . . . . . . 8
β’ (π = π β (((ββπ΄)βπ) / (!βπ)) = (((ββπ΄)βπ) / (!βπ))) |
51 | 50, 2 | fvmptg 5592 |
. . . . . . 7
β’ ((π β β0
β§ (((ββπ΄)βπ) / (!βπ)) β β) β ((π β β0
β¦ (((ββπ΄)βπ) / (!βπ)))βπ) = (((ββπ΄)βπ) / (!βπ))) |
52 | 42, 47, 51 | syl2anc 411 |
. . . . . 6
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β ((π β β0 β¦
(((ββπ΄)βπ) / (!βπ)))βπ) = (((ββπ΄)βπ) / (!βπ))) |
53 | 52, 47 | eqeltrd 2254 |
. . . . 5
β’ (((π΄ β β β§ π β β0)
β§ π β
(β€β₯β0)) β ((π β β0 β¦
(((ββπ΄)βπ) / (!βπ)))βπ) β β) |
54 | 17, 21, 23, 25, 41, 53, 17 | seq3homo 10509 |
. . . 4
β’ ((π΄ β β β§ π β β0)
β (ββ(seq0( + , (π β β0 β¦ ((π΄βπ) / (!βπ))))βπ)) = (seq0( + , (π β β0 β¦
(((ββπ΄)βπ) / (!βπ))))βπ)) |
55 | 54 | eqcomd 2183 |
. . 3
β’ ((π΄ β β β§ π β β0)
β (seq0( + , (π β
β0 β¦ (((ββπ΄)βπ) / (!βπ))))βπ) = (ββ(seq0( + , (π β β0
β¦ ((π΄βπ) / (!βπ))))βπ))) |
56 | 5, 7, 9, 10, 15, 55 | climcj 11328 |
. 2
β’ (π΄ β β β seq0( + ,
(π β
β0 β¦ (((ββπ΄)βπ) / (!βπ)))) β (ββ(expβπ΄))) |
57 | | climuni 11300 |
. 2
β’ ((seq0( +
, (π β
β0 β¦ (((ββπ΄)βπ) / (!βπ)))) β (expβ(ββπ΄)) β§ seq0( + , (π β β0
β¦ (((ββπ΄)βπ) / (!βπ)))) β (ββ(expβπ΄))) β
(expβ(ββπ΄)) = (ββ(expβπ΄))) |
58 | 4, 56, 57 | syl2anc 411 |
1
β’ (π΄ β β β
(expβ(ββπ΄)) = (ββ(expβπ΄))) |