Step | Hyp | Ref
| Expression |
1 | | poimirlem2.3 |
. . . . . . . . . . . . . . . 16
β’ (π β π:(1...π)β1-1-ontoβ(1...π)) |
2 | | dff1o3 6790 |
. . . . . . . . . . . . . . . . 17
β’ (π:(1...π)β1-1-ontoβ(1...π) β (π:(1...π)βontoβ(1...π) β§ Fun β‘π)) |
3 | 2 | simprbi 497 |
. . . . . . . . . . . . . . . 16
β’ (π:(1...π)β1-1-ontoβ(1...π) β Fun β‘π) |
4 | 1, 3 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β Fun β‘π) |
5 | | imadif 6585 |
. . . . . . . . . . . . . . 15
β’ (Fun
β‘π β (π β ((1...π) β {(π + 1)})) = ((π β (1...π)) β (π β {(π + 1)}))) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π β ((1...π) β {(π + 1)})) = ((π β (1...π)) β (π β {(π + 1)}))) |
7 | | poimirlem2.4 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β (1...(π β 1))) |
8 | | fzp1elp1 13494 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...(π β 1)) β (π + 1) β (1...((π β 1) + 1))) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π + 1) β (1...((π β 1) + 1))) |
10 | | poimir.0 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β β) |
11 | 10 | nncnd 12169 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β β) |
12 | | npcan1 11580 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β ((π β 1) + 1) = π) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π β 1) + 1) = π) |
14 | 13 | oveq2d 7373 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...((π β 1) + 1)) = (1...π)) |
15 | 9, 14 | eleqtrd 2839 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π + 1) β (1...π)) |
16 | | fzsplit 13467 |
. . . . . . . . . . . . . . . . . 18
β’ ((π + 1) β (1...π) β (1...π) = ((1...(π + 1)) βͺ (((π + 1) + 1)...π))) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) = ((1...(π + 1)) βͺ (((π + 1) + 1)...π))) |
18 | 17 | difeq1d 4081 |
. . . . . . . . . . . . . . . 16
β’ (π β ((1...π) β {(π + 1)}) = (((1...(π + 1)) βͺ (((π + 1) + 1)...π)) β {(π + 1)})) |
19 | | difundir 4240 |
. . . . . . . . . . . . . . . . 17
β’
(((1...(π + 1))
βͺ (((π + 1) +
1)...π)) β {(π + 1)}) = (((1...(π + 1)) β {(π + 1)}) βͺ ((((π + 1) + 1)...π) β {(π + 1)})) |
20 | | elfzuz 13437 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1...(π β 1)) β π β
(β€β₯β1)) |
21 | 7, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β
(β€β₯β1)) |
22 | | fzsuc 13488 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(β€β₯β1) β (1...(π + 1)) = ((1...π) βͺ {(π + 1)})) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...(π + 1)) = ((1...π) βͺ {(π + 1)})) |
24 | 23 | difeq1d 4081 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((1...(π + 1)) β {(π + 1)}) = (((1...π) βͺ {(π + 1)}) β {(π + 1)})) |
25 | | difun2 4440 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((1...π) βͺ
{(π + 1)}) β {(π + 1)}) = ((1...π) β {(π + 1)}) |
26 | 7 | elfzelzd 13442 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β β€) |
27 | 26 | zred 12607 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β β) |
28 | 27 | ltp1d 12085 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π < (π + 1)) |
29 | 26 | peano2zd 12610 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π + 1) β β€) |
30 | 29 | zred 12607 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π + 1) β β) |
31 | 27, 30 | ltnled 11302 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π < (π + 1) β Β¬ (π + 1) β€ π)) |
32 | 28, 31 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β Β¬ (π + 1) β€ π) |
33 | | elfzle2 13445 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π + 1) β (1...π) β (π + 1) β€ π) |
34 | 32, 33 | nsyl 140 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Β¬ (π + 1) β (1...π)) |
35 | | difsn 4758 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Β¬
(π + 1) β (1...π) β ((1...π) β {(π + 1)}) = (1...π)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((1...π) β {(π + 1)}) = (1...π)) |
37 | 25, 36 | eqtrid 2788 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (((1...π) βͺ {(π + 1)}) β {(π + 1)}) = (1...π)) |
38 | 24, 37 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((1...(π + 1)) β {(π + 1)}) = (1...π)) |
39 | 30 | ltp1d 12085 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π + 1) < ((π + 1) + 1)) |
40 | | peano2re 11328 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π + 1) β β β
((π + 1) + 1) β
β) |
41 | 30, 40 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((π + 1) + 1) β β) |
42 | 30, 41 | ltnled 11302 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((π + 1) < ((π + 1) + 1) β Β¬ ((π + 1) + 1) β€ (π + 1))) |
43 | 39, 42 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Β¬ ((π + 1) + 1) β€ (π + 1)) |
44 | | elfzle1 13444 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π + 1) β (((π + 1) + 1)...π) β ((π + 1) + 1) β€ (π + 1)) |
45 | 43, 44 | nsyl 140 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Β¬ (π + 1) β (((π + 1) + 1)...π)) |
46 | | difsn 4758 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
(π + 1) β (((π + 1) + 1)...π) β ((((π + 1) + 1)...π) β {(π + 1)}) = (((π + 1) + 1)...π)) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((((π + 1) + 1)...π) β {(π + 1)}) = (((π + 1) + 1)...π)) |
48 | 38, 47 | uneq12d 4124 |
. . . . . . . . . . . . . . . . 17
β’ (π β (((1...(π + 1)) β {(π + 1)}) βͺ ((((π + 1) + 1)...π) β {(π + 1)})) = ((1...π) βͺ (((π + 1) + 1)...π))) |
49 | 19, 48 | eqtrid 2788 |
. . . . . . . . . . . . . . . 16
β’ (π β (((1...(π + 1)) βͺ (((π + 1) + 1)...π)) β {(π + 1)}) = ((1...π) βͺ (((π + 1) + 1)...π))) |
50 | 18, 49 | eqtrd 2776 |
. . . . . . . . . . . . . . 15
β’ (π β ((1...π) β {(π + 1)}) = ((1...π) βͺ (((π + 1) + 1)...π))) |
51 | 50 | imaeq2d 6013 |
. . . . . . . . . . . . . 14
β’ (π β (π β ((1...π) β {(π + 1)})) = (π β ((1...π) βͺ (((π + 1) + 1)...π)))) |
52 | 6, 51 | eqtr3d 2778 |
. . . . . . . . . . . . 13
β’ (π β ((π β (1...π)) β (π β {(π + 1)})) = (π β ((1...π) βͺ (((π + 1) + 1)...π)))) |
53 | | imaundi 6102 |
. . . . . . . . . . . . 13
β’ (π β ((1...π) βͺ (((π + 1) + 1)...π))) = ((π β (1...π)) βͺ (π β (((π + 1) + 1)...π))) |
54 | 52, 53 | eqtrdi 2792 |
. . . . . . . . . . . 12
β’ (π β ((π β (1...π)) β (π β {(π + 1)})) = ((π β (1...π)) βͺ (π β (((π + 1) + 1)...π)))) |
55 | 54 | eleq2d 2823 |
. . . . . . . . . . 11
β’ (π β (π β ((π β (1...π)) β (π β {(π + 1)})) β π β ((π β (1...π)) βͺ (π β (((π + 1) + 1)...π))))) |
56 | | eldif 3920 |
. . . . . . . . . . 11
β’ (π β ((π β (1...π)) β (π β {(π + 1)})) β (π β (π β (1...π)) β§ Β¬ π β (π β {(π + 1)}))) |
57 | | elun 4108 |
. . . . . . . . . . 11
β’ (π β ((π β (1...π)) βͺ (π β (((π + 1) + 1)...π))) β (π β (π β (1...π)) β¨ π β (π β (((π + 1) + 1)...π)))) |
58 | 55, 56, 57 | 3bitr3g 312 |
. . . . . . . . . 10
β’ (π β ((π β (π β (1...π)) β§ Β¬ π β (π β {(π + 1)})) β (π β (π β (1...π)) β¨ π β (π β (((π + 1) + 1)...π))))) |
59 | 58 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π < π) β ((π β (π β (1...π)) β§ Β¬ π β (π β {(π + 1)})) β (π β (π β (1...π)) β¨ π β (π β (((π + 1) + 1)...π))))) |
60 | | imassrn 6024 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π)) β ran π |
61 | | f1of 6784 |
. . . . . . . . . . . . . . . . . 18
β’ (π:(1...π)β1-1-ontoβ(1...π) β π:(1...π)βΆ(1...π)) |
62 | 1, 61 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π:(1...π)βΆ(1...π)) |
63 | 62 | frnd 6676 |
. . . . . . . . . . . . . . . 16
β’ (π β ran π β (1...π)) |
64 | 60, 63 | sstrid 3955 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (1...π)) β (1...π)) |
65 | 64 | sselda 3944 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π β (1...π))) β π β (1...π)) |
66 | | poimirlem2.2 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π:(1...π)βΆβ€) |
67 | 66 | ffnd 6669 |
. . . . . . . . . . . . . . . . 17
β’ (π β π Fn (1...π)) |
68 | 67 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β (1...π))) β π Fn (1...π)) |
69 | | 1ex 11151 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 1 β
V |
70 | | fnconstg 6730 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1 β
V β ((π β
(1...π)) Γ {1}) Fn
(π β (1...π))) |
71 | 69, 70 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (1...π)) Γ {1}) Fn (π β (1...π)) |
72 | | c0ex 11149 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 β
V |
73 | | fnconstg 6730 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (0 β
V β ((π β
((π + 1)...π)) Γ {0}) Fn (π β ((π + 1)...π))) |
74 | 72, 73 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β ((π + 1)...π)) Γ {0}) Fn (π β ((π + 1)...π)) |
75 | 71, 74 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (1...π)) Γ {1}) Fn (π β (1...π)) β§ ((π β ((π + 1)...π)) Γ {0}) Fn (π β ((π + 1)...π))) |
76 | | imain 6586 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Fun
β‘π β (π β ((1...π) β© ((π + 1)...π))) = ((π β (1...π)) β© (π β ((π + 1)...π)))) |
77 | 4, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β ((1...π) β© ((π + 1)...π))) = ((π β (1...π)) β© (π β ((π + 1)...π)))) |
78 | | fzdisj 13468 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π < (π + 1) β ((1...π) β© ((π + 1)...π)) = β
) |
79 | 28, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((1...π) β© ((π + 1)...π)) = β
) |
80 | 79 | imaeq2d 6013 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π β ((1...π) β© ((π + 1)...π))) = (π β β
)) |
81 | | ima0 6029 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β
) =
β
|
82 | 80, 81 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β ((1...π) β© ((π + 1)...π))) = β
) |
83 | 77, 82 | eqtr3d 2778 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π β (1...π)) β© (π β ((π + 1)...π))) = β
) |
84 | | fnun 6614 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β
(1...π)) Γ {1}) Fn
(π β (1...π)) β§ ((π β ((π + 1)...π)) Γ {0}) Fn (π β ((π + 1)...π))) β§ ((π β (1...π)) β© (π β ((π + 1)...π))) = β
) β (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) Fn ((π β (1...π)) βͺ (π β ((π + 1)...π)))) |
85 | 75, 83, 84 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) Fn ((π β (1...π)) βͺ (π β ((π + 1)...π)))) |
86 | | imaundi 6102 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((1...π) βͺ ((π + 1)...π))) = ((π β (1...π)) βͺ (π β ((π + 1)...π))) |
87 | 10 | nnzd 12526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β β€) |
88 | | peano2zm 12546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β€ β (π β 1) β
β€) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π β 1) β β€) |
90 | | uzid 12778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β 1) β β€
β (π β 1) β
(β€β₯β(π β 1))) |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (π β 1) β
(β€β₯β(π β 1))) |
92 | | peano2uz 12826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β 1) β
(β€β₯β(π β 1)) β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
94 | 13, 93 | eqeltrrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β (β€β₯β(π β 1))) |
95 | | fzss2 13481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β
(β€β₯β(π β 1)) β (1...(π β 1)) β (1...π)) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...(π β 1)) β (1...π)) |
97 | 96, 7 | sseldd 3945 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β (1...π)) |
98 | | fzsplit 13467 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1...π) β (1...π) = ((1...π) βͺ ((π + 1)...π))) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1...π) = ((1...π) βͺ ((π + 1)...π))) |
100 | 99 | imaeq2d 6013 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π β (1...π)) = (π β ((1...π) βͺ ((π + 1)...π)))) |
101 | | f1ofo 6791 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π:(1...π)β1-1-ontoβ(1...π) β π:(1...π)βontoβ(1...π)) |
102 | 1, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π:(1...π)βontoβ(1...π)) |
103 | | foima 6761 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π:(1...π)βontoβ(1...π) β (π β (1...π)) = (1...π)) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π β (1...π)) = (1...π)) |
105 | 100, 104 | eqtr3d 2778 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β ((1...π) βͺ ((π + 1)...π))) = (1...π)) |
106 | 86, 105 | eqtr3id 2790 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π β (1...π)) βͺ (π β ((π + 1)...π))) = (1...π)) |
107 | 106 | fneq2d 6596 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) Fn ((π β (1...π)) βͺ (π β ((π + 1)...π))) β (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) Fn (1...π))) |
108 | 85, 107 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (π β (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) Fn (1...π)) |
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β (1...π))) β (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) Fn (1...π)) |
110 | | fzfid 13878 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β (1...π))) β (1...π) β Fin) |
111 | | inidm 4178 |
. . . . . . . . . . . . . . . 16
β’
((1...π) β©
(1...π)) = (1...π) |
112 | | eqidd 2737 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π β (1...π))) β§ π β (1...π)) β (πβπ) = (πβπ)) |
113 | | fvun1 6932 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β (1...π)) Γ {1}) Fn (π β (1...π)) β§ ((π β ((π + 1)...π)) Γ {0}) Fn (π β ((π + 1)...π)) β§ (((π β (1...π)) β© (π β ((π + 1)...π))) = β
β§ π β (π β (1...π)))) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = (((π β (1...π)) Γ {1})βπ)) |
114 | 71, 74, 113 | mp3an12 1451 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β (1...π)) β© (π β ((π + 1)...π))) = β
β§ π β (π β (1...π))) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = (((π β (1...π)) Γ {1})βπ)) |
115 | 83, 114 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π β (1...π))) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = (((π β (1...π)) Γ {1})βπ)) |
116 | 69 | fvconst2 7153 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β (1...π)) β (((π β (1...π)) Γ {1})βπ) = 1) |
117 | 116 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π β (1...π))) β (((π β (1...π)) Γ {1})βπ) = 1) |
118 | 115, 117 | eqtrd 2776 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π β (1...π))) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = 1) |
119 | 118 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π β (1...π))) β§ π β (1...π)) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = 1) |
120 | 68, 109, 110, 110, 111, 112, 119 | ofval 7628 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π β (1...π))) β§ π β (1...π)) β ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ) = ((πβπ) + 1)) |
121 | | fnconstg 6730 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1 β
V β ((π β
(1...(π + 1))) Γ {1})
Fn (π β (1...(π + 1)))) |
122 | 69, 121 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (1...(π + 1))) Γ {1}) Fn (π β (1...(π + 1))) |
123 | | fnconstg 6730 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (0 β
V β ((π β
(((π + 1) + 1)...π)) Γ {0}) Fn (π β (((π + 1) + 1)...π))) |
124 | 72, 123 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (((π + 1) + 1)...π)) Γ {0}) Fn (π β (((π + 1) + 1)...π)) |
125 | 122, 124 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (1...(π + 1))) Γ {1}) Fn (π β (1...(π + 1))) β§ ((π β (((π + 1) + 1)...π)) Γ {0}) Fn (π β (((π + 1) + 1)...π))) |
126 | | imain 6586 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Fun
β‘π β (π β ((1...(π + 1)) β© (((π + 1) + 1)...π))) = ((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π)))) |
127 | 4, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β ((1...(π + 1)) β© (((π + 1) + 1)...π))) = ((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π)))) |
128 | | fzdisj 13468 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π + 1) < ((π + 1) + 1) β ((1...(π + 1)) β© (((π + 1) + 1)...π)) = β
) |
129 | 39, 128 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((1...(π + 1)) β© (((π + 1) + 1)...π)) = β
) |
130 | 129 | imaeq2d 6013 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π β ((1...(π + 1)) β© (((π + 1) + 1)...π))) = (π β β
)) |
131 | 130, 81 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β ((1...(π + 1)) β© (((π + 1) + 1)...π))) = β
) |
132 | 127, 131 | eqtr3d 2778 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π))) = β
) |
133 | | fnun 6614 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β
(1...(π + 1))) Γ {1})
Fn (π β (1...(π + 1))) β§ ((π β (((π + 1) + 1)...π)) Γ {0}) Fn (π β (((π + 1) + 1)...π))) β§ ((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π))) = β
) β (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})) Fn ((π β (1...(π + 1))) βͺ (π β (((π + 1) + 1)...π)))) |
134 | 125, 132,
133 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})) Fn ((π β (1...(π + 1))) βͺ (π β (((π + 1) + 1)...π)))) |
135 | | imaundi 6102 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((1...(π + 1)) βͺ (((π + 1) + 1)...π))) = ((π β (1...(π + 1))) βͺ (π β (((π + 1) + 1)...π))) |
136 | 17 | imaeq2d 6013 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π β (1...π)) = (π β ((1...(π + 1)) βͺ (((π + 1) + 1)...π)))) |
137 | 136, 104 | eqtr3d 2778 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β ((1...(π + 1)) βͺ (((π + 1) + 1)...π))) = (1...π)) |
138 | 135, 137 | eqtr3id 2790 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π β (1...(π + 1))) βͺ (π β (((π + 1) + 1)...π))) = (1...π)) |
139 | 138 | fneq2d 6596 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})) Fn ((π β (1...(π + 1))) βͺ (π β (((π + 1) + 1)...π))) β (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})) Fn (1...π))) |
140 | 134, 139 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (π β (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})) Fn (1...π)) |
141 | 140 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β (1...π))) β (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})) Fn (1...π)) |
142 | | uzid 12778 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β€ β π β
(β€β₯βπ)) |
143 | 26, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β (β€β₯βπ)) |
144 | | peano2uz 12826 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β
(β€β₯βπ) β (π + 1) β
(β€β₯βπ)) |
145 | 143, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π + 1) β
(β€β₯βπ)) |
146 | | fzss2 13481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π + 1) β
(β€β₯βπ) β (1...π) β (1...(π + 1))) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...π) β (1...(π + 1))) |
148 | | imass2 6054 |
. . . . . . . . . . . . . . . . . . . 20
β’
((1...π) β
(1...(π + 1)) β (π β (1...π)) β (π β (1...(π + 1)))) |
149 | 147, 148 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β (1...π)) β (π β (1...(π + 1)))) |
150 | 149 | sselda 3944 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π β (1...π))) β π β (π β (1...(π + 1)))) |
151 | | fvun1 6932 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β (1...(π + 1))) Γ {1}) Fn (π β (1...(π + 1))) β§ ((π β (((π + 1) + 1)...π)) Γ {0}) Fn (π β (((π + 1) + 1)...π)) β§ (((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π))) = β
β§ π β (π β (1...(π + 1))))) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = (((π β (1...(π + 1))) Γ {1})βπ)) |
152 | 122, 124,
151 | mp3an12 1451 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π))) = β
β§ π β (π β (1...(π + 1)))) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = (((π β (1...(π + 1))) Γ {1})βπ)) |
153 | 132, 152 | sylan 580 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π β (1...(π + 1)))) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = (((π β (1...(π + 1))) Γ {1})βπ)) |
154 | 69 | fvconst2 7153 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β (1...(π + 1))) β (((π β (1...(π + 1))) Γ {1})βπ) = 1) |
155 | 154 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π β (1...(π + 1)))) β (((π β (1...(π + 1))) Γ {1})βπ) = 1) |
156 | 153, 155 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π β (1...(π + 1)))) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = 1) |
157 | 150, 156 | syldan 591 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π β (1...π))) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = 1) |
158 | 157 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π β (1...π))) β§ π β (1...π)) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = 1) |
159 | 68, 141, 110, 110, 111, 112, 158 | ofval 7628 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π β (1...π))) β§ π β (1...π)) β ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ) = ((πβπ) + 1)) |
160 | 120, 159 | eqtr4d 2779 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π β (1...π))) β§ π β (1...π)) β ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ) = ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ)) |
161 | 65, 160 | mpdan 685 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π β (1...π))) β ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ) = ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ)) |
162 | | imassrn 6024 |
. . . . . . . . . . . . . . . 16
β’ (π β (((π + 1) + 1)...π)) β ran π |
163 | 162, 63 | sstrid 3955 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (((π + 1) + 1)...π)) β (1...π)) |
164 | 163 | sselda 3944 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π β (((π + 1) + 1)...π))) β π β (1...π)) |
165 | 67 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β (((π + 1) + 1)...π))) β π Fn (1...π)) |
166 | 108 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β (((π + 1) + 1)...π))) β (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) Fn (1...π)) |
167 | | fzfid 13878 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β (((π + 1) + 1)...π))) β (1...π) β Fin) |
168 | | eqidd 2737 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π β (((π + 1) + 1)...π))) β§ π β (1...π)) β (πβπ) = (πβπ)) |
169 | | uzid 12778 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π + 1) β β€ β
(π + 1) β
(β€β₯β(π + 1))) |
170 | 29, 169 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π + 1) β
(β€β₯β(π + 1))) |
171 | | peano2uz 12826 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π + 1) β
(β€β₯β(π + 1)) β ((π + 1) + 1) β
(β€β₯β(π + 1))) |
172 | 170, 171 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((π + 1) + 1) β
(β€β₯β(π + 1))) |
173 | | fzss1 13480 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π + 1) + 1) β
(β€β₯β(π + 1)) β (((π + 1) + 1)...π) β ((π + 1)...π)) |
174 | 172, 173 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (((π + 1) + 1)...π) β ((π + 1)...π)) |
175 | | imass2 6054 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π + 1) + 1)...π) β ((π + 1)...π) β (π β (((π + 1) + 1)...π)) β (π β ((π + 1)...π))) |
176 | 174, 175 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β (((π + 1) + 1)...π)) β (π β ((π + 1)...π))) |
177 | 176 | sselda 3944 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π β (((π + 1) + 1)...π))) β π β (π β ((π + 1)...π))) |
178 | | fvun2 6933 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β (1...π)) Γ {1}) Fn (π β (1...π)) β§ ((π β ((π + 1)...π)) Γ {0}) Fn (π β ((π + 1)...π)) β§ (((π β (1...π)) β© (π β ((π + 1)...π))) = β
β§ π β (π β ((π + 1)...π)))) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = (((π β ((π + 1)...π)) Γ {0})βπ)) |
179 | 71, 74, 178 | mp3an12 1451 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β (1...π)) β© (π β ((π + 1)...π))) = β
β§ π β (π β ((π + 1)...π))) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = (((π β ((π + 1)...π)) Γ {0})βπ)) |
180 | 83, 179 | sylan 580 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π β ((π + 1)...π))) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = (((π β ((π + 1)...π)) Γ {0})βπ)) |
181 | 72 | fvconst2 7153 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β ((π + 1)...π)) β (((π β ((π + 1)...π)) Γ {0})βπ) = 0) |
182 | 181 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π β ((π + 1)...π))) β (((π β ((π + 1)...π)) Γ {0})βπ) = 0) |
183 | 180, 182 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π β ((π + 1)...π))) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = 0) |
184 | 177, 183 | syldan 591 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π β (((π + 1) + 1)...π))) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = 0) |
185 | 184 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π β (((π + 1) + 1)...π))) β§ π β (1...π)) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = 0) |
186 | 165, 166,
167, 167, 111, 168, 185 | ofval 7628 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π β (((π + 1) + 1)...π))) β§ π β (1...π)) β ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ) = ((πβπ) + 0)) |
187 | 140 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β (((π + 1) + 1)...π))) β (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})) Fn (1...π)) |
188 | | fvun2 6933 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β (1...(π + 1))) Γ {1}) Fn (π β (1...(π + 1))) β§ ((π β (((π + 1) + 1)...π)) Γ {0}) Fn (π β (((π + 1) + 1)...π)) β§ (((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π))) = β
β§ π β (π β (((π + 1) + 1)...π)))) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = (((π β (((π + 1) + 1)...π)) Γ {0})βπ)) |
189 | 122, 124,
188 | mp3an12 1451 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π))) = β
β§ π β (π β (((π + 1) + 1)...π))) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = (((π β (((π + 1) + 1)...π)) Γ {0})βπ)) |
190 | 132, 189 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π β (((π + 1) + 1)...π))) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = (((π β (((π + 1) + 1)...π)) Γ {0})βπ)) |
191 | 72 | fvconst2 7153 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β (((π + 1) + 1)...π)) β (((π β (((π + 1) + 1)...π)) Γ {0})βπ) = 0) |
192 | 191 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π β (((π + 1) + 1)...π))) β (((π β (((π + 1) + 1)...π)) Γ {0})βπ) = 0) |
193 | 190, 192 | eqtrd 2776 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π β (((π + 1) + 1)...π))) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = 0) |
194 | 193 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π β (((π + 1) + 1)...π))) β§ π β (1...π)) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = 0) |
195 | 165, 187,
167, 167, 111, 168, 194 | ofval 7628 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π β (((π + 1) + 1)...π))) β§ π β (1...π)) β ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ) = ((πβπ) + 0)) |
196 | 186, 195 | eqtr4d 2779 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π β (((π + 1) + 1)...π))) β§ π β (1...π)) β ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ) = ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ)) |
197 | 164, 196 | mpdan 685 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π β (((π + 1) + 1)...π))) β ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ) = ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ)) |
198 | 161, 197 | jaodan 956 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (π β (1...π)) β¨ π β (π β (((π + 1) + 1)...π)))) β ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ) = ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ)) |
199 | 198 | adantlr 713 |
. . . . . . . . . . 11
β’ (((π β§ π < π) β§ (π β (π β (1...π)) β¨ π β (π β (((π + 1) + 1)...π)))) β ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ) = ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ)) |
200 | | poimirlem2.1 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))))) |
201 | 200 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < π) β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))))) |
202 | | vex 3449 |
. . . . . . . . . . . . . . . . 17
β’ π¦ β V |
203 | | ovex 7390 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ + 1) β V |
204 | 202, 203 | ifex 4536 |
. . . . . . . . . . . . . . . 16
β’ if(π¦ < π, π¦, (π¦ + 1)) β V |
205 | 204 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π < π) β§ π¦ = (π β 1)) β if(π¦ < π, π¦, (π¦ + 1)) β V) |
206 | | breq1 5108 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = (π β 1) β (π¦ < π β (π β 1) < π)) |
207 | 206 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ = (π β 1)) β (π¦ < π β (π β 1) < π)) |
208 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ = (π β 1)) β π¦ = (π β 1)) |
209 | | oveq1 7364 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ = (π β 1) β (π¦ + 1) = ((π β 1) + 1)) |
210 | 26 | zcnd 12608 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β β) |
211 | | npcan1 11580 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β ((π β 1) + 1) = π) |
212 | 210, 211 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((π β 1) + 1) = π) |
213 | 209, 212 | sylan9eqr 2798 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π¦ = (π β 1)) β (π¦ + 1) = π) |
214 | 207, 208,
213 | ifbieq12d 4514 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π¦ = (π β 1)) β if(π¦ < π, π¦, (π¦ + 1)) = if((π β 1) < π, (π β 1), π)) |
215 | 214 | adantlr 713 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π < π) β§ π¦ = (π β 1)) β if(π¦ < π, π¦, (π¦ + 1)) = if((π β 1) < π, (π β 1), π)) |
216 | | poimirlem2.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β ((0...π) β {π})) |
217 | 216 | eldifad 3922 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β (0...π)) |
218 | 217 | elfzelzd 13442 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β β€) |
219 | | zltlem1 12556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β β€ β§ π β β€) β (π < π β π β€ (π β 1))) |
220 | 218, 26, 219 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π < π β π β€ (π β 1))) |
221 | 218 | zred 12607 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β β) |
222 | | peano2zm 12546 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β€ β (π β 1) β
β€) |
223 | 26, 222 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π β 1) β β€) |
224 | 223 | zred 12607 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π β 1) β β) |
225 | 221, 224 | lenltd 11301 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π β€ (π β 1) β Β¬ (π β 1) < π)) |
226 | 220, 225 | bitrd 278 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π < π β Β¬ (π β 1) < π)) |
227 | 226 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π < π) β Β¬ (π β 1) < π) |
228 | 227 | iffalsed 4497 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π < π) β if((π β 1) < π, (π β 1), π) = π) |
229 | 228 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π < π) β§ π¦ = (π β 1)) β if((π β 1) < π, (π β 1), π) = π) |
230 | 215, 229 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π < π) β§ π¦ = (π β 1)) β if(π¦ < π, π¦, (π¦ + 1)) = π) |
231 | 230 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π < π) β§ π¦ = (π β 1)) β (π = if(π¦ < π, π¦, (π¦ + 1)) β π = π)) |
232 | 231 | biimpa 477 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π < π) β§ π¦ = (π β 1)) β§ π = if(π¦ < π, π¦, (π¦ + 1))) β π = π) |
233 | | oveq2 7365 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (1...π) = (1...π)) |
234 | 233 | imaeq2d 6013 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π β (1...π)) = (π β (1...π))) |
235 | 234 | xpeq1d 5662 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((π β (1...π)) Γ {1}) = ((π β (1...π)) Γ {1})) |
236 | | oveq1 7364 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π + 1) = (π + 1)) |
237 | 236 | oveq1d 7372 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((π + 1)...π) = ((π + 1)...π)) |
238 | 237 | imaeq2d 6013 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π β ((π + 1)...π)) = (π β ((π + 1)...π))) |
239 | 238 | xpeq1d 5662 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((π β ((π + 1)...π)) Γ {0}) = ((π β ((π + 1)...π)) Γ {0})) |
240 | 235, 239 | uneq12d 4124 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) = (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) |
241 | 240 | oveq2d 7373 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))) |
242 | 232, 241 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π < π) β§ π¦ = (π β 1)) β§ π = if(π¦ < π, π¦, (π¦ + 1))) β (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))) |
243 | 205, 242 | csbied 3893 |
. . . . . . . . . . . . . 14
β’ (((π β§ π < π) β§ π¦ = (π β 1)) β β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))) |
244 | | elfzm1b 13519 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β€ β§ π β β€) β (π β (1...π) β (π β 1) β (0...(π β 1)))) |
245 | 26, 87, 244 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β (1...π) β (π β 1) β (0...(π β 1)))) |
246 | 97, 245 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (π β (π β 1) β (0...(π β 1))) |
247 | 246 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < π) β (π β 1) β (0...(π β 1))) |
248 | | ovexd 7392 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < π) β (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) β V) |
249 | 201, 243,
247, 248 | fvmptd 6955 |
. . . . . . . . . . . . 13
β’ ((π β§ π < π) β (πΉβ(π β 1)) = (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))) |
250 | 249 | fveq1d 6844 |
. . . . . . . . . . . 12
β’ ((π β§ π < π) β ((πΉβ(π β 1))βπ) = ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ)) |
251 | 250 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ π < π) β§ (π β (π β (1...π)) β¨ π β (π β (((π + 1) + 1)...π)))) β ((πΉβ(π β 1))βπ) = ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ)) |
252 | 204 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π < π) β§ π¦ = π) β if(π¦ < π, π¦, (π¦ + 1)) β V) |
253 | | breq1 5108 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π β (π¦ < π β π < π)) |
254 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π β π¦ = π) |
255 | | oveq1 7364 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π β (π¦ + 1) = (π + 1)) |
256 | 253, 254,
255 | ifbieq12d 4514 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π β if(π¦ < π, π¦, (π¦ + 1)) = if(π < π, π, (π + 1))) |
257 | | ltnsym 11253 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ π β β) β (π < π β Β¬ π < π)) |
258 | 221, 27, 257 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π < π β Β¬ π < π)) |
259 | 258 | imp 407 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π < π) β Β¬ π < π) |
260 | 259 | iffalsed 4497 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π < π) β if(π < π, π, (π + 1)) = (π + 1)) |
261 | 256, 260 | sylan9eqr 2798 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π < π) β§ π¦ = π) β if(π¦ < π, π¦, (π¦ + 1)) = (π + 1)) |
262 | 261 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π < π) β§ π¦ = π) β (π = if(π¦ < π, π¦, (π¦ + 1)) β π = (π + 1))) |
263 | 262 | biimpa 477 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π < π) β§ π¦ = π) β§ π = if(π¦ < π, π¦, (π¦ + 1))) β π = (π + 1)) |
264 | | oveq2 7365 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π + 1) β (1...π) = (1...(π + 1))) |
265 | 264 | imaeq2d 6013 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + 1) β (π β (1...π)) = (π β (1...(π + 1)))) |
266 | 265 | xpeq1d 5662 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + 1) β ((π β (1...π)) Γ {1}) = ((π β (1...(π + 1))) Γ {1})) |
267 | | oveq1 7364 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π + 1) β (π + 1) = ((π + 1) + 1)) |
268 | 267 | oveq1d 7372 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π + 1) β ((π + 1)...π) = (((π + 1) + 1)...π)) |
269 | 268 | imaeq2d 6013 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + 1) β (π β ((π + 1)...π)) = (π β (((π + 1) + 1)...π))) |
270 | 269 | xpeq1d 5662 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + 1) β ((π β ((π + 1)...π)) Γ {0}) = ((π β (((π + 1) + 1)...π)) Γ {0})) |
271 | 266, 270 | uneq12d 4124 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) = (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))) |
272 | 271 | oveq2d 7373 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))) |
273 | 263, 272 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π < π) β§ π¦ = π) β§ π = if(π¦ < π, π¦, (π¦ + 1))) β (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))) |
274 | 252, 273 | csbied 3893 |
. . . . . . . . . . . . . 14
β’ (((π β§ π < π) β§ π¦ = π) β β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))) |
275 | | fz1ssfz0 13537 |
. . . . . . . . . . . . . . . 16
β’
(1...(π β 1))
β (0...(π β
1)) |
276 | 275, 7 | sselid 3942 |
. . . . . . . . . . . . . . 15
β’ (π β π β (0...(π β 1))) |
277 | 276 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < π) β π β (0...(π β 1))) |
278 | | ovexd 7392 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < π) β (π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))) β V) |
279 | 201, 274,
277, 278 | fvmptd 6955 |
. . . . . . . . . . . . 13
β’ ((π β§ π < π) β (πΉβπ) = (π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))) |
280 | 279 | fveq1d 6844 |
. . . . . . . . . . . 12
β’ ((π β§ π < π) β ((πΉβπ)βπ) = ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ)) |
281 | 280 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ π < π) β§ (π β (π β (1...π)) β¨ π β (π β (((π + 1) + 1)...π)))) β ((πΉβπ)βπ) = ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ)) |
282 | 199, 251,
281 | 3eqtr4d 2786 |
. . . . . . . . . 10
β’ (((π β§ π < π) β§ (π β (π β (1...π)) β¨ π β (π β (((π + 1) + 1)...π)))) β ((πΉβ(π β 1))βπ) = ((πΉβπ)βπ)) |
283 | 282 | ex 413 |
. . . . . . . . 9
β’ ((π β§ π < π) β ((π β (π β (1...π)) β¨ π β (π β (((π + 1) + 1)...π))) β ((πΉβ(π β 1))βπ) = ((πΉβπ)βπ))) |
284 | 59, 283 | sylbid 239 |
. . . . . . . 8
β’ ((π β§ π < π) β ((π β (π β (1...π)) β§ Β¬ π β (π β {(π + 1)})) β ((πΉβ(π β 1))βπ) = ((πΉβπ)βπ))) |
285 | 284 | expdimp 453 |
. . . . . . 7
β’ (((π β§ π < π) β§ π β (π β (1...π))) β (Β¬ π β (π β {(π + 1)}) β ((πΉβ(π β 1))βπ) = ((πΉβπ)βπ))) |
286 | 285 | necon1ad 2960 |
. . . . . 6
β’ (((π β§ π < π) β§ π β (π β (1...π))) β (((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π β (π β {(π + 1)}))) |
287 | | elimasni 6043 |
. . . . . . . 8
β’ (π β (π β {(π + 1)}) β (π + 1)ππ) |
288 | | eqcom 2743 |
. . . . . . . . 9
β’ (π = (πβ(π + 1)) β (πβ(π + 1)) = π) |
289 | | f1ofn 6785 |
. . . . . . . . . . 11
β’ (π:(1...π)β1-1-ontoβ(1...π) β π Fn (1...π)) |
290 | 1, 289 | syl 17 |
. . . . . . . . . 10
β’ (π β π Fn (1...π)) |
291 | | fnbrfvb 6895 |
. . . . . . . . . 10
β’ ((π Fn (1...π) β§ (π + 1) β (1...π)) β ((πβ(π + 1)) = π β (π + 1)ππ)) |
292 | 290, 15, 291 | syl2anc 584 |
. . . . . . . . 9
β’ (π β ((πβ(π + 1)) = π β (π + 1)ππ)) |
293 | 288, 292 | bitrid 282 |
. . . . . . . 8
β’ (π β (π = (πβ(π + 1)) β (π + 1)ππ)) |
294 | 287, 293 | syl5ibr 245 |
. . . . . . 7
β’ (π β (π β (π β {(π + 1)}) β π = (πβ(π + 1)))) |
295 | 294 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ π < π) β§ π β (π β (1...π))) β (π β (π β {(π + 1)}) β π = (πβ(π + 1)))) |
296 | 286, 295 | syld 47 |
. . . . 5
β’ (((π β§ π < π) β§ π β (π β (1...π))) β (((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = (πβ(π + 1)))) |
297 | 296 | ralrimiva 3143 |
. . . 4
β’ ((π β§ π < π) β βπ β (π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = (πβ(π + 1)))) |
298 | | fvex 6855 |
. . . . 5
β’ (πβ(π + 1)) β V |
299 | | eqeq2 2748 |
. . . . . . 7
β’ (π = (πβ(π + 1)) β (π = π β π = (πβ(π + 1)))) |
300 | 299 | imbi2d 340 |
. . . . . 6
β’ (π = (πβ(π + 1)) β ((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = π) β (((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = (πβ(π + 1))))) |
301 | 300 | ralbidv 3174 |
. . . . 5
β’ (π = (πβ(π + 1)) β (βπ β (π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = π) β βπ β (π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = (πβ(π + 1))))) |
302 | 298, 301 | spcev 3565 |
. . . 4
β’
(βπ β
(π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = (πβ(π + 1))) β βπβπ β (π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = π)) |
303 | 297, 302 | syl 17 |
. . 3
β’ ((π β§ π < π) β βπβπ β (π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = π)) |
304 | | imadif 6585 |
. . . . . . . . . . . . . . 15
β’ (Fun
β‘π β (π β ((1...π) β {π})) = ((π β (1...π)) β (π β {π}))) |
305 | 4, 304 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π β ((1...π) β {π})) = ((π β (1...π)) β (π β {π}))) |
306 | 99 | difeq1d 4081 |
. . . . . . . . . . . . . . . 16
β’ (π β ((1...π) β {π}) = (((1...π) βͺ ((π + 1)...π)) β {π})) |
307 | | difundir 4240 |
. . . . . . . . . . . . . . . . 17
β’
(((1...π) βͺ
((π + 1)...π)) β {π}) = (((1...π) β {π}) βͺ (((π + 1)...π) β {π})) |
308 | 212, 21 | eqeltrd 2837 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((π β 1) + 1) β
(β€β₯β1)) |
309 | | uzid 12778 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β 1) β β€
β (π β 1) β
(β€β₯β(π β 1))) |
310 | 223, 309 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π β 1) β
(β€β₯β(π β 1))) |
311 | | peano2uz 12826 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β 1) β
(β€β₯β(π β 1)) β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
312 | 310, 311 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
313 | 212, 312 | eqeltrrd 2838 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β (β€β₯β(π β 1))) |
314 | | fzsplit2 13466 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β 1) + 1) β
(β€β₯β1) β§ π β (β€β₯β(π β 1))) β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
315 | 308, 313,
314 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
316 | 212 | oveq1d 7372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (((π β 1) + 1)...π) = (π...π)) |
317 | | fzsn 13483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β€ β (π...π) = {π}) |
318 | 26, 317 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π...π) = {π}) |
319 | 316, 318 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (((π β 1) + 1)...π) = {π}) |
320 | 319 | uneq2d 4123 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((1...(π β 1)) βͺ (((π β 1) + 1)...π)) = ((1...(π β 1)) βͺ {π})) |
321 | 315, 320 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...π) = ((1...(π β 1)) βͺ {π})) |
322 | 321 | difeq1d 4081 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((1...π) β {π}) = (((1...(π β 1)) βͺ {π}) β {π})) |
323 | | difun2 4440 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((1...(π β
1)) βͺ {π}) β
{π}) = ((1...(π β 1)) β {π}) |
324 | 27 | ltm1d 12087 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π β 1) < π) |
325 | 224, 27 | ltnled 11302 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((π β 1) < π β Β¬ π β€ (π β 1))) |
326 | 324, 325 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β Β¬ π β€ (π β 1)) |
327 | | elfzle2 13445 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1...(π β 1)) β π β€ (π β 1)) |
328 | 326, 327 | nsyl 140 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Β¬ π β (1...(π β 1))) |
329 | | difsn 4758 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Β¬
π β (1...(π β 1)) β ((1...(π β 1)) β {π}) = (1...(π β 1))) |
330 | 328, 329 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((1...(π β 1)) β {π}) = (1...(π β 1))) |
331 | 323, 330 | eqtrid 2788 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (((1...(π β 1)) βͺ {π}) β {π}) = (1...(π β 1))) |
332 | 322, 331 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((1...π) β {π}) = (1...(π β 1))) |
333 | | elfzle1 13444 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π + 1)...π) β (π + 1) β€ π) |
334 | 32, 333 | nsyl 140 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Β¬ π β ((π + 1)...π)) |
335 | | difsn 4758 |
. . . . . . . . . . . . . . . . . . 19
β’ (Β¬
π β ((π + 1)...π) β (((π + 1)...π) β {π}) = ((π + 1)...π)) |
336 | 334, 335 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((π + 1)...π) β {π}) = ((π + 1)...π)) |
337 | 332, 336 | uneq12d 4124 |
. . . . . . . . . . . . . . . . 17
β’ (π β (((1...π) β {π}) βͺ (((π + 1)...π) β {π})) = ((1...(π β 1)) βͺ ((π + 1)...π))) |
338 | 307, 337 | eqtrid 2788 |
. . . . . . . . . . . . . . . 16
β’ (π β (((1...π) βͺ ((π + 1)...π)) β {π}) = ((1...(π β 1)) βͺ ((π + 1)...π))) |
339 | 306, 338 | eqtrd 2776 |
. . . . . . . . . . . . . . 15
β’ (π β ((1...π) β {π}) = ((1...(π β 1)) βͺ ((π + 1)...π))) |
340 | 339 | imaeq2d 6013 |
. . . . . . . . . . . . . 14
β’ (π β (π β ((1...π) β {π})) = (π β ((1...(π β 1)) βͺ ((π + 1)...π)))) |
341 | 305, 340 | eqtr3d 2778 |
. . . . . . . . . . . . 13
β’ (π β ((π β (1...π)) β (π β {π})) = (π β ((1...(π β 1)) βͺ ((π + 1)...π)))) |
342 | | imaundi 6102 |
. . . . . . . . . . . . 13
β’ (π β ((1...(π β 1)) βͺ ((π + 1)...π))) = ((π β (1...(π β 1))) βͺ (π β ((π + 1)...π))) |
343 | 341, 342 | eqtrdi 2792 |
. . . . . . . . . . . 12
β’ (π β ((π β (1...π)) β (π β {π})) = ((π β (1...(π β 1))) βͺ (π β ((π + 1)...π)))) |
344 | 343 | eleq2d 2823 |
. . . . . . . . . . 11
β’ (π β (π β ((π β (1...π)) β (π β {π})) β π β ((π β (1...(π β 1))) βͺ (π β ((π + 1)...π))))) |
345 | | eldif 3920 |
. . . . . . . . . . 11
β’ (π β ((π β (1...π)) β (π β {π})) β (π β (π β (1...π)) β§ Β¬ π β (π β {π}))) |
346 | | elun 4108 |
. . . . . . . . . . 11
β’ (π β ((π β (1...(π β 1))) βͺ (π β ((π + 1)...π))) β (π β (π β (1...(π β 1))) β¨ π β (π β ((π + 1)...π)))) |
347 | 344, 345,
346 | 3bitr3g 312 |
. . . . . . . . . 10
β’ (π β ((π β (π β (1...π)) β§ Β¬ π β (π β {π})) β (π β (π β (1...(π β 1))) β¨ π β (π β ((π + 1)...π))))) |
348 | 347 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π < π) β ((π β (π β (1...π)) β§ Β¬ π β (π β {π})) β (π β (π β (1...(π β 1))) β¨ π β (π β ((π + 1)...π))))) |
349 | | imassrn 6024 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...(π β 1))) β ran π |
350 | 349, 63 | sstrid 3955 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (1...(π β 1))) β (1...π)) |
351 | 350 | sselda 3944 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π β (1...(π β 1)))) β π β (1...π)) |
352 | 67 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β (1...(π β 1)))) β π Fn (1...π)) |
353 | | fnconstg 6730 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1 β
V β ((π β
(1...(π β 1)))
Γ {1}) Fn (π β
(1...(π β
1)))) |
354 | 69, 353 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (1...(π β 1))) Γ {1}) Fn (π β (1...(π β 1))) |
355 | | fnconstg 6730 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (0 β
V β ((π β (π...π)) Γ {0}) Fn (π β (π...π))) |
356 | 72, 355 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (π...π)) Γ {0}) Fn (π β (π...π)) |
357 | 354, 356 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β (1...(π β 1))) Γ {1}) Fn (π β (1...(π β 1))) β§ ((π β (π...π)) Γ {0}) Fn (π β (π...π))) |
358 | | imain 6586 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (Fun
β‘π β (π β ((1...(π β 1)) β© (π...π))) = ((π β (1...(π β 1))) β© (π β (π...π)))) |
359 | 4, 358 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β ((1...(π β 1)) β© (π...π))) = ((π β (1...(π β 1))) β© (π β (π...π)))) |
360 | | fzdisj 13468 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β 1) < π β ((1...(π β 1)) β© (π...π)) = β
) |
361 | 324, 360 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((1...(π β 1)) β© (π...π)) = β
) |
362 | 361 | imaeq2d 6013 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π β ((1...(π β 1)) β© (π...π))) = (π β β
)) |
363 | 362, 81 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β ((1...(π β 1)) β© (π...π))) = β
) |
364 | 359, 363 | eqtr3d 2778 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π β (1...(π β 1))) β© (π β (π...π))) = β
) |
365 | | fnun 6614 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β
(1...(π β 1)))
Γ {1}) Fn (π β
(1...(π β 1))) β§
((π β (π...π)) Γ {0}) Fn (π β (π...π))) β§ ((π β (1...(π β 1))) β© (π β (π...π))) = β
) β (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})) Fn ((π β (1...(π β 1))) βͺ (π β (π...π)))) |
366 | 357, 364,
365 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})) Fn ((π β (1...(π β 1))) βͺ (π β (π...π)))) |
367 | | imaundi 6102 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((1...(π β 1)) βͺ (π...π))) = ((π β (1...(π β 1))) βͺ (π β (π...π))) |
368 | | uzss 12786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β
(β€β₯β(π β 1)) β
(β€β₯βπ) β
(β€β₯β(π β 1))) |
369 | 313, 368 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β
(β€β₯βπ) β
(β€β₯β(π β 1))) |
370 | | elfzuz3 13438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (1...(π β 1)) β (π β 1) β
(β€β₯βπ)) |
371 | 7, 370 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (π β 1) β
(β€β₯βπ)) |
372 | 369, 371 | sseldd 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (π β 1) β
(β€β₯β(π β 1))) |
373 | | peano2uz 12826 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β 1) β
(β€β₯β(π β 1)) β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
374 | 372, 373 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
375 | 13, 374 | eqeltrrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β (β€β₯β(π β 1))) |
376 | | fzsplit2 13466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β 1) + 1) β
(β€β₯β1) β§ π β (β€β₯β(π β 1))) β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
377 | 308, 375,
376 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
378 | 212 | oveq1d 7372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (((π β 1) + 1)...π) = (π...π)) |
379 | 378 | uneq2d 4123 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((1...(π β 1)) βͺ (((π β 1) + 1)...π)) = ((1...(π β 1)) βͺ (π...π))) |
380 | 377, 379 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (1...π) = ((1...(π β 1)) βͺ (π...π))) |
381 | 380 | imaeq2d 6013 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π β (1...π)) = (π β ((1...(π β 1)) βͺ (π...π)))) |
382 | 381, 104 | eqtr3d 2778 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β ((1...(π β 1)) βͺ (π...π))) = (1...π)) |
383 | 367, 382 | eqtr3id 2790 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π β (1...(π β 1))) βͺ (π β (π...π))) = (1...π)) |
384 | 383 | fneq2d 6596 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})) Fn ((π β (1...(π β 1))) βͺ (π β (π...π))) β (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})) Fn (1...π))) |
385 | 366, 384 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ (π β (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})) Fn (1...π)) |
386 | 385 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β (1...(π β 1)))) β (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})) Fn (1...π)) |
387 | | fzfid 13878 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β (1...(π β 1)))) β (1...π) β Fin) |
388 | | eqidd 2737 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π β (1...(π β 1)))) β§ π β (1...π)) β (πβπ) = (πβπ)) |
389 | | fvun1 6932 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β (1...(π β 1))) Γ {1}) Fn (π β (1...(π β 1))) β§ ((π β (π...π)) Γ {0}) Fn (π β (π...π)) β§ (((π β (1...(π β 1))) β© (π β (π...π))) = β
β§ π β (π β (1...(π β 1))))) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = (((π β (1...(π β 1))) Γ {1})βπ)) |
390 | 354, 356,
389 | mp3an12 1451 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β (1...(π β 1))) β© (π β (π...π))) = β
β§ π β (π β (1...(π β 1)))) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = (((π β (1...(π β 1))) Γ {1})βπ)) |
391 | 364, 390 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π β (1...(π β 1)))) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = (((π β (1...(π β 1))) Γ {1})βπ)) |
392 | 69 | fvconst2 7153 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β (1...(π β 1))) β (((π β (1...(π β 1))) Γ {1})βπ) = 1) |
393 | 392 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π β (1...(π β 1)))) β (((π β (1...(π β 1))) Γ {1})βπ) = 1) |
394 | 391, 393 | eqtrd 2776 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π β (1...(π β 1)))) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = 1) |
395 | 394 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π β (1...(π β 1)))) β§ π β (1...π)) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = 1) |
396 | 352, 386,
387, 387, 111, 388, 395 | ofval 7628 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π β (1...(π β 1)))) β§ π β (1...π)) β ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ) = ((πβπ) + 1)) |
397 | 108 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β (1...(π β 1)))) β (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) Fn (1...π)) |
398 | | fzss2 13481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(β€β₯β(π β 1)) β (1...(π β 1)) β (1...π)) |
399 | 313, 398 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...(π β 1)) β (1...π)) |
400 | | imass2 6054 |
. . . . . . . . . . . . . . . . . . . 20
β’
((1...(π β 1))
β (1...π) β
(π β (1...(π β 1))) β (π β (1...π))) |
401 | 399, 400 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β (1...(π β 1))) β (π β (1...π))) |
402 | 401 | sselda 3944 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π β (1...(π β 1)))) β π β (π β (1...π))) |
403 | 402, 118 | syldan 591 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π β (1...(π β 1)))) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = 1) |
404 | 403 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π β (1...(π β 1)))) β§ π β (1...π)) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = 1) |
405 | 352, 397,
387, 387, 111, 388, 404 | ofval 7628 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π β (1...(π β 1)))) β§ π β (1...π)) β ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ) = ((πβπ) + 1)) |
406 | 396, 405 | eqtr4d 2779 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π β (1...(π β 1)))) β§ π β (1...π)) β ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ) = ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ)) |
407 | 351, 406 | mpdan 685 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π β (1...(π β 1)))) β ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ) = ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ)) |
408 | | imassrn 6024 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π + 1)...π)) β ran π |
409 | 408, 63 | sstrid 3955 |
. . . . . . . . . . . . . . 15
β’ (π β (π β ((π + 1)...π)) β (1...π)) |
410 | 409 | sselda 3944 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π β ((π + 1)...π))) β π β (1...π)) |
411 | 67 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β ((π + 1)...π))) β π Fn (1...π)) |
412 | 385 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β ((π + 1)...π))) β (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})) Fn (1...π)) |
413 | | fzfid 13878 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β ((π + 1)...π))) β (1...π) β Fin) |
414 | | eqidd 2737 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π β ((π + 1)...π))) β§ π β (1...π)) β (πβπ) = (πβπ)) |
415 | | fzss1 13480 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π + 1) β
(β€β₯βπ) β ((π + 1)...π) β (π...π)) |
416 | 145, 415 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π + 1)...π) β (π...π)) |
417 | | imass2 6054 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π + 1)...π) β (π...π) β (π β ((π + 1)...π)) β (π β (π...π))) |
418 | 416, 417 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β ((π + 1)...π)) β (π β (π...π))) |
419 | 418 | sselda 3944 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π β ((π + 1)...π))) β π β (π β (π...π))) |
420 | | fvun2 6933 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β (1...(π β 1))) Γ {1}) Fn (π β (1...(π β 1))) β§ ((π β (π...π)) Γ {0}) Fn (π β (π...π)) β§ (((π β (1...(π β 1))) β© (π β (π...π))) = β
β§ π β (π β (π...π)))) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = (((π β (π...π)) Γ {0})βπ)) |
421 | 354, 356,
420 | mp3an12 1451 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β (1...(π β 1))) β© (π β (π...π))) = β
β§ π β (π β (π...π))) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = (((π β (π...π)) Γ {0})βπ)) |
422 | 364, 421 | sylan 580 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π β (π...π))) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = (((π β (π...π)) Γ {0})βπ)) |
423 | 72 | fvconst2 7153 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β (π...π)) β (((π β (π...π)) Γ {0})βπ) = 0) |
424 | 423 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π β (π...π))) β (((π β (π...π)) Γ {0})βπ) = 0) |
425 | 422, 424 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π β (π...π))) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = 0) |
426 | 419, 425 | syldan 591 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π β ((π + 1)...π))) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = 0) |
427 | 426 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π β ((π + 1)...π))) β§ π β (1...π)) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = 0) |
428 | 411, 412,
413, 413, 111, 414, 427 | ofval 7628 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π β ((π + 1)...π))) β§ π β (1...π)) β ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ) = ((πβπ) + 0)) |
429 | 108 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π β ((π + 1)...π))) β (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) Fn (1...π)) |
430 | 183 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π β ((π + 1)...π))) β§ π β (1...π)) β ((((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))βπ) = 0) |
431 | 411, 429,
413, 413, 111, 414, 430 | ofval 7628 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π β ((π + 1)...π))) β§ π β (1...π)) β ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ) = ((πβπ) + 0)) |
432 | 428, 431 | eqtr4d 2779 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π β ((π + 1)...π))) β§ π β (1...π)) β ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ) = ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ)) |
433 | 410, 432 | mpdan 685 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π β ((π + 1)...π))) β ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ) = ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ)) |
434 | 407, 433 | jaodan 956 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (π β (1...(π β 1))) β¨ π β (π β ((π + 1)...π)))) β ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ) = ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ)) |
435 | 434 | adantlr 713 |
. . . . . . . . . . 11
β’ (((π β§ π < π) β§ (π β (π β (1...(π β 1))) β¨ π β (π β ((π + 1)...π)))) β ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ) = ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ)) |
436 | 200 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < π) β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))))) |
437 | 204 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π < π) β§ π¦ = (π β 1)) β if(π¦ < π, π¦, (π¦ + 1)) β V) |
438 | 214 | adantlr 713 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π < π) β§ π¦ = (π β 1)) β if(π¦ < π, π¦, (π¦ + 1)) = if((π β 1) < π, (π β 1), π)) |
439 | | lttr 11231 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β 1) β β β§
π β β β§
π β β) β
(((π β 1) < π β§ π < π) β (π β 1) < π)) |
440 | 224, 27, 221, 439 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (((π β 1) < π β§ π < π) β (π β 1) < π)) |
441 | 324, 440 | mpand 693 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π < π β (π β 1) < π)) |
442 | 441 | imp 407 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π < π) β (π β 1) < π) |
443 | 442 | iftrued 4494 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π < π) β if((π β 1) < π, (π β 1), π) = (π β 1)) |
444 | 443 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π < π) β§ π¦ = (π β 1)) β if((π β 1) < π, (π β 1), π) = (π β 1)) |
445 | 438, 444 | eqtrd 2776 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π < π) β§ π¦ = (π β 1)) β if(π¦ < π, π¦, (π¦ + 1)) = (π β 1)) |
446 | | simpll 765 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π < π) β§ π¦ = (π β 1)) β π) |
447 | | oveq2 7365 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π β 1) β (1...π) = (1...(π β 1))) |
448 | 447 | imaeq2d 6013 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π β 1) β (π β (1...π)) = (π β (1...(π β 1)))) |
449 | 448 | xpeq1d 5662 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π β 1) β ((π β (1...π)) Γ {1}) = ((π β (1...(π β 1))) Γ {1})) |
450 | 449 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π = (π β 1)) β ((π β (1...π)) Γ {1}) = ((π β (1...(π β 1))) Γ {1})) |
451 | | oveq1 7364 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π β 1) β (π + 1) = ((π β 1) + 1)) |
452 | 451, 212 | sylan9eqr 2798 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π = (π β 1)) β (π + 1) = π) |
453 | 452 | oveq1d 7372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π = (π β 1)) β ((π + 1)...π) = (π...π)) |
454 | 453 | imaeq2d 6013 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π = (π β 1)) β (π β ((π + 1)...π)) = (π β (π...π))) |
455 | 454 | xpeq1d 5662 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π = (π β 1)) β ((π β ((π + 1)...π)) Γ {0}) = ((π β (π...π)) Γ {0})) |
456 | 450, 455 | uneq12d 4124 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π = (π β 1)) β (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) = (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))) |
457 | 456 | oveq2d 7373 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π = (π β 1)) β (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))) |
458 | 446, 457 | sylan 580 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π < π) β§ π¦ = (π β 1)) β§ π = (π β 1)) β (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))) |
459 | 437, 445,
458 | csbied2 3895 |
. . . . . . . . . . . . . 14
β’ (((π β§ π < π) β§ π¦ = (π β 1)) β β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))) |
460 | 246 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < π) β (π β 1) β (0...(π β 1))) |
461 | | ovexd 7392 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < π) β (π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))) β V) |
462 | 436, 459,
460, 461 | fvmptd 6955 |
. . . . . . . . . . . . 13
β’ ((π β§ π < π) β (πΉβ(π β 1)) = (π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))) |
463 | 462 | fveq1d 6844 |
. . . . . . . . . . . 12
β’ ((π β§ π < π) β ((πΉβ(π β 1))βπ) = ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ)) |
464 | 463 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ π < π) β§ (π β (π β (1...(π β 1))) β¨ π β (π β ((π + 1)...π)))) β ((πΉβ(π β 1))βπ) = ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ)) |
465 | 204 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π < π β§ π¦ = π) β if(π¦ < π, π¦, (π¦ + 1)) β V) |
466 | | iftrue 4492 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π < π β if(π < π, π, (π + 1)) = π) |
467 | 256, 466 | sylan9eqr 2798 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π < π β§ π¦ = π) β if(π¦ < π, π¦, (π¦ + 1)) = π) |
468 | 467 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . 18
β’ ((π < π β§ π¦ = π) β (π = if(π¦ < π, π¦, (π¦ + 1)) β π = π)) |
469 | 468 | biimpa 477 |
. . . . . . . . . . . . . . . . 17
β’ (((π < π β§ π¦ = π) β§ π = if(π¦ < π, π¦, (π¦ + 1))) β π = π) |
470 | 469, 241 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π < π β§ π¦ = π) β§ π = if(π¦ < π, π¦, (π¦ + 1))) β (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))) |
471 | 465, 470 | csbied 3893 |
. . . . . . . . . . . . . . 15
β’ ((π < π β§ π¦ = π) β β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))) |
472 | 471 | adantll 712 |
. . . . . . . . . . . . . 14
β’ (((π β§ π < π) β§ π¦ = π) β β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))) |
473 | 276 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < π) β π β (0...(π β 1))) |
474 | | ovexd 7392 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < π) β (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) β V) |
475 | 436, 472,
473, 474 | fvmptd 6955 |
. . . . . . . . . . . . 13
β’ ((π β§ π < π) β (πΉβπ) = (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))) |
476 | 475 | fveq1d 6844 |
. . . . . . . . . . . 12
β’ ((π β§ π < π) β ((πΉβπ)βπ) = ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ)) |
477 | 476 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ π < π) β§ (π β (π β (1...(π β 1))) β¨ π β (π β ((π + 1)...π)))) β ((πΉβπ)βπ) = ((π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))βπ)) |
478 | 435, 464,
477 | 3eqtr4d 2786 |
. . . . . . . . . 10
β’ (((π β§ π < π) β§ (π β (π β (1...(π β 1))) β¨ π β (π β ((π + 1)...π)))) β ((πΉβ(π β 1))βπ) = ((πΉβπ)βπ)) |
479 | 478 | ex 413 |
. . . . . . . . 9
β’ ((π β§ π < π) β ((π β (π β (1...(π β 1))) β¨ π β (π β ((π + 1)...π))) β ((πΉβ(π β 1))βπ) = ((πΉβπ)βπ))) |
480 | 348, 479 | sylbid 239 |
. . . . . . . 8
β’ ((π β§ π < π) β ((π β (π β (1...π)) β§ Β¬ π β (π β {π})) β ((πΉβ(π β 1))βπ) = ((πΉβπ)βπ))) |
481 | 480 | expdimp 453 |
. . . . . . 7
β’ (((π β§ π < π) β§ π β (π β (1...π))) β (Β¬ π β (π β {π}) β ((πΉβ(π β 1))βπ) = ((πΉβπ)βπ))) |
482 | 481 | necon1ad 2960 |
. . . . . 6
β’ (((π β§ π < π) β§ π β (π β (1...π))) β (((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π β (π β {π}))) |
483 | | elimasni 6043 |
. . . . . . . 8
β’ (π β (π β {π}) β πππ) |
484 | | eqcom 2743 |
. . . . . . . . 9
β’ (π = (πβπ) β (πβπ) = π) |
485 | | fnbrfvb 6895 |
. . . . . . . . . 10
β’ ((π Fn (1...π) β§ π β (1...π)) β ((πβπ) = π β πππ)) |
486 | 290, 97, 485 | syl2anc 584 |
. . . . . . . . 9
β’ (π β ((πβπ) = π β πππ)) |
487 | 484, 486 | bitrid 282 |
. . . . . . . 8
β’ (π β (π = (πβπ) β πππ)) |
488 | 483, 487 | syl5ibr 245 |
. . . . . . 7
β’ (π β (π β (π β {π}) β π = (πβπ))) |
489 | 488 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ π < π) β§ π β (π β (1...π))) β (π β (π β {π}) β π = (πβπ))) |
490 | 482, 489 | syld 47 |
. . . . 5
β’ (((π β§ π < π) β§ π β (π β (1...π))) β (((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = (πβπ))) |
491 | 490 | ralrimiva 3143 |
. . . 4
β’ ((π β§ π < π) β βπ β (π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = (πβπ))) |
492 | | fvex 6855 |
. . . . 5
β’ (πβπ) β V |
493 | | eqeq2 2748 |
. . . . . . 7
β’ (π = (πβπ) β (π = π β π = (πβπ))) |
494 | 493 | imbi2d 340 |
. . . . . 6
β’ (π = (πβπ) β ((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = π) β (((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = (πβπ)))) |
495 | 494 | ralbidv 3174 |
. . . . 5
β’ (π = (πβπ) β (βπ β (π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = π) β βπ β (π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = (πβπ)))) |
496 | 492, 495 | spcev 3565 |
. . . 4
β’
(βπ β
(π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = (πβπ)) β βπβπ β (π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = π)) |
497 | 491, 496 | syl 17 |
. . 3
β’ ((π β§ π < π) β βπβπ β (π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = π)) |
498 | | eldifsni 4750 |
. . . . 5
β’ (π β ((0...π) β {π}) β π β π) |
499 | 216, 498 | syl 17 |
. . . 4
β’ (π β π β π) |
500 | 221, 27 | lttri2d 11294 |
. . . 4
β’ (π β (π β π β (π < π β¨ π < π))) |
501 | 499, 500 | mpbid 231 |
. . 3
β’ (π β (π < π β¨ π < π)) |
502 | 303, 497,
501 | mpjaodan 957 |
. 2
β’ (π β βπβπ β (π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = π)) |
503 | | nfv 1917 |
. . . 4
β’
β²π((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) |
504 | 503 | rmo2 3843 |
. . 3
β’
(β*π β
(π β (1...π))((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β βπβπ β (π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = π)) |
505 | | rmoeq1 3391 |
. . . 4
β’ ((π β (1...π)) = (1...π) β (β*π β (π β (1...π))((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β β*π β (1...π)((πΉβ(π β 1))βπ) β ((πΉβπ)βπ))) |
506 | 104, 505 | syl 17 |
. . 3
β’ (π β (β*π β (π β (1...π))((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β β*π β (1...π)((πΉβ(π β 1))βπ) β ((πΉβπ)βπ))) |
507 | 504, 506 | bitr3id 284 |
. 2
β’ (π β (βπβπ β (π β (1...π))(((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β π = π) β β*π β (1...π)((πΉβ(π β 1))βπ) β ((πΉβπ)βπ))) |
508 | 502, 507 | mpbid 231 |
1
β’ (π β β*π β (1...π)((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) |