Step | Hyp | Ref
| Expression |
1 | | 1z 10791 |
. . . . . 6
 |
2 | 1 | a1i 11 |
. . . . 5
   
             |
3 | | ballotth.m |
. . . . . . . 8
 |
4 | | ballotth.n |
. . . . . . . 8
 |
5 | | nnaddcl 10459 |
. . . . . . . 8
 
     |
6 | 3, 4, 5 | mp2an 672 |
. . . . . . 7
   |
7 | 6 | nnzi 10785 |
. . . . . 6
   |
8 | 7 | a1i 11 |
. . . . 5
   
               |
9 | | ballotth.o |
. . . . . . . . 9
     
        |
10 | | ballotth.p |
. . . . . . . . 9
              |
11 | | ballotth.f |
. . . . . . . . 9
          
                |
12 | | ballotth.e |
. . . . . . . . 9
                   |
13 | | ballotth.mgtn |
. . . . . . . . 9
 |
14 | | ballotth.i |
. . . . . . . . 9
                      
  |
15 | | ballotth.s |
. . . . . . . . 9
                              |
16 | 3, 4, 9, 10, 11, 12, 13, 14, 15 | ballotlemsdom 27061 |
. . . . . . . 8
   
                       |
17 | | elfzelz 11574 |
. . . . . . . 8
            
 
          |
18 | 16, 17 | syl 16 |
. . . . . . 7
   
                 |
19 | 18 | 3adant3 1008 |
. . . . . 6
   
                     |
20 | 19, 2 | zsubcld 10867 |
. . . . 5
   
                       |
21 | 3, 4, 9, 10, 11, 12, 13, 14, 15 | ballotlemsgt1 27060 |
. . . . . 6
   
          
          |
22 | | zltlem1 10812 |
. . . . . . 7
                                 |
23 | 22 | biimpa 484 |
. . . . . 6
                    
            |
24 | 2, 19, 21, 23 | syl21anc 1218 |
. . . . 5
   
          
            |
25 | 19 | zred 10862 |
. . . . . . 7
   
                     |
26 | | 1re 9500 |
. . . . . . . 8
 |
27 | 26 | a1i 11 |
. . . . . . 7
   
             |
28 | 25, 27 | resubcld 9891 |
. . . . . 6
   
                       |
29 | | simp1 988 |
. . . . . . . 8
   
          
    |
30 | 3, 4, 9, 10, 11, 12, 13, 14 | ballotlemiex 27051 |
. . . . . . . . 9
                             |
31 | 30 | simpld 459 |
. . . . . . . 8
          
    |
32 | | elfzelz 11574 |
. . . . . . . 8
                 |
33 | 29, 31, 32 | 3syl 20 |
. . . . . . 7
   
                 |
34 | 33 | zred 10862 |
. . . . . 6
   
                 |
35 | 8 | zred 10862 |
. . . . . 6
   
               |
36 | | elfzelz 11574 |
. . . . . . . . . . . 12
         |
37 | 36 | 3ad2ant2 1010 |
. . . . . . . . . . 11
   
          
  |
38 | | elfzle1 11575 |
. . . . . . . . . . . 12
         |
39 | 38 | 3ad2ant2 1010 |
. . . . . . . . . . 11
   
          
  |
40 | 37 | zred 10862 |
. . . . . . . . . . . 12
   
          
  |
41 | | simp3 990 |
. . . . . . . . . . . 12
   
                 |
42 | 40, 34, 41 | ltled 9637 |
. . . . . . . . . . 11
   
                 |
43 | | elfz4 11567 |
. . . . . . . . . . 11
      
 
     
          |
44 | 2, 33, 37, 39, 42, 43 | syl32anc 1227 |
. . . . . . . . . 10
   
          
          |
45 | 3, 4, 9, 10, 11, 12, 13, 14, 15 | ballotlemsel1i 27062 |
. . . . . . . . . 10
   
                           |
46 | 29, 44, 45 | syl2anc 661 |
. . . . . . . . 9
   
                             |
47 | | elfzle2 11576 |
. . . . . . . . 9
                
              |
48 | 46, 47 | syl 16 |
. . . . . . . 8
   
                  
      |
49 | | zlem1lt 10811 |
. . . . . . . . 9
                                             |
