Step | Hyp | Ref
| Expression |
1 | | fzfi 12223 |
. . . . . . . 8
           |
2 | | xpfi 7860 |
. . . . . . . 8
                                               |
3 | 1, 1, 2 | mp2an 686 |
. . . . . . 7
                       |
4 | | isfinite 8175 |
. . . . . . 7
                                               |
5 | 3, 4 | mpbi 213 |
. . . . . 6
                       |
6 | | nnenom 12231 |
. . . . . . 7
 |
7 | 6 | ensymi 7637 |
. . . . . 6
 |
8 | | sdomentr 7724 |
. . . . . 6
                                                 |
9 | 5, 7, 8 | mp2an 686 |
. . . . 5
                       |
10 | | ensym 7636 |
. . . . . 6
                     
                       |
11 | 10 | ad2antll 743 |
. . . . 5
              
 
      
         
                       |
12 | | sdomentr 7724 |
. . . . 5
                                             
                         
 
      
          |
13 | 9, 11, 12 | sylancr 676 |
. . . 4
              
 
      
         
                         
 
      
          |
14 | | opabssxp 4914 |
. . . . . . . 8
            
           |
15 | 14 | sseli 3414 |
. . . . . . 7
             
            |
16 | | simprrl 782 |
. . . . . . . . . . . 12
         


                     |
17 | 16 | nnzd 11062 |
. . . . . . . . . . 11
         


                     |
18 | | simpllr 777 |
. . . . . . . . . . . 12
         


                 |
19 | | simplr 770 |
. . . . . . . . . . . 12
         


                 |
20 | | nnabscl 13465 |
. . . . . . . . . . . 12
         |
21 | 18, 19, 20 | syl2anc 673 |
. . . . . . . . . . 11
         


                     |
22 | | zmodfz 12151 |
. . . . . . . . . . 11
               
                 |
23 | 17, 21, 22 | syl2anc 673 |
. . . . . . . . . 10
         


                   
                 |
24 | | simprrr 783 |
. . . . . . . . . . . 12
         


                     |
25 | 24 | nnzd 11062 |
. . . . . . . . . . 11
         


                     |
26 | | zmodfz 12151 |
. . . . . . . . . . 11
               
                 |
27 | 25, 21, 26 | syl2anc 673 |
. . . . . . . . . 10
         


                   
                 |
28 | 23, 27 | jca 541 |
. . . . . . . . 9
         


                    
                                      |
29 | 28 | ex 441 |
. . . . . . . 8
                                                                       |
30 | | elxp7 6845 |
. . . . . . . 8
  
                |
31 | | opelxp 4869 |
. . . . . . . 8
      
          
                           
     
                                      |
32 | 29, 30, 31 | 3imtr4g 278 |
. . . . . . 7
                   
          
                               |
33 | 15, 32 | syl5 32 |
. . . . . 6
                        
             
          
                               |
34 | 33 | imp 436 |
. . . . 5
         


                     
                
                              |
35 | 34 | adantlrr 735 |
. . . 4
         
     
 
      
             
 
      
              
          
                              |
36 | | fveq2 5879 |
. . . . . 6
           |
37 | 36 | oveq1d 6323 |
. . . . 5
     
         
       |
38 | | fveq2 5879 |
. . . . . 6
           |
39 | 38 | oveq1d 6323 |
. . . . 5
     
         
       |
40 | 37, 39 | opeq12d 4166 |
. . . 4
      
          
                               |
41 | 13, 35, 40 | fphpd 35730 |
. . 3
              
 
      
         
    
 
      
             
 
      
              
          
                                |
42 | | eleq1 2537 |
. . . . . . . . . . . 12
 
   |
43 | | eleq1 2537 |
. . . . . . . . . . . 12
 
   |
44 | 42, 43 | bi2anan9 890 |
. . . . . . . . . . 11
 
   
     |
45 | | oveq1 6315 |
. . . . . . . . . . . . 13
           |
46 | | oveq1 6315 |
. . . . . . . . . . . . . 14
           |
47 | 46 | oveq2d 6324 |
. . . . . . . . . . . . 13
 
             |
48 | 45, 47 | oveqan12d 6327 |
. . . . . . . . . . . 12
 
      
                    |
49 | 48 | eqeq1d 2473 |
. . . . . . . . . . 11
 
       
           
         |
50 | 44, 49 | anbi12d 725 |
. . . . . . . . . 10
 
                 
 
      
          |
