Proof of Theorem fz1isolem
Step | Hyp | Ref
| Expression |
1 | | hashcl 12545 |
. . . . . . . . 9
       |
2 | 1 | adantl 468 |
. . . . . . . 8
 
       |
3 | | nnuz 11201 |
. . . . . . . . . . 11
     |
4 | | 1z 10974 |
. . . . . . . . . . . . 13
 |
5 | | fz1iso.1 |
. . . . . . . . . . . . 13
           |
6 | 4, 5 | om2uzisoi 12175 |
. . . . . . . . . . . 12
        |
7 | | isoeq5 6219 |
. . . . . . . . . . . 12
    
  

          |
8 | 6, 7 | mpbiri 237 |
. . . . . . . . . . 11
    
     |
9 | 3, 8 | ax-mp 5 |
. . . . . . . . . 10
    |
10 | | isocnv 6226 |
. . . . . . . . . 10

   
     |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . 9
  
  |
12 | | nn0p1nn 10916 |
. . . . . . . . 9
    
        |
13 | | fz1iso.2 |
. . . . . . . . . 10
              |
14 | | fz1iso.3 |
. . . . . . . . . . 11
              |
15 | | fvex 5880 |
. . . . . . . . . . . . 13
            |
16 | 15 | epini 5201 |
. . . . . . . . . . . 12
                            |
17 | 16 | ineq2i 3633 |
. . . . . . . . . . 11
                                |
18 | 14, 17 | eqtr4i 2478 |
. . . . . . . . . 10
                   |
19 | 13, 18 | isoini2 6235 |
. . . . . . . . 9
  
                  |
20 | 11, 12, 19 | sylancr 670 |
. . . . . . . 8
    
  
     |
21 | 2, 20 | syl 17 |
. . . . . . 7
 
         |
22 | | nnz 10966 |
. . . . . . . . . . . . 13
   |
23 | 2 | nn0zd 11045 |
. . . . . . . . . . . . 13
 
       |
24 | | eluz 11179 |
. . . . . . . . . . . . 13
               
       |
25 | 22, 23, 24 | syl2anr 481 |
. . . . . . . . . . . 12
  
          
       |
26 | | zleltp1 10994 |
. . . . . . . . . . . . . 14
           
         |
27 | 22, 23, 26 | syl2anr 481 |
. . . . . . . . . . . . 13
  
      
         |
28 | | ovex 6323 |
. . . . . . . . . . . . . 14
       |
29 | | vex 3050 |
. . . . . . . . . . . . . . 15
 |
30 | 29 | eliniseg 5200 |
. . . . . . . . . . . . . 14
                            |
31 | 28, 30 | ax-mp 5 |
. . . . . . . . . . . . 13
           
        |
32 | 27, 31 | syl6bbr 267 |
. . . . . . . . . . . 12
  
                     |
33 | 25, 32 | bitr2d 258 |
. . . . . . . . . . 11
  
             
           |
34 | 33 | pm5.32da 647 |
. . . . . . . . . 10
 
              
             |
35 | 13 | elin2 3623 |
. . . . . . . . . 10

               |
36 | | elfzuzb 11801 |
. . . . . . . . . . 11
        
                |
37 | | elnnuz 11202 |
. . . . . . . . . . . 12

      |
38 | 37 | anbi1i 702 |
. . . . . . . . . . 11
          
                |
39 | 36, 38 | bitr4i 256 |
. . . . . . . . . 10
        
            |
40 | 34, 35, 39 | 3bitr4g 292 |
. . . . . . . . 9
 
             |
41 | 40 | eqrdv 2451 |
. . . . . . . 8
 
           |
42 | | isoeq4 6218 |
. . . . . . . 8
               
  
              |
43 | 41, 42 | syl 17 |
. . . . . . 7
 
       
  
              |
44 | 21, 43 | mpbid 214 |
. . . . . 6
 
                 |
45 | | fz1iso.4 |
. . . . . . . . . . . . . . . . . 18
OrdIso    |
46 | 45 | oion 8056 |
. . . . . . . . . . . . . . . . 17
   |
47 | 46 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
   |
48 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
 
   |
49 | | wofi 7825 |
. . . . . . . . . . . . . . . . . 18
 
   |
50 | 45 | oien 8058 |
. . . . . . . . . . . . . . . . . 18
 
   |
51 | 48, 49, 50 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
 
   |
52 | | enfii 7794 |
. . . . . . . . . . . . . . . . 17
  
  |