50 | 19, 33, 49 | syl2anc 661 |
. . . . . . . 8
   
                                         |
51 | 48, 50 | mpbid 210 |
. . . . . . 7
   
                           |
52 | 28, 34, 51 | ltled 9637 |
. . . . . 6
   
                    
      |
53 | | elfzle2 11576 |
. . . . . . 7
                   |
54 | 29, 31, 53 | 3syl 20 |
. . . . . 6
   
              
    |
55 | 28, 34, 35, 52, 54 | letrd 9643 |
. . . . 5
   
                    
    |
56 | | elfz4 11567 |
. . . . 5
                                                           |
57 | 2, 8, 20, 24, 55, 56 | syl32anc 1227 |
. . . 4
   
                             |
58 | | fvex 5812 |
. . . . . . . . . 10
     |
59 | | ovex 6228 |
. . . . . . . . . 10
           |
60 | 58, 59 | brcnv 5133 |
. . . . . . . . 9
               
                |
61 | 51, 60 | sylibr 212 |
. . . . . . . 8
   
                            |
62 | 3, 4, 9, 10, 11, 12, 13, 14 | ballotlemi 27050 |
. . . . . . . . . 10
                          
  |
63 | 62 | breq1d 4413 |
. . . . . . . . 9
                         
            
              |
64 | 63 | 3ad2ant1 1009 |
. . . . . . . 8
   
                                 
            
              |
65 | 61, 64 | mpbid 210 |
. . . . . . 7
   
                 
            
             |
66 | | ltso 9570 |
. . . . . . . . . . 11
 |
67 | | cnvso 5487 |
. . . . . . . . . . 11
  |
68 | 66, 67 | mpbi 208 |
. . . . . . . . . 10
 |
69 | 68 | a1i 11 |
. . . . . . . . 9
     |
70 | 3, 4, 9, 10, 11, 12, 13, 14 | ballotlemsup 27054 |
. . . . . . . . 9
                       
                         |
71 | 69, 70 | supub 7824 |
. . . . . . . 8
                                                 
              |
72 | 71 | con2d 115 |
. . . . . . 7
          
            
                                        |
73 | 29, 65, 72 | sylc 60 |
. . . . . 6
   
                                       |
74 | | fveq2 5802 |
. . . . . . . 8
                                       |
75 | 74 | eqeq1d 2456 |
. . . . . . 7
                                         |
76 | 75 | elrab 3224 |
. . . . . 6
               
          
                                      |
77 | 73, 76 | sylnib 304 |
. . . . 5
   
                                                 |
78 | | imnan 422 |
. . . . 5
                                                                           |
79 | 77, 78 | sylibr 212 |
. . . 4
   
                           
                     |
80 | 57, 79 | mpd 15 |
. . 3
   
                               |
81 | 80 | neneqad 2656 |
. 2
   
                               |
82 | | ballotth.r |
. . . . . . . . . 10
             |
83 | 3, 4, 9, 10, 11, 12, 13, 14, 15, 82 | ballotlemro 27072 |
. . . . . . . . 9
         |
84 | 83 | adantr 465 |
. . . . . . . 8
   
               |
85 | | elfzelz 11574 |
. . . . . . . . 9
           |
86 | 85 | adantl 466 |
. . . . . . . 8
   
           |
87 | 3, 4, 9, 10, 11, 84, 86 | ballotlemfelz 27040 |
. . . . . . 7
   
                       |
88 | 87 | zcnd 10863 |
. . . . . 6
   
                       |
89 | 88 | negeq0d 9826 |
. . . . 5
   
                                      |
90 | | eqid 2454 |
. . . . . . 7
                       
           |
91 | 3, 4, 9, 10, 11, 12, 13, 14, 15, 82, 90 | ballotlemfrceq 27078 |
. . . . . 6
   
                                          |
92 | 91 | eqeq1d 2456 |
. . . . 5
   
                                            |
93 | 89, 92 | bitr4d 256 |
. . . 4
   
                                           |
94 | 93 | necon3bid 2710 |
. . 3
   
                                           |
95 | 29, 44, 94 | syl2anc 661 |
. 2
   
                                             |
96 | 81, 95 | mpbird 232 |
1
   
                         |