Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . 3
β’ (π β π β β) |
2 | | poimirlem22.s |
. . 3
β’ π = {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} |
3 | | poimirlem22.1 |
. . 3
β’ (π β πΉ:(0...(π β 1))βΆ((0...πΎ) βm (1...π))) |
4 | | poimirlem22.2 |
. . 3
β’ (π β π β π) |
5 | | poimirlem18.3 |
. . 3
β’ ((π β§ π β (1...π)) β βπ β ran πΉ(πβπ) β πΎ) |
6 | | poimirlem18.4 |
. . 3
β’ (π β (2nd
βπ) =
0) |
7 | 1, 2, 3, 4, 5, 6 | poimirlem17 36095 |
. 2
β’ (π β βπ§ β π π§ β π) |
8 | 6 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π§ β π) β (2nd βπ) = 0) |
9 | | 0nnn 12189 |
. . . . . . . . . . . . 13
β’ Β¬ 0
β β |
10 | | elfznn 13470 |
. . . . . . . . . . . . 13
β’ (0 β
(1...(π β 1)) β
0 β β) |
11 | 9, 10 | mto 196 |
. . . . . . . . . . . 12
β’ Β¬ 0
β (1...(π β
1)) |
12 | | eleq1 2825 |
. . . . . . . . . . . 12
β’
((2nd βπ§) = 0 β ((2nd βπ§) β (1...(π β 1)) β 0 β (1...(π β 1)))) |
13 | 11, 12 | mtbiri 326 |
. . . . . . . . . . 11
β’
((2nd βπ§) = 0 β Β¬ (2nd
βπ§) β
(1...(π β
1))) |
14 | 13 | necon2ai 2973 |
. . . . . . . . . 10
β’
((2nd βπ§) β (1...(π β 1)) β (2nd
βπ§) β
0) |
15 | 1 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β π) β§ (2nd βπ§) β (1...(π β 1))) β π β β) |
16 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π‘ = π§ β (2nd βπ‘) = (2nd βπ§)) |
17 | 16 | breq2d 5117 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π‘ = π§ β (π¦ < (2nd βπ‘) β π¦ < (2nd βπ§))) |
18 | 17 | ifbid 4509 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ = π§ β if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) = if(π¦ < (2nd βπ§), π¦, (π¦ + 1))) |
19 | 18 | csbeq1d 3859 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π‘ = π§ β β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})))) |
20 | | 2fveq3 6847 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π‘ = π§ β (1st
β(1st βπ‘)) = (1st β(1st
βπ§))) |
21 | | 2fveq3 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π‘ = π§ β (2nd
β(1st βπ‘)) = (2nd β(1st
βπ§))) |
22 | 21 | imaeq1d 6012 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π‘ = π§ β ((2nd
β(1st βπ‘)) β (1...π)) = ((2nd β(1st
βπ§)) β
(1...π))) |
23 | 22 | xpeq1d 5662 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π‘ = π§ β (((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) = (((2nd
β(1st βπ§)) β (1...π)) Γ {1})) |
24 | 21 | imaeq1d 6012 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π‘ = π§ β ((2nd
β(1st βπ‘)) β ((π + 1)...π)) = ((2nd β(1st
βπ§)) β ((π + 1)...π))) |
25 | 24 | xpeq1d 5662 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π‘ = π§ β (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}) = (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})) |
26 | 23, 25 | uneq12d 4124 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π‘ = π§ β ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})) = ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))) |
27 | 20, 26 | oveq12d 7375 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ = π§ β ((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = ((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})))) |
28 | 27 | csbeq2dv 3862 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π‘ = π§ β β¦if(π¦ < (2nd βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})))) |
29 | 19, 28 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = π§ β β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})))) |
30 | 29 | mpteq2dv 5207 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ = π§ β (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})))) = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))))) |
31 | 30 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ = π§ β (πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})))) β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})))))) |
32 | 31, 2 | elrab2 3648 |
. . . . . . . . . . . . . . . 16
β’ (π§ β π β (π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β§ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0})))))) |
33 | 32 | simprbi 497 |
. . . . . . . . . . . . . . 15
β’ (π§ β π β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))))) |
34 | 33 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β π) β§ (2nd βπ§) β (1...(π β 1))) β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ§), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ§)) βf + ((((2nd
β(1st βπ§)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ§)) β ((π + 1)...π)) Γ {0}))))) |
35 | | elrabi 3639 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π§ β {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} β π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) |
36 | 35, 2 | eleq2s 2855 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β π β π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) |
37 | | xp1st 7953 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β (1st βπ§) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β π β (1st βπ§) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
39 | | xp1st 7953 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ§) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (1st
β(1st βπ§)) β ((0..^πΎ) βm (1...π))) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β π β (1st
β(1st βπ§)) β ((0..^πΎ) βm (1...π))) |
41 | | elmapi 8787 |
. . . . . . . . . . . . . . . . 17
β’
((1st β(1st βπ§)) β ((0..^πΎ) βm (1...π)) β (1st
β(1st βπ§)):(1...π)βΆ(0..^πΎ)) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π§ β π β (1st
β(1st βπ§)):(1...π)βΆ(0..^πΎ)) |
43 | | elfzoelz 13572 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0..^πΎ) β π β β€) |
44 | 43 | ssriv 3948 |
. . . . . . . . . . . . . . . 16
β’
(0..^πΎ) β
β€ |
45 | | fss 6685 |
. . . . . . . . . . . . . . . 16
β’
(((1st β(1st βπ§)):(1...π)βΆ(0..^πΎ) β§ (0..^πΎ) β β€) β (1st
β(1st βπ§)):(1...π)βΆβ€) |
46 | 42, 44, 45 | sylancl 586 |
. . . . . . . . . . . . . . 15
β’ (π§ β π β (1st
β(1st βπ§)):(1...π)βΆβ€) |
47 | 46 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β π) β§ (2nd βπ§) β (1...(π β 1))) β (1st
β(1st βπ§)):(1...π)βΆβ€) |
48 | | xp2nd 7954 |
. . . . . . . . . . . . . . . . 17
β’
((1st βπ§) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (2nd
β(1st βπ§)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
49 | 38, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π§ β π β (2nd
β(1st βπ§)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
50 | | fvex 6855 |
. . . . . . . . . . . . . . . . 17
β’
(2nd β(1st βπ§)) β V |
51 | | f1oeq1 6772 |
. . . . . . . . . . . . . . . . 17
β’ (π = (2nd
β(1st βπ§)) β (π:(1...π)β1-1-ontoβ(1...π) β (2nd
β(1st βπ§)):(1...π)β1-1-ontoβ(1...π))) |
52 | 50, 51 | elab 3630 |
. . . . . . . . . . . . . . . 16
β’
((2nd β(1st βπ§)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)} β (2nd
β(1st βπ§)):(1...π)β1-1-ontoβ(1...π)) |
53 | 49, 52 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ (π§ β π β (2nd
β(1st βπ§)):(1...π)β1-1-ontoβ(1...π)) |
54 | 53 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β π) β§ (2nd βπ§) β (1...(π β 1))) β (2nd
β(1st βπ§)):(1...π)β1-1-ontoβ(1...π)) |
55 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β π) β§ (2nd βπ§) β (1...(π β 1))) β (2nd
βπ§) β
(1...(π β
1))) |
56 | 15, 34, 47, 54, 55 | poimirlem1 36079 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π) β§ (2nd βπ§) β (1...(π β 1))) β Β¬ β*π β (1...π)((πΉβ((2nd βπ§) β 1))βπ) β ((πΉβ(2nd βπ§))βπ)) |
57 | 1 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
(2nd βπ)
β (2nd βπ§)) β π β β) |
58 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π‘ = π β (2nd βπ‘) = (2nd βπ)) |
59 | 58 | breq2d 5117 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π‘ = π β (π¦ < (2nd βπ‘) β π¦ < (2nd βπ))) |
60 | 59 | ifbid 4509 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π‘ = π β if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) = if(π¦ < (2nd βπ), π¦, (π¦ + 1))) |
61 | 60 | csbeq1d 3859 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π‘ = π β β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})))) |
62 | | 2fveq3 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π‘ = π β (1st
β(1st βπ‘)) = (1st β(1st
βπ))) |
63 | | 2fveq3 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π‘ = π β (2nd
β(1st βπ‘)) = (2nd β(1st
βπ))) |
64 | 63 | imaeq1d 6012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π‘ = π β ((2nd
β(1st βπ‘)) β (1...π)) = ((2nd β(1st
βπ)) β
(1...π))) |
65 | 64 | xpeq1d 5662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π‘ = π β (((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) = (((2nd
β(1st βπ)) β (1...π)) Γ {1})) |
66 | 63 | imaeq1d 6012 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π‘ = π β ((2nd
β(1st βπ‘)) β ((π + 1)...π)) = ((2nd β(1st
βπ)) β ((π + 1)...π))) |
67 | 66 | xpeq1d 5662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π‘ = π β (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}) = (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})) |
68 | 65, 67 | uneq12d 4124 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π‘ = π β ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})) = ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))) |
69 | 62, 68 | oveq12d 7375 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π‘ = π β ((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = ((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})))) |
70 | 69 | csbeq2dv 3862 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π‘ = π β β¦if(π¦ < (2nd βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})))) |
71 | 61, 70 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π‘ = π β β¦if(π¦ < (2nd βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))) = β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})))) |
72 | 71 | mpteq2dv 5207 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π‘ = π β (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})))) = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))))) |
73 | 72 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ = π β (πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0})))) β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})))))) |
74 | 73, 2 | elrab2 3648 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β (π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β§ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0})))))) |
75 | 74 | simprbi 497 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))))) |
76 | 4, 75 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))))) |
77 | 76 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
(2nd βπ)
β (2nd βπ§)) β πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ)) βf + ((((2nd
β(1st βπ)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ)) β ((π + 1)...π)) Γ {0}))))) |
78 | | elrabi 3639 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β {π‘ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β£ πΉ = (π¦ β (0...(π β 1)) β¦ β¦if(π¦ < (2nd
βπ‘), π¦, (π¦ + 1)) / πβ¦((1st
β(1st βπ‘)) βf + ((((2nd
β(1st βπ‘)) β (1...π)) Γ {1}) βͺ (((2nd
β(1st βπ‘)) β ((π + 1)...π)) Γ {0}))))} β π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) |
79 | 78, 2 | eleq2s 2855 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) |
80 | 4, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π))) |
81 | | xp1st 7953 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β (1st βπ) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1st
βπ) β
(((0..^πΎ)
βm (1...π))
Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)})) |
83 | | xp1st 7953 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((1st βπ) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (1st
β(1st βπ)) β ((0..^πΎ) βm (1...π))) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1st
β(1st βπ)) β ((0..^πΎ) βm (1...π))) |
85 | | elmapi 8787 |
. . . . . . . . . . . . . . . . . . . 20
β’
((1st β(1st βπ)) β ((0..^πΎ) βm (1...π)) β (1st
β(1st βπ)):(1...π)βΆ(0..^πΎ)) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1st
β(1st βπ)):(1...π)βΆ(0..^πΎ)) |
87 | | fss 6685 |
. . . . . . . . . . . . . . . . . . 19
β’
(((1st β(1st βπ)):(1...π)βΆ(0..^πΎ) β§ (0..^πΎ) β β€) β (1st
β(1st βπ)):(1...π)βΆβ€) |
88 | 86, 44, 87 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1st
β(1st βπ)):(1...π)βΆβ€) |
89 | 88 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
(2nd βπ)
β (2nd βπ§)) β (1st
β(1st βπ)):(1...π)βΆβ€) |
90 | | xp2nd 7954 |
. . . . . . . . . . . . . . . . . . . 20
β’
((1st βπ) β (((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) β (2nd
β(1st βπ)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
91 | 82, 90 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (2nd
β(1st βπ)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)}) |
92 | | fvex 6855 |
. . . . . . . . . . . . . . . . . . . 20
β’
(2nd β(1st βπ)) β V |
93 | | f1oeq1 6772 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (2nd
β(1st βπ)) β (π:(1...π)β1-1-ontoβ(1...π) β (2nd
β(1st βπ)):(1...π)β1-1-ontoβ(1...π))) |
94 | 92, 93 | elab 3630 |
. . . . . . . . . . . . . . . . . . 19
β’
((2nd β(1st βπ)) β {π β£ π:(1...π)β1-1-ontoβ(1...π)} β (2nd
β(1st βπ)):(1...π)β1-1-ontoβ(1...π)) |
95 | 91, 94 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (2nd
β(1st βπ)):(1...π)β1-1-ontoβ(1...π)) |
96 | 95 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
(2nd βπ)
β (2nd βπ§)) β (2nd
β(1st βπ)):(1...π)β1-1-ontoβ(1...π)) |
97 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
(2nd βπ)
β (2nd βπ§)) β (2nd βπ§) β (1...(π β 1))) |
98 | | xp2nd 7954 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β (2nd βπ) β (0...π)) |
99 | 80, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (2nd
βπ) β (0...π)) |
100 | 99 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (2nd
βπ§) β
(1...(π β 1))) β
(2nd βπ)
β (0...π)) |
101 | | eldifsn 4747 |
. . . . . . . . . . . . . . . . . . 19
β’
((2nd βπ) β ((0...π) β {(2nd βπ§)}) β ((2nd
βπ) β (0...π) β§ (2nd
βπ) β
(2nd βπ§))) |
102 | 101 | biimpri 227 |
. . . . . . . . . . . . . . . . . 18
β’
(((2nd βπ) β (0...π) β§ (2nd βπ) β (2nd
βπ§)) β
(2nd βπ)
β ((0...π) β
{(2nd βπ§)})) |
103 | 100, 102 | sylan 580 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
(2nd βπ)
β (2nd βπ§)) β (2nd βπ) β ((0...π) β {(2nd βπ§)})) |
104 | 57, 77, 89, 96, 97, 103 | poimirlem2 36080 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (2nd
βπ§) β
(1...(π β 1))) β§
(2nd βπ)
β (2nd βπ§)) β β*π β (1...π)((πΉβ((2nd βπ§) β 1))βπ) β ((πΉβ(2nd βπ§))βπ)) |
105 | 104 | ex 413 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (2nd
βπ§) β
(1...(π β 1))) β
((2nd βπ)
β (2nd βπ§) β β*π β (1...π)((πΉβ((2nd βπ§) β 1))βπ) β ((πΉβ(2nd βπ§))βπ))) |
106 | 105 | necon1bd 2961 |
. . . . . . . . . . . . . 14
β’ ((π β§ (2nd
βπ§) β
(1...(π β 1))) β
(Β¬ β*π β
(1...π)((πΉβ((2nd βπ§) β 1))βπ) β ((πΉβ(2nd βπ§))βπ) β (2nd βπ) = (2nd βπ§))) |
107 | 106 | adantlr 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β π) β§ (2nd βπ§) β (1...(π β 1))) β (Β¬ β*π β (1...π)((πΉβ((2nd βπ§) β 1))βπ) β ((πΉβ(2nd βπ§))βπ) β (2nd βπ) = (2nd βπ§))) |
108 | 56, 107 | mpd 15 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β π) β§ (2nd βπ§) β (1...(π β 1))) β (2nd
βπ) = (2nd
βπ§)) |
109 | 108 | neeq1d 3003 |
. . . . . . . . . . 11
β’ (((π β§ π§ β π) β§ (2nd βπ§) β (1...(π β 1))) β ((2nd
βπ) β 0 β
(2nd βπ§)
β 0)) |
110 | 109 | exbiri 809 |
. . . . . . . . . 10
β’ ((π β§ π§ β π) β ((2nd βπ§) β (1...(π β 1)) β ((2nd
βπ§) β 0 β
(2nd βπ)
β 0))) |
111 | 14, 110 | mpdi 45 |
. . . . . . . . 9
β’ ((π β§ π§ β π) β ((2nd βπ§) β (1...(π β 1)) β (2nd
βπ) β
0)) |
112 | 111 | necon2bd 2959 |
. . . . . . . 8
β’ ((π β§ π§ β π) β ((2nd βπ) = 0 β Β¬
(2nd βπ§)
β (1...(π β
1)))) |
113 | 8, 112 | mpd 15 |
. . . . . . 7
β’ ((π β§ π§ β π) β Β¬ (2nd βπ§) β (1...(π β 1))) |
114 | | xp2nd 7954 |
. . . . . . . . 9
β’ (π§ β ((((0..^πΎ) βm (1...π)) Γ {π β£ π:(1...π)β1-1-ontoβ(1...π)}) Γ (0...π)) β (2nd βπ§) β (0...π)) |
115 | 36, 114 | syl 17 |
. . . . . . . 8
β’ (π§ β π β (2nd βπ§) β (0...π)) |
116 | 1 | nncnd 12169 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β) |
117 | | npcan1 11580 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β ((π β 1) + 1) = π) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π β 1) + 1) = π) |
119 | | nnuz 12806 |
. . . . . . . . . . . . . . . . . . 19
β’ β =
(β€β₯β1) |
120 | 1, 119 | eleqtrdi 2847 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β
(β€β₯β1)) |
121 | 118, 120 | eqeltrd 2837 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π β 1) + 1) β
(β€β₯β1)) |
122 | 1 | nnzd 12526 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β β€) |
123 | | peano2zm 12546 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β€ β (π β 1) β
β€) |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π β 1) β β€) |
125 | | uzid 12778 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β 1) β β€
β (π β 1) β
(β€β₯β(π β 1))) |
126 | | peano2uz 12826 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β 1) β
(β€β₯β(π β 1)) β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
127 | 124, 125,
126 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π β 1) + 1) β
(β€β₯β(π β 1))) |
128 | 118, 127 | eqeltrrd 2838 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (β€β₯β(π β 1))) |
129 | | fzsplit2 13466 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β 1) + 1) β
(β€β₯β1) β§ π β (β€β₯β(π β 1))) β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
130 | 121, 128,
129 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) = ((1...(π β 1)) βͺ (((π β 1) + 1)...π))) |
131 | 118 | oveq1d 7372 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((π β 1) + 1)...π) = (π...π)) |
132 | | fzsn 13483 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β€ β (π...π) = {π}) |
133 | 122, 132 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π...π) = {π}) |
134 | 131, 133 | eqtrd 2776 |
. . . . . . . . . . . . . . . . 17
β’ (π β (((π β 1) + 1)...π) = {π}) |
135 | 134 | uneq2d 4123 |
. . . . . . . . . . . . . . . 16
β’ (π β ((1...(π β 1)) βͺ (((π β 1) + 1)...π)) = ((1...(π β 1)) βͺ {π})) |
136 | 130, 135 | eqtrd 2776 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) = ((1...(π β 1)) βͺ {π})) |
137 | 136 | eleq2d 2823 |
. . . . . . . . . . . . . 14
β’ (π β ((2nd
βπ§) β (1...π) β (2nd
βπ§) β
((1...(π β 1)) βͺ
{π}))) |
138 | 137 | notbid 317 |
. . . . . . . . . . . . 13
β’ (π β (Β¬ (2nd
βπ§) β (1...π) β Β¬ (2nd
βπ§) β
((1...(π β 1)) βͺ
{π}))) |
139 | | ioran 982 |
. . . . . . . . . . . . . 14
β’ (Β¬
((2nd βπ§)
β (1...(π β 1))
β¨ (2nd βπ§) = π) β (Β¬ (2nd βπ§) β (1...(π β 1)) β§ Β¬ (2nd
βπ§) = π)) |
140 | | elun 4108 |
. . . . . . . . . . . . . . 15
β’
((2nd βπ§) β ((1...(π β 1)) βͺ {π}) β ((2nd βπ§) β (1...(π β 1)) β¨ (2nd
βπ§) β {π})) |
141 | | fvex 6855 |
. . . . . . . . . . . . . . . . 17
β’
(2nd βπ§) β V |
142 | 141 | elsn 4601 |
. . . . . . . . . . . . . . . 16
β’
((2nd βπ§) β {π} β (2nd βπ§) = π) |
143 | 142 | orbi2i 911 |
. . . . . . . . . . . . . . 15
β’
(((2nd βπ§) β (1...(π β 1)) β¨ (2nd
βπ§) β {π}) β ((2nd
βπ§) β
(1...(π β 1)) β¨
(2nd βπ§) =
π)) |
144 | 140, 143 | bitri 274 |
. . . . . . . . . . . . . 14
β’
((2nd βπ§) β ((1...(π β 1)) βͺ {π}) β ((2nd βπ§) β (1...(π β 1)) β¨ (2nd
βπ§) = π)) |
145 | 139, 144 | xchnxbir 332 |
. . . . . . . . . . . . 13
β’ (Β¬
(2nd βπ§)
β ((1...(π β 1))
βͺ {π}) β (Β¬
(2nd βπ§)
β (1...(π β 1))
β§ Β¬ (2nd βπ§) = π)) |
146 | 138, 145 | bitrdi 286 |
. . . . . . . . . . . 12
β’ (π β (Β¬ (2nd
βπ§) β (1...π) β (Β¬ (2nd
βπ§) β
(1...(π β 1)) β§
Β¬ (2nd βπ§) = π))) |
147 | 146 | anbi2d 629 |
. . . . . . . . . . 11
β’ (π β (((2nd
βπ§) β (0...π) β§ Β¬ (2nd
βπ§) β (1...π)) β ((2nd
βπ§) β (0...π) β§ (Β¬ (2nd
βπ§) β
(1...(π β 1)) β§
Β¬ (2nd βπ§) = π)))) |
148 | 1 | nnnn0d 12473 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β
β0) |
149 | | nn0uz 12805 |
. . . . . . . . . . . . . . . . 17
β’
β0 = (β€β₯β0) |
150 | 148, 149 | eleqtrdi 2847 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
(β€β₯β0)) |
151 | | fzpred 13489 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β0) β (0...π) = ({0} βͺ ((0 + 1)...π))) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π) = ({0} βͺ ((0 + 1)...π))) |
153 | 152 | difeq1d 4081 |
. . . . . . . . . . . . . 14
β’ (π β ((0...π) β (1...π)) = (({0} βͺ ((0 + 1)...π)) β (1...π))) |
154 | | difun2 4440 |
. . . . . . . . . . . . . . 15
β’ (({0}
βͺ (1...π)) β
(1...π)) = ({0} β
(1...π)) |
155 | | 0p1e1 12275 |
. . . . . . . . . . . . . . . . . 18
β’ (0 + 1) =
1 |
156 | 155 | oveq1i 7367 |
. . . . . . . . . . . . . . . . 17
β’ ((0 +
1)...π) = (1...π) |
157 | 156 | uneq2i 4120 |
. . . . . . . . . . . . . . . 16
β’ ({0}
βͺ ((0 + 1)...π)) = ({0}
βͺ (1...π)) |
158 | 157 | difeq1i 4078 |
. . . . . . . . . . . . . . 15
β’ (({0}
βͺ ((0 + 1)...π))
β (1...π)) = (({0}
βͺ (1...π)) β
(1...π)) |
159 | | incom 4161 |
. . . . . . . . . . . . . . . . 17
β’ ({0}
β© (1...π)) =
((1...π) β©
{0}) |
160 | | elfznn 13470 |
. . . . . . . . . . . . . . . . . . 19
β’ (0 β
(1...π) β 0 β
β) |
161 | 9, 160 | mto 196 |
. . . . . . . . . . . . . . . . . 18
β’ Β¬ 0
β (1...π) |
162 | | disjsn 4672 |
. . . . . . . . . . . . . . . . . 18
β’
(((1...π) β© {0})
= β
β Β¬ 0 β (1...π)) |
163 | 161, 162 | mpbir 230 |
. . . . . . . . . . . . . . . . 17
β’
((1...π) β© {0})
= β
|
164 | 159, 163 | eqtri 2764 |
. . . . . . . . . . . . . . . 16
β’ ({0}
β© (1...π)) =
β
|
165 | | disj3 4413 |
. . . . . . . . . . . . . . . 16
β’ (({0}
β© (1...π)) = β
β {0} = ({0} β (1...π))) |
166 | 164, 165 | mpbi 229 |
. . . . . . . . . . . . . . 15
β’ {0} =
({0} β (1...π)) |
167 | 154, 158,
166 | 3eqtr4i 2774 |
. . . . . . . . . . . . . 14
β’ (({0}
βͺ ((0 + 1)...π))
β (1...π)) =
{0} |
168 | 153, 167 | eqtrdi 2792 |
. . . . . . . . . . . . 13
β’ (π β ((0...π) β (1...π)) = {0}) |
169 | 168 | eleq2d 2823 |
. . . . . . . . . . . 12
β’ (π β ((2nd
βπ§) β
((0...π) β (1...π)) β (2nd
βπ§) β
{0})) |
170 | | eldif 3920 |
. . . . . . . . . . . 12
β’
((2nd βπ§) β ((0...π) β (1...π)) β ((2nd βπ§) β (0...π) β§ Β¬ (2nd βπ§) β (1...π))) |
171 | 141 | elsn 4601 |
. . . . . . . . . . . 12
β’
((2nd βπ§) β {0} β (2nd
βπ§) =
0) |
172 | 169, 170,
171 | 3bitr3g 312 |
. . . . . . . . . . 11
β’ (π β (((2nd
βπ§) β (0...π) β§ Β¬ (2nd
βπ§) β (1...π)) β (2nd
βπ§) =
0)) |
173 | 147, 172 | bitr3d 280 |
. . . . . . . . . 10
β’ (π β (((2nd
βπ§) β (0...π) β§ (Β¬ (2nd
βπ§) β
(1...(π β 1)) β§
Β¬ (2nd βπ§) = π)) β (2nd βπ§) = 0)) |
174 | 173 | biimpd 228 |
. . . . . . . . 9
β’ (π β (((2nd
βπ§) β (0...π) β§ (Β¬ (2nd
βπ§) β
(1...(π β 1)) β§
Β¬ (2nd βπ§) = π)) β (2nd βπ§) = 0)) |
175 | 174 | expdimp 453 |
. . . . . . . 8
β’ ((π β§ (2nd
βπ§) β (0...π)) β ((Β¬
(2nd βπ§)
β (1...(π β 1))
β§ Β¬ (2nd βπ§) = π) β (2nd βπ§) = 0)) |
176 | 115, 175 | sylan2 593 |
. . . . . . 7
β’ ((π β§ π§ β π) β ((Β¬ (2nd
βπ§) β
(1...(π β 1)) β§
Β¬ (2nd βπ§) = π) β (2nd βπ§) = 0)) |
177 | 113, 176 | mpand 693 |
. . . . . 6
β’ ((π β§ π§ β π) β (Β¬ (2nd βπ§) = π β (2nd βπ§) = 0)) |
178 | 1, 2, 3 | poimirlem13 36091 |
. . . . . . . . . 10
β’ (π β β*π§ β π (2nd βπ§) = 0) |
179 | | fveqeq2 6851 |
. . . . . . . . . . 11
β’ (π§ = π β ((2nd βπ§) = 0 β (2nd
βπ ) =
0)) |
180 | 179 | rmo4 3688 |
. . . . . . . . . 10
β’
(β*π§ β
π (2nd
βπ§) = 0 β
βπ§ β π βπ β π (((2nd βπ§) = 0 β§ (2nd βπ ) = 0) β π§ = π )) |
181 | 178, 180 | sylib 217 |
. . . . . . . . 9
β’ (π β βπ§ β π βπ β π (((2nd βπ§) = 0 β§ (2nd βπ ) = 0) β π§ = π )) |
182 | 181 | r19.21bi 3234 |
. . . . . . . 8
β’ ((π β§ π§ β π) β βπ β π (((2nd βπ§) = 0 β§ (2nd βπ ) = 0) β π§ = π )) |
183 | 4 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π§ β π) β π β π) |
184 | | fveqeq2 6851 |
. . . . . . . . . . 11
β’ (π = π β ((2nd βπ ) = 0 β (2nd
βπ) =
0)) |
185 | 184 | anbi2d 629 |
. . . . . . . . . 10
β’ (π = π β (((2nd βπ§) = 0 β§ (2nd
βπ ) = 0) β
((2nd βπ§)
= 0 β§ (2nd βπ) = 0))) |
186 | | eqeq2 2748 |
. . . . . . . . . 10
β’ (π = π β (π§ = π β π§ = π)) |
187 | 185, 186 | imbi12d 344 |
. . . . . . . . 9
β’ (π = π β ((((2nd βπ§) = 0 β§ (2nd
βπ ) = 0) β π§ = π ) β (((2nd βπ§) = 0 β§ (2nd
βπ) = 0) β π§ = π))) |
188 | 187 | rspccv 3578 |
. . . . . . . 8
β’
(βπ β
π (((2nd
βπ§) = 0 β§
(2nd βπ ) =
0) β π§ = π ) β (π β π β (((2nd βπ§) = 0 β§ (2nd
βπ) = 0) β π§ = π))) |
189 | 182, 183,
188 | sylc 65 |
. . . . . . 7
β’ ((π β§ π§ β π) β (((2nd βπ§) = 0 β§ (2nd
βπ) = 0) β π§ = π)) |
190 | 8, 189 | mpan2d 692 |
. . . . . 6
β’ ((π β§ π§ β π) β ((2nd βπ§) = 0 β π§ = π)) |
191 | 177, 190 | syld 47 |
. . . . 5
β’ ((π β§ π§ β π) β (Β¬ (2nd βπ§) = π β π§ = π)) |
192 | 191 | necon1ad 2960 |
. . . 4
β’ ((π β§ π§ β π) β (π§ β π β (2nd βπ§) = π)) |
193 | 192 | ralrimiva 3143 |
. . 3
β’ (π β βπ§ β π (π§ β π β (2nd βπ§) = π)) |
194 | 1, 2, 3 | poimirlem14 36092 |
. . 3
β’ (π β β*π§ β π (2nd βπ§) = π) |
195 | | rmoim 3698 |
. . 3
β’
(βπ§ β
π (π§ β π β (2nd βπ§) = π) β (β*π§ β π (2nd βπ§) = π β β*π§ β π π§ β π)) |
196 | 193, 194,
195 | sylc 65 |
. 2
β’ (π β β*π§ β π π§ β π) |
197 | | reu5 3355 |
. 2
β’
(β!π§ β
π π§ β π β (βπ§ β π π§ β π β§ β*π§ β π π§ β π)) |
198 | 7, 196, 197 | sylanbrc 583 |
1
β’ (π β β!π§ β π π§ β π) |