Step | Hyp | Ref
| Expression |
1 | | fzfid 13934 |
. . . . . 6
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
(0...π) β
Fin) |
2 | | rpcn 12980 |
. . . . . . 7
β’ (π₯ β β+
β π₯ β
β) |
3 | 2 | adantl 482 |
. . . . . 6
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β π₯ β
β) |
4 | | rpdivcl 12995 |
. . . . . . . . . . 11
β’ ((π΄ β β+
β§ π₯ β
β+) β (π΄ / π₯) β
β+) |
5 | 4 | adantlr 713 |
. . . . . . . . . 10
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β (π΄ / π₯) β
β+) |
6 | 5 | relogcld 26122 |
. . . . . . . . 9
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
(logβ(π΄ / π₯)) β
β) |
7 | | elfznn0 13590 |
. . . . . . . . 9
β’ (π β (0...π) β π β β0) |
8 | | reexpcl 14040 |
. . . . . . . . 9
β’
(((logβ(π΄ /
π₯)) β β β§
π β
β0) β ((logβ(π΄ / π₯))βπ) β β) |
9 | 6, 7, 8 | syl2an 596 |
. . . . . . . 8
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0...π)) β ((logβ(π΄ / π₯))βπ) β β) |
10 | 7 | adantl 482 |
. . . . . . . . 9
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0...π)) β π β β0) |
11 | 10 | faccld 14240 |
. . . . . . . 8
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0...π)) β (!βπ) β β) |
12 | 9, 11 | nndivred 12262 |
. . . . . . 7
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0...π)) β (((logβ(π΄ / π₯))βπ) / (!βπ)) β β) |
13 | 12 | recnd 11238 |
. . . . . 6
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0...π)) β (((logβ(π΄ / π₯))βπ) / (!βπ)) β β) |
14 | 1, 3, 13 | fsummulc2 15726 |
. . . . 5
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β (π₯ Β· Ξ£π β (0...π)(((logβ(π΄ / π₯))βπ) / (!βπ))) = Ξ£π β (0...π)(π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ)))) |
15 | | simplr 767 |
. . . . . . 7
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β π β
β0) |
16 | | nn0uz 12860 |
. . . . . . 7
β’
β0 = (β€β₯β0) |
17 | 15, 16 | eleqtrdi 2843 |
. . . . . 6
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β π β
(β€β₯β0)) |
18 | 3 | adantr 481 |
. . . . . . 7
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0...π)) β π₯ β β) |
19 | 18, 13 | mulcld 11230 |
. . . . . 6
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0...π)) β (π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ))) β β) |
20 | | oveq2 7413 |
. . . . . . . 8
β’ (π = 0 β ((logβ(π΄ / π₯))βπ) = ((logβ(π΄ / π₯))β0)) |
21 | | fveq2 6888 |
. . . . . . . . 9
β’ (π = 0 β (!βπ) =
(!β0)) |
22 | | fac0 14232 |
. . . . . . . . 9
β’
(!β0) = 1 |
23 | 21, 22 | eqtrdi 2788 |
. . . . . . . 8
β’ (π = 0 β (!βπ) = 1) |
24 | 20, 23 | oveq12d 7423 |
. . . . . . 7
β’ (π = 0 β (((logβ(π΄ / π₯))βπ) / (!βπ)) = (((logβ(π΄ / π₯))β0) / 1)) |
25 | 24 | oveq2d 7421 |
. . . . . 6
β’ (π = 0 β (π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ))) = (π₯ Β· (((logβ(π΄ / π₯))β0) / 1))) |
26 | 17, 19, 25 | fsum1p 15695 |
. . . . 5
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
Ξ£π β (0...π)(π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ))) = ((π₯ Β· (((logβ(π΄ / π₯))β0) / 1)) + Ξ£π β ((0 + 1)...π)(π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ))))) |
27 | 6 | recnd 11238 |
. . . . . . . . . . 11
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
(logβ(π΄ / π₯)) β
β) |
28 | 27 | exp0d 14101 |
. . . . . . . . . 10
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
((logβ(π΄ / π₯))β0) = 1) |
29 | 28 | oveq1d 7420 |
. . . . . . . . 9
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
(((logβ(π΄ / π₯))β0) / 1) = (1 /
1)) |
30 | | 1div1e1 11900 |
. . . . . . . . 9
β’ (1 / 1) =
1 |
31 | 29, 30 | eqtrdi 2788 |
. . . . . . . 8
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
(((logβ(π΄ / π₯))β0) / 1) =
1) |
32 | 31 | oveq2d 7421 |
. . . . . . 7
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β (π₯ Β· (((logβ(π΄ / π₯))β0) / 1)) = (π₯ Β· 1)) |
33 | 3 | mulridd 11227 |
. . . . . . 7
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β (π₯ Β· 1) = π₯) |
34 | 32, 33 | eqtrd 2772 |
. . . . . 6
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β (π₯ Β· (((logβ(π΄ / π₯))β0) / 1)) = π₯) |
35 | | 1zzd 12589 |
. . . . . . . 8
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β 1 β
β€) |
36 | | nn0z 12579 |
. . . . . . . . 9
β’ (π β β0
β π β
β€) |
37 | 36 | ad2antlr 725 |
. . . . . . . 8
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β π β
β€) |
38 | | fz1ssfz0 13593 |
. . . . . . . . . 10
β’
(1...π) β
(0...π) |
39 | 38 | sseli 3977 |
. . . . . . . . 9
β’ (π β (1...π) β π β (0...π)) |
40 | 39, 19 | sylan2 593 |
. . . . . . . 8
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (1...π)) β (π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ))) β β) |
41 | | oveq2 7413 |
. . . . . . . . . 10
β’ (π = (π + 1) β ((logβ(π΄ / π₯))βπ) = ((logβ(π΄ / π₯))β(π + 1))) |
42 | | fveq2 6888 |
. . . . . . . . . 10
β’ (π = (π + 1) β (!βπ) = (!β(π + 1))) |
43 | 41, 42 | oveq12d 7423 |
. . . . . . . . 9
β’ (π = (π + 1) β (((logβ(π΄ / π₯))βπ) / (!βπ)) = (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))) |
44 | 43 | oveq2d 7421 |
. . . . . . . 8
β’ (π = (π + 1) β (π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ))) = (π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))))) |
45 | 35, 35, 37, 40, 44 | fsumshftm 15723 |
. . . . . . 7
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
Ξ£π β (1...π)(π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ))) = Ξ£π β ((1 β 1)...(π β 1))(π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))))) |
46 | | 0p1e1 12330 |
. . . . . . . . . 10
β’ (0 + 1) =
1 |
47 | 46 | oveq1i 7415 |
. . . . . . . . 9
β’ ((0 +
1)...π) = (1...π) |
48 | 47 | sumeq1i 15640 |
. . . . . . . 8
β’
Ξ£π β ((0
+ 1)...π)(π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ))) = Ξ£π β (1...π)(π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ))) |
49 | 48 | a1i 11 |
. . . . . . 7
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
Ξ£π β ((0 +
1)...π)(π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ))) = Ξ£π β (1...π)(π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ)))) |
50 | | 1m1e0 12280 |
. . . . . . . . . 10
β’ (1
β 1) = 0 |
51 | 50 | oveq1i 7415 |
. . . . . . . . 9
β’ ((1
β 1)..^π) =
(0..^π) |
52 | | fzoval 13629 |
. . . . . . . . . 10
β’ (π β β€ β ((1
β 1)..^π) = ((1
β 1)...(π β
1))) |
53 | 37, 52 | syl 17 |
. . . . . . . . 9
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β ((1
β 1)..^π) = ((1
β 1)...(π β
1))) |
54 | 51, 53 | eqtr3id 2786 |
. . . . . . . 8
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
(0..^π) = ((1 β
1)...(π β
1))) |
55 | 54 | sumeq1d 15643 |
. . . . . . 7
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
Ξ£π β (0..^π)(π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))) = Ξ£π β ((1 β 1)...(π β 1))(π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))))) |
56 | 45, 49, 55 | 3eqtr4d 2782 |
. . . . . 6
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
Ξ£π β ((0 +
1)...π)(π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ))) = Ξ£π β (0..^π)(π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))))) |
57 | 34, 56 | oveq12d 7423 |
. . . . 5
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β ((π₯ Β· (((logβ(π΄ / π₯))β0) / 1)) + Ξ£π β ((0 + 1)...π)(π₯ Β· (((logβ(π΄ / π₯))βπ) / (!βπ)))) = (π₯ + Ξ£π β (0..^π)(π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))))) |
58 | 14, 26, 57 | 3eqtrd 2776 |
. . . 4
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β (π₯ Β· Ξ£π β (0...π)(((logβ(π΄ / π₯))βπ) / (!βπ))) = (π₯ + Ξ£π β (0..^π)(π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))))) |
59 | 58 | mpteq2dva 5247 |
. . 3
β’ ((π΄ β β+
β§ π β
β0) β (π₯ β β+ β¦ (π₯ Β· Ξ£π β (0...π)(((logβ(π΄ / π₯))βπ) / (!βπ)))) = (π₯ β β+ β¦ (π₯ + Ξ£π β (0..^π)(π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))))))) |
60 | 59 | oveq2d 7421 |
. 2
β’ ((π΄ β β+
β§ π β
β0) β (β D (π₯ β β+ β¦ (π₯ Β· Ξ£π β (0...π)(((logβ(π΄ / π₯))βπ) / (!βπ))))) = (β D (π₯ β β+ β¦ (π₯ + Ξ£π β (0..^π)(π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))))))) |
61 | | reelprrecn 11198 |
. . . 4
β’ β
β {β, β} |
62 | 61 | a1i 11 |
. . 3
β’ ((π΄ β β+
β§ π β
β0) β β β {β, β}) |
63 | | 1cnd 11205 |
. . 3
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β 1 β
β) |
64 | | recn 11196 |
. . . . 5
β’ (π₯ β β β π₯ β
β) |
65 | 64 | adantl 482 |
. . . 4
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β) β π₯ β β) |
66 | | 1cnd 11205 |
. . . 4
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β) β 1 β
β) |
67 | 62 | dvmptid 25465 |
. . . 4
β’ ((π΄ β β+
β§ π β
β0) β (β D (π₯ β β β¦ π₯)) = (π₯ β β β¦ 1)) |
68 | | rpssre 12977 |
. . . . 5
β’
β+ β β |
69 | 68 | a1i 11 |
. . . 4
β’ ((π΄ β β+
β§ π β
β0) β β+ β
β) |
70 | | eqid 2732 |
. . . . 5
β’
(TopOpenββfld) =
(TopOpenββfld) |
71 | 70 | tgioo2 24310 |
. . . 4
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
72 | | ioorp 13398 |
. . . . . 6
β’
(0(,)+β) = β+ |
73 | | iooretop 24273 |
. . . . . 6
β’
(0(,)+β) β (topGenβran (,)) |
74 | 72, 73 | eqeltrri 2830 |
. . . . 5
β’
β+ β (topGenβran (,)) |
75 | 74 | a1i 11 |
. . . 4
β’ ((π΄ β β+
β§ π β
β0) β β+ β (topGenβran
(,))) |
76 | 62, 65, 66, 67, 69, 71, 70, 75 | dvmptres 25471 |
. . 3
β’ ((π΄ β β+
β§ π β
β0) β (β D (π₯ β β+ β¦ π₯)) = (π₯ β β+ β¦
1)) |
77 | | fzofi 13935 |
. . . . 5
β’
(0..^π) β
Fin |
78 | 77 | a1i 11 |
. . . 4
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
(0..^π) β
Fin) |
79 | 3 | adantr 481 |
. . . . 5
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β π₯ β β) |
80 | | elfzonn0 13673 |
. . . . . . . . 9
β’ (π β (0..^π) β π β β0) |
81 | | peano2nn0 12508 |
. . . . . . . . 9
β’ (π β β0
β (π + 1) β
β0) |
82 | 80, 81 | syl 17 |
. . . . . . . 8
β’ (π β (0..^π) β (π + 1) β
β0) |
83 | | reexpcl 14040 |
. . . . . . . 8
β’
(((logβ(π΄ /
π₯)) β β β§
(π + 1) β
β0) β ((logβ(π΄ / π₯))β(π + 1)) β β) |
84 | 6, 82, 83 | syl2an 596 |
. . . . . . 7
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β ((logβ(π΄ / π₯))β(π + 1)) β β) |
85 | 82 | adantl 482 |
. . . . . . . 8
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β (π + 1) β
β0) |
86 | 85 | faccld 14240 |
. . . . . . 7
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β (!β(π + 1)) β β) |
87 | 84, 86 | nndivred 12262 |
. . . . . 6
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β β) |
88 | 87 | recnd 11238 |
. . . . 5
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β β) |
89 | 79, 88 | mulcld 11230 |
. . . 4
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β (π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))) β β) |
90 | 78, 89 | fsumcl 15675 |
. . 3
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
Ξ£π β (0..^π)(π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))) β β) |
91 | 6, 15 | reexpcld 14124 |
. . . . . 6
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
((logβ(π΄ / π₯))βπ) β β) |
92 | | faccl 14239 |
. . . . . . 7
β’ (π β β0
β (!βπ) β
β) |
93 | 92 | ad2antlr 725 |
. . . . . 6
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
(!βπ) β
β) |
94 | 91, 93 | nndivred 12262 |
. . . . 5
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
(((logβ(π΄ / π₯))βπ) / (!βπ)) β β) |
95 | 94 | recnd 11238 |
. . . 4
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
(((logβ(π΄ / π₯))βπ) / (!βπ)) β β) |
96 | | ax-1cn 11164 |
. . . 4
β’ 1 β
β |
97 | | subcl 11455 |
. . . 4
β’
(((((logβ(π΄ /
π₯))βπ) / (!βπ)) β β β§ 1 β β)
β ((((logβ(π΄ /
π₯))βπ) / (!βπ)) β 1) β
β) |
98 | 95, 96, 97 | sylancl 586 |
. . 3
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
((((logβ(π΄ / π₯))βπ) / (!βπ)) β 1) β
β) |
99 | 77 | a1i 11 |
. . . . 5
β’ ((π΄ β β+
β§ π β
β0) β (0..^π) β Fin) |
100 | 89 | an32s 650 |
. . . . . 6
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β (π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))) β β) |
101 | 100 | 3impa 1110 |
. . . . 5
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π) β§ π₯ β β+) β (π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))) β β) |
102 | | reexpcl 14040 |
. . . . . . . . . . 11
β’
(((logβ(π΄ /
π₯)) β β β§
π β
β0) β ((logβ(π΄ / π₯))βπ) β β) |
103 | 6, 80, 102 | syl2an 596 |
. . . . . . . . . 10
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β ((logβ(π΄ / π₯))βπ) β β) |
104 | 80 | adantl 482 |
. . . . . . . . . . 11
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β π β β0) |
105 | 104 | faccld 14240 |
. . . . . . . . . 10
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β (!βπ) β β) |
106 | 103, 105 | nndivred 12262 |
. . . . . . . . 9
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β (((logβ(π΄ / π₯))βπ) / (!βπ)) β β) |
107 | 106 | recnd 11238 |
. . . . . . . 8
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β (((logβ(π΄ / π₯))βπ) / (!βπ)) β β) |
108 | 88, 107 | subcld 11567 |
. . . . . . 7
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β ((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β (((logβ(π΄ / π₯))βπ) / (!βπ))) β β) |
109 | 108 | an32s 650 |
. . . . . 6
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β
((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β (((logβ(π΄ / π₯))βπ) / (!βπ))) β β) |
110 | 109 | 3impa 1110 |
. . . . 5
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π) β§ π₯ β β+) β
((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β (((logβ(π΄ / π₯))βπ) / (!βπ))) β β) |
111 | 61 | a1i 11 |
. . . . . . 7
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β β β {β,
β}) |
112 | 2 | adantl 482 |
. . . . . . 7
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β π₯ β
β) |
113 | | 1cnd 11205 |
. . . . . . 7
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β 1 β
β) |
114 | 76 | adantr 481 |
. . . . . . 7
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π₯ β β+ β¦ π₯)) = (π₯ β β+ β¦
1)) |
115 | 88 | an32s 650 |
. . . . . . 7
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β
(((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β β) |
116 | | negex 11454 |
. . . . . . . 8
β’
-((((logβ(π΄ /
π₯))βπ) / (!βπ)) / π₯) β V |
117 | 116 | a1i 11 |
. . . . . . 7
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β
-((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) β V) |
118 | | cnelprrecn 11199 |
. . . . . . . . . 10
β’ β
β {β, β} |
119 | 118 | a1i 11 |
. . . . . . . . 9
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β β β {β,
β}) |
120 | 27 | adantlr 713 |
. . . . . . . . 9
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β
(logβ(π΄ / π₯)) β
β) |
121 | | negex 11454 |
. . . . . . . . . 10
β’ -(1 /
π₯) β
V |
122 | 121 | a1i 11 |
. . . . . . . . 9
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β -(1 /
π₯) β
V) |
123 | | id 22 |
. . . . . . . . . . 11
β’ (π¦ β β β π¦ β
β) |
124 | 80 | adantl 482 |
. . . . . . . . . . . 12
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β π β β0) |
125 | 124, 81 | syl 17 |
. . . . . . . . . . 11
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (π + 1) β
β0) |
126 | | expcl 14041 |
. . . . . . . . . . 11
β’ ((π¦ β β β§ (π + 1) β
β0) β (π¦β(π + 1)) β β) |
127 | 123, 125,
126 | syl2anr 597 |
. . . . . . . . . 10
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (π¦β(π + 1)) β β) |
128 | 125 | faccld 14240 |
. . . . . . . . . . . 12
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (!β(π + 1)) β β) |
129 | 128 | nncnd 12224 |
. . . . . . . . . . 11
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (!β(π + 1)) β β) |
130 | 129 | adantr 481 |
. . . . . . . . . 10
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (!β(π + 1)) β
β) |
131 | 128 | nnne0d 12258 |
. . . . . . . . . . 11
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (!β(π + 1)) β 0) |
132 | 131 | adantr 481 |
. . . . . . . . . 10
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (!β(π + 1)) β 0) |
133 | 127, 130,
132 | divcld 11986 |
. . . . . . . . 9
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β ((π¦β(π + 1)) / (!β(π + 1))) β β) |
134 | | expcl 14041 |
. . . . . . . . . . 11
β’ ((π¦ β β β§ π β β0)
β (π¦βπ) β
β) |
135 | 123, 124,
134 | syl2anr 597 |
. . . . . . . . . 10
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (π¦βπ) β β) |
136 | 124 | faccld 14240 |
. . . . . . . . . . . 12
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (!βπ) β β) |
137 | 136 | nncnd 12224 |
. . . . . . . . . . 11
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (!βπ) β β) |
138 | 137 | adantr 481 |
. . . . . . . . . 10
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (!βπ) β
β) |
139 | 124 | adantr 481 |
. . . . . . . . . . . 12
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β π β β0) |
140 | 139 | faccld 14240 |
. . . . . . . . . . 11
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (!βπ) β
β) |
141 | 140 | nnne0d 12258 |
. . . . . . . . . 10
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (!βπ) β 0) |
142 | 135, 138,
141 | divcld 11986 |
. . . . . . . . 9
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β ((π¦βπ) / (!βπ)) β β) |
143 | | simplll 773 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β π΄ β
β+) |
144 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β π₯ β
β+) |
145 | 143, 144 | relogdivd 26125 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β
(logβ(π΄ / π₯)) = ((logβπ΄) β (logβπ₯))) |
146 | 145 | mpteq2dva 5247 |
. . . . . . . . . . . 12
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (π₯ β β+ β¦
(logβ(π΄ / π₯))) = (π₯ β β+ β¦
((logβπ΄) β
(logβπ₯)))) |
147 | 146 | oveq2d 7421 |
. . . . . . . . . . 11
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π₯ β β+ β¦
(logβ(π΄ / π₯)))) = (β D (π₯ β β+
β¦ ((logβπ΄)
β (logβπ₯))))) |
148 | | relogcl 26075 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β+
β (logβπ΄) β
β) |
149 | 148 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (logβπ΄) β β) |
150 | 149 | recnd 11238 |
. . . . . . . . . . . . 13
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (logβπ΄) β β) |
151 | 150 | adantr 481 |
. . . . . . . . . . . 12
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β
(logβπ΄) β
β) |
152 | | 0cnd 11203 |
. . . . . . . . . . . 12
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β 0 β
β) |
153 | 150 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β) β (logβπ΄) β
β) |
154 | | 0cnd 11203 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β) β 0 β
β) |
155 | 111, 150 | dvmptc 25466 |
. . . . . . . . . . . . 13
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π₯ β β β¦ (logβπ΄))) = (π₯ β β β¦ 0)) |
156 | 68 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β β+ β
β) |
157 | 74 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β β+ β
(topGenβran (,))) |
158 | 111, 153,
154, 155, 156, 71, 70, 157 | dvmptres 25471 |
. . . . . . . . . . . 12
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π₯ β β+ β¦
(logβπ΄))) = (π₯ β β+
β¦ 0)) |
159 | 144 | relogcld 26122 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β
(logβπ₯) β
β) |
160 | 159 | recnd 11238 |
. . . . . . . . . . . 12
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β
(logβπ₯) β
β) |
161 | 144 | rpreccld 13022 |
. . . . . . . . . . . 12
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β (1 /
π₯) β
β+) |
162 | | relogf1o 26066 |
. . . . . . . . . . . . . . . . 17
β’ (log
βΎ β+):β+β1-1-ontoββ |
163 | | f1of 6830 |
. . . . . . . . . . . . . . . . 17
β’ ((log
βΎ β+):β+β1-1-ontoββ β (log βΎ
β+):β+βΆβ) |
164 | 162, 163 | mp1i 13 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (log βΎ
β+):β+βΆβ) |
165 | 164 | feqmptd 6957 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (log βΎ β+)
= (π₯ β
β+ β¦ ((log βΎ β+)βπ₯))) |
166 | | fvres 6907 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β+
β ((log βΎ β+)βπ₯) = (logβπ₯)) |
167 | 166 | mpteq2ia 5250 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β+
β¦ ((log βΎ β+)βπ₯)) = (π₯ β β+ β¦
(logβπ₯)) |
168 | 165, 167 | eqtrdi 2788 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (log βΎ β+)
= (π₯ β
β+ β¦ (logβπ₯))) |
169 | 168 | oveq2d 7421 |
. . . . . . . . . . . . 13
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (log βΎ
β+)) = (β D (π₯ β β+ β¦
(logβπ₯)))) |
170 | | dvrelog 26136 |
. . . . . . . . . . . . 13
β’ (β
D (log βΎ β+)) = (π₯ β β+ β¦ (1 /
π₯)) |
171 | 169, 170 | eqtr3di 2787 |
. . . . . . . . . . . 12
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π₯ β β+ β¦
(logβπ₯))) = (π₯ β β+
β¦ (1 / π₯))) |
172 | 111, 151,
152, 158, 160, 161, 171 | dvmptsub 25475 |
. . . . . . . . . . 11
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π₯ β β+ β¦
((logβπ΄) β
(logβπ₯)))) = (π₯ β β+
β¦ (0 β (1 / π₯)))) |
173 | 147, 172 | eqtrd 2772 |
. . . . . . . . . 10
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π₯ β β+ β¦
(logβ(π΄ / π₯)))) = (π₯ β β+ β¦ (0
β (1 / π₯)))) |
174 | | df-neg 11443 |
. . . . . . . . . . 11
β’ -(1 /
π₯) = (0 β (1 / π₯)) |
175 | 174 | mpteq2i 5252 |
. . . . . . . . . 10
β’ (π₯ β β+
β¦ -(1 / π₯)) = (π₯ β β+
β¦ (0 β (1 / π₯))) |
176 | 173, 175 | eqtr4di 2790 |
. . . . . . . . 9
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π₯ β β+ β¦
(logβ(π΄ / π₯)))) = (π₯ β β+ β¦ -(1 /
π₯))) |
177 | | ovexd 7440 |
. . . . . . . . . . 11
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β ((π + 1) Β· (π¦β((π + 1) β 1))) β V) |
178 | | nn0p1nn 12507 |
. . . . . . . . . . . . 13
β’ (π β β0
β (π + 1) β
β) |
179 | 124, 178 | syl 17 |
. . . . . . . . . . . 12
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (π + 1) β β) |
180 | | dvexp 25461 |
. . . . . . . . . . . 12
β’ ((π + 1) β β β
(β D (π¦ β
β β¦ (π¦β(π + 1)))) = (π¦ β β β¦ ((π + 1) Β· (π¦β((π + 1) β 1))))) |
181 | 179, 180 | syl 17 |
. . . . . . . . . . 11
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π¦ β β β¦ (π¦β(π + 1)))) = (π¦ β β β¦ ((π + 1) Β· (π¦β((π + 1) β 1))))) |
182 | 119, 127,
177, 181, 129, 131 | dvmptdivc 25473 |
. . . . . . . . . 10
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π¦ β β β¦ ((π¦β(π + 1)) / (!β(π + 1))))) = (π¦ β β β¦ (((π + 1) Β· (π¦β((π + 1) β 1))) / (!β(π + 1))))) |
183 | 124 | nn0cnd 12530 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β π β β) |
184 | 183 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β π β β) |
185 | | pncan 11462 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
186 | 184, 96, 185 | sylancl 586 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β ((π + 1) β 1) = π) |
187 | 186 | oveq2d 7421 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (π¦β((π + 1) β 1)) = (π¦βπ)) |
188 | 187 | oveq2d 7421 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β ((π + 1) Β· (π¦β((π + 1) β 1))) = ((π + 1) Β· (π¦βπ))) |
189 | | facp1 14234 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (!β(π + 1)) =
((!βπ) Β·
(π + 1))) |
190 | 139, 189 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (!β(π + 1)) = ((!βπ) Β· (π + 1))) |
191 | | peano2cn 11382 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π + 1) β
β) |
192 | 184, 191 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (π + 1) β β) |
193 | 138, 192 | mulcomd 11231 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β ((!βπ) Β· (π + 1)) = ((π + 1) Β· (!βπ))) |
194 | 190, 193 | eqtrd 2772 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (!β(π + 1)) = ((π + 1) Β· (!βπ))) |
195 | 188, 194 | oveq12d 7423 |
. . . . . . . . . . . 12
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (((π + 1) Β· (π¦β((π + 1) β 1))) / (!β(π + 1))) = (((π + 1) Β· (π¦βπ)) / ((π + 1) Β· (!βπ)))) |
196 | 179 | nnne0d 12258 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (π + 1) β 0) |
197 | 196 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (π + 1) β 0) |
198 | 135, 138,
192, 141, 197 | divcan5d 12012 |
. . . . . . . . . . . 12
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (((π + 1) Β· (π¦βπ)) / ((π + 1) Β· (!βπ))) = ((π¦βπ) / (!βπ))) |
199 | 195, 198 | eqtrd 2772 |
. . . . . . . . . . 11
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π¦ β β) β (((π + 1) Β· (π¦β((π + 1) β 1))) / (!β(π + 1))) = ((π¦βπ) / (!βπ))) |
200 | 199 | mpteq2dva 5247 |
. . . . . . . . . 10
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (π¦ β β β¦ (((π + 1) Β· (π¦β((π + 1) β 1))) / (!β(π + 1)))) = (π¦ β β β¦ ((π¦βπ) / (!βπ)))) |
201 | 182, 200 | eqtrd 2772 |
. . . . . . . . 9
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π¦ β β β¦ ((π¦β(π + 1)) / (!β(π + 1))))) = (π¦ β β β¦ ((π¦βπ) / (!βπ)))) |
202 | | oveq1 7412 |
. . . . . . . . . 10
β’ (π¦ = (logβ(π΄ / π₯)) β (π¦β(π + 1)) = ((logβ(π΄ / π₯))β(π + 1))) |
203 | 202 | oveq1d 7420 |
. . . . . . . . 9
β’ (π¦ = (logβ(π΄ / π₯)) β ((π¦β(π + 1)) / (!β(π + 1))) = (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))) |
204 | | oveq1 7412 |
. . . . . . . . . 10
β’ (π¦ = (logβ(π΄ / π₯)) β (π¦βπ) = ((logβ(π΄ / π₯))βπ)) |
205 | 204 | oveq1d 7420 |
. . . . . . . . 9
β’ (π¦ = (logβ(π΄ / π₯)) β ((π¦βπ) / (!βπ)) = (((logβ(π΄ / π₯))βπ) / (!βπ))) |
206 | 111, 119,
120, 122, 133, 142, 176, 201, 203, 205 | dvmptco 25480 |
. . . . . . . 8
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π₯ β β+ β¦
(((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))))) = (π₯ β β+ β¦
((((logβ(π΄ / π₯))βπ) / (!βπ)) Β· -(1 / π₯)))) |
207 | 107 | an32s 650 |
. . . . . . . . . . 11
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β
(((logβ(π΄ / π₯))βπ) / (!βπ)) β β) |
208 | 161 | rpcnd 13014 |
. . . . . . . . . . 11
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β (1 /
π₯) β
β) |
209 | 207, 208 | mulneg2d 11664 |
. . . . . . . . . 10
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β
((((logβ(π΄ / π₯))βπ) / (!βπ)) Β· -(1 / π₯)) = -((((logβ(π΄ / π₯))βπ) / (!βπ)) Β· (1 / π₯))) |
210 | | rpne0 12986 |
. . . . . . . . . . . . 13
β’ (π₯ β β+
β π₯ β
0) |
211 | 210 | adantl 482 |
. . . . . . . . . . . 12
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β π₯ β 0) |
212 | 207, 112,
211 | divrecd 11989 |
. . . . . . . . . . 11
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β
((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) = ((((logβ(π΄ / π₯))βπ) / (!βπ)) Β· (1 / π₯))) |
213 | 212 | negeqd 11450 |
. . . . . . . . . 10
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β
-((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) = -((((logβ(π΄ / π₯))βπ) / (!βπ)) Β· (1 / π₯))) |
214 | 209, 213 | eqtr4d 2775 |
. . . . . . . . 9
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β
((((logβ(π΄ / π₯))βπ) / (!βπ)) Β· -(1 / π₯)) = -((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯)) |
215 | 214 | mpteq2dva 5247 |
. . . . . . . 8
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (π₯ β β+ β¦
((((logβ(π΄ / π₯))βπ) / (!βπ)) Β· -(1 / π₯))) = (π₯ β β+ β¦
-((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯))) |
216 | 206, 215 | eqtrd 2772 |
. . . . . . 7
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π₯ β β+ β¦
(((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))))) = (π₯ β β+ β¦
-((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯))) |
217 | 111, 112,
113, 114, 115, 117, 216 | dvmptmul 25469 |
. . . . . 6
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π₯ β β+ β¦ (π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))))) = (π₯ β β+ β¦ ((1
Β· (((logβ(π΄ /
π₯))β(π + 1)) / (!β(π + 1)))) +
(-((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) Β· π₯)))) |
218 | 88 | mullidd 11228 |
. . . . . . . . . 10
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β (1 Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))) = (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))) |
219 | | simplr 767 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β π₯ β β+) |
220 | 106, 219 | rerpdivcld 13043 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β ((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) β β) |
221 | 220 | recnd 11238 |
. . . . . . . . . . . 12
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β ((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) β β) |
222 | 221, 79 | mulneg1d 11663 |
. . . . . . . . . . 11
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β (-((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) Β· π₯) = -(((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) Β· π₯)) |
223 | 211 | an32s 650 |
. . . . . . . . . . . . 13
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β π₯ β 0) |
224 | 107, 79, 223 | divcan1d 11987 |
. . . . . . . . . . . 12
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β (((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) Β· π₯) = (((logβ(π΄ / π₯))βπ) / (!βπ))) |
225 | 224 | negeqd 11450 |
. . . . . . . . . . 11
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β -(((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) Β· π₯) = -(((logβ(π΄ / π₯))βπ) / (!βπ))) |
226 | 222, 225 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β (-((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) Β· π₯) = -(((logβ(π΄ / π₯))βπ) / (!βπ))) |
227 | 218, 226 | oveq12d 7423 |
. . . . . . . . 9
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β ((1 Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))) + (-((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) Β· π₯)) = ((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) + -(((logβ(π΄ / π₯))βπ) / (!βπ)))) |
228 | 88, 107 | negsubd 11573 |
. . . . . . . . 9
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β ((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) + -(((logβ(π΄ / π₯))βπ) / (!βπ))) = ((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β (((logβ(π΄ / π₯))βπ) / (!βπ)))) |
229 | 227, 228 | eqtrd 2772 |
. . . . . . . 8
β’ ((((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β§ π β (0..^π)) β ((1 Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))) + (-((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) Β· π₯)) = ((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β (((logβ(π΄ / π₯))βπ) / (!βπ)))) |
230 | 229 | an32s 650 |
. . . . . . 7
β’ ((((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β§ π₯ β β+) β ((1
Β· (((logβ(π΄ /
π₯))β(π + 1)) / (!β(π + 1)))) +
(-((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) Β· π₯)) = ((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β (((logβ(π΄ / π₯))βπ) / (!βπ)))) |
231 | 230 | mpteq2dva 5247 |
. . . . . 6
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (π₯ β β+ β¦ ((1
Β· (((logβ(π΄ /
π₯))β(π + 1)) / (!β(π + 1)))) +
(-((((logβ(π΄ / π₯))βπ) / (!βπ)) / π₯) Β· π₯))) = (π₯ β β+ β¦
((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β (((logβ(π΄ / π₯))βπ) / (!βπ))))) |
232 | 217, 231 | eqtrd 2772 |
. . . . 5
β’ (((π΄ β β+
β§ π β
β0) β§ π β (0..^π)) β (β D (π₯ β β+ β¦ (π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))))) = (π₯ β β+ β¦
((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β (((logβ(π΄ / π₯))βπ) / (!βπ))))) |
233 | 71, 70, 62, 75, 99, 101, 110, 232 | dvmptfsum 25483 |
. . . 4
β’ ((π΄ β β+
β§ π β
β0) β (β D (π₯ β β+ β¦
Ξ£π β (0..^π)(π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))))) = (π₯ β β+ β¦
Ξ£π β (0..^π)((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β (((logβ(π΄ / π₯))βπ) / (!βπ))))) |
234 | | oveq2 7413 |
. . . . . . . 8
β’ (π = π β ((logβ(π΄ / π₯))βπ) = ((logβ(π΄ / π₯))βπ)) |
235 | | fveq2 6888 |
. . . . . . . 8
β’ (π = π β (!βπ) = (!βπ)) |
236 | 234, 235 | oveq12d 7423 |
. . . . . . 7
β’ (π = π β (((logβ(π΄ / π₯))βπ) / (!βπ)) = (((logβ(π΄ / π₯))βπ) / (!βπ))) |
237 | | oveq2 7413 |
. . . . . . . 8
β’ (π = π β ((logβ(π΄ / π₯))βπ) = ((logβ(π΄ / π₯))βπ)) |
238 | | fveq2 6888 |
. . . . . . . 8
β’ (π = π β (!βπ) = (!βπ)) |
239 | 237, 238 | oveq12d 7423 |
. . . . . . 7
β’ (π = π β (((logβ(π΄ / π₯))βπ) / (!βπ)) = (((logβ(π΄ / π₯))βπ) / (!βπ))) |
240 | 236, 43, 24, 239, 17, 13 | telfsumo2 15745 |
. . . . . 6
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
Ξ£π β (0..^π)((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β (((logβ(π΄ / π₯))βπ) / (!βπ))) = ((((logβ(π΄ / π₯))βπ) / (!βπ)) β (((logβ(π΄ / π₯))β0) / 1))) |
241 | 31 | oveq2d 7421 |
. . . . . 6
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
((((logβ(π΄ / π₯))βπ) / (!βπ)) β (((logβ(π΄ / π₯))β0) / 1)) = ((((logβ(π΄ / π₯))βπ) / (!βπ)) β 1)) |
242 | 240, 241 | eqtrd 2772 |
. . . . 5
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β
Ξ£π β (0..^π)((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β (((logβ(π΄ / π₯))βπ) / (!βπ))) = ((((logβ(π΄ / π₯))βπ) / (!βπ)) β 1)) |
243 | 242 | mpteq2dva 5247 |
. . . 4
β’ ((π΄ β β+
β§ π β
β0) β (π₯ β β+ β¦
Ξ£π β (0..^π)((((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))) β (((logβ(π΄ / π₯))βπ) / (!βπ)))) = (π₯ β β+ β¦
((((logβ(π΄ / π₯))βπ) / (!βπ)) β 1))) |
244 | 233, 243 | eqtrd 2772 |
. . 3
β’ ((π΄ β β+
β§ π β
β0) β (β D (π₯ β β+ β¦
Ξ£π β (0..^π)(π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1)))))) = (π₯ β β+ β¦
((((logβ(π΄ / π₯))βπ) / (!βπ)) β 1))) |
245 | 62, 3, 63, 76, 90, 98, 244 | dvmptadd 25468 |
. 2
β’ ((π΄ β β+
β§ π β
β0) β (β D (π₯ β β+ β¦ (π₯ + Ξ£π β (0..^π)(π₯ Β· (((logβ(π΄ / π₯))β(π + 1)) / (!β(π + 1))))))) = (π₯ β β+ β¦ (1 +
((((logβ(π΄ / π₯))βπ) / (!βπ)) β 1)))) |
246 | | pncan3 11464 |
. . . 4
β’ ((1
β β β§ (((logβ(π΄ / π₯))βπ) / (!βπ)) β β) β (1 +
((((logβ(π΄ / π₯))βπ) / (!βπ)) β 1)) = (((logβ(π΄ / π₯))βπ) / (!βπ))) |
247 | 96, 95, 246 | sylancr 587 |
. . 3
β’ (((π΄ β β+
β§ π β
β0) β§ π₯ β β+) β (1 +
((((logβ(π΄ / π₯))βπ) / (!βπ)) β 1)) = (((logβ(π΄ / π₯))βπ) / (!βπ))) |
248 | 247 | mpteq2dva 5247 |
. 2
β’ ((π΄ β β+
β§ π β
β0) β (π₯ β β+ β¦ (1 +
((((logβ(π΄ / π₯))βπ) / (!βπ)) β 1))) = (π₯ β β+ β¦
(((logβ(π΄ / π₯))βπ) / (!βπ)))) |
249 | 60, 245, 248 | 3eqtrd 2776 |
1
β’ ((π΄ β β+
β§ π β
β0) β (β D (π₯ β β+ β¦ (π₯ Β· Ξ£π β (0...π)(((logβ(π΄ / π₯))βπ) / (!βπ))))) = (π₯ β β+ β¦
(((logβ(π΄ / π₯))βπ) / (!βπ)))) |