Step | Hyp | Ref
| Expression |
1 | | etransclem27.g |
. . 3
β’ πΊ = (π₯ β π β¦ Ξ£π β dom πΆβπ β (0...π)(((π Dπ (π»βπ))β((πΆβπ)βπ))βπ₯)) |
2 | | fveq2 6891 |
. . . . 5
β’ (π₯ = π½ β (((π Dπ (π»βπ))β((πΆβπ)βπ))βπ₯) = (((π Dπ (π»βπ))β((πΆβπ)βπ))βπ½)) |
3 | 2 | prodeq2ad 44393 |
. . . 4
β’ (π₯ = π½ β βπ β (0...π)(((π Dπ (π»βπ))β((πΆβπ)βπ))βπ₯) = βπ β (0...π)(((π Dπ (π»βπ))β((πΆβπ)βπ))βπ½)) |
4 | 3 | sumeq2sdv 15652 |
. . 3
β’ (π₯ = π½ β Ξ£π β dom πΆβπ β (0...π)(((π Dπ (π»βπ))β((πΆβπ)βπ))βπ₯) = Ξ£π β dom πΆβπ β (0...π)(((π Dπ (π»βπ))β((πΆβπ)βπ))βπ½)) |
5 | | etransclem27.jx |
. . 3
β’ (π β π½ β π) |
6 | | etransclem27.cfi |
. . . . 5
β’ (π β πΆ β Fin) |
7 | | dmfi 9332 |
. . . . 5
β’ (πΆ β Fin β dom πΆ β Fin) |
8 | 6, 7 | syl 17 |
. . . 4
β’ (π β dom πΆ β Fin) |
9 | | fzfid 13940 |
. . . . 5
β’ ((π β§ π β dom πΆ) β (0...π) β Fin) |
10 | | etransclem27.s |
. . . . . . . 8
β’ (π β π β {β, β}) |
11 | 10 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β π β {β, β}) |
12 | | etransclem27.x |
. . . . . . . 8
β’ (π β π β
((TopOpenββfld) βΎt π)) |
13 | 12 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β π β
((TopOpenββfld) βΎt π)) |
14 | | etransclem27.p |
. . . . . . . 8
β’ (π β π β β) |
15 | 14 | ad2antrr 724 |
. . . . . . 7
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β π β β) |
16 | | etransclem27.h |
. . . . . . . 8
β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) |
17 | | etransclem5 45040 |
. . . . . . . 8
β’ (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) = (π§ β (0...π) β¦ (π¦ β π β¦ ((π¦ β π§)βif(π§ = 0, (π β 1), π)))) |
18 | 16, 17 | eqtri 2760 |
. . . . . . 7
β’ π» = (π§ β (0...π) β¦ (π¦ β π β¦ ((π¦ β π§)βif(π§ = 0, (π β 1), π)))) |
19 | | simpr 485 |
. . . . . . 7
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β π β (0...π)) |
20 | | etransclem27.cf |
. . . . . . . . . 10
β’ (π β πΆ:dom πΆβΆ(β0
βm (0...π))) |
21 | 20 | ffvelcdmda 7086 |
. . . . . . . . 9
β’ ((π β§ π β dom πΆ) β (πΆβπ) β (β0
βm (0...π))) |
22 | | elmapi 8845 |
. . . . . . . . 9
β’ ((πΆβπ) β (β0
βm (0...π))
β (πΆβπ):(0...π)βΆβ0) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β dom πΆ) β (πΆβπ):(0...π)βΆβ0) |
24 | 23 | ffvelcdmda 7086 |
. . . . . . 7
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β ((πΆβπ)βπ) β
β0) |
25 | 11, 13, 15, 18, 19, 24 | etransclem20 45055 |
. . . . . 6
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β ((π Dπ (π»βπ))β((πΆβπ)βπ)):πβΆβ) |
26 | 5 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β π½ β π) |
27 | 25, 26 | ffvelcdmd 7087 |
. . . . 5
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β (((π Dπ (π»βπ))β((πΆβπ)βπ))βπ½) β β) |
28 | 9, 27 | fprodcl 15898 |
. . . 4
β’ ((π β§ π β dom πΆ) β βπ β (0...π)(((π Dπ (π»βπ))β((πΆβπ)βπ))βπ½) β β) |
29 | 8, 28 | fsumcl 15681 |
. . 3
β’ (π β Ξ£π β dom πΆβπ β (0...π)(((π Dπ (π»βπ))β((πΆβπ)βπ))βπ½) β β) |
30 | 1, 4, 5, 29 | fvmptd3 7021 |
. 2
β’ (π β (πΊβπ½) = Ξ£π β dom πΆβπ β (0...π)(((π Dπ (π»βπ))β((πΆβπ)βπ))βπ½)) |
31 | 11, 13, 15, 18, 19, 24, 26 | etransclem21 45056 |
. . . . 5
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β (((π Dπ (π»βπ))β((πΆβπ)βπ))βπ½) = if(if(π = 0, (π β 1), π) < ((πΆβπ)βπ), 0, (((!βif(π = 0, (π β 1), π)) / (!β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ)))) Β· ((π½ β π)β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ)))))) |
32 | | iftrue 4534 |
. . . . . . . 8
β’ (if(π = 0, (π β 1), π) < ((πΆβπ)βπ) β if(if(π = 0, (π β 1), π) < ((πΆβπ)βπ), 0, (((!βif(π = 0, (π β 1), π)) / (!β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ)))) Β· ((π½ β π)β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ))))) = 0) |
33 | | 0zd 12572 |
. . . . . . . 8
β’ (if(π = 0, (π β 1), π) < ((πΆβπ)βπ) β 0 β β€) |
34 | 32, 33 | eqeltrd 2833 |
. . . . . . 7
β’ (if(π = 0, (π β 1), π) < ((πΆβπ)βπ) β if(if(π = 0, (π β 1), π) < ((πΆβπ)βπ), 0, (((!βif(π = 0, (π β 1), π)) / (!β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ)))) Β· ((π½ β π)β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ))))) β β€) |
35 | 34 | adantl 482 |
. . . . . 6
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β if(if(π = 0, (π β 1), π) < ((πΆβπ)βπ), 0, (((!βif(π = 0, (π β 1), π)) / (!β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ)))) Β· ((π½ β π)β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ))))) β β€) |
36 | | 0zd 12572 |
. . . . . . 7
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β 0 β β€) |
37 | | nnm1nn0 12515 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π β 1) β
β0) |
38 | 14, 37 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π β 1) β
β0) |
39 | 14 | nnnn0d 12534 |
. . . . . . . . . . . . . 14
β’ (π β π β
β0) |
40 | 38, 39 | ifcld 4574 |
. . . . . . . . . . . . 13
β’ (π β if(π = 0, (π β 1), π) β
β0) |
41 | 40 | nn0zd 12586 |
. . . . . . . . . . . 12
β’ (π β if(π = 0, (π β 1), π) β β€) |
42 | 41 | ad3antrrr 728 |
. . . . . . . . . . 11
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β if(π = 0, (π β 1), π) β β€) |
43 | 24 | nn0zd 12586 |
. . . . . . . . . . . . 13
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β ((πΆβπ)βπ) β β€) |
44 | 43 | adantr 481 |
. . . . . . . . . . . 12
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β ((πΆβπ)βπ) β β€) |
45 | 42, 44 | zsubcld 12673 |
. . . . . . . . . . 11
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β (if(π = 0, (π β 1), π) β ((πΆβπ)βπ)) β β€) |
46 | 44 | zred 12668 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β ((πΆβπ)βπ) β β) |
47 | 42 | zred 12668 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β if(π = 0, (π β 1), π) β β) |
48 | | simpr 485 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) |
49 | 46, 47, 48 | nltled 11366 |
. . . . . . . . . . . 12
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β ((πΆβπ)βπ) β€ if(π = 0, (π β 1), π)) |
50 | 47, 46 | subge0d 11806 |
. . . . . . . . . . . 12
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β (0 β€ (if(π = 0, (π β 1), π) β ((πΆβπ)βπ)) β ((πΆβπ)βπ) β€ if(π = 0, (π β 1), π))) |
51 | 49, 50 | mpbird 256 |
. . . . . . . . . . 11
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β 0 β€ (if(π = 0, (π β 1), π) β ((πΆβπ)βπ))) |
52 | | 0red 11219 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β 0 β β) |
53 | 24 | nn0red 12535 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β ((πΆβπ)βπ) β β) |
54 | 40 | nn0red 12535 |
. . . . . . . . . . . . . . 15
β’ (π β if(π = 0, (π β 1), π) β β) |
55 | 54 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β if(π = 0, (π β 1), π) β β) |
56 | 24 | nn0ge0d 12537 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β 0 β€ ((πΆβπ)βπ)) |
57 | 52, 53, 55, 56 | lesub2dd 11833 |
. . . . . . . . . . . . 13
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β (if(π = 0, (π β 1), π) β ((πΆβπ)βπ)) β€ (if(π = 0, (π β 1), π) β 0)) |
58 | 55 | recnd 11244 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β if(π = 0, (π β 1), π) β β) |
59 | 58 | subid1d 11562 |
. . . . . . . . . . . . 13
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β (if(π = 0, (π β 1), π) β 0) = if(π = 0, (π β 1), π)) |
60 | 57, 59 | breqtrd 5174 |
. . . . . . . . . . . 12
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β (if(π = 0, (π β 1), π) β ((πΆβπ)βπ)) β€ if(π = 0, (π β 1), π)) |
61 | 60 | adantr 481 |
. . . . . . . . . . 11
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β (if(π = 0, (π β 1), π) β ((πΆβπ)βπ)) β€ if(π = 0, (π β 1), π)) |
62 | 36, 42, 45, 51, 61 | elfzd 13494 |
. . . . . . . . . 10
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β (if(π = 0, (π β 1), π) β ((πΆβπ)βπ)) β (0...if(π = 0, (π β 1), π))) |
63 | | permnn 14288 |
. . . . . . . . . 10
β’
((if(π = 0, (π β 1), π) β ((πΆβπ)βπ)) β (0...if(π = 0, (π β 1), π)) β ((!βif(π = 0, (π β 1), π)) / (!β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ)))) β β) |
64 | 62, 63 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β ((!βif(π = 0, (π β 1), π)) / (!β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ)))) β β) |
65 | 64 | nnzd 12587 |
. . . . . . . 8
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β ((!βif(π = 0, (π β 1), π)) / (!β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ)))) β β€) |
66 | | etransclem27.jz |
. . . . . . . . . . 11
β’ (π β π½ β β€) |
67 | 66 | ad3antrrr 728 |
. . . . . . . . . 10
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β π½ β β€) |
68 | | elfzelz 13503 |
. . . . . . . . . . 11
β’ (π β (0...π) β π β β€) |
69 | 68 | ad2antlr 725 |
. . . . . . . . . 10
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β π β β€) |
70 | 67, 69 | zsubcld 12673 |
. . . . . . . . 9
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β (π½ β π) β β€) |
71 | | elnn0z 12573 |
. . . . . . . . . 10
β’
((if(π = 0, (π β 1), π) β ((πΆβπ)βπ)) β β0 β
((if(π = 0, (π β 1), π) β ((πΆβπ)βπ)) β β€ β§ 0 β€ (if(π = 0, (π β 1), π) β ((πΆβπ)βπ)))) |
72 | 45, 51, 71 | sylanbrc 583 |
. . . . . . . . 9
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β (if(π = 0, (π β 1), π) β ((πΆβπ)βπ)) β
β0) |
73 | | zexpcl 14044 |
. . . . . . . . 9
β’ (((π½ β π) β β€ β§ (if(π = 0, (π β 1), π) β ((πΆβπ)βπ)) β β0) β ((π½ β π)β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ))) β β€) |
74 | 70, 72, 73 | syl2anc 584 |
. . . . . . . 8
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β ((π½ β π)β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ))) β β€) |
75 | 65, 74 | zmulcld 12674 |
. . . . . . 7
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β (((!βif(π = 0, (π β 1), π)) / (!β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ)))) Β· ((π½ β π)β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ)))) β β€) |
76 | 36, 75 | ifcld 4574 |
. . . . . 6
β’ ((((π β§ π β dom πΆ) β§ π β (0...π)) β§ Β¬ if(π = 0, (π β 1), π) < ((πΆβπ)βπ)) β if(if(π = 0, (π β 1), π) < ((πΆβπ)βπ), 0, (((!βif(π = 0, (π β 1), π)) / (!β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ)))) Β· ((π½ β π)β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ))))) β β€) |
77 | 35, 76 | pm2.61dan 811 |
. . . . 5
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β if(if(π = 0, (π β 1), π) < ((πΆβπ)βπ), 0, (((!βif(π = 0, (π β 1), π)) / (!β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ)))) Β· ((π½ β π)β(if(π = 0, (π β 1), π) β ((πΆβπ)βπ))))) β β€) |
78 | 31, 77 | eqeltrd 2833 |
. . . 4
β’ (((π β§ π β dom πΆ) β§ π β (0...π)) β (((π Dπ (π»βπ))β((πΆβπ)βπ))βπ½) β β€) |
79 | 9, 78 | fprodzcl 15900 |
. . 3
β’ ((π β§ π β dom πΆ) β βπ β (0...π)(((π Dπ (π»βπ))β((πΆβπ)βπ))βπ½) β β€) |
80 | 8, 79 | fsumzcl 15683 |
. 2
β’ (π β Ξ£π β dom πΆβπ β (0...π)(((π Dπ (π»βπ))β((πΆβπ)βπ))βπ½) β β€) |
81 | 30, 80 | eqeltrd 2833 |
1
β’ (π β (πΊβπ½) β β€) |