Step | Hyp | Ref
| Expression |
1 | | nnex 12220 |
. . . . . . . . . . . . 13
β’ β
β V |
2 | 1 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β
V) |
3 | | reprinfz1.a |
. . . . . . . . . . . 12
β’ (π β π΄ β β) |
4 | 2, 3 | ssexd 5324 |
. . . . . . . . . . 11
β’ (π β π΄ β V) |
5 | | ovex 7444 |
. . . . . . . . . . 11
β’
(0..^π) β
V |
6 | | elmapg 8835 |
. . . . . . . . . . 11
β’ ((π΄ β V β§ (0..^π) β V) β (π β (π΄ βm (0..^π)) β π:(0..^π)βΆπ΄)) |
7 | 4, 5, 6 | sylancl 586 |
. . . . . . . . . 10
β’ (π β (π β (π΄ βm (0..^π)) β π:(0..^π)βΆπ΄)) |
8 | 7 | biimpa 477 |
. . . . . . . . 9
β’ ((π β§ π β (π΄ βm (0..^π))) β π:(0..^π)βΆπ΄) |
9 | 8 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π β (π΄ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β π:(0..^π)βΆπ΄) |
10 | | elmapfn 8861 |
. . . . . . . . . . 11
β’ (π β (π΄ βm (0..^π)) β π Fn (0..^π)) |
11 | 10 | ad2antlr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β π Fn (0..^π)) |
12 | | simplr 767 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β§ βπ β (0..^π) Β¬ (πβπ) β (1...π)) β Ξ£π β (0..^π)(πβπ) = π) |
13 | | reprinfz1.n |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β
β0) |
14 | 13 | nn0red 12535 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β) |
15 | 14 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β π β β) |
16 | 3 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β π΄ β β) |
17 | | simpllr 774 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β π β (π΄ βm (0..^π))) |
18 | 7 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β (π β (π΄ βm (0..^π)) β π:(0..^π)βΆπ΄)) |
19 | 17, 18 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β π:(0..^π)βΆπ΄) |
20 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β π β (0..^π)) |
21 | 19, 20 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β (πβπ) β π΄) |
22 | 16, 21 | sseldd 3983 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β (πβπ) β β) |
23 | 22 | nnred 12229 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β (πβπ) β β) |
24 | | fzofi 13941 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(0..^π) β
Fin |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β (0..^π) β Fin) |
26 | 3 | ad4antr 730 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β§ π β (0..^π)) β π΄ β β) |
27 | 19 | ffvelcdmda 7086 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β§ π β (0..^π)) β (πβπ) β π΄) |
28 | 26, 27 | sseldd 3983 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β§ π β (0..^π)) β (πβπ) β β) |
29 | 28 | nnred 12229 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β§ π β (0..^π)) β (πβπ) β β) |
30 | 25, 29 | fsumrecl 15682 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β Ξ£π β (0..^π)(πβπ) β β) |
31 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β Β¬ (πβπ) β (1...π)) |
32 | 13 | nn0zd 12586 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β β€) |
33 | 32 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β π β β€) |
34 | | fznn 13571 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β€ β ((πβπ) β (1...π) β ((πβπ) β β β§ (πβπ) β€ π))) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β ((πβπ) β (1...π) β ((πβπ) β β β§ (πβπ) β€ π))) |
36 | 22 | biantrurd 533 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β ((πβπ) β€ π β ((πβπ) β β β§ (πβπ) β€ π))) |
37 | 35, 36 | bitr4d 281 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β ((πβπ) β (1...π) β (πβπ) β€ π)) |
38 | 37 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β (Β¬ (πβπ) β (1...π) β Β¬ (πβπ) β€ π)) |
39 | 31, 38 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β Β¬ (πβπ) β€ π) |
40 | 15, 23 | ltnled 11363 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β (π < (πβπ) β Β¬ (πβπ) β€ π)) |
41 | 39, 40 | mpbird 256 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β π < (πβπ)) |
42 | 23 | recnd 11244 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β (πβπ) β β) |
43 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β (πβπ) = (πβπ)) |
44 | 43 | sumsn 15694 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (0..^π) β§ (πβπ) β β) β Ξ£π β {π} (πβπ) = (πβπ)) |
45 | 20, 42, 44 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β Ξ£π β {π} (πβπ) = (πβπ)) |
46 | 28 | nnnn0d 12534 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β§ π β (0..^π)) β (πβπ) β
β0) |
47 | | nn0ge0 12499 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πβπ) β β0 β 0 β€
(πβπ)) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β§ π β (0..^π)) β 0 β€ (πβπ)) |
49 | | snssi 4811 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0..^π) β {π} β (0..^π)) |
50 | 49 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β {π} β (0..^π)) |
51 | 25, 29, 48, 50 | fsumless 15744 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β Ξ£π β {π} (πβπ) β€ Ξ£π β (0..^π)(πβπ)) |
52 | 45, 51 | eqbrtrrd 5172 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β (πβπ) β€ Ξ£π β (0..^π)(πβπ)) |
53 | 15, 23, 30, 41, 52 | ltletrd 11376 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β π < Ξ£π β (0..^π)(πβπ)) |
54 | 15, 53 | ltned 11352 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β π β Ξ£π β (0..^π)(πβπ)) |
55 | 54 | necomd 2996 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ π β (0..^π)) β§ Β¬ (πβπ) β (1...π)) β Ξ£π β (0..^π)(πβπ) β π) |
56 | 55 | r19.29an 3158 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π΄ βm (0..^π))) β§ βπ β (0..^π) Β¬ (πβπ) β (1...π)) β Ξ£π β (0..^π)(πβπ) β π) |
57 | 56 | neneqd 2945 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π΄ βm (0..^π))) β§ βπ β (0..^π) Β¬ (πβπ) β (1...π)) β Β¬ Ξ£π β (0..^π)(πβπ) = π) |
58 | 57 | adantlr 713 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (π΄ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β§ βπ β (0..^π) Β¬ (πβπ) β (1...π)) β Β¬ Ξ£π β (0..^π)(πβπ) = π) |
59 | 12, 58 | pm2.65da 815 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π΄ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β Β¬ βπ β (0..^π) Β¬ (πβπ) β (1...π)) |
60 | | dfral2 3099 |
. . . . . . . . . . . 12
β’
(βπ β
(0..^π)(πβπ) β (1...π) β Β¬ βπ β (0..^π) Β¬ (πβπ) β (1...π)) |
61 | 59, 60 | sylibr 233 |
. . . . . . . . . . 11
β’ (((π β§ π β (π΄ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β βπ β (0..^π)(πβπ) β (1...π)) |
62 | 43 | eleq1d 2818 |
. . . . . . . . . . . 12
β’ (π = π β ((πβπ) β (1...π) β (πβπ) β (1...π))) |
63 | 62 | cbvralvw 3234 |
. . . . . . . . . . 11
β’
(βπ β
(0..^π)(πβπ) β (1...π) β βπ β (0..^π)(πβπ) β (1...π)) |
64 | 61, 63 | sylibr 233 |
. . . . . . . . . 10
β’ (((π β§ π β (π΄ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β βπ β (0..^π)(πβπ) β (1...π)) |
65 | 11, 64 | jca 512 |
. . . . . . . . 9
β’ (((π β§ π β (π΄ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β (π Fn (0..^π) β§ βπ β (0..^π)(πβπ) β (1...π))) |
66 | | ffnfv 7120 |
. . . . . . . . 9
β’ (π:(0..^π)βΆ(1...π) β (π Fn (0..^π) β§ βπ β (0..^π)(πβπ) β (1...π))) |
67 | 65, 66 | sylibr 233 |
. . . . . . . 8
β’ (((π β§ π β (π΄ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β π:(0..^π)βΆ(1...π)) |
68 | 9, 67 | jca 512 |
. . . . . . 7
β’ (((π β§ π β (π΄ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β (π:(0..^π)βΆπ΄ β§ π:(0..^π)βΆ(1...π))) |
69 | | fin 6771 |
. . . . . . 7
β’ (π:(0..^π)βΆ(π΄ β© (1...π)) β (π:(0..^π)βΆπ΄ β§ π:(0..^π)βΆ(1...π))) |
70 | 68, 69 | sylibr 233 |
. . . . . 6
β’ (((π β§ π β (π΄ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β π:(0..^π)βΆ(π΄ β© (1...π))) |
71 | | ovex 7444 |
. . . . . . . 8
β’
(1...π) β
V |
72 | 71 | inex2 5318 |
. . . . . . 7
β’ (π΄ β© (1...π)) β V |
73 | 72, 5 | elmap 8867 |
. . . . . 6
β’ (π β ((π΄ β© (1...π)) βm (0..^π)) β π:(0..^π)βΆ(π΄ β© (1...π))) |
74 | 70, 73 | sylibr 233 |
. . . . 5
β’ (((π β§ π β (π΄ βm (0..^π))) β§ Ξ£π β (0..^π)(πβπ) = π) β π β ((π΄ β© (1...π)) βm (0..^π))) |
75 | 74 | anasss 467 |
. . . 4
β’ ((π β§ (π β (π΄ βm (0..^π)) β§ Ξ£π β (0..^π)(πβπ) = π)) β π β ((π΄ β© (1...π)) βm (0..^π))) |
76 | 75 | rabss3d 4079 |
. . 3
β’ (π β {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π} β {π β ((π΄ β© (1...π)) βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π}) |
77 | | reprinfz1.s |
. . . 4
β’ (π β π β
β0) |
78 | 3, 32, 77 | reprval 33691 |
. . 3
β’ (π β (π΄(reprβπ)π) = {π β (π΄ βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π}) |
79 | | inss1 4228 |
. . . . . 6
β’ (π΄ β© (1...π)) β π΄ |
80 | 79 | a1i 11 |
. . . . 5
β’ (π β (π΄ β© (1...π)) β π΄) |
81 | 80, 3 | sstrd 3992 |
. . . 4
β’ (π β (π΄ β© (1...π)) β β) |
82 | 81, 32, 77 | reprval 33691 |
. . 3
β’ (π β ((π΄ β© (1...π))(reprβπ)π) = {π β ((π΄ β© (1...π)) βm (0..^π)) β£ Ξ£π β (0..^π)(πβπ) = π}) |
83 | 76, 78, 82 | 3sstr4d 4029 |
. 2
β’ (π β (π΄(reprβπ)π) β ((π΄ β© (1...π))(reprβπ)π)) |
84 | 3, 32, 77, 80 | reprss 33698 |
. 2
β’ (π β ((π΄ β© (1...π))(reprβπ)π) β (π΄(reprβπ)π)) |
85 | 83, 84 | eqssd 3999 |
1
β’ (π β (π΄(reprβπ)π) = ((π΄ β© (1...π))(reprβπ)π)) |