51 | 50 | cbvopabv 4465 |
. . . . . . . . 9
            
                              |
52 | 51 | eleq2i 2541 |
. . . . . . . 8
             
       
                       |
53 | 52 | biimpi 199 |
. . . . . . 7
             
           
 
      
          |
54 | | elopab 4709 |
. . . . . . . . 9
             
       
                           |
55 | | elopab 4709 |
. . . . . . . . . . . 12
             
       
                           |
56 | | simp3ll 1101 |
. . . . . . . . . . . . . . . . 17
         


                      |
57 | 56 | 3expb 1232 |
. . . . . . . . . . . . . . . 16
         


                     
  |
58 | 57 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . 15
            
                                                 
          
                                 |
59 | | simp3lr 1102 |
. . . . . . . . . . . . . . . . 17
         


                      |
60 | 59 | 3expb 1232 |
. . . . . . . . . . . . . . . 16
         


                     
  |
61 | 60 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . 15
            
                                                 
          
                                 |
62 | | simp1lr 1094 |
. . . . . . . . . . . . . . . 16
         


                           
          
                                 |
63 | 62 | 3adant1r 1285 |
. . . . . . . . . . . . . . 15
            
                                                 
          
                                 |
64 | | simp-4l 784 |
. . . . . . . . . . . . . . . 16
         


                     
  |
65 | 64 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . 15
            
                                                 
          
                                 |
66 | | simp-4r 785 |
. . . . . . . . . . . . . . . 16
         


                     
      |
67 | 66 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . 15
            
                                                 
          
                                     |
68 | | simp2ll 1097 |
. . . . . . . . . . . . . . . 16
            
                       
      
             
          
                                 |
69 | 68 | 3adant2l 1286 |
. . . . . . . . . . . . . . 15
            
                                                 
          
                                 |
70 | | simp2lr 1098 |
. . . . . . . . . . . . . . . 16
            
                       
      
             
          
                                 |
71 | 70 | 3adant2l 1286 |
. . . . . . . . . . . . . . 15
            
                                                 
          
                                 |
72 | | simp2l 1056 |
. . . . . . . . . . . . . . . 16
            
                                                 
          
                                    |
73 | | simp1rl 1095 |
. . . . . . . . . . . . . . . 16
            
                                                 
          
                                    |
74 | | simp3l 1058 |
. . . . . . . . . . . . . . . 16
            
                                                 
          
                                 |
75 | | simp3 1032 |
. . . . . . . . . . . . . . . . . 18
        
  |
76 | | simp2 1031 |
. . . . . . . . . . . . . . . . . 18
        
     |
77 | | simp1 1030 |
. . . . . . . . . . . . . . . . . 18
        
     |
78 | 75, 76, 77 | 3netr3d 2719 |
. . . . . . . . . . . . . . . . 17
        
  
     |
79 | | vex 3034 |
. . . . . . . . . . . . . . . . . . 19
 |
80 | | vex 3034 |
. . . . . . . . . . . . . . . . . . 19
 |
81 | 79, 80 | opth 4676 |
. . . . . . . . . . . . . . . . . 18
           |
82 | 81 | necon3abii 2689 |
. . . . . . . . . . . . . . . . 17
           |
83 | 78, 82 | sylib 201 |
. . . . . . . . . . . . . . . 16
        

   |
84 | 72, 73, 74, 83 | syl3anc 1292 |
. . . . . . . . . . . . . . 15
            
                                                 
          
                                   |
85 | | simp1lr 1094 |
. . . . . . . . . . . . . . 15
            
                                                 
          
                                 |
86 | | simp1rr 1096 |
. . . . . . . . . . . . . . . 16
              
                    
              
          
                                             |
87 | 86 | 3adant1l 1284 |
. . . . . . . . . . . . . . 15
            
                                                 
          
                                             |
88 | | simp2rr 1100 |
. . . . . . . . . . . . . . 15
            
                                                 
          
                                             |
89 | | simp3r 1059 |
. . . . . . . . . . . . . . . . 17
            
                                                 
          
                                    
          
                               |
90 | | simp3 1032 |
. . . . . . . . . . . . . . . . . . 19
                              
                
      
                
                               |
91 | | ovex 6336 |
. . . . . . . . . . . . . . . . . . . 20
           |
92 | | ovex 6336 |
. . . . . . . . . . . . . . . . . . . 20
           |
93 | 91, 92 | opth 4676 |
. . . . . . . . . . . . . . . . . . 19
      
          
                                                                         |
