Step | Hyp | Ref
| Expression |
1 | | fveq2 5870 |
. . . . . 6

          |
2 | 1 | oveq1d 6310 |
. . . . 5

              |
3 | | pweq 3956 |
. . . . . . 7

    |
4 | | rabeq 3040 |
. . . . . . 7
          
        |
5 | 3, 4 | syl 17 |
. . . . . 6

       
        |
6 | 5 | fveq2d 5874 |
. . . . 5

    
                   |
7 | 2, 6 | eqeq12d 2468 |
. . . 4

                                      |
8 | 7 | ralbidv 2829 |
. . 3

 
                            
         |
9 | | fveq2 5870 |
. . . . . 6
           |
10 | 9 | oveq1d 6310 |
. . . . 5
               |
11 | | pweq 3956 |
. . . . . . 7
 
   |
12 | | rabeq 3040 |
. . . . . . 7
    
              |
13 | 11, 12 | syl 17 |
. . . . . 6
        

       |
14 | 13 | fveq2d 5874 |
. . . . 5
                         |
15 | 10, 14 | eqeq12d 2468 |
. . . 4
                             
         |
16 | 15 | ralbidv 2829 |
. . 3
  
                                      |
17 | | fveq2 5870 |
. . . . . 6
                   |
18 | 17 | oveq1d 6310 |
. . . . 5
                       |
19 | | pweq 3956 |
. . . . . . 7
             |
20 | | rabeq 3040 |
. . . . . . 7
              
            |
21 | 19, 20 | syl 17 |
. . . . . 6
            
            |
22 | 21 | fveq2d 5874 |
. . . . 5
                                 |
23 | 18, 22 | eqeq12d 2468 |
. . . 4
                                                   |
24 | 23 | ralbidv 2829 |
. . 3
                 
                                   |
25 | | fveq2 5870 |
. . . . . 6
           |
26 | 25 | oveq1d 6310 |
. . . . 5
               |
27 | | pweq 3956 |
. . . . . . 7
 
   |
28 | | rabeq 3040 |
. . . . . . 7
    
              |
29 | 27, 28 | syl 17 |
. . . . . 6
        

       |
30 | 29 | fveq2d 5874 |
. . . . 5
                         |
31 | 26, 30 | eqeq12d 2468 |
. . . 4
                             
         |
32 | 31 | ralbidv 2829 |
. . 3
  
                                      |
33 | | hash0 12555 |
. . . . . . . . . 10
     |
34 | 33 | a1i 11 |
. . . . . . . . 9
           |
35 | | elfz1eq 11817 |
. . . . . . . . 9
       |
36 | 34, 35 | oveq12d 6313 |
. . . . . . . 8
               |
37 | | 0nn0 10891 |
. . . . . . . . 9
 |
38 | | bcn0 12502 |
. . . . . . . . 9

    |
39 | 37, 38 | ax-mp 5 |
. . . . . . . 8
   |
40 | 36, 39 | syl6eq 2503 |
. . . . . . 7
             |
41 | | pw0 4122 |
. . . . . . . . . 10
    |
42 | 35 | eqcomd 2459 |
. . . . . . . . . . . 12
       |
43 | 41 | raleqi 2993 |
. . . . . . . . . . . . 13
 
     
        |
44 | | 0ex 4538 |
. . . . . . . . . . . . . 14
 |
45 | | fveq2 5870 |
. . . . . . . . . . . . . . . 16

          |
46 | 45, 33 | syl6eq 2503 |
. . . . . . . . . . . . . . 15

      |
47 | 46 | eqeq1d 2455 |
. . . . . . . . . . . . . 14

    
   |
48 | 44, 47 | ralsn 4012 |
. . . . . . . . . . . . 13
 
        |
49 | 43, 48 | bitri 253 |
. . . . . . . . . . . 12
 
       |
50 | 42, 49 | sylibr 216 |
. . . . . . . . . . 11
             |
51 | | rabid2 2970 |
. . . . . . . . . . 11
                 |
52 | 50, 51 | sylibr 216 |
. . . . . . . . . 10
               |
53 | 41, 52 | syl5reqr 2502 |
. . . . . . . . 9
      
         |
54 | 53 | fveq2d 5874 |
. . . . . . . 8
                        |
55 | | hashsng 12556 |
. . . . . . . . 9

        |
56 | 44, 55 | ax-mp 5 |
. . . . . . . 8
       |
57 | 54, 56 | syl6eq 2503 |
. . . . . . 7
                  |
