Step | Hyp | Ref
| Expression |
1 | | etransclem22.s |
. . 3
β’ (π β π β {β, β}) |
2 | | etransclem22.x |
. . 3
β’ (π β π β
((TopOpenββfld) βΎt π)) |
3 | | etransclem22.p |
. . 3
β’ (π β π β β) |
4 | | etransclem22.h |
. . 3
β’ π» = (π β (0...π) β¦ (π₯ β π β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) |
5 | | etransclem22.J |
. . 3
β’ (π β π½ β (0...π)) |
6 | | etransclem22.n |
. . 3
β’ (π β π β
β0) |
7 | 1, 2, 3, 4, 5, 6 | etransclem17 45562 |
. 2
β’ (π β ((π Dπ (π»βπ½))βπ) = (π₯ β π β¦ if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π)))))) |
8 | | simpr 484 |
. . . . . 6
β’ ((π β§ if(π½ = 0, (π β 1), π) < π) β if(π½ = 0, (π β 1), π) < π) |
9 | 8 | iftrued 4532 |
. . . . 5
β’ ((π β§ if(π½ = 0, (π β 1), π) < π) β if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π)))) = 0) |
10 | 9 | mpteq2dv 5244 |
. . . 4
β’ ((π β§ if(π½ = 0, (π β 1), π) < π) β (π₯ β π β¦ if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π))))) = (π₯ β π β¦ 0)) |
11 | 1, 2 | dvdmsscn 45247 |
. . . . . 6
β’ (π β π β β) |
12 | | 0cnd 11229 |
. . . . . 6
β’ (π β 0 β
β) |
13 | | ssid 4000 |
. . . . . . 7
β’ β
β β |
14 | 13 | a1i 11 |
. . . . . 6
β’ (π β β β
β) |
15 | 11, 12, 14 | constcncfg 45183 |
. . . . 5
β’ (π β (π₯ β π β¦ 0) β (πβcnββ)) |
16 | 15 | adantr 480 |
. . . 4
β’ ((π β§ if(π½ = 0, (π β 1), π) < π) β (π₯ β π β¦ 0) β (πβcnββ)) |
17 | 10, 16 | eqeltrd 2828 |
. . 3
β’ ((π β§ if(π½ = 0, (π β 1), π) < π) β (π₯ β π β¦ if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π))))) β (πβcnββ)) |
18 | | simpr 484 |
. . . . . 6
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β Β¬ if(π½ = 0, (π β 1), π) < π) |
19 | 18 | iffalsed 4535 |
. . . . 5
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π)))) = (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π)))) |
20 | 19 | mpteq2dv 5244 |
. . . 4
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (π₯ β π β¦ if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π))))) = (π₯ β π β¦ (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π))))) |
21 | | nfv 1910 |
. . . . 5
β’
β²π₯(π β§ Β¬ if(π½ = 0, (π β 1), π) < π) |
22 | 11, 14 | idcncfg 45184 |
. . . . . . 7
β’ (π β (π₯ β π β¦ π₯) β (πβcnββ)) |
23 | 5 | elfzelzd 13526 |
. . . . . . . . 9
β’ (π β π½ β β€) |
24 | 23 | zcnd 12689 |
. . . . . . . 8
β’ (π β π½ β β) |
25 | 11, 24, 14 | constcncfg 45183 |
. . . . . . 7
β’ (π β (π₯ β π β¦ π½) β (πβcnββ)) |
26 | 22, 25 | subcncf 25360 |
. . . . . 6
β’ (π β (π₯ β π β¦ (π₯ β π½)) β (πβcnββ)) |
27 | 26 | adantr 480 |
. . . . 5
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (π₯ β π β¦ (π₯ β π½)) β (πβcnββ)) |
28 | 13 | a1i 11 |
. . . . . . 7
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β β β
β) |
29 | | nnm1nn0 12535 |
. . . . . . . . . . . . 13
β’ (π β β β (π β 1) β
β0) |
30 | 3, 29 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π β 1) β
β0) |
31 | 3 | nnnn0d 12554 |
. . . . . . . . . . . 12
β’ (π β π β
β0) |
32 | 30, 31 | ifcld 4570 |
. . . . . . . . . . 11
β’ (π β if(π½ = 0, (π β 1), π) β
β0) |
33 | 32 | faccld 14267 |
. . . . . . . . . 10
β’ (π β (!βif(π½ = 0, (π β 1), π)) β β) |
34 | 33 | nncnd 12250 |
. . . . . . . . 9
β’ (π β (!βif(π½ = 0, (π β 1), π)) β β) |
35 | 34 | adantr 480 |
. . . . . . . 8
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (!βif(π½ = 0, (π β 1), π)) β β) |
36 | 32 | nn0zd 12606 |
. . . . . . . . . . . . 13
β’ (π β if(π½ = 0, (π β 1), π) β β€) |
37 | 6 | nn0zd 12606 |
. . . . . . . . . . . . 13
β’ (π β π β β€) |
38 | 36, 37 | zsubcld 12693 |
. . . . . . . . . . . 12
β’ (π β (if(π½ = 0, (π β 1), π) β π) β β€) |
39 | 38 | adantr 480 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (if(π½ = 0, (π β 1), π) β π) β β€) |
40 | 6 | nn0red 12555 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β π β β) |
42 | 32 | nn0red 12555 |
. . . . . . . . . . . . . 14
β’ (π β if(π½ = 0, (π β 1), π) β β) |
43 | 42 | adantr 480 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β if(π½ = 0, (π β 1), π) β β) |
44 | 41, 43, 18 | nltled 11386 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β π β€ if(π½ = 0, (π β 1), π)) |
45 | 43, 41 | subge0d 11826 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (0 β€ (if(π½ = 0, (π β 1), π) β π) β π β€ if(π½ = 0, (π β 1), π))) |
46 | 44, 45 | mpbird 257 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β 0 β€ (if(π½ = 0, (π β 1), π) β π)) |
47 | | elnn0z 12593 |
. . . . . . . . . . 11
β’
((if(π½ = 0, (π β 1), π) β π) β β0 β
((if(π½ = 0, (π β 1), π) β π) β β€ β§ 0 β€ (if(π½ = 0, (π β 1), π) β π))) |
48 | 39, 46, 47 | sylanbrc 582 |
. . . . . . . . . 10
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (if(π½ = 0, (π β 1), π) β π) β
β0) |
49 | 48 | faccld 14267 |
. . . . . . . . 9
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (!β(if(π½ = 0, (π β 1), π) β π)) β β) |
50 | 49 | nncnd 12250 |
. . . . . . . 8
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (!β(if(π½ = 0, (π β 1), π) β π)) β β) |
51 | 49 | nnne0d 12284 |
. . . . . . . 8
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (!β(if(π½ = 0, (π β 1), π) β π)) β 0) |
52 | 35, 50, 51 | divcld 12012 |
. . . . . . 7
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β ((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) β β) |
53 | 28, 52, 28 | constcncfg 45183 |
. . . . . 6
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (π¦ β β β¦ ((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π)))) β (ββcnββ)) |
54 | | expcncf 24834 |
. . . . . . 7
β’
((if(π½ = 0, (π β 1), π) β π) β β0 β (π¦ β β β¦ (π¦β(if(π½ = 0, (π β 1), π) β π))) β (ββcnββ)) |
55 | 48, 54 | syl 17 |
. . . . . 6
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (π¦ β β β¦ (π¦β(if(π½ = 0, (π β 1), π) β π))) β (ββcnββ)) |
56 | 53, 55 | mulcncf 25361 |
. . . . 5
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (π¦ β β β¦ (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· (π¦β(if(π½ = 0, (π β 1), π) β π)))) β (ββcnββ)) |
57 | | oveq1 7421 |
. . . . . 6
β’ (π¦ = (π₯ β π½) β (π¦β(if(π½ = 0, (π β 1), π) β π)) = ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π))) |
58 | 57 | oveq2d 7430 |
. . . . 5
β’ (π¦ = (π₯ β π½) β (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· (π¦β(if(π½ = 0, (π β 1), π) β π))) = (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π)))) |
59 | 21, 27, 56, 28, 58 | cncfcompt2 24815 |
. . . 4
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (π₯ β π β¦ (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π)))) β (πβcnββ)) |
60 | 20, 59 | eqeltrd 2828 |
. . 3
β’ ((π β§ Β¬ if(π½ = 0, (π β 1), π) < π) β (π₯ β π β¦ if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π))))) β (πβcnββ)) |
61 | 17, 60 | pm2.61dan 812 |
. 2
β’ (π β (π₯ β π β¦ if(if(π½ = 0, (π β 1), π) < π, 0, (((!βif(π½ = 0, (π β 1), π)) / (!β(if(π½ = 0, (π β 1), π) β π))) Β· ((π₯ β π½)β(if(π½ = 0, (π β 1), π) β π))))) β (πβcnββ)) |
62 | 7, 61 | eqeltrd 2828 |
1
β’ (π β ((π Dπ (π»βπ½))βπ) β (πβcnββ)) |