Step | Hyp | Ref
| Expression |
1 | | bcval2 14211 |
. . . 4
β’ (πΎ β (0...π) β (πCπΎ) = ((!βπ) / ((!β(π β πΎ)) Β· (!βπΎ)))) |
2 | 1 | adantl 483 |
. . 3
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (πCπΎ) = ((!βπ) / ((!β(π β πΎ)) Β· (!βπΎ)))) |
3 | | mulcl 11140 |
. . . . . . . . 9
β’ ((π β β β§ π₯ β β) β (π Β· π₯) β β) |
4 | 3 | adantl 483 |
. . . . . . . 8
β’ ((((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β§ (π β β β§ π₯ β β)) β (π Β· π₯) β β) |
5 | | mulass 11144 |
. . . . . . . . 9
β’ ((π β β β§ π₯ β β β§ π¦ β β) β ((π Β· π₯) Β· π¦) = (π Β· (π₯ Β· π¦))) |
6 | 5 | adantl 483 |
. . . . . . . 8
β’ ((((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β§ (π β β β§ π₯ β β β§ π¦ β β)) β ((π Β· π₯) Β· π¦) = (π Β· (π₯ Β· π¦))) |
7 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β πΎ β β) |
8 | | elfzuz3 13444 |
. . . . . . . . . . . . . 14
β’ (πΎ β (0...π) β π β (β€β₯βπΎ)) |
9 | 8 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β π β (β€β₯βπΎ)) |
10 | | eluznn 12848 |
. . . . . . . . . . . . 13
β’ ((πΎ β β β§ π β
(β€β₯βπΎ)) β π β β) |
11 | 7, 9, 10 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β π β β) |
12 | 11 | adantrr 716 |
. . . . . . . . . . 11
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β π β β) |
13 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β πΎ β β) |
14 | | nnre 12165 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
15 | | nnrp 12931 |
. . . . . . . . . . . 12
β’ (πΎ β β β πΎ β
β+) |
16 | | ltsubrp 12956 |
. . . . . . . . . . . 12
β’ ((π β β β§ πΎ β β+)
β (π β πΎ) < π) |
17 | 14, 15, 16 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β β β§ πΎ β β) β (π β πΎ) < π) |
18 | 12, 13, 17 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β (π β πΎ) < π) |
19 | 12 | nnzd 12531 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β π β β€) |
20 | | nnz 12525 |
. . . . . . . . . . . . 13
β’ (πΎ β β β πΎ β
β€) |
21 | 20 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β πΎ β β€) |
22 | 19, 21 | zsubcld 12617 |
. . . . . . . . . . 11
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β (π β πΎ) β β€) |
23 | | zltp1le 12558 |
. . . . . . . . . . 11
β’ (((π β πΎ) β β€ β§ π β β€) β ((π β πΎ) < π β ((π β πΎ) + 1) β€ π)) |
24 | 22, 19, 23 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β ((π β πΎ) < π β ((π β πΎ) + 1) β€ π)) |
25 | 18, 24 | mpbid 231 |
. . . . . . . . 9
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β ((π β πΎ) + 1) β€ π) |
26 | 22 | peano2zd 12615 |
. . . . . . . . . 10
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β ((π β πΎ) + 1) β β€) |
27 | | eluz 12782 |
. . . . . . . . . 10
β’ ((((π β πΎ) + 1) β β€ β§ π β β€) β (π β
(β€β₯β((π β πΎ) + 1)) β ((π β πΎ) + 1) β€ π)) |
28 | 26, 19, 27 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β (π β
(β€β₯β((π β πΎ) + 1)) β ((π β πΎ) + 1) β€ π)) |
29 | 25, 28 | mpbird 257 |
. . . . . . . 8
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β π β
(β€β₯β((π β πΎ) + 1))) |
30 | | simprr 772 |
. . . . . . . . 9
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β (π β πΎ) β β) |
31 | | nnuz 12811 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
32 | 30, 31 | eleqtrdi 2844 |
. . . . . . . 8
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β (π β πΎ) β
(β€β₯β1)) |
33 | | fvi 6918 |
. . . . . . . . . 10
β’ (π β (1...π) β ( I βπ) = π) |
34 | | elfzelz 13447 |
. . . . . . . . . . 11
β’ (π β (1...π) β π β β€) |
35 | 34 | zcnd 12613 |
. . . . . . . . . 10
β’ (π β (1...π) β π β β) |
36 | 33, 35 | eqeltrd 2834 |
. . . . . . . . 9
β’ (π β (1...π) β ( I βπ) β β) |
37 | 36 | adantl 483 |
. . . . . . . 8
β’ ((((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β§ π β (1...π)) β ( I βπ) β β) |
38 | 4, 6, 29, 32, 37 | seqsplit 13947 |
. . . . . . 7
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β (seq1( Β· ,
I )βπ) = ((seq1(
Β· , I )β(π
β πΎ)) Β·
(seq((π β πΎ) + 1)( Β· , I
)βπ))) |
39 | | facnn 14181 |
. . . . . . . 8
β’ (π β β β
(!βπ) = (seq1(
Β· , I )βπ)) |
40 | 12, 39 | syl 17 |
. . . . . . 7
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β (!βπ) = (seq1( Β· , I
)βπ)) |
41 | | facnn 14181 |
. . . . . . . . 9
β’ ((π β πΎ) β β β (!β(π β πΎ)) = (seq1( Β· , I )β(π β πΎ))) |
42 | 30, 41 | syl 17 |
. . . . . . . 8
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β (!β(π β πΎ)) = (seq1( Β· , I )β(π β πΎ))) |
43 | 42 | oveq1d 7373 |
. . . . . . 7
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β ((!β(π β πΎ)) Β· (seq((π β πΎ) + 1)( Β· , I )βπ)) = ((seq1( Β· , I
)β(π β πΎ)) Β· (seq((π β πΎ) + 1)( Β· , I )βπ))) |
44 | 38, 40, 43 | 3eqtr4d 2783 |
. . . . . 6
β’ (((π β β0
β§ πΎ β β)
β§ (πΎ β (0...π) β§ (π β πΎ) β β)) β (!βπ) = ((!β(π β πΎ)) Β· (seq((π β πΎ) + 1)( Β· , I )βπ))) |
45 | 44 | expr 458 |
. . . . 5
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β ((π β πΎ) β β β (!βπ) = ((!β(π β πΎ)) Β· (seq((π β πΎ) + 1)( Β· , I )βπ)))) |
46 | | simpll 766 |
. . . . . . . . 9
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β π β
β0) |
47 | | faccl 14189 |
. . . . . . . . 9
β’ (π β β0
β (!βπ) β
β) |
48 | | nncn 12166 |
. . . . . . . . 9
β’
((!βπ) β
β β (!βπ)
β β) |
49 | 46, 47, 48 | 3syl 18 |
. . . . . . . 8
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (!βπ) β
β) |
50 | 49 | mulid2d 11178 |
. . . . . . 7
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (1 Β·
(!βπ)) =
(!βπ)) |
51 | 11, 39 | syl 17 |
. . . . . . . 8
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (!βπ) = (seq1( Β· , I
)βπ)) |
52 | 51 | oveq2d 7374 |
. . . . . . 7
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (1 Β·
(!βπ)) = (1 Β·
(seq1( Β· , I )βπ))) |
53 | 50, 52 | eqtr3d 2775 |
. . . . . 6
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (!βπ) = (1 Β· (seq1( Β·
, I )βπ))) |
54 | | fveq2 6843 |
. . . . . . . . 9
β’ ((π β πΎ) = 0 β (!β(π β πΎ)) = (!β0)) |
55 | | fac0 14182 |
. . . . . . . . 9
β’
(!β0) = 1 |
56 | 54, 55 | eqtrdi 2789 |
. . . . . . . 8
β’ ((π β πΎ) = 0 β (!β(π β πΎ)) = 1) |
57 | | oveq1 7365 |
. . . . . . . . . . 11
β’ ((π β πΎ) = 0 β ((π β πΎ) + 1) = (0 + 1)) |
58 | | 0p1e1 12280 |
. . . . . . . . . . 11
β’ (0 + 1) =
1 |
59 | 57, 58 | eqtrdi 2789 |
. . . . . . . . . 10
β’ ((π β πΎ) = 0 β ((π β πΎ) + 1) = 1) |
60 | 59 | seqeq1d 13918 |
. . . . . . . . 9
β’ ((π β πΎ) = 0 β seq((π β πΎ) + 1)( Β· , I ) = seq1( Β· , I
)) |
61 | 60 | fveq1d 6845 |
. . . . . . . 8
β’ ((π β πΎ) = 0 β (seq((π β πΎ) + 1)( Β· , I )βπ) = (seq1( Β· , I
)βπ)) |
62 | 56, 61 | oveq12d 7376 |
. . . . . . 7
β’ ((π β πΎ) = 0 β ((!β(π β πΎ)) Β· (seq((π β πΎ) + 1)( Β· , I )βπ)) = (1 Β· (seq1( Β·
, I )βπ))) |
63 | 62 | eqeq2d 2744 |
. . . . . 6
β’ ((π β πΎ) = 0 β ((!βπ) = ((!β(π β πΎ)) Β· (seq((π β πΎ) + 1)( Β· , I )βπ)) β (!βπ) = (1 Β· (seq1( Β·
, I )βπ)))) |
64 | 53, 63 | syl5ibrcom 247 |
. . . . 5
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β ((π β πΎ) = 0 β (!βπ) = ((!β(π β πΎ)) Β· (seq((π β πΎ) + 1)( Β· , I )βπ)))) |
65 | | fznn0sub 13479 |
. . . . . . 7
β’ (πΎ β (0...π) β (π β πΎ) β
β0) |
66 | 65 | adantl 483 |
. . . . . 6
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (π β πΎ) β
β0) |
67 | | elnn0 12420 |
. . . . . 6
β’ ((π β πΎ) β β0 β ((π β πΎ) β β β¨ (π β πΎ) = 0)) |
68 | 66, 67 | sylib 217 |
. . . . 5
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β ((π β πΎ) β β β¨ (π β πΎ) = 0)) |
69 | 45, 64, 68 | mpjaod 859 |
. . . 4
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (!βπ) = ((!β(π β πΎ)) Β· (seq((π β πΎ) + 1)( Β· , I )βπ))) |
70 | 69 | oveq1d 7373 |
. . 3
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β ((!βπ) / ((!β(π β πΎ)) Β· (!βπΎ))) = (((!β(π β πΎ)) Β· (seq((π β πΎ) + 1)( Β· , I )βπ)) / ((!β(π β πΎ)) Β· (!βπΎ)))) |
71 | | eqid 2733 |
. . . . . 6
β’
(β€β₯β((π β πΎ) + 1)) =
(β€β₯β((π β πΎ) + 1)) |
72 | | nn0z 12529 |
. . . . . . . . 9
β’ (π β β0
β π β
β€) |
73 | | zsubcl 12550 |
. . . . . . . . 9
β’ ((π β β€ β§ πΎ β β€) β (π β πΎ) β β€) |
74 | 72, 20, 73 | syl2an 597 |
. . . . . . . 8
β’ ((π β β0
β§ πΎ β β)
β (π β πΎ) β
β€) |
75 | 74 | peano2zd 12615 |
. . . . . . 7
β’ ((π β β0
β§ πΎ β β)
β ((π β πΎ) + 1) β
β€) |
76 | 75 | adantr 482 |
. . . . . 6
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β ((π β πΎ) + 1) β β€) |
77 | | fvi 6918 |
. . . . . . . 8
β’ (π β
(β€β₯β((π β πΎ) + 1)) β ( I βπ) = π) |
78 | | eluzelcn 12780 |
. . . . . . . 8
β’ (π β
(β€β₯β((π β πΎ) + 1)) β π β β) |
79 | 77, 78 | eqeltrd 2834 |
. . . . . . 7
β’ (π β
(β€β₯β((π β πΎ) + 1)) β ( I βπ) β β) |
80 | 79 | adantl 483 |
. . . . . 6
β’ ((((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β§ π β (β€β₯β((π β πΎ) + 1))) β ( I βπ) β
β) |
81 | 3 | adantl 483 |
. . . . . 6
β’ ((((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β§ (π β β β§ π₯ β β)) β (π Β· π₯) β β) |
82 | 71, 76, 80, 81 | seqf 13935 |
. . . . 5
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β seq((π β πΎ) + 1)( Β· , I
):(β€β₯β((π β πΎ) + 1))βΆβ) |
83 | 11, 7, 17 | syl2anc 585 |
. . . . . . 7
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (π β πΎ) < π) |
84 | 74 | adantr 482 |
. . . . . . . 8
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (π β πΎ) β β€) |
85 | 11 | nnzd 12531 |
. . . . . . . 8
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β π β β€) |
86 | 84, 85, 23 | syl2anc 585 |
. . . . . . 7
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β ((π β πΎ) < π β ((π β πΎ) + 1) β€ π)) |
87 | 83, 86 | mpbid 231 |
. . . . . 6
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β ((π β πΎ) + 1) β€ π) |
88 | 76, 85, 27 | syl2anc 585 |
. . . . . 6
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (π β
(β€β₯β((π β πΎ) + 1)) β ((π β πΎ) + 1) β€ π)) |
89 | 87, 88 | mpbird 257 |
. . . . 5
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β π β
(β€β₯β((π β πΎ) + 1))) |
90 | 82, 89 | ffvelcdmd 7037 |
. . . 4
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (seq((π β πΎ) + 1)( Β· , I )βπ) β
β) |
91 | | elfznn0 13540 |
. . . . . . 7
β’ (πΎ β (0...π) β πΎ β
β0) |
92 | 91 | adantl 483 |
. . . . . 6
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β πΎ β
β0) |
93 | 92 | faccld 14190 |
. . . . 5
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (!βπΎ) β
β) |
94 | 93 | nncnd 12174 |
. . . 4
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (!βπΎ) β
β) |
95 | 66 | faccld 14190 |
. . . . 5
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (!β(π β πΎ)) β β) |
96 | 95 | nncnd 12174 |
. . . 4
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (!β(π β πΎ)) β β) |
97 | 93 | nnne0d 12208 |
. . . 4
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (!βπΎ) β 0) |
98 | 95 | nnne0d 12208 |
. . . 4
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (!β(π β πΎ)) β 0) |
99 | 90, 94, 96, 97, 98 | divcan5d 11962 |
. . 3
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (((!β(π β πΎ)) Β· (seq((π β πΎ) + 1)( Β· , I )βπ)) / ((!β(π β πΎ)) Β· (!βπΎ))) = ((seq((π β πΎ) + 1)( Β· , I )βπ) / (!βπΎ))) |
100 | 2, 70, 99 | 3eqtrd 2777 |
. 2
β’ (((π β β0
β§ πΎ β β)
β§ πΎ β (0...π)) β (πCπΎ) = ((seq((π β πΎ) + 1)( Β· , I )βπ) / (!βπΎ))) |
101 | | nnnn0 12425 |
. . . . 5
β’ (πΎ β β β πΎ β
β0) |
102 | 101 | ad2antlr 726 |
. . . 4
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β πΎ β
β0) |
103 | | faccl 14189 |
. . . 4
β’ (πΎ β β0
β (!βπΎ) β
β) |
104 | | nncn 12166 |
. . . . 5
β’
((!βπΎ) β
β β (!βπΎ)
β β) |
105 | | nnne0 12192 |
. . . . 5
β’
((!βπΎ) β
β β (!βπΎ)
β 0) |
106 | 104, 105 | div0d 11935 |
. . . 4
β’
((!βπΎ) β
β β (0 / (!βπΎ)) = 0) |
107 | 102, 103,
106 | 3syl 18 |
. . 3
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β (0 /
(!βπΎ)) =
0) |
108 | 3 | adantl 483 |
. . . . 5
β’ ((((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β§ (π β β β§ π₯ β β)) β (π Β· π₯) β β) |
109 | | fvi 6918 |
. . . . . . 7
β’ (π β (((π β πΎ) + 1)...π) β ( I βπ) = π) |
110 | | elfzelz 13447 |
. . . . . . . 8
β’ (π β (((π β πΎ) + 1)...π) β π β β€) |
111 | 110 | zcnd 12613 |
. . . . . . 7
β’ (π β (((π β πΎ) + 1)...π) β π β β) |
112 | 109, 111 | eqeltrd 2834 |
. . . . . 6
β’ (π β (((π β πΎ) + 1)...π) β ( I βπ) β β) |
113 | 112 | adantl 483 |
. . . . 5
β’ ((((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β§ π β (((π β πΎ) + 1)...π)) β ( I βπ) β β) |
114 | | mul02 11338 |
. . . . . 6
β’ (π β β β (0
Β· π) =
0) |
115 | 114 | adantl 483 |
. . . . 5
β’ ((((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β§ π β β) β (0
Β· π) =
0) |
116 | | mul01 11339 |
. . . . . 6
β’ (π β β β (π Β· 0) =
0) |
117 | 116 | adantl 483 |
. . . . 5
β’ ((((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β§ π β β) β (π Β· 0) =
0) |
118 | 75 | adantr 482 |
. . . . . 6
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β ((π β πΎ) + 1) β β€) |
119 | 72 | ad2antrr 725 |
. . . . . 6
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β π β
β€) |
120 | | 0zd 12516 |
. . . . . 6
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β 0 β
β€) |
121 | | simpr 486 |
. . . . . . . . 9
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β Β¬ πΎ β (0...π)) |
122 | | nn0uz 12810 |
. . . . . . . . . . . 12
β’
β0 = (β€β₯β0) |
123 | 102, 122 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β πΎ β
(β€β₯β0)) |
124 | | elfz5 13439 |
. . . . . . . . . . 11
β’ ((πΎ β
(β€β₯β0) β§ π β β€) β (πΎ β (0...π) β πΎ β€ π)) |
125 | 123, 119,
124 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β (πΎ β (0...π) β πΎ β€ π)) |
126 | | nn0re 12427 |
. . . . . . . . . . . 12
β’ (π β β0
β π β
β) |
127 | 126 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β π β
β) |
128 | | nnre 12165 |
. . . . . . . . . . . 12
β’ (πΎ β β β πΎ β
β) |
129 | 128 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β πΎ β
β) |
130 | 127, 129 | subge0d 11750 |
. . . . . . . . . 10
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β (0 β€
(π β πΎ) β πΎ β€ π)) |
131 | 125, 130 | bitr4d 282 |
. . . . . . . . 9
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β (πΎ β (0...π) β 0 β€ (π β πΎ))) |
132 | 121, 131 | mtbid 324 |
. . . . . . . 8
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β Β¬ 0
β€ (π β πΎ)) |
133 | 74 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β (π β πΎ) β β€) |
134 | 133 | zred 12612 |
. . . . . . . . 9
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β (π β πΎ) β β) |
135 | | 0re 11162 |
. . . . . . . . 9
β’ 0 β
β |
136 | | ltnle 11239 |
. . . . . . . . 9
β’ (((π β πΎ) β β β§ 0 β β)
β ((π β πΎ) < 0 β Β¬ 0 β€
(π β πΎ))) |
137 | 134, 135,
136 | sylancl 587 |
. . . . . . . 8
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β ((π β πΎ) < 0 β Β¬ 0 β€ (π β πΎ))) |
138 | 132, 137 | mpbird 257 |
. . . . . . 7
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β (π β πΎ) < 0) |
139 | | 0z 12515 |
. . . . . . . 8
β’ 0 β
β€ |
140 | | zltp1le 12558 |
. . . . . . . 8
β’ (((π β πΎ) β β€ β§ 0 β β€)
β ((π β πΎ) < 0 β ((π β πΎ) + 1) β€ 0)) |
141 | 133, 139,
140 | sylancl 587 |
. . . . . . 7
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β ((π β πΎ) < 0 β ((π β πΎ) + 1) β€ 0)) |
142 | 138, 141 | mpbid 231 |
. . . . . 6
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β ((π β πΎ) + 1) β€ 0) |
143 | | nn0ge0 12443 |
. . . . . . 7
β’ (π β β0
β 0 β€ π) |
144 | 143 | ad2antrr 725 |
. . . . . 6
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β 0 β€
π) |
145 | 118, 119,
120, 142, 144 | elfzd 13438 |
. . . . 5
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β 0 β
(((π β πΎ) + 1)...π)) |
146 | | simpll 766 |
. . . . 5
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β π β
β0) |
147 | | 0cn 11152 |
. . . . . 6
β’ 0 β
β |
148 | | fvi 6918 |
. . . . . 6
β’ (0 β
β β ( I β0) = 0) |
149 | 147, 148 | mp1i 13 |
. . . . 5
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β ( I
β0) = 0) |
150 | 108, 113,
115, 117, 145, 146, 149 | seqz 13962 |
. . . 4
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β (seq((π β πΎ) + 1)( Β· , I )βπ) = 0) |
151 | 150 | oveq1d 7373 |
. . 3
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β
((seq((π β πΎ) + 1)( Β· , I
)βπ) / (!βπΎ)) = (0 / (!βπΎ))) |
152 | | bcval3 14212 |
. . . . 5
β’ ((π β β0
β§ πΎ β β€
β§ Β¬ πΎ β
(0...π)) β (πCπΎ) = 0) |
153 | 20, 152 | syl3an2 1165 |
. . . 4
β’ ((π β β0
β§ πΎ β β
β§ Β¬ πΎ β
(0...π)) β (πCπΎ) = 0) |
154 | 153 | 3expa 1119 |
. . 3
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β (πCπΎ) = 0) |
155 | 107, 151,
154 | 3eqtr4rd 2784 |
. 2
β’ (((π β β0
β§ πΎ β β)
β§ Β¬ πΎ β
(0...π)) β (πCπΎ) = ((seq((π β πΎ) + 1)( Β· , I )βπ) / (!βπΎ))) |
156 | 100, 155 | pm2.61dan 812 |
1
β’ ((π β β0
β§ πΎ β β)
β (πCπΎ) = ((seq((π β πΎ) + 1)( Β· , I )βπ) / (!βπΎ))) |