Step | Hyp | Ref
| Expression |
1 | | 1zzd 10965 |
. . . . 5
   
             |
2 | | ballotthOLD.m |
. . . . . . . 8
 |
3 | | ballotthOLD.n |
. . . . . . . 8
 |
4 | | nnaddcl 10628 |
. . . . . . . 8
 
     |
5 | 2, 3, 4 | mp2an 677 |
. . . . . . 7
   |
6 | 5 | nnzi 10958 |
. . . . . 6
   |
7 | 6 | a1i 11 |
. . . . 5
   
               |
8 | | ballotthOLD.o |
. . . . . . . . 9
     
        |
9 | | ballotthOLD.p |
. . . . . . . . 9
              |
10 | | ballotthOLD.f |
. . . . . . . . 9
          
                |
11 | | ballotthOLD.e |
. . . . . . . . 9
                   |
12 | | ballotthOLD.mgtn |
. . . . . . . . 9
 |
13 | | ballotthOLD.i |
. . . . . . . . 9
                      
  |
14 | | ballotthOLD.s |
. . . . . . . . 9
                              |
15 | 2, 3, 8, 9, 10, 11, 12, 13, 14 | ballotlemsdomOLD 29375 |
. . . . . . . 8
   
                       |
16 | | elfzelz 11797 |
. . . . . . . 8
            
 
          |
17 | 15, 16 | syl 17 |
. . . . . . 7
   
                 |
18 | 17 | 3adant3 1027 |
. . . . . 6
   
                     |
19 | 18, 1 | zsubcld 11042 |
. . . . 5
   
                       |
20 | 2, 3, 8, 9, 10, 11, 12, 13, 14 | ballotlemsgt1OLD 29374 |
. . . . . 6
   
          
          |
21 | | zltlem1 10986 |
. . . . . . 7
                                 |
22 | 21 | biimpa 487 |
. . . . . 6
                    
            |
23 | 1, 18, 20, 22 | syl21anc 1266 |
. . . . 5
   
          
            |
24 | 18 | zred 11037 |
. . . . . . 7
   
                     |
25 | | 1red 9655 |
. . . . . . 7
   
             |
26 | 24, 25 | resubcld 10044 |
. . . . . 6
   
                       |
27 | | simp1 1007 |
. . . . . . . 8
   
          
    |
28 | 2, 3, 8, 9, 10, 11, 12, 13 | ballotlemiexOLD 29365 |
. . . . . . . . 9
                             |
29 | 28 | simpld 461 |
. . . . . . . 8
          
    |
30 | | elfzelz 11797 |
. . . . . . . 8
                 |
31 | 27, 29, 30 | 3syl 18 |
. . . . . . 7
   
                 |
32 | 31 | zred 11037 |
. . . . . 6
   
                 |
33 | 7 | zred 11037 |
. . . . . 6
   
               |
34 | | elfzelz 11797 |
. . . . . . . . . . . 12
         |
35 | 34 | 3ad2ant2 1029 |
. . . . . . . . . . 11
   
          
  |
36 | | elfzle1 11799 |
. . . . . . . . . . . 12
         |
37 | 36 | 3ad2ant2 1029 |
. . . . . . . . . . 11
   
          
  |
38 | 35 | zred 11037 |
. . . . . . . . . . . 12
   
          
  |
39 | | simp3 1009 |
. . . . . . . . . . . 12
   
                 |
40 | 38, 32, 39 | ltled 9780 |
. . . . . . . . . . 11
   
                 |
41 | | elfz4 11790 |
. . . . . . . . . . 11
      
 
     
          |
42 | 1, 31, 35, 37, 40, 41 | syl32anc 1275 |
. . . . . . . . . 10
   
          
          |
43 | 2, 3, 8, 9, 10, 11, 12, 13, 14 | ballotlemsel1iOLD 29376 |
. . . . . . . . . 10
   
                           |
44 | 27, 42, 43 | syl2anc 666 |
. . . . . . . . 9
   
                             |
45 | | elfzle2 11800 |
. . . . . . . . 9
                
              |
46 | 44, 45 | syl 17 |
. . . . . . . 8
   
                  
      |
