Step | Hyp | Ref
| Expression |
1 | | poimirlem2.3 |
. . . . 5
β’ (π β π:(1...π)β1-1-ontoβ(1...π)) |
2 | | f1of 6789 |
. . . . 5
β’ (π:(1...π)β1-1-ontoβ(1...π) β π:(1...π)βΆ(1...π)) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β π:(1...π)βΆ(1...π)) |
4 | | poimir.0 |
. . . . . . . . 9
β’ (π β π β β) |
5 | 4 | nncnd 12176 |
. . . . . . . 8
β’ (π β π β β) |
6 | | npcan1 11587 |
. . . . . . . 8
β’ (π β β β ((π β 1) + 1) = π) |
7 | 5, 6 | syl 17 |
. . . . . . 7
β’ (π β ((π β 1) + 1) = π) |
8 | 4 | nnzd 12533 |
. . . . . . . 8
β’ (π β π β β€) |
9 | | peano2zm 12553 |
. . . . . . . 8
β’ (π β β€ β (π β 1) β
β€) |
10 | | uzid 12785 |
. . . . . . . 8
β’ ((π β 1) β β€
β (π β 1) β
(β€β₯β(π β 1))) |
11 | | peano2uz 12833 |
. . . . . . . 8
β’ ((π β 1) β
(β€β₯β(π β 1)) β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
12 | 8, 9, 10, 11 | 4syl 19 |
. . . . . . 7
β’ (π β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
13 | 7, 12 | eqeltrrd 2839 |
. . . . . 6
β’ (π β π β (β€β₯β(π β 1))) |
14 | | fzss2 13488 |
. . . . . 6
β’ (π β
(β€β₯β(π β 1)) β (1...(π β 1)) β (1...π)) |
15 | 13, 14 | syl 17 |
. . . . 5
β’ (π β (1...(π β 1)) β (1...π)) |
16 | | poimirlem1.4 |
. . . . 5
β’ (π β π β (1...(π β 1))) |
17 | 15, 16 | sseldd 3950 |
. . . 4
β’ (π β π β (1...π)) |
18 | 3, 17 | ffvelcdmd 7041 |
. . 3
β’ (π β (πβπ) β (1...π)) |
19 | | fzp1elp1 13501 |
. . . . . 6
β’ (π β (1...(π β 1)) β (π + 1) β (1...((π β 1) + 1))) |
20 | 16, 19 | syl 17 |
. . . . 5
β’ (π β (π + 1) β (1...((π β 1) + 1))) |
21 | 7 | oveq2d 7378 |
. . . . 5
β’ (π β (1...((π β 1) + 1)) = (1...π)) |
22 | 20, 21 | eleqtrd 2840 |
. . . 4
β’ (π β (π + 1) β (1...π)) |
23 | 3, 22 | ffvelcdmd 7041 |
. . 3
β’ (π β (πβ(π + 1)) β (1...π)) |
24 | | imassrn 6029 |
. . . . . . . . . 10
β’ (π β (π...(π + 1))) β ran π |
25 | | frn 6680 |
. . . . . . . . . . 11
β’ (π:(1...π)βΆ(1...π) β ran π β (1...π)) |
26 | 1, 2, 25 | 3syl 18 |
. . . . . . . . . 10
β’ (π β ran π β (1...π)) |
27 | 24, 26 | sstrid 3960 |
. . . . . . . . 9
β’ (π β (π β (π...(π + 1))) β (1...π)) |
28 | 27 | sselda 3949 |
. . . . . . . 8
β’ ((π β§ π β (π β (π...(π + 1)))) β π β (1...π)) |
29 | | poimirlem2.2 |
. . . . . . . . . . 11
β’ (π β π:(1...π)βΆβ€) |
30 | 29 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (πβπ) β β€) |
31 | 30 | zred 12614 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (πβπ) β β) |
32 | 31 | ltp1d 12092 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (πβπ) < ((πβπ) + 1)) |
33 | 31, 32 | ltned 11298 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (πβπ) β ((πβπ) + 1)) |
34 | 28, 33 | syldan 592 |
. . . . . . 7
β’ ((π β§ π β (π β (π...(π + 1)))) β (πβπ) β ((πβπ) + 1)) |
35 | | poimirlem2.1 |
. . . . . . . . . . 11
β’ (π β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))))) |
36 | | breq1 5113 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (π β 1) β (π¦ < π β (π β 1) < π)) |
37 | | id 22 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (π β 1) β π¦ = (π β 1)) |
38 | 36, 37 | ifbieq1d 4515 |
. . . . . . . . . . . . . 14
β’ (π¦ = (π β 1) β if(π¦ < π, π¦, (π¦ + 1)) = if((π β 1) < π, (π β 1), (π¦ + 1))) |
39 | | elfzelz 13448 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...(π β 1)) β π β β€) |
40 | 16, 39 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β€) |
41 | 40 | zred 12614 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
42 | 41 | ltm1d 12094 |
. . . . . . . . . . . . . . 15
β’ (π β (π β 1) < π) |
43 | 42 | iftrued 4499 |
. . . . . . . . . . . . . 14
β’ (π β if((π β 1) < π, (π β 1), (π¦ + 1)) = (π β 1)) |
44 | 38, 43 | sylan9eqr 2799 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ = (π β 1)) β if(π¦ < π, π¦, (π¦ + 1)) = (π β 1)) |
45 | 44 | csbeq1d 3864 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ = (π β 1)) β β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = β¦(π β 1) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))) |
46 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β 1) β β€) |
47 | | elfzm1b 13526 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ (π β 1) β β€)
β (π β
(1...(π β 1)) β
(π β 1) β
(0...((π β 1) β
1)))) |
48 | 40, 46, 47 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (1...(π β 1)) β (π β 1) β (0...((π β 1) β 1)))) |
49 | 16, 48 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ (π β (π β 1) β (0...((π β 1) β 1))) |
50 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π β 1) β (1...π) = (1...(π β 1))) |
51 | 50 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π β 1) β (π β (1...π)) = (π β (1...(π β 1)))) |
52 | 51 | xpeq1d 5667 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π β 1) β ((π β (1...π)) Γ {1}) = ((π β (1...(π β 1))) Γ {1})) |
53 | 52 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π = (π β 1)) β ((π β (1...π)) Γ {1}) = ((π β (1...(π β 1))) Γ {1})) |
54 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (π β 1) β (π + 1) = ((π β 1) + 1)) |
55 | 40 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β β) |
56 | | npcan1 11587 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β ((π β 1) + 1) = π) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π β 1) + 1) = π) |
58 | 54, 57 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π = (π β 1)) β (π + 1) = π) |
59 | 58 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π = (π β 1)) β ((π + 1)...π) = (π...π)) |
60 | 59 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π = (π β 1)) β (π β ((π + 1)...π)) = (π β (π...π))) |
61 | 60 | xpeq1d 5667 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π = (π β 1)) β ((π β ((π + 1)...π)) Γ {0}) = ((π β (π...π)) Γ {0})) |
62 | 53, 61 | uneq12d 4129 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π = (π β 1)) β (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) = (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))) |
63 | 62 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ ((π β§ π = (π β 1)) β (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))) |
64 | 49, 63 | csbied 3898 |
. . . . . . . . . . . . 13
β’ (π β β¦(π β 1) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))) |
65 | 64 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ = (π β 1)) β β¦(π β 1) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))) |
66 | 45, 65 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ π¦ = (π β 1)) β β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))) |
67 | 46 | zcnd 12615 |
. . . . . . . . . . . . . . 15
β’ (π β (π β 1) β β) |
68 | | npcan1 11587 |
. . . . . . . . . . . . . . 15
β’ ((π β 1) β β
β (((π β 1)
β 1) + 1) = (π
β 1)) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (((π β 1) β 1) + 1) = (π β 1)) |
70 | | peano2zm 12553 |
. . . . . . . . . . . . . . 15
β’ ((π β 1) β β€
β ((π β 1)
β 1) β β€) |
71 | | uzid 12785 |
. . . . . . . . . . . . . . 15
β’ (((π β 1) β 1) β
β€ β ((π β
1) β 1) β (β€β₯β((π β 1) β 1))) |
72 | | peano2uz 12833 |
. . . . . . . . . . . . . . 15
β’ (((π β 1) β 1) β
(β€β₯β((π β 1) β 1)) β (((π β 1) β 1) + 1)
β (β€β₯β((π β 1) β 1))) |
73 | 46, 70, 71, 72 | 4syl 19 |
. . . . . . . . . . . . . 14
β’ (π β (((π β 1) β 1) + 1) β
(β€β₯β((π β 1) β 1))) |
74 | 69, 73 | eqeltrrd 2839 |
. . . . . . . . . . . . 13
β’ (π β (π β 1) β
(β€β₯β((π β 1) β 1))) |
75 | | fzss2 13488 |
. . . . . . . . . . . . 13
β’ ((π β 1) β
(β€β₯β((π β 1) β 1)) β (0...((π β 1) β 1)) β
(0...(π β
1))) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (0...((π β 1) β 1)) β (0...(π β 1))) |
77 | 76, 49 | sseldd 3950 |
. . . . . . . . . . 11
β’ (π β (π β 1) β (0...(π β 1))) |
78 | | ovexd 7397 |
. . . . . . . . . . 11
β’ (π β (π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))) β V) |
79 | 35, 66, 77, 78 | fvmptd 6960 |
. . . . . . . . . 10
β’ (π β (πΉβ(π β 1)) = (π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))) |
80 | 79 | fveq1d 6849 |
. . . . . . . . 9
β’ (π β ((πΉβ(π β 1))βπ) = ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ)) |
81 | 80 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (π β (π...(π + 1)))) β ((πΉβ(π β 1))βπ) = ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ)) |
82 | 29 | ffnd 6674 |
. . . . . . . . . . 11
β’ (π β π Fn (1...π)) |
83 | 82 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π β (π...(π + 1)))) β π Fn (1...π)) |
84 | | 1ex 11158 |
. . . . . . . . . . . . . . 15
β’ 1 β
V |
85 | | fnconstg 6735 |
. . . . . . . . . . . . . . 15
β’ (1 β
V β ((π β
(1...(π β 1)))
Γ {1}) Fn (π β
(1...(π β
1)))) |
86 | 84, 85 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ ((π β (1...(π β 1))) Γ {1}) Fn (π β (1...(π β 1))) |
87 | | c0ex 11156 |
. . . . . . . . . . . . . . 15
β’ 0 β
V |
88 | | fnconstg 6735 |
. . . . . . . . . . . . . . 15
β’ (0 β
V β ((π β (π...π)) Γ {0}) Fn (π β (π...π))) |
89 | 87, 88 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ ((π β (π...π)) Γ {0}) Fn (π β (π...π)) |
90 | 86, 89 | pm3.2i 472 |
. . . . . . . . . . . . 13
β’ (((π β (1...(π β 1))) Γ {1}) Fn (π β (1...(π β 1))) β§ ((π β (π...π)) Γ {0}) Fn (π β (π...π))) |
91 | | dff1o3 6795 |
. . . . . . . . . . . . . . . 16
β’ (π:(1...π)β1-1-ontoβ(1...π) β (π:(1...π)βontoβ(1...π) β§ Fun β‘π)) |
92 | 91 | simprbi 498 |
. . . . . . . . . . . . . . 15
β’ (π:(1...π)β1-1-ontoβ(1...π) β Fun β‘π) |
93 | | imain 6591 |
. . . . . . . . . . . . . . 15
β’ (Fun
β‘π β (π β ((1...(π β 1)) β© (π...π))) = ((π β (1...(π β 1))) β© (π β (π...π)))) |
94 | 1, 92, 93 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β (π β ((1...(π β 1)) β© (π...π))) = ((π β (1...(π β 1))) β© (π β (π...π)))) |
95 | | fzdisj 13475 |
. . . . . . . . . . . . . . . . 17
β’ ((π β 1) < π β ((1...(π β 1)) β© (π...π)) = β
) |
96 | 42, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β ((1...(π β 1)) β© (π...π)) = β
) |
97 | 96 | imaeq2d 6018 |
. . . . . . . . . . . . . . 15
β’ (π β (π β ((1...(π β 1)) β© (π...π))) = (π β β
)) |
98 | | ima0 6034 |
. . . . . . . . . . . . . . 15
β’ (π β β
) =
β
|
99 | 97, 98 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’ (π β (π β ((1...(π β 1)) β© (π...π))) = β
) |
100 | 94, 99 | eqtr3d 2779 |
. . . . . . . . . . . . 13
β’ (π β ((π β (1...(π β 1))) β© (π β (π...π))) = β
) |
101 | | fnun 6619 |
. . . . . . . . . . . . 13
β’
(((((π β
(1...(π β 1)))
Γ {1}) Fn (π β
(1...(π β 1))) β§
((π β (π...π)) Γ {0}) Fn (π β (π...π))) β§ ((π β (1...(π β 1))) β© (π β (π...π))) = β
) β (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})) Fn ((π β (1...(π β 1))) βͺ (π β (π...π)))) |
102 | 90, 100, 101 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π β (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})) Fn ((π β (1...(π β 1))) βͺ (π β (π...π)))) |
103 | | elfzuz 13444 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...(π β 1)) β π β
(β€β₯β1)) |
104 | 16, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β
(β€β₯β1)) |
105 | 57, 104 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π β 1) + 1) β
(β€β₯β1)) |
106 | | peano2zm 12553 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β€ β (π β 1) β
β€) |
107 | | uzid 12785 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β 1) β β€
β (π β 1) β
(β€β₯β(π β 1))) |
108 | | peano2uz 12833 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β 1) β
(β€β₯β(π β 1)) β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
109 | 40, 106, 107, 108 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
110 | 57, 109 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β (β€β₯β(π β 1))) |
111 | | peano2uz 12833 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β
(β€β₯β(π β 1)) β (π + 1) β
(β€β₯β(π β 1))) |
112 | | uzss 12793 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π + 1) β
(β€β₯β(π β 1)) β
(β€β₯β(π + 1)) β
(β€β₯β(π β 1))) |
113 | 110, 111,
112 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(β€β₯β(π + 1)) β
(β€β₯β(π β 1))) |
114 | | elfzuz3 13445 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...(π β 1)) β (π β 1) β
(β€β₯βπ)) |
115 | | eluzp1p1 12798 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β 1) β
(β€β₯βπ) β ((π β 1) + 1) β
(β€β₯β(π + 1))) |
116 | 16, 114, 115 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π β 1) + 1) β
(β€β₯β(π + 1))) |
117 | 7, 116 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β (β€β₯β(π + 1))) |
118 | 113, 117 | sseldd 3950 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β (β€β₯β(π β 1))) |
119 | | fzsplit2 13473 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β 1) + 1) β
(β€β₯β1) β§ π β (β€β₯β(π β 1))) β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
120 | 105, 118,
119 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
121 | 57 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((π β 1) + 1)...π) = (π...π)) |
122 | 121 | uneq2d 4128 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((1...(π β 1)) βͺ (((π β 1) + 1)...π)) = ((1...(π β 1)) βͺ (π...π))) |
123 | 120, 122 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) = ((1...(π β 1)) βͺ (π...π))) |
124 | 123 | imaeq2d 6018 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (1...π)) = (π β ((1...(π β 1)) βͺ (π...π)))) |
125 | | imaundi 6107 |
. . . . . . . . . . . . . . 15
β’ (π β ((1...(π β 1)) βͺ (π...π))) = ((π β (1...(π β 1))) βͺ (π β (π...π))) |
126 | 124, 125 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’ (π β (π β (1...π)) = ((π β (1...(π β 1))) βͺ (π β (π...π)))) |
127 | | f1ofo 6796 |
. . . . . . . . . . . . . . 15
β’ (π:(1...π)β1-1-ontoβ(1...π) β π:(1...π)βontoβ(1...π)) |
128 | | foima 6766 |
. . . . . . . . . . . . . . 15
β’ (π:(1...π)βontoβ(1...π) β (π β (1...π)) = (1...π)) |
129 | 1, 127, 128 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β (π β (1...π)) = (1...π)) |
130 | 126, 129 | eqtr3d 2779 |
. . . . . . . . . . . . 13
β’ (π β ((π β (1...(π β 1))) βͺ (π β (π...π))) = (1...π)) |
131 | 130 | fneq2d 6601 |
. . . . . . . . . . . 12
β’ (π β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})) Fn ((π β (1...(π β 1))) βͺ (π β (π...π))) β (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})) Fn (1...π))) |
132 | 102, 131 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})) Fn (1...π)) |
133 | 132 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π β (π...(π + 1)))) β (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})) Fn (1...π)) |
134 | | ovexd 7397 |
. . . . . . . . . 10
β’ ((π β§ π β (π β (π...(π + 1)))) β (1...π) β V) |
135 | | inidm 4183 |
. . . . . . . . . 10
β’
((1...π) β©
(1...π)) = (1...π) |
136 | | eqidd 2738 |
. . . . . . . . . 10
β’ (((π β§ π β (π β (π...(π + 1)))) β§ π β (1...π)) β (πβπ) = (πβπ)) |
137 | 100 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π β (π...(π + 1)))) β ((π β (1...(π β 1))) β© (π β (π...π))) = β
) |
138 | | fzss2 13488 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β(π + 1)) β (π...(π + 1)) β (π...π)) |
139 | | imass2 6059 |
. . . . . . . . . . . . . . 15
β’ ((π...(π + 1)) β (π...π) β (π β (π...(π + 1))) β (π β (π...π))) |
140 | 117, 138,
139 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β (π β (π...(π + 1))) β (π β (π...π))) |
141 | 140 | sselda 3949 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π β (π...(π + 1)))) β π β (π β (π...π))) |
142 | | fvun2 6938 |
. . . . . . . . . . . . . 14
β’ ((((π β (1...(π β 1))) Γ {1}) Fn (π β (1...(π β 1))) β§ ((π β (π...π)) Γ {0}) Fn (π β (π...π)) β§ (((π β (1...(π β 1))) β© (π β (π...π))) = β
β§ π β (π β (π...π)))) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = (((π β (π...π)) Γ {0})βπ)) |
143 | 86, 89, 142 | mp3an12 1452 |
. . . . . . . . . . . . 13
β’ ((((π β (1...(π β 1))) β© (π β (π...π))) = β
β§ π β (π β (π...π))) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = (((π β (π...π)) Γ {0})βπ)) |
144 | 137, 141,
143 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π β (π...(π + 1)))) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = (((π β (π...π)) Γ {0})βπ)) |
145 | 87 | fvconst2 7158 |
. . . . . . . . . . . . 13
β’ (π β (π β (π...π)) β (((π β (π...π)) Γ {0})βπ) = 0) |
146 | 141, 145 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π β (π...(π + 1)))) β (((π β (π...π)) Γ {0})βπ) = 0) |
147 | 144, 146 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ π β (π β (π...(π + 1)))) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = 0) |
148 | 147 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β (π β (π...(π + 1)))) β§ π β (1...π)) β ((((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0}))βπ) = 0) |
149 | 83, 133, 134, 134, 135, 136, 148 | ofval 7633 |
. . . . . . . . 9
β’ (((π β§ π β (π β (π...(π + 1)))) β§ π β (1...π)) β ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ) = ((πβπ) + 0)) |
150 | 28, 149 | mpdan 686 |
. . . . . . . 8
β’ ((π β§ π β (π β (π...(π + 1)))) β ((π βf + (((π β (1...(π β 1))) Γ {1}) βͺ ((π β (π...π)) Γ {0})))βπ) = ((πβπ) + 0)) |
151 | 30 | zcnd 12615 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (πβπ) β β) |
152 | 151 | addid1d 11362 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β ((πβπ) + 0) = (πβπ)) |
153 | 28, 152 | syldan 592 |
. . . . . . . 8
β’ ((π β§ π β (π β (π...(π + 1)))) β ((πβπ) + 0) = (πβπ)) |
154 | 81, 150, 153 | 3eqtrd 2781 |
. . . . . . 7
β’ ((π β§ π β (π β (π...(π + 1)))) β ((πΉβ(π β 1))βπ) = (πβπ)) |
155 | | breq1 5113 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β (π¦ < π β π < π)) |
156 | | oveq1 7369 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β (π¦ + 1) = (π + 1)) |
157 | 155, 156 | ifbieq2d 4517 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β if(π¦ < π, π¦, (π¦ + 1)) = if(π < π, π¦, (π + 1))) |
158 | 41 | ltnrd 11296 |
. . . . . . . . . . . . . . 15
β’ (π β Β¬ π < π) |
159 | 158 | iffalsed 4502 |
. . . . . . . . . . . . . 14
β’ (π β if(π < π, π¦, (π + 1)) = (π + 1)) |
160 | 157, 159 | sylan9eqr 2799 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ = π) β if(π¦ < π, π¦, (π¦ + 1)) = (π + 1)) |
161 | 160 | csbeq1d 3864 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ = π) β β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = β¦(π + 1) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})))) |
162 | | ovex 7395 |
. . . . . . . . . . . . 13
β’ (π + 1) β V |
163 | | oveq2 7370 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β (1...π) = (1...(π + 1))) |
164 | 163 | imaeq2d 6018 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (π β (1...π)) = (π β (1...(π + 1)))) |
165 | 164 | xpeq1d 5667 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β ((π β (1...π)) Γ {1}) = ((π β (1...(π + 1))) Γ {1})) |
166 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + 1) β (π + 1) = ((π + 1) + 1)) |
167 | 166 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β ((π + 1)...π) = (((π + 1) + 1)...π)) |
168 | 167 | imaeq2d 6018 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (π β ((π + 1)...π)) = (π β (((π + 1) + 1)...π))) |
169 | 168 | xpeq1d 5667 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β ((π β ((π + 1)...π)) Γ {0}) = ((π β (((π + 1) + 1)...π)) Γ {0})) |
170 | 165, 169 | uneq12d 4129 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0})) = (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))) |
171 | 170 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β (π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))) |
172 | 162, 171 | csbie 3896 |
. . . . . . . . . . . 12
β’
β¦(π +
1) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))) |
173 | 161, 172 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ ((π β§ π¦ = π) β β¦if(π¦ < π, π¦, (π¦ + 1)) / πβ¦(π βf + (((π β (1...π)) Γ {1}) βͺ ((π β ((π + 1)...π)) Γ {0}))) = (π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))) |
174 | | fz1ssfz0 13544 |
. . . . . . . . . . . 12
β’
(1...(π β 1))
β (0...(π β
1)) |
175 | 174, 16 | sselid 3947 |
. . . . . . . . . . 11
β’ (π β π β (0...(π β 1))) |
176 | | ovexd 7397 |
. . . . . . . . . . 11
β’ (π β (π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))) β V) |
177 | 35, 173, 175, 176 | fvmptd 6960 |
. . . . . . . . . 10
β’ (π β (πΉβπ) = (π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))) |
178 | 177 | fveq1d 6849 |
. . . . . . . . 9
β’ (π β ((πΉβπ)βπ) = ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ)) |
179 | 178 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (π β (π...(π + 1)))) β ((πΉβπ)βπ) = ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ)) |
180 | | fnconstg 6735 |
. . . . . . . . . . . . . . 15
β’ (1 β
V β ((π β
(1...(π + 1))) Γ {1})
Fn (π β (1...(π + 1)))) |
181 | 84, 180 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ ((π β (1...(π + 1))) Γ {1}) Fn (π β (1...(π + 1))) |
182 | | fnconstg 6735 |
. . . . . . . . . . . . . . 15
β’ (0 β
V β ((π β
(((π + 1) + 1)...π)) Γ {0}) Fn (π β (((π + 1) + 1)...π))) |
183 | 87, 182 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ ((π β (((π + 1) + 1)...π)) Γ {0}) Fn (π β (((π + 1) + 1)...π)) |
184 | 181, 183 | pm3.2i 472 |
. . . . . . . . . . . . 13
β’ (((π β (1...(π + 1))) Γ {1}) Fn (π β (1...(π + 1))) β§ ((π β (((π + 1) + 1)...π)) Γ {0}) Fn (π β (((π + 1) + 1)...π))) |
185 | | imain 6591 |
. . . . . . . . . . . . . . . 16
β’ (Fun
β‘π β (π β ((1...(π + 1)) β© (((π + 1) + 1)...π))) = ((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π)))) |
186 | 1, 92, 185 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β (π β ((1...(π + 1)) β© (((π + 1) + 1)...π))) = ((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π)))) |
187 | | peano2re 11335 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β (π + 1) β
β) |
188 | 41, 187 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π + 1) β β) |
189 | 188 | ltp1d 12092 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π + 1) < ((π + 1) + 1)) |
190 | | fzdisj 13475 |
. . . . . . . . . . . . . . . . 17
β’ ((π + 1) < ((π + 1) + 1) β ((1...(π + 1)) β© (((π + 1) + 1)...π)) = β
) |
191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β ((1...(π + 1)) β© (((π + 1) + 1)...π)) = β
) |
192 | 191 | imaeq2d 6018 |
. . . . . . . . . . . . . . 15
β’ (π β (π β ((1...(π + 1)) β© (((π + 1) + 1)...π))) = (π β β
)) |
193 | 186, 192 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
β’ (π β ((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π))) = (π β β
)) |
194 | 193, 98 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (π β ((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π))) = β
) |
195 | | fnun 6619 |
. . . . . . . . . . . . 13
β’
(((((π β
(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)...π)))) |
196 | 184, 194,
195 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π β (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})) Fn ((π β (1...(π + 1))) βͺ (π β (((π + 1) + 1)...π)))) |
197 | | fzsplit 13474 |
. . . . . . . . . . . . . . . . 17
β’ ((π + 1) β (1...π) β (1...π) = ((1...(π + 1)) βͺ (((π + 1) + 1)...π))) |
198 | 22, 197 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) = ((1...(π + 1)) βͺ (((π + 1) + 1)...π))) |
199 | 198 | imaeq2d 6018 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (1...π)) = (π β ((1...(π + 1)) βͺ (((π + 1) + 1)...π)))) |
200 | | imaundi 6107 |
. . . . . . . . . . . . . . 15
β’ (π β ((1...(π + 1)) βͺ (((π + 1) + 1)...π))) = ((π β (1...(π + 1))) βͺ (π β (((π + 1) + 1)...π))) |
201 | 199, 200 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’ (π β (π β (1...π)) = ((π β (1...(π + 1))) βͺ (π β (((π + 1) + 1)...π)))) |
202 | 201, 129 | eqtr3d 2779 |
. . . . . . . . . . . . 13
β’ (π β ((π β (1...(π + 1))) βͺ (π β (((π + 1) + 1)...π))) = (1...π)) |
203 | 202 | fneq2d 6601 |
. . . . . . . . . . . 12
β’ (π β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})) Fn ((π β (1...(π + 1))) βͺ (π β (((π + 1) + 1)...π))) β (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})) Fn (1...π))) |
204 | 196, 203 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})) Fn (1...π)) |
205 | 204 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π β (π...(π + 1)))) β (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})) Fn (1...π)) |
206 | 194 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π β (π...(π + 1)))) β ((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π))) = β
) |
207 | | fzss1 13487 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β1) β (π...(π + 1)) β (1...(π + 1))) |
208 | | imass2 6059 |
. . . . . . . . . . . . . . 15
β’ ((π...(π + 1)) β (1...(π + 1)) β (π β (π...(π + 1))) β (π β (1...(π + 1)))) |
209 | 104, 207,
208 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β (π β (π...(π + 1))) β (π β (1...(π + 1)))) |
210 | 209 | sselda 3949 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π β (π...(π + 1)))) β π β (π β (1...(π + 1)))) |
211 | | fvun1 6937 |
. . . . . . . . . . . . . 14
β’ ((((π β (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})βπ)) |
212 | 181, 183,
211 | mp3an12 1452 |
. . . . . . . . . . . . 13
β’ ((((π β (1...(π + 1))) β© (π β (((π + 1) + 1)...π))) = β
β§ π β (π β (1...(π + 1)))) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = (((π β (1...(π + 1))) Γ {1})βπ)) |
213 | 206, 210,
212 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π β (π...(π + 1)))) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = (((π β (1...(π + 1))) Γ {1})βπ)) |
214 | 84 | fvconst2 7158 |
. . . . . . . . . . . . 13
β’ (π β (π β (1...(π + 1))) β (((π β (1...(π + 1))) Γ {1})βπ) = 1) |
215 | 210, 214 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π β (π...(π + 1)))) β (((π β (1...(π + 1))) Γ {1})βπ) = 1) |
216 | 213, 215 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ π β (π β (π...(π + 1)))) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = 1) |
217 | 216 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β (π β (π...(π + 1)))) β§ π β (1...π)) β ((((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0}))βπ) = 1) |
218 | 83, 205, 134, 134, 135, 136, 217 | ofval 7633 |
. . . . . . . . 9
β’ (((π β§ π β (π β (π...(π + 1)))) β§ π β (1...π)) β ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ) = ((πβπ) + 1)) |
219 | 28, 218 | mpdan 686 |
. . . . . . . 8
β’ ((π β§ π β (π β (π...(π + 1)))) β ((π βf + (((π β (1...(π + 1))) Γ {1}) βͺ ((π β (((π + 1) + 1)...π)) Γ {0})))βπ) = ((πβπ) + 1)) |
220 | 179, 219 | eqtrd 2777 |
. . . . . . 7
β’ ((π β§ π β (π β (π...(π + 1)))) β ((πΉβπ)βπ) = ((πβπ) + 1)) |
221 | 34, 154, 220 | 3netr4d 3022 |
. . . . . 6
β’ ((π β§ π β (π β (π...(π + 1)))) β ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) |
222 | 221 | ralrimiva 3144 |
. . . . 5
β’ (π β βπ β (π β (π...(π + 1)))((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) |
223 | | fzpr 13503 |
. . . . . . . . 9
β’ (π β β€ β (π...(π + 1)) = {π, (π + 1)}) |
224 | 16, 39, 223 | 3syl 18 |
. . . . . . . 8
β’ (π β (π...(π + 1)) = {π, (π + 1)}) |
225 | 224 | imaeq2d 6018 |
. . . . . . 7
β’ (π β (π β (π...(π + 1))) = (π β {π, (π + 1)})) |
226 | | f1ofn 6790 |
. . . . . . . . 9
β’ (π:(1...π)β1-1-ontoβ(1...π) β π Fn (1...π)) |
227 | 1, 226 | syl 17 |
. . . . . . . 8
β’ (π β π Fn (1...π)) |
228 | | fnimapr 6930 |
. . . . . . . 8
β’ ((π Fn (1...π) β§ π β (1...π) β§ (π + 1) β (1...π)) β (π β {π, (π + 1)}) = {(πβπ), (πβ(π + 1))}) |
229 | 227, 17, 22, 228 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π β {π, (π + 1)}) = {(πβπ), (πβ(π + 1))}) |
230 | 225, 229 | eqtrd 2777 |
. . . . . 6
β’ (π β (π β (π...(π + 1))) = {(πβπ), (πβ(π + 1))}) |
231 | 230 | raleqdv 3316 |
. . . . 5
β’ (π β (βπ β (π β (π...(π + 1)))((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β βπ β {(πβπ), (πβ(π + 1))} ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ))) |
232 | 222, 231 | mpbid 231 |
. . . 4
β’ (π β βπ β {(πβπ), (πβ(π + 1))} ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) |
233 | | fvex 6860 |
. . . . 5
β’ (πβπ) β V |
234 | | fvex 6860 |
. . . . 5
β’ (πβ(π + 1)) β V |
235 | | fveq2 6847 |
. . . . . 6
β’ (π = (πβπ) β ((πΉβ(π β 1))βπ) = ((πΉβ(π β 1))β(πβπ))) |
236 | | fveq2 6847 |
. . . . . 6
β’ (π = (πβπ) β ((πΉβπ)βπ) = ((πΉβπ)β(πβπ))) |
237 | 235, 236 | neeq12d 3006 |
. . . . 5
β’ (π = (πβπ) β (((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β ((πΉβ(π β 1))β(πβπ)) β ((πΉβπ)β(πβπ)))) |
238 | | fveq2 6847 |
. . . . . 6
β’ (π = (πβ(π + 1)) β ((πΉβ(π β 1))βπ) = ((πΉβ(π β 1))β(πβ(π + 1)))) |
239 | | fveq2 6847 |
. . . . . 6
β’ (π = (πβ(π + 1)) β ((πΉβπ)βπ) = ((πΉβπ)β(πβ(π + 1)))) |
240 | 238, 239 | neeq12d 3006 |
. . . . 5
β’ (π = (πβ(π + 1)) β (((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β ((πΉβ(π β 1))β(πβ(π + 1))) β ((πΉβπ)β(πβ(π + 1))))) |
241 | 233, 234,
237, 240 | ralpr 4666 |
. . . 4
β’
(βπ β
{(πβπ), (πβ(π + 1))} ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β (((πΉβ(π β 1))β(πβπ)) β ((πΉβπ)β(πβπ)) β§ ((πΉβ(π β 1))β(πβ(π + 1))) β ((πΉβπ)β(πβ(π + 1))))) |
242 | 232, 241 | sylib 217 |
. . 3
β’ (π β (((πΉβ(π β 1))β(πβπ)) β ((πΉβπ)β(πβπ)) β§ ((πΉβ(π β 1))β(πβ(π + 1))) β ((πΉβπ)β(πβ(π + 1))))) |
243 | 41 | ltp1d 12092 |
. . . . 5
β’ (π β π < (π + 1)) |
244 | 41, 243 | ltned 11298 |
. . . 4
β’ (π β π β (π + 1)) |
245 | | f1of1 6788 |
. . . . . . 7
β’ (π:(1...π)β1-1-ontoβ(1...π) β π:(1...π)β1-1β(1...π)) |
246 | 1, 245 | syl 17 |
. . . . . 6
β’ (π β π:(1...π)β1-1β(1...π)) |
247 | | f1veqaeq 7209 |
. . . . . 6
β’ ((π:(1...π)β1-1β(1...π) β§ (π β (1...π) β§ (π + 1) β (1...π))) β ((πβπ) = (πβ(π + 1)) β π = (π + 1))) |
248 | 246, 17, 22, 247 | syl12anc 836 |
. . . . 5
β’ (π β ((πβπ) = (πβ(π + 1)) β π = (π + 1))) |
249 | 248 | necon3d 2965 |
. . . 4
β’ (π β (π β (π + 1) β (πβπ) β (πβ(π + 1)))) |
250 | 244, 249 | mpd 15 |
. . 3
β’ (π β (πβπ) β (πβ(π + 1))) |
251 | 237 | anbi1d 631 |
. . . . 5
β’ (π = (πβπ) β ((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β (((πΉβ(π β 1))β(πβπ)) β ((πΉβπ)β(πβπ)) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)))) |
252 | | neeq1 3007 |
. . . . 5
β’ (π = (πβπ) β (π β π β (πβπ) β π)) |
253 | 251, 252 | anbi12d 632 |
. . . 4
β’ (π = (πβπ) β (((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ π β π) β ((((πΉβ(π β 1))β(πβπ)) β ((πΉβπ)β(πβπ)) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ (πβπ) β π))) |
254 | | fveq2 6847 |
. . . . . . 7
β’ (π = (πβ(π + 1)) β ((πΉβ(π β 1))βπ) = ((πΉβ(π β 1))β(πβ(π + 1)))) |
255 | | fveq2 6847 |
. . . . . . 7
β’ (π = (πβ(π + 1)) β ((πΉβπ)βπ) = ((πΉβπ)β(πβ(π + 1)))) |
256 | 254, 255 | neeq12d 3006 |
. . . . . 6
β’ (π = (πβ(π + 1)) β (((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β ((πΉβ(π β 1))β(πβ(π + 1))) β ((πΉβπ)β(πβ(π + 1))))) |
257 | 256 | anbi2d 630 |
. . . . 5
β’ (π = (πβ(π + 1)) β ((((πΉβ(π β 1))β(πβπ)) β ((πΉβπ)β(πβπ)) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β (((πΉβ(π β 1))β(πβπ)) β ((πΉβπ)β(πβπ)) β§ ((πΉβ(π β 1))β(πβ(π + 1))) β ((πΉβπ)β(πβ(π + 1)))))) |
258 | | neeq2 3008 |
. . . . 5
β’ (π = (πβ(π + 1)) β ((πβπ) β π β (πβπ) β (πβ(π + 1)))) |
259 | 257, 258 | anbi12d 632 |
. . . 4
β’ (π = (πβ(π + 1)) β (((((πΉβ(π β 1))β(πβπ)) β ((πΉβπ)β(πβπ)) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ (πβπ) β π) β ((((πΉβ(π β 1))β(πβπ)) β ((πΉβπ)β(πβπ)) β§ ((πΉβ(π β 1))β(πβ(π + 1))) β ((πΉβπ)β(πβ(π + 1)))) β§ (πβπ) β (πβ(π + 1))))) |
260 | 253, 259 | rspc2ev 3595 |
. . 3
β’ (((πβπ) β (1...π) β§ (πβ(π + 1)) β (1...π) β§ ((((πΉβ(π β 1))β(πβπ)) β ((πΉβπ)β(πβπ)) β§ ((πΉβ(π β 1))β(πβ(π + 1))) β ((πΉβπ)β(πβ(π + 1)))) β§ (πβπ) β (πβ(π + 1)))) β βπ β (1...π)βπ β (1...π)((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ π β π)) |
261 | 18, 23, 242, 250, 260 | syl112anc 1375 |
. 2
β’ (π β βπ β (1...π)βπ β (1...π)((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ π β π)) |
262 | | dfrex2 3077 |
. . 3
β’
(βπ β
(1...π)βπ β (1...π)((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ π β π) β Β¬ βπ β (1...π) Β¬ βπ β (1...π)((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ π β π)) |
263 | | fveq2 6847 |
. . . . . 6
β’ (π = π β ((πΉβ(π β 1))βπ) = ((πΉβ(π β 1))βπ)) |
264 | | fveq2 6847 |
. . . . . 6
β’ (π = π β ((πΉβπ)βπ) = ((πΉβπ)βπ)) |
265 | 263, 264 | neeq12d 3006 |
. . . . 5
β’ (π = π β (((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ))) |
266 | 265 | rmo4 3693 |
. . . 4
β’
(β*π β
(1...π)((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β βπ β (1...π)βπ β (1...π)((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β π = π)) |
267 | | dfral2 3103 |
. . . . . 6
β’
(βπ β
(1...π)((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β π = π) β Β¬ βπ β (1...π) Β¬ ((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β π = π)) |
268 | | df-ne 2945 |
. . . . . . . . 9
β’ (π β π β Β¬ π = π) |
269 | 268 | anbi2i 624 |
. . . . . . . 8
β’
(((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ π β π) β ((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ Β¬ π = π)) |
270 | | annim 405 |
. . . . . . . 8
β’
(((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ Β¬ π = π) β Β¬ ((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β π = π)) |
271 | 269, 270 | bitri 275 |
. . . . . . 7
β’
(((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ π β π) β Β¬ ((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β π = π)) |
272 | 271 | rexbii 3098 |
. . . . . 6
β’
(βπ β
(1...π)((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ π β π) β βπ β (1...π) Β¬ ((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β π = π)) |
273 | 267, 272 | xchbinxr 335 |
. . . . 5
β’
(βπ β
(1...π)((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β π = π) β Β¬ βπ β (1...π)((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ π β π)) |
274 | 273 | ralbii 3097 |
. . . 4
β’
(βπ β
(1...π)βπ β (1...π)((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β π = π) β βπ β (1...π) Β¬ βπ β (1...π)((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ π β π)) |
275 | 266, 274 | bitri 275 |
. . 3
β’
(β*π β
(1...π)((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β βπ β (1...π) Β¬ βπ β (1...π)((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ π β π)) |
276 | 262, 275 | xchbinxr 335 |
. 2
β’
(βπ β
(1...π)βπ β (1...π)((((πΉβ(π β 1))βπ) β ((πΉβπ)βπ) β§ ((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) β§ π β π) β Β¬ β*π β (1...π)((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) |
277 | 261, 276 | sylib 217 |
1
β’ (π β Β¬ β*π β (1...π)((πΉβ(π β 1))βπ) β ((πΉβπ)βπ)) |