Step | Hyp | Ref
| Expression |
1 | | elfznelfzo 12045 |
. . . . . . 7
     
 ..^      |
2 | | fvinim0ffz 12055 |
. . . . . . . . . . . . 13
                        ..^       
    ..^          ..^      |
3 | | df-nel 2644 |
. . . . . . . . . . . . . . . . . 18
         ..^ 
        ..^    |
4 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
5 | 4 | eqcoms 2479 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
6 | 5 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . 21
          ..^ 
        ..^     |
7 | 6 | notbid 301 |
. . . . . . . . . . . . . . . . . . . 20
          ..^ 
        ..^     |
8 | 7 | biimpd 212 |
. . . . . . . . . . . . . . . . . . 19
          ..^          ..^     |
9 | | ffn 5739 |
. . . . . . . . . . . . . . . . . . . . . . 23
        
      |
10 | | 1eluzge0 11226 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
11 | | fzoss1 11972 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
 ..^  ..^   |
12 | 10, 11 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . 24

 ..^  ..^   |
13 | | fzossfz 11965 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 ..^      |
14 | 12, 13 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . . . . . . 23

 ..^       |
15 | | fvelimab 5936 |
. . . . . . . . . . . . . . . . . . . . . . 23
       ..^               ..^ 
  ..^             |
16 | 9, 14, 15 | syl2an 485 |
. . . . . . . . . . . . . . . . . . . . . 22
                    ..^  
 ..^             |
17 | 16 | notbid 301 |
. . . . . . . . . . . . . . . . . . . . 21
                    ..^    ..^             |
18 | | ralnex 2834 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 ..^        
  ..^            |
19 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
           |
20 | 19 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         
           |
21 | 20 | notbid 301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
           |
22 | 21 | rspcva 3134 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   ..^ 
 ..^                    |
23 | | pm2.21 111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                     |
24 | 23 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                               |
25 | 24 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                       
                         |
26 | 22, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   ..^ 
 ..^                        
                         |
27 | 26 | expcom 442 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 ..^           ..^                                          |
28 | 27 | com24 89 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
 ..^                           ..^                          |
29 | 18, 28 | sylbir 218 |
. . . . . . . . . . . . . . . . . . . . . 22
   ..^                            ..^                          |
30 | 29 | com12 31 |
. . . . . . . . . . . . . . . . . . . . 21
            
 ..^         
    
  ..^         
                |
31 | 17, 30 | sylbid 223 |
. . . . . . . . . . . . . . . . . . . 20
                    ..^      
  ..^         
                |
32 | 31 | com12 31 |
. . . . . . . . . . . . . . . . . . 19
         ..^                    ..^                          |
33 | 8, 32 | syl6com 35 |
. . . . . . . . . . . . . . . . . 18
         ..^                     ..^                           |
34 | 3, 33 | sylbi 200 |
. . . . . . . . . . . . . . . . 17
         ..^ 
                   ..^                           |
35 | 34 | adantr 472 |
. . . . . . . . . . . . . . . 16
     
    ..^          ..^   
         
        ..^         
                 |
36 | 35 | com12 31 |
. . . . . . . . . . . . . . 15
           ..^          ..^  
         
        ..^         
                 |
37 | | df-nel 2644 |
. . . . . . . . . . . . . . . . . 18
         ..^ 
        ..^    |
38 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
39 | 38 | eqcoms 2479 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
40 | 39 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . 21
          ..^ 
        ..^     |
41 | 40 | notbid 301 |
. . . . . . . . . . . . . . . . . . . 20
          ..^ 
        ..^     |
42 | 41 | biimpd 212 |
. . . . . . . . . . . . . . . . . . 19
          ..^          ..^     |
43 | 42, 32 | syl6com 35 |
. . . . . . . . . . . . . . . . . 18
         ..^                     ..^                           |
44 | 37, 43 | sylbi 200 |
. . . . . . . . . . . . . . . . 17
         ..^ 

               
  ..^         
                 |
45 | 44 | adantl 473 |
. . . . . . . . . . . . . . . 16
     
    ..^          ..^   
         
        ..^         
                 |
46 | 45 | com12 31 |
. . . . . . . . . . . . . . 15
           ..^          ..^  
         
        ..^         
                 |
47 | 36, 46 | jaoi 386 |
. . . . . . . . . . . . . 14
             ..^          ..^            
        ..^         
                 |
