Step | Hyp | Ref
| Expression |
1 | | ssrab2 3687 |
. . . . 5
|
2 | | ballotth.m |
. . . . . . 7
|
3 | | ballotth.n |
. . . . . . 7
|
4 | | ballotth.o |
. . . . . . 7
|
5 | 2, 3, 4 | ballotlemoex 30547 |
. . . . . 6
|
6 | 5 | elpw2 4828 |
. . . . 5
|
7 | 1, 6 | mpbir 221 |
. . . 4
|
8 | | fveq2 6191 |
. . . . . 6
|
9 | 8 | oveq1d 6665 |
. . . . 5
|
10 | | ballotth.p |
. . . . 5
|
11 | | ovex 6678 |
. . . . 5
|
12 | 9, 10, 11 | fvmpt 6282 |
. . . 4
|
13 | 7, 12 | ax-mp 5 |
. . 3
|
14 | | an32 839 |
. . . . . . . . 9
|
15 | | 2eluzge1 11734 |
. . . . . . . . . . . . . . 15
|
16 | | fzss1 12380 |
. . . . . . . . . . . . . . 15
|
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
18 | | sspwb 4917 |
. . . . . . . . . . . . . 14
|
19 | 17, 18 | mpbi 220 |
. . . . . . . . . . . . 13
|
20 | 19 | sseli 3599 |
. . . . . . . . . . . 12
|
21 | | 1lt2 11194 |
. . . . . . . . . . . . . . . . 17
|
22 | | 1re 10039 |
. . . . . . . . . . . . . . . . . 18
|
23 | | 2re 11090 |
. . . . . . . . . . . . . . . . . 18
|
24 | 22, 23 | ltnlei 10158 |
. . . . . . . . . . . . . . . . 17
|
25 | 21, 24 | mpbi 220 |
. . . . . . . . . . . . . . . 16
|
26 | | elfzle1 12344 |
. . . . . . . . . . . . . . . 16
|
27 | 25, 26 | mto 188 |
. . . . . . . . . . . . . . 15
|
28 | | elelpwi 4171 |
. . . . . . . . . . . . . . 15
|
29 | 27, 28 | mto 188 |
. . . . . . . . . . . . . 14
|
30 | | ancom 466 |
. . . . . . . . . . . . . 14
|
31 | 29, 30 | mtbi 312 |
. . . . . . . . . . . . 13
|
32 | 31 | imnani 439 |
. . . . . . . . . . . 12
|
33 | 20, 32 | jca 554 |
. . . . . . . . . . 11
|
34 | | ssin 3835 |
. . . . . . . . . . . . 13
|
35 | | 1le2 11241 |
. . . . . . . . . . . . . . . . . . . . . 22
|
36 | | 1p1e2 11134 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
37 | | nnge1 11046 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
38 | 2, 37 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
39 | | nnge1 11046 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
40 | 3, 39 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
41 | 2 | nnrei 11029 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
42 | 3 | nnrei 11029 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
43 | 22, 22, 41, 42 | le2addi 10591 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
44 | 38, 40, 43 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
45 | 36, 44 | eqbrtrri 4676 |
. . . . . . . . . . . . . . . . . . . . . 22
|
46 | 41, 42 | readdcli 10053 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
47 | 22, 23, 46 | letri 10166 |
. . . . . . . . . . . . . . . . . . . . . 22
|
48 | 35, 45, 47 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . 21
|
49 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . . . 22
|
50 | | nnaddcl 11042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
51 | 2, 3, 50 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
52 | 51 | nnzi 11401 |
. . . . . . . . . . . . . . . . . . . . . 22
|
53 | | eluz 11701 |
. . . . . . . . . . . . . . . . . . . . . 22
|
54 | 49, 52, 53 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . 21
|
55 | 48, 54 | mpbir 221 |
. . . . . . . . . . . . . . . . . . . 20
|
56 | | elfzp12 12419 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
58 | 57 | biimpi 206 |
. . . . . . . . . . . . . . . . . 18
|
59 | 58 | orcanai 952 |
. . . . . . . . . . . . . . . . 17
|
60 | 36 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
|
61 | 59, 60 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
|
62 | 61 | ss2abi 3674 |
. . . . . . . . . . . . . . 15
|
63 | | inab 3895 |
. . . . . . . . . . . . . . . 16
|
64 | | abid2 2745 |
. . . . . . . . . . . . . . . . 17
|
65 | 64 | ineq1i 3810 |
. . . . . . . . . . . . . . . 16
|
66 | 63, 65 | eqtr3i 2646 |
. . . . . . . . . . . . . . 15
|
67 | | abid2 2745 |
. . . . . . . . . . . . . . 15
|
68 | 62, 66, 67 | 3sstr3i 3643 |
. . . . . . . . . . . . . 14
|
69 | | sstr 3611 |
. . . . . . . . . . . . . 14
|
70 | 68, 69 | mpan2 707 |
. . . . . . . . . . . . 13
|
71 | 34, 70 | sylbi 207 |
. . . . . . . . . . . 12
|
72 | | selpw 4165 |
. . . . . . . . . . . . 13
|
73 | | ssab 3672 |
. . . . . . . . . . . . . 14
|
74 | | df-ex 1705 |
. . . . . . . . . . . . . . . . 17
|
75 | 74 | bicomi 214 |
. . . . . . . . . . . . . . . 16
|
76 | 75 | con1bii 346 |
. . . . . . . . . . . . . . 15
|
77 | | df-clel 2618 |
. . . . . . . . . . . . . . . 16
|
78 | 77 | notbii 310 |
. . . . . . . . . . . . . . 15
|
79 | | imnang 1769 |
. . . . . . . . . . . . . . . 16
|
80 | | ancom 466 |
. . . . . . . . . . . . . . . . . 18
|
81 | 80 | notbii 310 |
. . . . . . . . . . . . . . . . 17
|
82 | 81 | albii 1747 |
. . . . . . . . . . . . . . . 16
|
83 | 79, 82 | bitr4i 267 |
. . . . . . . . . . . . . . 15
|
84 | 76, 78, 83 | 3bitr4ri 293 |
. . . . . . . . . . . . . 14
|
85 | 73, 84 | bitr2i 265 |
. . . . . . . . . . . . 13
|
86 | 72, 85 | anbi12i 733 |
. . . . . . . . . . . 12
|
87 | | selpw 4165 |
. . . . . . . . . . . 12
|
88 | 71, 86, 87 | 3imtr4i 281 |
. . . . . . . . . . 11
|
89 | 33, 88 | impbii 199 |
. . . . . . . . . 10
|
90 | 89 | anbi1i 731 |
. . . . . . . . 9
|
91 | 4 | rabeq2i 3197 |
. . . . . . . . . 10
|
92 | 91 | anbi1i 731 |
. . . . . . . . 9
|
93 | 14, 90, 92 | 3bitr4i 292 |
. . . . . . . 8
|
94 | 93 | abbii 2739 |
. . . . . . 7
|
95 | | df-rab 2921 |
. . . . . . 7
|
96 | | df-rab 2921 |
. . . . . . 7
|
97 | 94, 95, 96 | 3eqtr4i 2654 |
. . . . . 6
|
98 | 97 | fveq2i 6194 |
. . . . 5
|
99 | | fzfi 12771 |
. . . . . . 7
|
100 | 2 | nnzi 11401 |
. . . . . . 7
|
101 | | hashbc 13237 |
. . . . . . 7
|
102 | 99, 100, 101 | mp2an 708 |
. . . . . 6
|
103 | | 2z 11409 |
. . . . . . . . . . . 12
|
104 | 103 | eluz1i 11695 |
. . . . . . . . . . 11
|
105 | 52, 45, 104 | mpbir2an 955 |
. . . . . . . . . 10
|
106 | | hashfz 13214 |
. . . . . . . . . 10
|
107 | 105, 106 | ax-mp 5 |
. . . . . . . . 9
|
108 | 2 | nncni 11030 |
. . . . . . . . . . 11
|
109 | 3 | nncni 11030 |
. . . . . . . . . . 11
|
110 | 108, 109 | addcli 10044 |
. . . . . . . . . 10
|
111 | | 2cn 11091 |
. . . . . . . . . 10
|
112 | | ax-1cn 9994 |
. . . . . . . . . 10
|
113 | | subadd23 10293 |
. . . . . . . . . 10
|
114 | 110, 111,
112, 113 | mp3an 1424 |
. . . . . . . . 9
|
115 | 111, 112 | negsubdi2i 10367 |
. . . . . . . . . . 11
|
116 | | 2m1e1 11135 |
. . . . . . . . . . . 12
|
117 | 116 | negeqi 10274 |
. . . . . . . . . . 11
|
118 | 115, 117 | eqtr3i 2646 |
. . . . . . . . . 10
|
119 | 118 | oveq2i 6661 |
. . . . . . . . 9
|
120 | 107, 114,
119 | 3eqtri 2648 |
. . . . . . . 8
|
121 | 110, 112 | negsubi 10359 |
. . . . . . . 8
|
122 | 120, 121 | eqtri 2644 |
. . . . . . 7
|
123 | 122 | oveq1i 6660 |
. . . . . 6
|
124 | 102, 123 | eqtr3i 2646 |
. . . . 5
|
125 | 98, 124 | eqtr3i 2646 |
. . . 4
|
126 | 2, 3, 4 | ballotlem1 30548 |
. . . 4
|
127 | 125, 126 | oveq12i 6662 |
. . 3
|
128 | 13, 127 | eqtri 2644 |
. 2
|
129 | | 0le1 10551 |
. . . . 5
|
130 | | 0re 10040 |
. . . . . 6
|
131 | 130, 22, 41 | letri 10166 |
. . . . 5
|
132 | 129, 38, 131 | mp2an 708 |
. . . 4
|
133 | 3 | nngt0i 11054 |
. . . . . 6
|
134 | 42, 133 | elrpii 11835 |
. . . . 5
|
135 | | ltaddrp 11867 |
. . . . 5
|
136 | 41, 134, 135 | mp2an 708 |
. . . 4
|
137 | | 0z 11388 |
. . . . 5
|
138 | | elfzm11 12411 |
. . . . 5
|
139 | 137, 52, 138 | mp2an 708 |
. . . 4
|
140 | 100, 132,
136, 139 | mpbir3an 1244 |
. . 3
|
141 | | bcm1n 29554 |
. . 3
|
142 | 140, 51, 141 | mp2an 708 |
. 2
|
143 | | pncan2 10288 |
. . . 4
|
144 | 108, 109,
143 | mp2an 708 |
. . 3
|
145 | 144 | oveq1i 6660 |
. 2
|
146 | 128, 142,
145 | 3eqtri 2648 |
1
|