Step | Hyp | Ref
| Expression |
1 | | fveq2 5892 |
. . . . . . . 8

          |
2 | 1 | neeq1d 2695 |
. . . . . . 7

        
           |
3 | 2 | raleqbi1dv 3007 |
. . . . . 6

 
                    |
4 | 3 | imbi2d 322 |
. . . . 5

            
             |
5 | | fveq2 5892 |
. . . . . . . 8
           |
6 | 5 | neeq1d 2695 |
. . . . . . 7
         
           |
7 | 6 | raleqbi1dv 3007 |
. . . . . 6
  
       

           |
8 | 7 | imbi2d 322 |
. . . . 5
  

                       |
9 | | fveq2 5892 |
. . . . . . . 8
       
   |
10 | 9 | neeq1d 2695 |
. . . . . . 7
                     |
11 | 10 | raleqbi1dv 3007 |
. . . . . 6
                        |
12 | 11 | imbi2d 322 |
. . . . 5
            
               |
13 | | fveq2 5892 |
. . . . . . . 8
           |
14 | 13 | neeq1d 2695 |
. . . . . . 7
         
           |
15 | 14 | raleqbi1dv 3007 |
. . . . . 6
  
       

           |
16 | 15 | imbi2d 322 |
. . . . 5
  

                       |
17 | | ral0 3886 |
. . . . . 6
          |
18 | 17 | a1i 11 |
. . . . 5
            |
19 | | infpssrlem.c |
. . . . . . . . . . . . . . . . . 18
       |
20 | | f1ocnv 5853 |
. . . . . . . . . . . . . . . . . 18
    
       |
21 | | f1of 5841 |
. . . . . . . . . . . . . . . . . 18
             |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
        |
23 | 22 | adantl 472 |
. . . . . . . . . . . . . . . 16
  
       |
24 | | infpssrlem.a |
. . . . . . . . . . . . . . . . . . 19

  |
25 | | infpssrlem.d |
. . . . . . . . . . . . . . . . . . 19
     |
26 | | infpssrlem.e |
. . . . . . . . . . . . . . . . . . 19
        |
27 | 24, 19, 25, 26 | infpssrlem3 8766 |
. . . . . . . . . . . . . . . . . 18
       |
28 | 27 | ffvelrnda 6050 |
. . . . . . . . . . . . . . . . 17
 

      |
29 | 28 | ancoms 459 |
. . . . . . . . . . . . . . . 16
  
      |
30 | 23, 29 | ffvelrnd 6051 |
. . . . . . . . . . . . . . 15
  
           |
31 | 25 | eldifbd 3429 |
. . . . . . . . . . . . . . . 16
   |
32 | 31 | adantl 472 |
. . . . . . . . . . . . . . 15
  
  |
33 | | nelne2 2733 |
. . . . . . . . . . . . . . 15
          

           |
34 | 30, 32, 33 | syl2anc 671 |
. . . . . . . . . . . . . 14
  
           |
35 | 24, 19, 25, 26 | infpssrlem2 8765 |
. . . . . . . . . . . . . . 15
                |
36 | 35 | adantr 471 |
. . . . . . . . . . . . . 14
  
               |
37 | 24, 19, 25, 26 | infpssrlem1 8764 |
. . . . . . . . . . . . . . 15
       |
38 | 37 | adantl 472 |
. . . . . . . . . . . . . 14
  
      |
39 | 34, 36, 38 | 3netr4d 2713 |
. . . . . . . . . . . . 13
  
          |
40 | 39 | 3adant3 1034 |
. . . . . . . . . . . 12
                      |
41 | 1 | neeq2d 2696 |
. . . . . . . . . . . 12

        
           |
42 | 40, 41 | syl5ibr 229 |
. . . . . . . . . . 11

                       |
43 | 42 | adantrd 474 |
. . . . . . . . . 10

  

        
            |
44 | | simpr 467 |
. . . . . . . . . . . . . . . 16
 
   |
45 | | peano2 6745 |
. . . . . . . . . . . . . . . . 17

  |
46 | 45 | adantr 471 |
. . . . . . . . . . . . . . . 16
 

  |
47 | | elnn 6734 |
. . . . . . . . . . . . . . . 16
     |
48 | 44, 46, 47 | syl2anc 671 |
. . . . . . . . . . . . . . 15
 
   |
49 | 48 | 3ad2antl1 1176 |
. . . . . . . . . . . . . 14
  

        
   |
50 | 49 | adantl 472 |
. . . . . . . . . . . . 13
   

        
    |
51 | | simpl 463 |
. . . . . . . . . . . . 13
   

        
    |
52 | | nnsuc 6741 |
. . . . . . . . . . . . 13
      |
53 | 50, 51, 52 | syl2anc 671 |
. . . . . . . . . . . 12
   

        
  
  |
54 | | nfv 1772 |
. . . . . . . . . . . . . . . 16
  |
55 | | nfv 1772 |
. . . . . . . . . . . . . . . 16
   |