48 | 47 | com13 82 |
. . . . . . . . . . . . 13
                     ..^          ..^             ..^                           |
49 | 2, 48 | sylbid 223 |
. . . . . . . . . . . 12
                        ..^             ..^                           |
50 | 49 | com14 90 |
. . . . . . . . . . 11
                  ..^                   ..^                           |
51 | 50 | com12 31 |
. . . . . . . . . 10
        
    ..^                        ..^                           |
52 | 51 | com15 95 |
. . . . . . . . 9
  ..^
    
            
              ..^                             |
53 | | elfznelfzo 12045 |
. . . . . . . . . . 11
     
 ..^      |
54 | | eqtr3 2492 |
. . . . . . . . . . . . . 14
     |
55 | | 2a1 27 |
. . . . . . . . . . . . . . 15
                       |
56 | 55 | 2a1d 26 |
. . . . . . . . . . . . . 14
                         ..^           
               |
57 | 54, 56 | syl 17 |
. . . . . . . . . . . . 13
            
              ..^                           |
58 | 5 | adantl 473 |
. . . . . . . . . . . . . . . 16
 
           |
59 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . 18
           |
60 | 59 | eqcoms 2479 |
. . . . . . . . . . . . . . . . 17
           |
61 | 60 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
           |
62 | 58, 61 | neeq12d 2704 |
. . . . . . . . . . . . . . 15
 
                     |
63 | | df-ne 2643 |
. . . . . . . . . . . . . . . 16
        
          |
64 | | pm2.24 112 |
. . . . . . . . . . . . . . . . . 18
                 
   |
65 | 64 | eqcoms 2479 |
. . . . . . . . . . . . . . . . 17
                 
   |
66 | 65 | com12 31 |
. . . . . . . . . . . . . . . 16
                     |
67 | 63, 66 | sylbi 200 |
. . . . . . . . . . . . . . 15
                 
   |
68 | 62, 67 | syl6bi 236 |
. . . . . . . . . . . . . 14
 
         
             |
69 | 68 | 2a1d 26 |
. . . . . . . . . . . . 13
 
          
              ..^                           |
70 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . 18
           |
71 | 70 | eqcoms 2479 |
. . . . . . . . . . . . . . . . 17
           |
72 | 71 | adantr 472 |
. . . . . . . . . . . . . . . 16
             |
73 | 39 | adantl 473 |
. . . . . . . . . . . . . . . 16
             |
74 | 72, 73 | neeq12d 2704 |
. . . . . . . . . . . . . . 15
                       |
75 | | df-ne 2643 |
. . . . . . . . . . . . . . . 16
        
          |
76 | 75, 23 | sylbi 200 |
. . . . . . . . . . . . . . 15
                 
   |
77 | 74, 76 | syl6bi 236 |
. . . . . . . . . . . . . 14
           
             |
78 | 77 | 2a1d 26 |
. . . . . . . . . . . . 13
            
              ..^                           |
79 | | eqtr3 2492 |
. . . . . . . . . . . . . 14
 
   |
80 | 79, 56 | syl 17 |
. . . . . . . . . . . . 13
 
                         ..^           
               |
81 | 57, 69, 78, 80 | ccase 961 |
. . . . . . . . . . . 12
                               ..^           
               |
82 | 81 | ex 441 |
. . . . . . . . . . 11
                              ..^           
                |
83 | 53, 82 | syl 17 |
. . . . . . . . . 10
     
 ..^                             ..^           
                |
84 | 83 | expcom 442 |
. . . . . . . . 9
  ..^                                 ..^           
                 |
85 | 52, 84 | pm2.61i 169 |
. . . . . . . 8
       
         
              ..^                            |
86 | 85 | com12 31 |
. . . . . . 7
       
         
              ..^                            |
87 | 1, 86 | syl 17 |
. . . . . 6
     
 ..^      
         
              ..^                            |
88 | 87 | ex 441 |
. . . . 5
     
 ..^               
              ..^                             |
89 | 88 | com23 80 |
. . . 4
            ..^          
              ..^                             |
90 | 89 | impcom 437 |
. . 3
     
       ..^          
              ..^                            |
91 | 90 | com12 31 |
. 2
  ..^           
         
              ..^                            |
92 | 91 | com25 93 |
1
  ..^                                  ..^                      
       |