94 | 90, 93 | sylib 201 |
. . . . . . . . . . . . . . . . . 18
                              
                
      
     
         
         
         
        |
95 | | simprl 772 |
. . . . . . . . . . . . . . . . . . . . . 22
         
     
         
         
         
      
              
       |
96 | | simpll 768 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
     
         
         
         
      
     |
97 | 96 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
     
         
         
         
      
             |
98 | 79, 80 | op1st 6820 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
 |
99 | 97, 98 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
     
         
         
         
      
      |
100 | 99 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . 22
         
     
         
         
         
      
                  |
101 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         
     
         
         
         
      
     |
102 | 101 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
     
         
         
         
      
             |
103 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
104 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
105 | 103, 104 | op1st 6820 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
 |
106 | 102, 105 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
     
         
         
         
      
      |
107 | 106 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . 22
         
     
         
         
         
      
                  |
108 | 95, 100, 107 | 3eqtr3d 2513 |
. . . . . . . . . . . . . . . . . . . . 21
         
     
         
         
         
      
              |
109 | | simprr 774 |
. . . . . . . . . . . . . . . . . . . . . 22
         
     
         
         
         
      
              
       |
110 | 96 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
     
         
         
         
      
             |
111 | 79, 80 | op2nd 6821 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
 |
112 | 110, 111 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
     
         
         
         
      
      |
113 | 112 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . 22
         
     
         
         
         
      
                  |
114 | 101 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
     
         
         
         
      
             |
115 | 103, 104 | op2nd 6821 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
 |
116 | 114, 115 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
     
         
         
         
      
      |
117 | 116 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . 22
         
     
         
         
         
      
                  |
118 | 109, 113,
117 | 3eqtr3d 2513 |
. . . . . . . . . . . . . . . . . . . . 21
         
     
         
         
         
      
              |
119 | 108, 118 | jca 541 |
. . . . . . . . . . . . . . . . . . . 20
         
     
         
         
         
      
 
                          |
120 | 119 | ex 441 |
. . . . . . . . . . . . . . . . . . 19
        
      
         
         
         
                                   |
121 | 120 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . 18
                              
                
      
      
         
         
         
                                   |
122 | 94, 121 | mpd 15 |
. . . . . . . . . . . . . . . . 17
                              
                
      
 
                          |
123 | 73, 72, 89, 122 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
            
                                                 
          
                                            
              |
124 | 123 | simpld 466 |
. . . . . . . . . . . . . . 15
            
                                                 
          
                               
             |
125 | 123 | simprd 470 |
. . . . . . . . . . . . . . 15
            
                                                 
          
                               
             |
126 | 58, 61, 63, 65, 67, 69, 71, 84, 85, 87, 88, 124, 125 | pellexlem6 35749 |
. . . . . . . . . . . . . 14
            
                                                 
          
                                      
        |
127 | 126 | 3exp 1230 |
. . . . . . . . . . . . 13
         


                     
             
                                
                
      
       
          |
128 | 127 | exlimdvv 1788 |
. . . . . . . . . . . 12
         


                     
                                 
          
                             
       
          |
129 | 55, 128 | syl5bi 225 |
. . . . . . . . . . 11
         


                     
    
 
      
       
       
          
                             
       
          |
130 | 129 | ex 441 |
. . . . . . . . . 10
                        
                     
                                
                
      
       
           |
131 | 130 | exlimdvv 1788 |
. . . . . . . . 9
                            
                     
                                
                
      
       
           |
132 | 54, 131 | syl5bi 225 |
. . . . . . . 8
                        
                     
                                
                
      
       
           |
133 | 132 | impd 438 |
. . . . . . 7
                                                       
       
          
                             
       
          |
134 | 53, 133 | sylan2i 667 |
. . . . . 6
                                                       
       
          
                             
       
          |
135 | 134 | rexlimdvv 2877 |
. . . . 5
            
            
             
 
      
              
          
                             
       
         |
136 | 135 | imp 436 |
. . . 4
         


    
 
      
             
 
      
              
          
                                      
        |
137 | 136 | adantlrr 735 |
. . 3
         
     
 
      
              
 
      
             
 
      
              
          
                                      
        |
138 | 41, 137 | mpdan 681 |
. 2
              
 
      
         
       
        |
139 | | pellexlem5 35748 |
. 2
            
 
      
           |
140 | 138, 139 | r19.29a 2918 |
1
                       |