Step | Hyp | Ref
| Expression |
1 | | imassrn 5178 |
. . . . . 6
                 |
2 | | ballotth.m |
. . . . . . . . 9
 |
3 | | ballotth.n |
. . . . . . . . 9
 |
4 | | ballotth.o |
. . . . . . . . 9
     
        |
5 | | ballotth.p |
. . . . . . . . 9
              |
6 | | ballotth.f |
. . . . . . . . 9
          
                |
7 | | ballotth.e |
. . . . . . . . 9
                   |
8 | | ballotth.mgtn |
. . . . . . . . 9
 |
9 | | ballotth.i |
. . . . . . . . 9
   inf     
               |
10 | | ballotth.s |
. . . . . . . . 9
                              |
11 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | ballotlemsf1o 29339 |
. . . . . . . 8
                                    |
12 | 11 | simpld 461 |
. . . . . . 7
                    
    |
13 | | f1of 5812 |
. . . . . . 7
                  
 
                 
    |
14 | | frn 5733 |
. . . . . . 7
                        
        |
15 | 12, 13, 14 | 3syl 18 |
. . . . . 6
               |
16 | 1, 15 | syl5ss 3442 |
. . . . 5
                       |
17 | | fzssuz 11836 |
. . . . . 6
           |
18 | | uzssz 11175 |
. . . . . 6
     |
19 | 17, 18 | sstri 3440 |
. . . . 5
       |
20 | 16, 19 | syl6ss 3443 |
. . . 4
                 |
21 | 20 | adantr 467 |
. . 3
   
                       |
22 | 21 | sselda 3431 |
. 2
                          
  |
23 | | elfzelz 11797 |
. . 3
                   |
24 | 23 | adantl 468 |
. 2
                                 |
25 | | f1ofn 5813 |
. . . . . . 7
                  
 
            |
26 | 12, 25 | syl 17 |
. . . . . 6
          
    |
27 | 26 | adantr 467 |
. . . . 5
   
                     |
28 | 2, 3, 4, 5, 6, 7, 8, 9 | ballotlemiex 29327 |
. . . . . . . . . 10
                             |
29 | 28 | simpld 461 |
. . . . . . . . 9
          
    |
30 | 29 | adantr 467 |
. . . . . . . 8
   
                     |
31 | | elfzuz3 11794 |
. . . . . . . 8
           
           |
32 | 30, 31 | syl 17 |
. . . . . . 7
   
                     |
33 | | elfzuz3 11794 |
. . . . . . . 8
                   |
34 | 33 | adantl 468 |
. . . . . . 7
   
                   |
35 | | uztrn 11172 |
. . . . . . 7
                    
        |
36 | 32, 34, 35 | syl2anc 666 |
. . . . . 6
   
                 |
37 | | fzss2 11835 |
. . . . . 6
      
       
    |
38 | 36, 37 | syl 17 |
. . . . 5
   
                     |
39 | | fvelimab 5919 |
. . . . 5
               
                    
                |
40 | 27, 38, 39 | syl2anc 666 |
. . . 4
   
                      
                |
41 | 40 | adantr 467 |
. . 3
                           
                 |
42 | | 1zzd 10965 |
. . . . . . . . . . 11
   
           |
43 | 2 | nnzi 10958 |
. . . . . . . . . . . . 13
 |
44 | 3 | nnzi 10958 |
. . . . . . . . . . . . 13
 |
45 | | zaddcl 10974 |
. . . . . . . . . . . . 13
 
     |
46 | 43, 44, 45 | mp2an 677 |
. . . . . . . . . . . 12
   |
47 | 46 | a1i 11 |
. . . . . . . . . . 11
   
             |
48 | | elfzelz 11797 |
. . . . . . . . . . . 12
           |
49 | 48 | adantl 468 |
. . . . . . . . . . 11
   
           |
50 | | elfzle1 11799 |
. . . . . . . . . . . 12
           |
51 | 50 | adantl 468 |
. . . . . . . . . . 11
   
           |
52 | 49 | zred 11037 |
. . . . . . . . . . . 12
   
           |
53 | | elfzelz 11797 |
. . . . . . . . . . . . . . 15
                 |
54 | 29, 53 | syl 17 |
. . . . . . . . . . . . . 14
         |
55 | 54 | adantr 467 |
. . . . . . . . . . . . 13
   
               |
56 | 55 | zred 11037 |
. . . . . . . . . . . 12
   
               |
57 | 47 | zred 11037 |
. . . . . . . . . . . 12
   
             |
58 | | elfzle2 11800 |
. . . . . . . . . . . . 13
               |
59 | 58 | adantl 468 |
. . . . . . . . . . . 12
   
               |
60 | | elfzle2 11800 |
. . . . . . . . . . . . . 14
                   |
61 | 29, 60 | syl 17 |
. . . . . . . . . . . . 13
           |
62 | 61 | adantr 467 |
. . . . . . . . . . . 12
   
             
   |
63 | 52, 56, 57, 59, 62 | letrd 9789 |
. . . . . . . . . . 11
   
         
   |
64 | | elfz4 11790 |
. . . . . . . . . . 11
    
 
   
   
    |
