Step | Hyp | Ref
| Expression |
1 | | 1zzd 10965 |
. . . . 5
   
             |
2 | | ballotth.m |
. . . . . . . 8
 |
3 | | ballotth.n |
. . . . . . . 8
 |
4 | | nnaddcl 10628 |
. . . . . . . 8
 
     |
5 | 2, 3, 4 | mp2an 677 |
. . . . . . 7
   |
6 | 5 | nnzi 10958 |
. . . . . 6
   |
7 | 6 | a1i 11 |
. . . . 5
   
               |
8 | | ballotth.o |
. . . . . . . . 9
     
        |
9 | | ballotth.p |
. . . . . . . . 9
              |
10 | | ballotth.f |
. . . . . . . . 9
          
                |
11 | | ballotth.e |
. . . . . . . . 9
                   |
12 | | ballotth.mgtn |
. . . . . . . . 9
 |
13 | | ballotth.i |
. . . . . . . . 9
   inf     
               |
14 | | ballotth.s |
. . . . . . . . 9
                              |
15 | 2, 3, 8, 9, 10, 11, 12, 13, 14 | ballotlemsdom 29337 |
. . . . . . . 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 | ballotlemsgt1 29336 |
. . . . . 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 | ballotlemiex 29327 |
. . . . . . . . 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 | ballotlemsel1i 29338 |
. . . . . . . . . 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 | | biid 240 |
. . . . . . . . 9
              
                |
57 | 49, 56 | sylibr 216 |
. . . . . . . 8
   
                           |
58 | 2, 3, 8, 9, 10, 11, 12, 13 | ballotlemi 29326 |
. . . . . . . . . 10
       inf     
               |
59 | 58 | breq2d 4413 |
. . . . . . . . 9
                 
          inf                      |
60 | 59 | 3ad2ant1 1028 |
. . . . . . . 8
   
                                    inf                  
   |
61 | 57, 60 | mpbid 214 |
. . . . . . 7
   
                    
inf                     |
62 | | ltso 9711 |
. . . . . . . . . 10
 |
63 | 62 | a1i 11 |
. . . . . . . . 9
     |
64 | 2, 3, 8, 9, 10, 11, 12, 13 | ballotlemsup 29330 |
. . . . . . . . 9
                     
 
                      |
65 | 63, 64 | inflb 8002 |
. . . . . . . 8
                                       
inf                      |
66 | 65 | con2d 119 |
. . . . . . 7
             
inf                  
                             |
67 | 27, 61, 66 | sylc 62 |
. . . . . 6
   
                                       |
68 | | fveq2 5863 |
. . . . . . . 8
                                       |
69 | 68 | eqeq1d 2452 |
. . . . . . 7
                                         |
70 | 69 | elrab 3195 |
. . . . . 6
               
          
                                      |
71 | 67, 70 | sylnib 306 |
. . . . 5
   
                                                 |
72 | | imnan 424 |
. . . . 5
                                                                           |
73 | 71, 72 | sylibr 216 |
. . . 4
   
                           
                     |
74 | 55, 73 | mpd 15 |
. . 3
   
                               |
75 | 74 | neqned 2630 |
. 2
   
                               |
76 | | ballotth.r |
. . . . . . . . . 10
             |
77 | 2, 3, 8, 9, 10, 11, 12, 13, 14, 76 | ballotlemro 29348 |
. . . . . . . . 9
         |
78 | 77 | adantr 467 |
. . . . . . . 8
   
               |
79 | | elfzelz 11797 |
. . . . . . . . 9
           |
80 | 79 | adantl 468 |
. . . . . . . 8
   
           |
81 | 2, 3, 8, 9, 10, 78, 80 | ballotlemfelz 29316 |
. . . . . . 7
   
                       |
82 | 81 | zcnd 11038 |
. . . . . 6
   
                       |
83 | 82 | negeq0d 9975 |
. . . . 5
   
                                      |
84 | | eqid 2450 |
. . . . . . 7
                       
           |
85 | 2, 3, 8, 9, 10, 11, 12, 13, 14, 76, 84 | ballotlemfrceq 29354 |
. . . . . 6
   
                                          |
86 | 85 | eqeq1d 2452 |
. . . . 5
   
                                            |
87 | 83, 86 | bitr4d 260 |
. . . 4
   
                                           |
88 | 87 | necon3bid 2667 |
. . 3
   
                                           |
89 | 27, 42, 88 | syl2anc 666 |
. 2
   
                                             |
90 | 75, 89 | mpbird 236 |
1
   
                         |