53 | 48, 51, 52 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
 
   |
54 | 47, 53 | elind 3620 |
. . . . . . . . . . . . . . 15
 
     |
55 | | onfin2 7769 |
. . . . . . . . . . . . . . 15

  |
56 | 54, 55 | syl6eleqr 2542 |
. . . . . . . . . . . . . 14
 
   |
57 | | eqid 2453 |
. . . . . . . . . . . . . . . 16
              
   
  |
58 | | 0z 10955 |
. . . . . . . . . . . . . . . 16
 |
59 | 5, 57, 4, 58 | uzrdgxfr 12187 |
. . . . . . . . . . . . . . 15
                         |
60 | | 1m0e1 10727 |
. . . . . . . . . . . . . . . 16
   |
61 | 60 | oveq2i 6306 |
. . . . . . . . . . . . . . 15
                                   |
62 | 59, 61 | syl6eq 2503 |
. . . . . . . . . . . . . 14
                       |
63 | 56, 62 | syl 17 |
. . . . . . . . . . . . 13
 
                       |
64 | 51 | ensymd 7625 |
. . . . . . . . . . . . . . . . 17
 
   |
65 | | cardennn 8422 |
. . . . . . . . . . . . . . . . 17
         |
66 | 64, 56, 65 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
 
       |
67 | 66 | fveq2d 5874 |
. . . . . . . . . . . . . . 15
 
      
   
                        |
68 | 57 | hashgval 12525 |
. . . . . . . . . . . . . . . 16
                         |
69 | 68 | adantl 468 |
. . . . . . . . . . . . . . 15
 
      
   
              |
70 | 67, 69 | eqtr3d 2489 |
. . . . . . . . . . . . . 14
 
      
   
          |
71 | 70 | oveq1d 6310 |
. . . . . . . . . . . . 13
 
                         |
72 | 63, 71 | eqtrd 2487 |
. . . . . . . . . . . 12
 
             |
73 | 72 | fveq2d 5874 |
. . . . . . . . . . 11
 
                       |
74 | | isof1o 6221 |
. . . . . . . . . . . . 13

         |
75 | 9, 74 | ax-mp 5 |
. . . . . . . . . . . 12
     |
76 | | f1ocnvfv1 6180 |
. . . . . . . . . . . 12
             
    |
77 | 75, 56, 76 | sylancr 670 |
. . . . . . . . . . 11
 
            |
78 | 73, 77 | eqtr3d 2489 |
. . . . . . . . . 10
 
              |
79 | 78 | ineq2d 3636 |
. . . . . . . . 9
 
                  |
80 | | ordom 6706 |
. . . . . . . . . . 11
 |
81 | | ordelss 5442 |
. . . . . . . . . . 11
  
  |
82 | 80, 56, 81 | sylancr 670 |
. . . . . . . . . 10
 
   |
83 | | sseqin2 3653 |
. . . . . . . . . 10

    |
84 | 82, 83 | sylib 200 |
. . . . . . . . 9
 
     |
85 | 79, 84 | eqtrd 2487 |
. . . . . . . 8
 
                |
86 | 14, 85 | syl5eq 2499 |
. . . . . . 7
 
   |
87 | | isoeq5 6219 |
. . . . . . 7
                                 |
88 | 86, 87 | syl 17 |
. . . . . 6
 
                                 |
89 | 44, 88 | mpbid 214 |
. . . . 5
 
                 |
90 | 45 | oiiso 8057 |
. . . . . 6
 

     |
91 | 48, 49, 90 | syl2anc 667 |
. . . . 5
 

     |
92 | | isotr 6232 |
. . . . 5
                   
    
             |
93 | 89, 91, 92 | syl2anc 667 |
. . . 4
 
   
 
             |
94 | | isof1o 6221 |
. . . 4
   
 
          
                   |
95 | | f1of 5819 |
. . . 4
   
             
                   |
96 | 93, 94, 95 | 3syl 18 |
. . 3
 
   
                |
97 | | fzfid 12193 |
. . 3
 
           |
98 | | fex 6143 |
. . 3
    
                         
    |
99 | 96, 97, 98 | syl2anc 667 |
. 2
 
   
    |
100 | | isoeq1 6215 |
. . 3
   
 
           
    
              |
101 | 100 | spcegv 3137 |
. 2
   
     
 
          

              |
102 | 99, 93, 101 | sylc 62 |
1
 
 
             |