47 | | zlem1lt 10985 |
. . . . . . . . 9
                                             |
48 | 18, 31, 47 | syl2anc 666 |
. . . . . . . 8
   
                                         |
49 | 46, 48 | mpbid 214 |
. . . . . . 7
   
                           |
50 | 26, 32, 49 | ltled 9780 |
. . . . . 6
   
                    
      |
51 | | elfzle2 11800 |
. . . . . . 7
                   |
52 | 27, 29, 51 | 3syl 18 |
. . . . . 6
   
              
    |
53 | 26, 32, 33, 50, 52 | letrd 9789 |
. . . . 5
   
                    
    |
54 | | elfz4 11790 |
. . . . 5
                                                           |
55 | 1, 7, 19, 23, 53, 54 | syl32anc 1275 |
. . . 4
   
                             |
56 | | fvex 5873 |
. . . . . . . . . 10
     |
57 | | ovex 6316 |
. . . . . . . . . 10
           |
58 | 56, 57 | brcnv 5016 |
. . . . . . . . 9
               
                |
59 | 49, 58 | sylibr 216 |
. . . . . . . 8
   
                            |
60 | 2, 3, 8, 9, 10, 11, 12, 13 | ballotlemiOLD 29364 |
. . . . . . . . . 10
                          
  |
61 | 60 | breq1d 4411 |
. . . . . . . . 9
                         
            
              |
62 | 61 | 3ad2ant1 1028 |
. . . . . . . 8
   
                                 
            
              |
63 | 59, 62 | mpbid 214 |
. . . . . . 7
   
                 
            
             |
64 | | gtso 9712 |
. . . . . . . . . 10
 |
65 | 64 | a1i 11 |
. . . . . . . . 9
     |
66 | 2, 3, 8, 9, 10, 11, 12, 13 | ballotlemsupOLD 29368 |
. . . . . . . . 9
                       
                         |
67 | 65, 66 | supub 7970 |
. . . . . . . 8
                                                 
              |
68 | 67 | con2d 119 |
. . . . . . 7
          
            
                                        |
69 | 27, 63, 68 | sylc 62 |
. . . . . 6
   
                                       |
70 | | fveq2 5863 |
. . . . . . . 8
                                       |
71 | 70 | eqeq1d 2452 |
. . . . . . 7
                                         |
72 | 71 | elrab 3195 |
. . . . . 6
               
          
                                      |
73 | 69, 72 | sylnib 306 |
. . . . 5
   
                                                 |
74 | | imnan 424 |
. . . . 5
                                                                           |
75 | 73, 74 | sylibr 216 |
. . . 4
   
                           
                     |
76 | 55, 75 | mpd 15 |
. . 3
   
                               |
77 | 76 | neqned 2630 |
. 2
   
                               |
78 | | ballotthOLD.r |
. . . . . . . . . 10
             |
79 | 2, 3, 8, 9, 10, 11, 12, 13, 14, 78 | ballotlemroOLD 29386 |
. . . . . . . . 9
         |
80 | 79 | adantr 467 |
. . . . . . . 8
   
               |
81 | | elfzelz 11797 |
. . . . . . . . 9
           |
82 | 81 | adantl 468 |
. . . . . . . 8
   
           |
83 | 2, 3, 8, 9, 10, 80, 82 | ballotlemfelz 29316 |
. . . . . . 7
   
                       |
84 | 83 | zcnd 11038 |
. . . . . 6
   
                       |
85 | 84 | negeq0d 9975 |
. . . . 5
   
                                      |
86 | | eqid 2450 |
. . . . . . 7
                       
           |
87 | 2, 3, 8, 9, 10, 11, 12, 13, 14, 78, 86 | ballotlemfrceqOLD 29392 |
. . . . . 6
   
                                          |
88 | 87 | eqeq1d 2452 |
. . . . 5
   
                                            |
89 | 85, 88 | bitr4d 260 |
. . . 4
   
                                           |
90 | 89 | necon3bid 2667 |
. . 3
   
                                           |
91 | 27, 42, 90 | syl2anc 666 |
. 2
   
                                             |
92 | 77, 91 | mpbird 236 |
1
   
                         |