65 | 42, 47, 49, 51, 63, 64 | syl32anc 1275 |
. . . . . . . . . 10
   
                 |
66 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | ballotlemsv 29335 |
. . . . . . . . . 10
   
                                  |
67 | 65, 66 | syldan 473 |
. . . . . . . . 9
   
                                    |
68 | | simpr 463 |
. . . . . . . . . 10
   
                   |
69 | | iftrue 3886 |
. . . . . . . . . 10
      
                         |
70 | 68, 58, 69 | 3syl 18 |
. . . . . . . . 9
   
                                    |
71 | 67, 70 | eqtrd 2484 |
. . . . . . . 8
   
                           |
72 | 71 | oveq1d 6303 |
. . . . . . 7
   
                                           |
73 | 72 | eleq2d 2513 |
. . . . . 6
   
                                             |
74 | 73 | adantr 467 |
. . . . 5
                               
                   |
75 | 54 | ad2antrr 731 |
. . . . . . . . 9
                     |
76 | 75 | zcnd 11038 |
. . . . . . . 8
                     |
77 | | 1cnd 9656 |
. . . . . . . 8
                 |
78 | 76, 77 | pncand 9984 |
. . . . . . 7
                             |
79 | 78 | oveq2d 6304 |
. . . . . 6
                                                     |
80 | 79 | eleq2d 2513 |
. . . . 5
                                   
                   |
81 | | 1zzd 10965 |
. . . . . 6
                 |
82 | 48 | ad2antlr 732 |
. . . . . 6
                 |
83 | 75 | peano2zd 11040 |
. . . . . 6
                       |
84 | | simpr 463 |
. . . . . 6
                 |
85 | | fzrev 11855 |
. . . . . 6
                                 
               |
86 | 81, 82, 83, 84, 85 | syl22anc 1268 |
. . . . 5
                                   
               |
87 | 74, 80, 86 | 3bitr2d 285 |
. . . 4
                               
               |
88 | | risset 2914 |
. . . . 5
            
                |
89 | 88 | a1i 11 |
. . . 4
                           
                 |
90 | | eqcom 2457 |
. . . . . . 7
        
          |
91 | 54 | ad2antrr 731 |
. . . . . . . . . . 11
                         |
92 | 91 | adantlr 720 |
. . . . . . . . . 10
     
                     |
93 | 92 | zcnd 11038 |
. . . . . . . . 9
     
                     |
94 | | 1cnd 9656 |
. . . . . . . . 9
     
                 |
95 | 93, 94 | addcld 9659 |
. . . . . . . 8
     
                       |
96 | | simplr 761 |
. . . . . . . . 9
     
                 |
97 | 96 | zcnd 11038 |
. . . . . . . 8
     
                 |
98 | | elfzelz 11797 |
. . . . . . . . . 10
       |
99 | 98 | adantl 468 |
. . . . . . . . 9
     
                 |
100 | 99 | zcnd 11038 |
. . . . . . . 8
     
                 |
101 | | subsub23 9877 |
. . . . . . . 8
       
         
           |
102 | 95, 97, 100, 101 | syl3anc 1267 |
. . . . . . 7
     
                       
           |
103 | 90, 102 | syl5bbr 263 |
. . . . . 6
     
                       
           |
104 | | simpll 759 |
. . . . . . . . . 10
                       |
105 | 38 | sselda 3431 |
. . . . . . . . . 10
                      
    |
106 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | ballotlemsv 29335 |
. . . . . . . . . 10
   
                                  |
107 | 104, 105,
106 | syl2anc 666 |
. . . . . . . . 9
                                              |
108 | 98 | adantl 468 |
. . . . . . . . . . . 12
                     |
109 | 108 | zred 11037 |
. . . . . . . . . . 11
                     |
110 | 48 | ad2antlr 732 |
. . . . . . . . . . . 12
                     |
111 | 110 | zred 11037 |
. . . . . . . . . . 11
                     |
112 | 91 | zred 11037 |
. . . . . . . . . . 11
                         |
113 | | elfzle2 11800 |
. . . . . . . . . . . 12
       |
114 | 113 | adantl 468 |
. . . . . . . . . . 11
                     |
115 | 58 | ad2antlr 732 |
. . . . . . . . . . 11
                         |
116 | 109, 111,
112, 114, 115 | letrd 9789 |
. . . . . . . . . 10
                         |
117 | | iftrue 3886 |
. . . . . . . . . 10
                                |
118 | 116, 117 | syl 17 |
. . . . . . . . 9
                                              |
119 | 107, 118 | eqtrd 2484 |
. . . . . . . 8
                                     |
120 | 119 | eqeq1d 2452 |
. . . . . . 7
                           
           |
121 | 120 | adantlr 720 |
. . . . . 6
     
                       
           |
122 | 103, 121 | bitr4d 260 |
. . . . 5
     
                       
           |
123 | 122 | rexbidva 2897 |
. . . 4
                
            
                 |
124 | 87, 89, 123 | 3bitrd 283 |
. . 3
                               
                 |
125 | 41, 124 | bitr4d 260 |
. 2
                           
                   |
126 | 22, 24, 125 | eqrdav 2449 |
1
   
                                       |