56 | | nfra1 2781 |
. . . . . . . . . . . . . . . 16
            |
57 | 54, 55, 56 | nf3an 2024 |
. . . . . . . . . . . . . . 15
  

          |
58 | | nfv 1772 |
. . . . . . . . . . . . . . 15
  |
59 | 57, 58 | nfan 2022 |
. . . . . . . . . . . . . 14
   

           |
60 | | nfv 1772 |
. . . . . . . . . . . . . 14
           |
61 | | simpl3 1019 |
. . . . . . . . . . . . . . . . . . 19
  

        

 

          |
62 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
 

  |
63 | | nnord 6732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
64 | 63 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
65 | | ordsucelsuc 6681 |
. . . . . . . . . . . . . . . . . . . . . . 23


   |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
   |
67 | 62, 66 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
68 | 67 | 3ad2antl1 1176 |
. . . . . . . . . . . . . . . . . . . 20
  

        
   |
69 | 68 | adantrr 728 |
. . . . . . . . . . . . . . . . . . 19
  

        

 
  |
70 | | rsp 2766 |
. . . . . . . . . . . . . . . . . . 19
 
       

           |
71 | 61, 69, 70 | sylc 62 |
. . . . . . . . . . . . . . . . . 18
  

        

 
          |
72 | | f1of1 5840 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
73 | 19, 20, 72 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        |
74 | 73 | ad2antlr 738 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            |
75 | 29 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
76 | 27 | ffvelrnda 6050 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

      |
77 | 76 | adantll 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
78 | | f1fveq 6193 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 
                  
           |
79 | 74, 75, 77, 78 | syl12anc 1274 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                   |
80 | 79 | necon3bid 2680 |
. . . . . . . . . . . . . . . . . . . . . 22
                                   |
81 | 80 | biimprd 231 |
. . . . . . . . . . . . . . . . . . . . 21
                                   |
82 | 35 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                |
83 | 24, 19, 25, 26 | infpssrlem2 8765 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                |
84 | 83 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                |
85 | 82, 84 | neeq12d 2697 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                               |
86 | 85 | adantlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
                                   |
87 | 81, 86 | sylibrd 242 |
. . . . . . . . . . . . . . . . . . . 20
                         |
88 | 87 | adantrl 727 |
. . . . . . . . . . . . . . . . . . 19
    
                      |
89 | 88 | 3adantl3 1172 |
. . . . . . . . . . . . . . . . . 18
  

        

 
        
           |
90 | 71, 89 | mpd 15 |
. . . . . . . . . . . . . . . . 17
  

        

 
          |
91 | 90 | expr 624 |
. . . . . . . . . . . . . . . 16
  

        
             |
92 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . 18
     |
93 | 92 | anbi2d 715 |
. . . . . . . . . . . . . . . . 17
              
                |
94 | | fveq2 5892 |
. . . . . . . . . . . . . . . . . . 19
       
   |
95 | 94 | neeq2d 2696 |
. . . . . . . . . . . . . . . . . 18
                
    |
96 | 95 | imbi2d 322 |
. . . . . . . . . . . . . . . . 17
                         |
97 | 93, 96 | imbi12d 326 |
. . . . . . . . . . . . . . . 16
                                                       |
98 | 91, 97 | mpbiri 241 |
. . . . . . . . . . . . . . 15
                            |
99 | 98 | com3l 84 |
. . . . . . . . . . . . . 14
  

        
               |
100 | 59, 60, 99 | rexlimd 2883 |
. . . . . . . . . . . . 13
  

        
  
           |
101 | 100 | adantl 472 |
. . . . . . . . . . . 12
   

        
               |
102 | 53, 101 | mpd 15 |
. . . . . . . . . . 11
   

        
            |
103 | 102 | ex 440 |
. . . . . . . . . 10

  

        
            |
104 | 43, 103 | pm2.61ine 2719 |
. . . . . . . . 9
  

        
           |
105 | 104 | ralrimiva 2814 |
. . . . . . . 8
                        |
106 | | fveq2 5892 |
. . . . . . . . . 10
           |
107 | 106 | neeq2d 2696 |
. . . . . . . . 9
                     |
108 | 107 | cbvralv 3031 |
. . . . . . . 8
 
        
    
       |
109 | 105, 108 | sylib 201 |
. . . . . . 7
                        |
110 | 109 | 3exp 1214 |
. . . . . 6
   
                      |
111 | 110 | a2d 29 |
. . . . 5
  

        
               |
112 | 4, 8, 12, 16, 18, 111 | finds 6751 |
. . . 4
              |
113 | 112 | impcom 436 |
. . 3
 


          |
114 | | fveq2 5892 |
. . . . 5
           |
115 | 114 | neeq2d 2696 |
. . . 4
         
           |
116 | 115 | rspccv 3159 |
. . 3
 
       

           |
117 | 113, 116 | syl 17 |
. 2
 


           |
118 | 117 | 3impia 1212 |
1
 

          |