Step | Hyp | Ref
| Expression |
1 | | etransclem44.k |
. . . 4
β’ πΎ = (Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1))) |
2 | 1 | a1i 11 |
. . 3
β’ (π β πΎ = (Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1)))) |
3 | | nfv 1918 |
. . . . 5
β’
β²ππ |
4 | | nfcv 2904 |
. . . . 5
β’
β²π((π΄β0) Β· (((β
Dπ πΉ)β(π β 1))β0)) |
5 | | fzfi 13933 |
. . . . . . 7
β’
(0...π) β
Fin |
6 | | fzfi 13933 |
. . . . . . 7
β’
(0...((π Β·
π) + (π β 1))) β Fin |
7 | | xpfi 9313 |
. . . . . . 7
β’
(((0...π) β Fin
β§ (0...((π Β·
π) + (π β 1))) β Fin) β ((0...π) Γ (0...((π Β· π) + (π β 1)))) β Fin) |
8 | 5, 6, 7 | mp2an 691 |
. . . . . 6
β’
((0...π) Γ
(0...((π Β· π) + (π β 1)))) β Fin |
9 | 8 | a1i 11 |
. . . . 5
β’ (π β ((0...π) Γ (0...((π Β· π) + (π β 1)))) β Fin) |
10 | | etransclem44.a |
. . . . . . . . 9
β’ (π β π΄:β0βΆβ€) |
11 | 10 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β π΄:β0βΆβ€) |
12 | | fzssnn0 43962 |
. . . . . . . . . 10
β’
(0...π) β
β0 |
13 | | xp1st 8002 |
. . . . . . . . . 10
β’ (π β ((0...π) Γ (0...((π Β· π) + (π β 1)))) β (1st
βπ) β (0...π)) |
14 | 12, 13 | sselid 3979 |
. . . . . . . . 9
β’ (π β ((0...π) Γ (0...((π Β· π) + (π β 1)))) β (1st
βπ) β
β0) |
15 | 14 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β (1st
βπ) β
β0) |
16 | 11, 15 | ffvelcdmd 7083 |
. . . . . . 7
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β (π΄β(1st βπ)) β
β€) |
17 | | reelprrecn 11198 |
. . . . . . . . 9
β’ β
β {β, β} |
18 | 17 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β β β
{β, β}) |
19 | | reopn 43934 |
. . . . . . . . . 10
β’ β
β (topGenβran (,)) |
20 | | eqid 2733 |
. . . . . . . . . . 11
β’
(TopOpenββfld) =
(TopOpenββfld) |
21 | 20 | tgioo2 24301 |
. . . . . . . . . 10
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
22 | 19, 21 | eleqtri 2832 |
. . . . . . . . 9
β’ β
β ((TopOpenββfld) βΎt
β) |
23 | 22 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β β β
((TopOpenββfld) βΎt
β)) |
24 | | etransclem44.p |
. . . . . . . . . 10
β’ (π β π β β) |
25 | | prmnn 16607 |
. . . . . . . . . 10
β’ (π β β β π β
β) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
β’ (π β π β β) |
27 | 26 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β π β β) |
28 | | etransclem44.m |
. . . . . . . . 9
β’ (π β π β
β0) |
29 | 28 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β π β
β0) |
30 | | etransclem44.f |
. . . . . . . 8
β’ πΉ = (π₯ β β β¦ ((π₯β(π β 1)) Β· βπ β (1...π)((π₯ β π)βπ))) |
31 | | xp2nd 8003 |
. . . . . . . . . 10
β’ (π β ((0...π) Γ (0...((π Β· π) + (π β 1)))) β (2nd
βπ) β
(0...((π Β· π) + (π β 1)))) |
32 | | elfznn0 13590 |
. . . . . . . . . 10
β’
((2nd βπ) β (0...((π Β· π) + (π β 1))) β (2nd
βπ) β
β0) |
33 | 31, 32 | syl 17 |
. . . . . . . . 9
β’ (π β ((0...π) Γ (0...((π Β· π) + (π β 1)))) β (2nd
βπ) β
β0) |
34 | 33 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β (2nd
βπ) β
β0) |
35 | 15 | nn0red 12529 |
. . . . . . . 8
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β (1st
βπ) β
β) |
36 | 15 | nn0zd 12580 |
. . . . . . . 8
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β (1st
βπ) β
β€) |
37 | 18, 23, 27, 29, 30, 34, 35, 36 | etransclem42 44927 |
. . . . . . 7
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ)) β
β€) |
38 | 16, 37 | zmulcld 12668 |
. . . . . 6
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β ((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) β
β€) |
39 | 38 | zcnd 12663 |
. . . . 5
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β ((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) β
β) |
40 | | nn0uz 12860 |
. . . . . . . 8
β’
β0 = (β€β₯β0) |
41 | 28, 40 | eleqtrdi 2844 |
. . . . . . 7
β’ (π β π β
(β€β₯β0)) |
42 | | eluzfz1 13504 |
. . . . . . 7
β’ (π β
(β€β₯β0) β 0 β (0...π)) |
43 | 41, 42 | syl 17 |
. . . . . 6
β’ (π β 0 β (0...π)) |
44 | | 0zd 12566 |
. . . . . . 7
β’ (π β 0 β
β€) |
45 | 28 | nn0zd 12580 |
. . . . . . . . 9
β’ (π β π β β€) |
46 | 26 | nnzd 12581 |
. . . . . . . . 9
β’ (π β π β β€) |
47 | 45, 46 | zmulcld 12668 |
. . . . . . . 8
β’ (π β (π Β· π) β β€) |
48 | | nnm1nn0 12509 |
. . . . . . . . . 10
β’ (π β β β (π β 1) β
β0) |
49 | 26, 48 | syl 17 |
. . . . . . . . 9
β’ (π β (π β 1) β
β0) |
50 | 49 | nn0zd 12580 |
. . . . . . . 8
β’ (π β (π β 1) β β€) |
51 | 47, 50 | zaddcld 12666 |
. . . . . . 7
β’ (π β ((π Β· π) + (π β 1)) β
β€) |
52 | 49 | nn0ge0d 12531 |
. . . . . . 7
β’ (π β 0 β€ (π β 1)) |
53 | 26 | nnnn0d 12528 |
. . . . . . . . . 10
β’ (π β π β
β0) |
54 | 28, 53 | nn0mulcld 12533 |
. . . . . . . . 9
β’ (π β (π Β· π) β
β0) |
55 | 54 | nn0ge0d 12531 |
. . . . . . . 8
β’ (π β 0 β€ (π Β· π)) |
56 | 49 | nn0red 12529 |
. . . . . . . . 9
β’ (π β (π β 1) β β) |
57 | 47 | zred 12662 |
. . . . . . . . 9
β’ (π β (π Β· π) β β) |
58 | 56, 57 | addge02d 11799 |
. . . . . . . 8
β’ (π β (0 β€ (π Β· π) β (π β 1) β€ ((π Β· π) + (π β 1)))) |
59 | 55, 58 | mpbid 231 |
. . . . . . 7
β’ (π β (π β 1) β€ ((π Β· π) + (π β 1))) |
60 | 44, 51, 50, 52, 59 | elfzd 13488 |
. . . . . 6
β’ (π β (π β 1) β (0...((π Β· π) + (π β 1)))) |
61 | | opelxp 5711 |
. . . . . 6
β’ (β¨0,
(π β 1)β© β
((0...π) Γ
(0...((π Β· π) + (π β 1)))) β (0 β (0...π) β§ (π β 1) β (0...((π Β· π) + (π β 1))))) |
62 | 43, 60, 61 | sylanbrc 584 |
. . . . 5
β’ (π β β¨0, (π β 1)β© β
((0...π) Γ
(0...((π Β· π) + (π β 1))))) |
63 | | fveq2 6888 |
. . . . . . . 8
β’ (π = β¨0, (π β 1)β© β (1st
βπ) = (1st
ββ¨0, (π β
1)β©)) |
64 | | 0re 11212 |
. . . . . . . . 9
β’ 0 β
β |
65 | | ovex 7437 |
. . . . . . . . 9
β’ (π β 1) β
V |
66 | | op1stg 7982 |
. . . . . . . . 9
β’ ((0
β β β§ (π
β 1) β V) β (1st ββ¨0, (π β 1)β©) = 0) |
67 | 64, 65, 66 | mp2an 691 |
. . . . . . . 8
β’
(1st ββ¨0, (π β 1)β©) = 0 |
68 | 63, 67 | eqtrdi 2789 |
. . . . . . 7
β’ (π = β¨0, (π β 1)β© β (1st
βπ) =
0) |
69 | 68 | fveq2d 6892 |
. . . . . 6
β’ (π = β¨0, (π β 1)β© β (π΄β(1st βπ)) = (π΄β0)) |
70 | | fveq2 6888 |
. . . . . . . . 9
β’ (π = β¨0, (π β 1)β© β (2nd
βπ) = (2nd
ββ¨0, (π β
1)β©)) |
71 | | op2ndg 7983 |
. . . . . . . . . 10
β’ ((0
β β β§ (π
β 1) β V) β (2nd ββ¨0, (π β 1)β©) = (π β 1)) |
72 | 64, 65, 71 | mp2an 691 |
. . . . . . . . 9
β’
(2nd ββ¨0, (π β 1)β©) = (π β 1) |
73 | 70, 72 | eqtrdi 2789 |
. . . . . . . 8
β’ (π = β¨0, (π β 1)β© β (2nd
βπ) = (π β 1)) |
74 | 73 | fveq2d 6892 |
. . . . . . 7
β’ (π = β¨0, (π β 1)β© β ((β
Dπ πΉ)β(2nd βπ)) = ((β
Dπ πΉ)β(π β 1))) |
75 | 74, 68 | fveq12d 6895 |
. . . . . 6
β’ (π = β¨0, (π β 1)β© β (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ)) = (((β
Dπ πΉ)β(π β 1))β0)) |
76 | 69, 75 | oveq12d 7422 |
. . . . 5
β’ (π = β¨0, (π β 1)β© β ((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) = ((π΄β0) Β· (((β
Dπ πΉ)β(π β 1))β0))) |
77 | 3, 4, 9, 39, 62, 76 | fsumsplit1 15687 |
. . . 4
β’ (π β Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) = (((π΄β0) Β· (((β
Dπ πΉ)β(π β 1))β0)) + Ξ£π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))))) |
78 | 77 | oveq1d 7419 |
. . 3
β’ (π β (Ξ£π β ((0...π) Γ (0...((π Β· π) + (π β 1))))((π΄β(1st βπ)) Β· (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1))) =
((((π΄β0) Β·
(((β Dπ πΉ)β(π β 1))β0)) + Ξ£π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ)))) /
(!β(π β
1)))) |
79 | 12, 43 | sselid 3979 |
. . . . . . 7
β’ (π β 0 β
β0) |
80 | 10, 79 | ffvelcdmd 7083 |
. . . . . 6
β’ (π β (π΄β0) β β€) |
81 | 17 | a1i 11 |
. . . . . . 7
β’ (π β β β {β,
β}) |
82 | 22 | a1i 11 |
. . . . . . 7
β’ (π β β β
((TopOpenββfld) βΎt
β)) |
83 | 64 | a1i 11 |
. . . . . . 7
β’ (π β 0 β
β) |
84 | 81, 82, 26, 28, 30, 49, 83, 44 | etransclem42 44927 |
. . . . . 6
β’ (π β (((β
Dπ πΉ)β(π β 1))β0) β
β€) |
85 | 80, 84 | zmulcld 12668 |
. . . . 5
β’ (π β ((π΄β0) Β· (((β
Dπ πΉ)β(π β 1))β0)) β
β€) |
86 | 85 | zcnd 12663 |
. . . 4
β’ (π β ((π΄β0) Β· (((β
Dπ πΉ)β(π β 1))β0)) β
β) |
87 | | difss 4130 |
. . . . . . . 8
β’
(((0...π) Γ
(0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©}) β
((0...π) Γ
(0...((π Β· π) + (π β 1)))) |
88 | | ssfi 9169 |
. . . . . . . 8
β’
((((0...π) Γ
(0...((π Β· π) + (π β 1)))) β Fin β§ (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©}) β
((0...π) Γ
(0...((π Β· π) + (π β 1))))) β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©}) β
Fin) |
89 | 8, 87, 88 | mp2an 691 |
. . . . . . 7
β’
(((0...π) Γ
(0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©}) β
Fin |
90 | 89 | a1i 11 |
. . . . . 6
β’ (π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©}) β
Fin) |
91 | | eldifi 4125 |
. . . . . . 7
β’ (π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©}) β π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) |
92 | 91, 38 | sylan2 594 |
. . . . . 6
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) β
β€) |
93 | 90, 92 | fsumzcl 15677 |
. . . . 5
β’ (π β Ξ£π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) β
β€) |
94 | 93 | zcnd 12663 |
. . . 4
β’ (π β Ξ£π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) β
β) |
95 | 49 | faccld 14240 |
. . . . 5
β’ (π β (!β(π β 1)) β
β) |
96 | 95 | nncnd 12224 |
. . . 4
β’ (π β (!β(π β 1)) β
β) |
97 | 95 | nnne0d 12258 |
. . . 4
β’ (π β (!β(π β 1)) β
0) |
98 | 86, 94, 96, 97 | divdird 12024 |
. . 3
β’ (π β ((((π΄β0) Β· (((β
Dπ πΉ)β(π β 1))β0)) + Ξ£π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ)))) /
(!β(π β 1))) =
((((π΄β0) Β·
(((β Dπ πΉ)β(π β 1))β0)) / (!β(π β 1))) + (Ξ£π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1))))) |
99 | 2, 78, 98 | 3eqtrd 2777 |
. 2
β’ (π β πΎ = ((((π΄β0) Β· (((β
Dπ πΉ)β(π β 1))β0)) / (!β(π β 1))) + (Ξ£π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1))))) |
100 | 26 | nnne0d 12258 |
. . 3
β’ (π β π β 0) |
101 | 80 | zcnd 12663 |
. . . . 5
β’ (π β (π΄β0) β β) |
102 | 84 | zcnd 12663 |
. . . . 5
β’ (π β (((β
Dπ πΉ)β(π β 1))β0) β
β) |
103 | 101, 102,
96, 97 | divassd 12021 |
. . . 4
β’ (π β (((π΄β0) Β· (((β
Dπ πΉ)β(π β 1))β0)) / (!β(π β 1))) = ((π΄β0) Β· ((((β
Dπ πΉ)β(π β 1))β0) / (!β(π β 1))))) |
104 | | etransclem5 44890 |
. . . . . . 7
β’ (π β (0...π) β¦ (π¦ β β β¦ ((π¦ β π)βif(π = 0, (π β 1), π)))) = (π β (0...π) β¦ (π₯ β β β¦ ((π₯ β π)βif(π = 0, (π β 1), π)))) |
105 | | etransclem11 44896 |
. . . . . . 7
β’ (π β β0
β¦ {π β
((0...π) βm
(0...π)) β£
Ξ£π β (0...π)(πβπ) = π}) = (π β β0 β¦ {π β ((0...π) βm (0...π)) β£ Ξ£π β (0...π)(πβπ) = π}) |
106 | 81, 82, 26, 28, 30, 49, 104, 105, 43, 83 | etransclem37 44922 |
. . . . . 6
β’ (π β (!β(π β 1)) β₯ (((β
Dπ πΉ)β(π β 1))β0)) |
107 | 95 | nnzd 12581 |
. . . . . . 7
β’ (π β (!β(π β 1)) β
β€) |
108 | | dvdsval2 16196 |
. . . . . . 7
β’
(((!β(π
β 1)) β β€ β§ (!β(π β 1)) β 0 β§ (((β
Dπ πΉ)β(π β 1))β0) β β€) β
((!β(π β 1))
β₯ (((β Dπ πΉ)β(π β 1))β0) β ((((β
Dπ πΉ)β(π β 1))β0) / (!β(π β 1))) β
β€)) |
109 | 107, 97, 84, 108 | syl3anc 1372 |
. . . . . 6
β’ (π β ((!β(π β 1)) β₯ (((β
Dπ πΉ)β(π β 1))β0) β ((((β
Dπ πΉ)β(π β 1))β0) / (!β(π β 1))) β
β€)) |
110 | 106, 109 | mpbid 231 |
. . . . 5
β’ (π β ((((β
Dπ πΉ)β(π β 1))β0) / (!β(π β 1))) β
β€) |
111 | 80, 110 | zmulcld 12668 |
. . . 4
β’ (π β ((π΄β0) Β· ((((β
Dπ πΉ)β(π β 1))β0) / (!β(π β 1)))) β
β€) |
112 | 103, 111 | eqeltrd 2834 |
. . 3
β’ (π β (((π΄β0) Β· (((β
Dπ πΉ)β(π β 1))β0)) / (!β(π β 1))) β
β€) |
113 | 91, 39 | sylan2 594 |
. . . . 5
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) β
β) |
114 | 90, 96, 113, 97 | fsumdivc 15728 |
. . . 4
β’ (π β (Ξ£π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1))) =
Ξ£π β
(((0...π) Γ
(0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})(((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1)))) |
115 | 16 | zcnd 12663 |
. . . . . . . 8
β’ ((π β§ π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) β (π΄β(1st βπ)) β
β) |
116 | 91, 115 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(π΄β(1st
βπ)) β
β) |
117 | 91, 37 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) β
β€) |
118 | 117 | zcnd 12663 |
. . . . . . 7
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) β
β) |
119 | 96 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(!β(π β 1))
β β) |
120 | 97 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(!β(π β 1))
β 0) |
121 | 116, 118,
119, 120 | divassd 12021 |
. . . . . 6
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1))) =
((π΄β(1st
βπ)) Β·
((((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) /
(!β(π β
1))))) |
122 | 91, 16 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(π΄β(1st
βπ)) β
β€) |
123 | 17 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
β β {β, β}) |
124 | 22 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
β β ((TopOpenββfld) βΎt
β)) |
125 | 26 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
π β
β) |
126 | 28 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
π β
β0) |
127 | 91 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
π β ((0...π) Γ (0...((π Β· π) + (π β 1))))) |
128 | 127, 33 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(2nd βπ)
β β0) |
129 | 127, 13 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(1st βπ)
β (0...π)) |
130 | 91, 35 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(1st βπ)
β β) |
131 | 123, 124,
125, 126, 30, 128, 104, 105, 129, 130 | etransclem37 44922 |
. . . . . . . 8
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(!β(π β 1))
β₯ (((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) |
132 | 107 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(!β(π β 1))
β β€) |
133 | | dvdsval2 16196 |
. . . . . . . . 9
β’
(((!β(π
β 1)) β β€ β§ (!β(π β 1)) β 0 β§ (((β
Dπ πΉ)β(2nd βπ))β(1st
βπ)) β β€)
β ((!β(π β
1)) β₯ (((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) β
((((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) /
(!β(π β 1)))
β β€)) |
134 | 132, 120,
117, 133 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
((!β(π β 1))
β₯ (((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) β
((((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) /
(!β(π β 1)))
β β€)) |
135 | 131, 134 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
((((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) /
(!β(π β 1)))
β β€) |
136 | 122, 135 | zmulcld 12668 |
. . . . . 6
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
((π΄β(1st
βπ)) Β·
((((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) /
(!β(π β 1))))
β β€) |
137 | 121, 136 | eqeltrd 2834 |
. . . . 5
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1)))
β β€) |
138 | 90, 137 | fsumzcl 15677 |
. . . 4
β’ (π β Ξ£π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})(((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1)))
β β€) |
139 | 114, 138 | eqeltrd 2834 |
. . 3
β’ (π β (Ξ£π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1)))
β β€) |
140 | | 1zzd 12589 |
. . . . . . . . . 10
β’ (π β 1 β
β€) |
141 | | zabscl 15256 |
. . . . . . . . . . 11
β’ ((π΄β0) β β€ β
(absβ(π΄β0))
β β€) |
142 | 80, 141 | syl 17 |
. . . . . . . . . 10
β’ (π β (absβ(π΄β0)) β
β€) |
143 | | nn0abscl 15255 |
. . . . . . . . . . . . 13
β’ ((π΄β0) β β€ β
(absβ(π΄β0))
β β0) |
144 | 80, 143 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (absβ(π΄β0)) β
β0) |
145 | | etransclem44.a0 |
. . . . . . . . . . . . 13
β’ (π β (π΄β0) β 0) |
146 | 101, 145 | absne0d 15390 |
. . . . . . . . . . . 12
β’ (π β (absβ(π΄β0)) β
0) |
147 | | elnnne0 12482 |
. . . . . . . . . . . 12
β’
((absβ(π΄β0)) β β β
((absβ(π΄β0))
β β0 β§ (absβ(π΄β0)) β 0)) |
148 | 144, 146,
147 | sylanbrc 584 |
. . . . . . . . . . 11
β’ (π β (absβ(π΄β0)) β
β) |
149 | 148 | nnge1d 12256 |
. . . . . . . . . 10
β’ (π β 1 β€ (absβ(π΄β0))) |
150 | | etransclem44.ap |
. . . . . . . . . . 11
β’ (π β (absβ(π΄β0)) < π) |
151 | | zltlem1 12611 |
. . . . . . . . . . . 12
β’
(((absβ(π΄β0)) β β€ β§ π β β€) β
((absβ(π΄β0))
< π β
(absβ(π΄β0))
β€ (π β
1))) |
152 | 142, 46, 151 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β ((absβ(π΄β0)) < π β (absβ(π΄β0)) β€ (π β 1))) |
153 | 150, 152 | mpbid 231 |
. . . . . . . . . 10
β’ (π β (absβ(π΄β0)) β€ (π β 1)) |
154 | 140, 50, 142, 149, 153 | elfzd 13488 |
. . . . . . . . 9
β’ (π β (absβ(π΄β0)) β (1...(π β 1))) |
155 | | fzm1ndvds 16261 |
. . . . . . . . 9
β’ ((π β β β§
(absβ(π΄β0))
β (1...(π β 1)))
β Β¬ π β₯
(absβ(π΄β0))) |
156 | 26, 154, 155 | syl2anc 585 |
. . . . . . . 8
β’ (π β Β¬ π β₯ (absβ(π΄β0))) |
157 | | dvdsabsb 16215 |
. . . . . . . . 9
β’ ((π β β€ β§ (π΄β0) β β€) β
(π β₯ (π΄β0) β π β₯ (absβ(π΄β0)))) |
158 | 46, 80, 157 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π β₯ (π΄β0) β π β₯ (absβ(π΄β0)))) |
159 | 156, 158 | mtbird 325 |
. . . . . . 7
β’ (π β Β¬ π β₯ (π΄β0)) |
160 | | etransclem44.mp |
. . . . . . . 8
β’ (π β (!βπ) < π) |
161 | 28, 24, 160, 30 | etransclem41 44926 |
. . . . . . 7
β’ (π β Β¬ π β₯ ((((β Dπ
πΉ)β(π β 1))β0) / (!β(π β 1)))) |
162 | 159, 161 | jca 513 |
. . . . . 6
β’ (π β (Β¬ π β₯ (π΄β0) β§ Β¬ π β₯ ((((β Dπ
πΉ)β(π β 1))β0) / (!β(π β 1))))) |
163 | | pm4.56 988 |
. . . . . 6
β’ ((Β¬
π β₯ (π΄β0) β§ Β¬ π β₯ ((((β
Dπ πΉ)β(π β 1))β0) / (!β(π β 1)))) β Β¬
(π β₯ (π΄β0) β¨ π β₯ ((((β Dπ
πΉ)β(π β 1))β0) / (!β(π β 1))))) |
164 | 162, 163 | sylib 217 |
. . . . 5
β’ (π β Β¬ (π β₯ (π΄β0) β¨ π β₯ ((((β Dπ
πΉ)β(π β 1))β0) / (!β(π β 1))))) |
165 | | euclemma 16646 |
. . . . . 6
β’ ((π β β β§ (π΄β0) β β€ β§
((((β Dπ πΉ)β(π β 1))β0) / (!β(π β 1))) β β€)
β (π β₯ ((π΄β0) Β· ((((β
Dπ πΉ)β(π β 1))β0) / (!β(π β 1)))) β (π β₯ (π΄β0) β¨ π β₯ ((((β Dπ
πΉ)β(π β 1))β0) / (!β(π β
1)))))) |
166 | 24, 80, 110, 165 | syl3anc 1372 |
. . . . 5
β’ (π β (π β₯ ((π΄β0) Β· ((((β
Dπ πΉ)β(π β 1))β0) / (!β(π β 1)))) β (π β₯ (π΄β0) β¨ π β₯ ((((β Dπ
πΉ)β(π β 1))β0) / (!β(π β
1)))))) |
167 | 164, 166 | mtbird 325 |
. . . 4
β’ (π β Β¬ π β₯ ((π΄β0) Β· ((((β
Dπ πΉ)β(π β 1))β0) / (!β(π β 1))))) |
168 | 103 | breq2d 5159 |
. . . 4
β’ (π β (π β₯ (((π΄β0) Β· (((β
Dπ πΉ)β(π β 1))β0)) / (!β(π β 1))) β π β₯ ((π΄β0) Β· ((((β
Dπ πΉ)β(π β 1))β0) / (!β(π β
1)))))) |
169 | 167, 168 | mtbird 325 |
. . 3
β’ (π β Β¬ π β₯ (((π΄β0) Β· (((β
Dπ πΉ)β(π β 1))β0)) / (!β(π β 1)))) |
170 | 46 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
π β
β€) |
171 | 170, 122,
135 | 3jca 1129 |
. . . . . . 7
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
(π β β€ β§
(π΄β(1st
βπ)) β β€
β§ ((((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) /
(!β(π β 1)))
β β€)) |
172 | | eldifn 4126 |
. . . . . . . . . 10
β’ (π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©}) β Β¬
π β {β¨0, (π β
1)β©}) |
173 | 91 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©}) β§
((2nd βπ)
= (π β 1) β§
(1st βπ) =
0)) β π β
((0...π) Γ
(0...((π Β· π) + (π β 1))))) |
174 | | 1st2nd2 8009 |
. . . . . . . . . . . . 13
β’ (π β ((0...π) Γ (0...((π Β· π) + (π β 1)))) β π = β¨(1st βπ), (2nd βπ)β©) |
175 | 173, 174 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©}) β§
((2nd βπ)
= (π β 1) β§
(1st βπ) =
0)) β π =
β¨(1st βπ), (2nd βπ)β©) |
176 | | simpr 486 |
. . . . . . . . . . . . . 14
β’
(((2nd βπ) = (π β 1) β§ (1st
βπ) = 0) β
(1st βπ) =
0) |
177 | | simpl 484 |
. . . . . . . . . . . . . 14
β’
(((2nd βπ) = (π β 1) β§ (1st
βπ) = 0) β
(2nd βπ) =
(π β
1)) |
178 | 176, 177 | opeq12d 4880 |
. . . . . . . . . . . . 13
β’
(((2nd βπ) = (π β 1) β§ (1st
βπ) = 0) β
β¨(1st βπ), (2nd βπ)β© = β¨0, (π β 1)β©) |
179 | 178 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©}) β§
((2nd βπ)
= (π β 1) β§
(1st βπ) =
0)) β β¨(1st βπ), (2nd βπ)β© = β¨0, (π β 1)β©) |
180 | 175, 179 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©}) β§
((2nd βπ)
= (π β 1) β§
(1st βπ) =
0)) β π = β¨0,
(π β
1)β©) |
181 | | velsn 4643 |
. . . . . . . . . . 11
β’ (π β {β¨0, (π β 1)β©} β π = β¨0, (π β 1)β©) |
182 | 180, 181 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©}) β§
((2nd βπ)
= (π β 1) β§
(1st βπ) =
0)) β π β
{β¨0, (π β
1)β©}) |
183 | 172, 182 | mtand 815 |
. . . . . . . . 9
β’ (π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©}) β Β¬
((2nd βπ)
= (π β 1) β§
(1st βπ) =
0)) |
184 | 183 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
Β¬ ((2nd βπ) = (π β 1) β§ (1st
βπ) =
0)) |
185 | 125, 126,
30, 128, 129, 184, 105 | etransclem38 44923 |
. . . . . . 7
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
π β₯ ((((β
Dπ πΉ)β(2nd βπ))β(1st
βπ)) /
(!β(π β
1)))) |
186 | | dvdsmultr2 16237 |
. . . . . . 7
β’ ((π β β€ β§ (π΄β(1st
βπ)) β β€
β§ ((((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) /
(!β(π β 1)))
β β€) β (π
β₯ ((((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) /
(!β(π β 1)))
β π β₯ ((π΄β(1st
βπ)) Β·
((((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) /
(!β(π β
1)))))) |
187 | 171, 185,
186 | sylc 65 |
. . . . . 6
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
π β₯ ((π΄β(1st
βπ)) Β·
((((β Dπ πΉ)β(2nd βπ))β(1st
βπ)) /
(!β(π β
1))))) |
188 | 187, 121 | breqtrrd 5175 |
. . . . 5
β’ ((π β§ π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})) β
π β₯ (((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1)))) |
189 | 90, 46, 137, 188 | fsumdvds 16247 |
. . . 4
β’ (π β π β₯ Ξ£π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})(((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1)))) |
190 | 189, 114 | breqtrrd 5175 |
. . 3
β’ (π β π β₯ (Ξ£π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β
1)))) |
191 | 46, 100, 112, 139, 169, 190 | etransclem9 44894 |
. 2
β’ (π β ((((π΄β0) Β· (((β
Dπ πΉ)β(π β 1))β0)) / (!β(π β 1))) + (Ξ£π β (((0...π) Γ (0...((π Β· π) + (π β 1)))) β {β¨0, (π β 1)β©})((π΄β(1st
βπ)) Β·
(((β Dπ πΉ)β(2nd βπ))β(1st
βπ))) /
(!β(π β 1))))
β 0) |
192 | 99, 191 | eqnetrd 3009 |
1
β’ (π β πΎ β 0) |