58 | 40, 57 | eqtr4d 2490 |
. . . . . 6
               
        |
59 | 58 | adantl 468 |
. . . . 5
 
                        |
60 | 33 | oveq1i 6305 |
. . . . . 6
         |
61 | | bcval3 12498 |
. . . . . . . 8
 
         |
62 | 37, 61 | mp3an1 1353 |
. . . . . . 7
 
         |
63 | | id 22 |
. . . . . . . . . . . . . 14
   |
64 | | 0z 10955 |
. . . . . . . . . . . . . . 15
 |
65 | | elfz3 11816 |
. . . . . . . . . . . . . . 15
       |
66 | 64, 65 | ax-mp 5 |
. . . . . . . . . . . . . 14
     |
67 | 63, 66 | syl6eqelr 2540 |
. . . . . . . . . . . . 13
       |
68 | 67 | con3i 141 |
. . . . . . . . . . . 12
    
  |
69 | 68 | adantl 468 |
. . . . . . . . . . 11
 
    
  |
70 | 41 | raleqi 2993 |
. . . . . . . . . . . 12
 
             |
71 | 47 | notbid 296 |
. . . . . . . . . . . . 13

    
   |
72 | 44, 71 | ralsn 4012 |
. . . . . . . . . . . 12
 
     
  |
73 | 70, 72 | bitri 253 |
. . . . . . . . . . 11
 
   
  |
74 | 69, 73 | sylibr 216 |
. . . . . . . . . 10
 
            |
75 | | rabeq0 3756 |
. . . . . . . . . 10
               |
76 | 74, 75 | sylibr 216 |
. . . . . . . . 9
 
              |
77 | 76 | fveq2d 5874 |
. . . . . . . 8
 
                      |
78 | 77, 33 | syl6eq 2503 |
. . . . . . 7
 
                  |
79 | 62, 78 | eqtr4d 2490 |
. . . . . 6
 
           
        |
80 | 60, 79 | syl5eq 2499 |
. . . . 5
 
                        |
81 | 59, 80 | pm2.61dan 801 |
. . . 4
           
        |
82 | 81 | rgen 2749 |
. . 3
                   |
83 | | oveq2 6303 |
. . . . . 6
               |
84 | | eqeq2 2464 |
. . . . . . . . 9
     
       |
85 | 84 | rabbidv 3038 |
. . . . . . . 8
        

       |
86 | | fveq2 5870 |
. . . . . . . . . 10
           |
87 | 86 | eqeq1d 2455 |
. . . . . . . . 9
     
       |
88 | 87 | cbvrabv 3046 |
. . . . . . . 8
        
      |
89 | 85, 88 | syl6eq 2503 |
. . . . . . 7
         
       |
90 | 89 | fveq2d 5874 |
. . . . . 6
                         |
91 | 83, 90 | eqeq12d 2468 |
. . . . 5
                             
         |
92 | 91 | cbvralv 3021 |
. . . 4
 
                                     |
93 | | simpll 761 |
. . . . . . 7
     
                     |
94 | | simplr 763 |
. . . . . . 7
     
                  
  |
95 | | simprr 767 |
. . . . . . . 8
     
                   
                   |
96 | 88 | fveq2i 5873 |
. . . . . . . . . 10
    
          
       |
97 | 96 | eqeq2i 2465 |
. . . . . . . . 9
                            
        |
98 | 97 | ralbii 2821 |
. . . . . . . 8
 
                                     |
99 | 95, 98 | sylibr 216 |
. . . . . . 7
     
                   
                   |
100 | | simprl 765 |
. . . . . . 7
     
                     |
101 | 93, 94, 99, 100 | hashbclem 12622 |
. . . . . 6
     
                                              |
102 | 101 | expr 620 |
. . . . 5
      
                
                            |
103 | 102 | ralrimdva 2808 |
. . . 4
 

 
                
                             |
104 | 92, 103 | syl5bi 221 |
. . 3
 

 
                
                             |
105 | 8, 16, 24, 32, 82, 104 | findcard2s 7817 |
. 2
            
        |
106 | | oveq2 6303 |
. . . 4
               |
107 | | eqeq2 2464 |
. . . . . 6
     
       |
108 | 107 | rabbidv 3038 |
. . . . 5
        

       |
109 | 108 | fveq2d 5874 |
. . . 4
                         |
110 | 106, 109 | eqeq12d 2468 |
. . 3
                             
         |
111 | 110 | rspccva 3151 |
. 2
                                        |
112 | 105, 111 | sylan 474 |
1
 
                    |