Step | Hyp | Ref
| Expression |
1 | | nfv 1760 |
. . . . . . . . 9
      
    |
2 | | nfcsb1v 3378 |
. . . . . . . . . 10
  
 ![]_ ]_](_urbrack.gif)                                 |
3 | | nfcv 2591 |
. . . . . . . . . 10
       |
4 | | nfcv 2591 |
. . . . . . . . . 10
       |
5 | 2, 3, 4 | nff 5722 |
. . . . . . . . 9
    ![]_ ]_](_urbrack.gif)                                             |
6 | 1, 5 | nfim 2002 |
. . . . . . . 8
   
         ![]_ ]_](_urbrack.gif)                                              |
7 | | eleq1 2516 |
. . . . . . . . . 10
       
   
     |
8 | 7 | anbi2d 709 |
. . . . . . . . 9
  
   
  
           |
9 | | csbeq1a 3371 |
. . . . . . . . . 10
                                  ![]_ ]_](_urbrack.gif)                                  |
10 | 9 | feq1d 5712 |
. . . . . . . . 9
                                            
  ![]_ ]_](_urbrack.gif)  
                                            |
11 | 8, 10 | imbi12d 322 |
. . . . . . . 8
   
        
                                         
        
  ![]_ ]_](_urbrack.gif)  
                                             |
12 | | poimir.0 |
. . . . . . . . . . . . . 14
   |
13 | 12 | nncnd 10622 |
. . . . . . . . . . . . 13
   |
14 | | npcan1 10041 |
. . . . . . . . . . . . 13
       |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . 12
       |
16 | 12 | nnzd 11036 |
. . . . . . . . . . . . . 14
   |
17 | | peano2zm 10977 |
. . . . . . . . . . . . . 14
 
   |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . 13
     |
19 | | uzid 11170 |
. . . . . . . . . . . . 13
   
    
    |
20 | | peano2uz 11209 |
. . . . . . . . . . . . 13
      
 
 
          |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . . . . . 12
        
    |
22 | 15, 21 | eqeltrrd 2529 |
. . . . . . . . . . 11
    
    |
23 | | fzss2 11835 |
. . . . . . . . . . 11
    
 
            |
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
    
 
      |
25 | 24 | sselda 3431 |
. . . . . . . . 9
 
   
         |
26 | | elun 3573 |
. . . . . . . . . . . . 13
      
  
     |
27 | | fzofzp1 12005 |
. . . . . . . . . . . . . . 15
  ..^
        |
28 | | elsni 3992 |
. . . . . . . . . . . . . . . . 17
     |
29 | 28 | oveq2d 6304 |
. . . . . . . . . . . . . . . 16
         |
30 | 29 | eleq1d 2512 |
. . . . . . . . . . . . . . 15
                   |
31 | 27, 30 | syl5ibrcom 226 |
. . . . . . . . . . . . . 14
  ..^
            |
32 | | elfzoelz 11917 |
. . . . . . . . . . . . . . . . . 18
  ..^
  |
33 | 32 | zcnd 11038 |
. . . . . . . . . . . . . . . . 17
  ..^
  |
34 | 33 | addid1d 9830 |
. . . . . . . . . . . . . . . 16
  ..^
    |
35 | | elfzofz 11932 |
. . . . . . . . . . . . . . . 16
  ..^
      |
36 | 34, 35 | eqeltrd 2528 |
. . . . . . . . . . . . . . 15
  ..^
        |
37 | | elsni 3992 |
. . . . . . . . . . . . . . . . 17
     |
38 | 37 | oveq2d 6304 |
. . . . . . . . . . . . . . . 16
         |
39 | 38 | eleq1d 2512 |
. . . . . . . . . . . . . . 15
                   |
40 | 36, 39 | syl5ibrcom 226 |
. . . . . . . . . . . . . 14
  ..^
            |
41 | 31, 40 | jaod 382 |
. . . . . . . . . . . . 13
  ..^
                |
42 | 26, 41 | syl5bi 221 |
. . . . . . . . . . . 12
  ..^
      
         |
43 | 42 | imp 431 |
. . . . . . . . . . 11
   ..^                |
44 | 43 | adantl 468 |
. . . . . . . . . 10
          ..^                 |
45 | | poimirlem25.3 |
. . . . . . . . . . 11
          ..^   |
46 | 45 | adantr 467 |
. . . . . . . . . 10
 
              ..^   |
47 | | 1ex 9635 |
. . . . . . . . . . . . . 14
 |
48 | 47 | fconst 5767 |
. . . . . . . . . . . . 13
                           |
49 | | c0ex 9634 |
. . . . . . . . . . . . . 14
 |
50 | 49 | fconst 5767 |
. . . . . . . . . . . . 13
                               |
51 | 48, 50 | pm3.2i 457 |
. . . . . . . . . . . 12
                                                           |
52 | | poimirlem25.4 |
. . . . . . . . . . . . . 14
               |
53 | | dff1o3 5818 |
. . . . . . . . . . . . . . 15
                              |
54 | 53 | simprbi 466 |
. . . . . . . . . . . . . 14
            
   |
55 | | imain 5657 |
. . . . . . . . . . . . . 14
 
                                      |
56 | 52, 54, 55 | 3syl 18 |
. . . . . . . . . . . . 13
        
                              |
57 | | elfznn0 11884 |
. . . . . . . . . . . . . . . . . 18
       |
58 | 57 | nn0red 10923 |
. . . . . . . . . . . . . . . . 17
       |
59 | 58 | ltp1d 10534 |
. . . . . . . . . . . . . . . 16
         |
60 | | fzdisj 11823 |
. . . . . . . . . . . . . . . 16
       
         |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
         
         |
62 | 61 | imaeq2d 5167 |
. . . . . . . . . . . . . 14
                           |
63 | | ima0 5182 |
. . . . . . . . . . . . . 14
     |
64 | 62, 63 | syl6eq 2500 |
. . . . . . . . . . . . 13
                       |
65 | 56, 64 | sylan9req 2505 |
. . . . . . . . . . . 12
 
                           |
66 | | fun 5744 |
. . . . . . . . . . . 12
                                                                                                                                             |
67 | 51, 65, 66 | sylancr 668 |
. . . . . . . . . . 11
 
                                                                 |
68 | | nn0p1nn 10906 |
. . . . . . . . . . . . . . . . . 18

    |
69 | 57, 68 | syl 17 |
. . . . . . . . . . . . . . . . 17
         |
70 | | nnuz 11191 |
. . . . . . . . . . . . . . . . 17
     |
71 | 69, 70 | syl6eleq 2538 |
. . . . . . . . . . . . . . . 16
             |
72 | | elfzuz3 11794 |
. . . . . . . . . . . . . . . 16
           |
73 | | fzsplit2 11821 |
. . . . . . . . . . . . . . . 16
            
                  |
74 | 71, 72, 73 | syl2anc 666 |
. . . . . . . . . . . . . . 15
                       |
75 | 74 | imaeq2d 5167 |
. . . . . . . . . . . . . 14
                               |
76 | | imaundi 5247 |
. . . . . . . . . . . . . 14
                                     |
77 | 75, 76 | syl6req 2501 |
. . . . . . . . . . . . 13
                                   |
78 | | f1ofo 5819 |
. . . . . . . . . . . . . 14
            
              |
79 | | foima 5796 |
. . . . . . . . . . . . . 14
                           |
80 | 52, 78, 79 | 3syl 18 |
. . . . . . . . . . . . 13
               |
81 | 77, 80 | sylan9eqr 2506 |
. . . . . . . . . . . 12
 
                               |
82 | 81 | feq2d 5713 |
. . . . . . . . . . 11
 
                                                               
                                             |
83 | 67, 82 | mpbid 214 |
. . . . . . . . . 10
 
                                                 |
84 | | ovex 6316 |
. . . . . . . . . . 11
     |
85 | 84 | a1i 11 |
. . . . . . . . . 10
 
           |
86 | | inidm 3640 |
. . . . . . . . . 10
               |
87 | 44, 46, 83, 85, 85, 86 | off 6543 |
. . . . . . . . 9
 
                                                  |
88 | 25, 87 | syldan 473 |
. . . . . . . 8
 
   
                                                |
89 | 6, 11, 88 | chvar 2105 |
. . . . . . 7
 
   
     ![]_ ]_](_urbrack.gif)                                              |
90 | | fzp1elp1 11846 |
. . . . . . . . 9
                   |
91 | 15 | oveq2d 6304 |
. . . . . . . . . . 11
               |
92 | 91 | eleq2d 2513 |
. . . . . . . . . 10
                     |
93 | 92 | biimpa 487 |
. . . . . . . . 9
 
                   |
94 | 90, 93 | sylan2 477 |
. . . . . . . 8
 
   
           |
95 | | nfv 1760 |
. . . . . . . . . 10
           |
96 | | nfcsb1v 3378 |
. . . . . . . . . . 11
      ![]_ ]_](_urbrack.gif) 
                               |
97 | 96, 3, 4 | nff 5722 |
. . . . . . . . . 10
      ![]_ ]_](_urbrack.gif)                                             |
98 | 95, 97 | nfim 2002 |
. . . . . . . . 9
               ![]_ ]_](_urbrack.gif)                                              |
99 | | ovex 6316 |
. . . . . . . . 9
   |
100 | | eleq1 2516 |
. . . . . . . . . . 11
       
         |
101 | 100 | anbi2d 709 |
. . . . . . . . . 10
    
    
           |
102 | | csbeq1a 3371 |
. . . . . . . . . . 11
                                      ![]_ ]_](_urbrack.gif)                                  |
103 | 102 | feq1d 5712 |
. . . . . . . . . 10
                                              
    ![]_ ]_](_urbrack.gif)  
                                            |
104 | 101, 103 | imbi12d 322 |
. . . . . . . . 9
     
      
                                         
        
    ![]_ ]_](_urbrack.gif)  
                                             |
105 | 98, 99, 104, 87 | vtoclf 3098 |
. . . . . . . 8
 
           ![]_ ]_](_urbrack.gif)                                              |
106 | 94, 105 | syldan 473 |
. . . . . . 7
 
   
       ![]_ ]_](_urbrack.gif)                                              |
107 | | csbeq1 3365 |
. . . . . . . . 9
        
 ![]_ ]_](_urbrack.gif)                                         ![]_ ]_](_urbrack.gif)  
                               |
108 | 107 | feq1d 5712 |
. . . . . . . 8
           ![]_ ]_](_urbrack.gif)                                           
         ![]_ ]_](_urbrack.gif)                                               |
109 | | csbeq1 3365 |
. . . . . . . . 9
              ![]_ ]_](_urbrack.gif) 
                                       ![]_ ]_](_urbrack.gif)  
                               |
110 | 109 | feq1d 5712 |
. . . . . . . 8
               ![]_ ]_](_urbrack.gif)                                           
         ![]_ ]_](_urbrack.gif)                                               |
111 | 108, 110 | ifboth 3916 |
. . . . . . 7
    ![]_ ]_](_urbrack.gif)                                                ![]_ ]_](_urbrack.gif)                                            
         ![]_ ]_](_urbrack.gif)                                              |
112 | 89, 106, 111 | syl2anc 666 |
. . . . . 6
 
   
            ![]_ ]_](_urbrack.gif) 
                                            |
113 | | ovex 6316 |
. . . . . . 7
     |
114 | 113, 84 | elmap 7497 |
. . . . . 6
          ![]_ ]_](_urbrack.gif) 
                                                 ![]_ ]_](_urbrack.gif)                                              |
115 | 112, 114 | sylibr 216 |
. . . . 5
 
   
            ![]_ ]_](_urbrack.gif) 
                                          |
116 | | eqid 2450 |
. . . . 5
                ![]_ ]_](_urbrack.gif) 
                                   
           ![]_ ]_](_urbrack.gif)  
                               |
117 | 115, 116 | fmptd 6044 |
. . . 4
                 ![]_ ]_](_urbrack.gif)  
                                                    |
118 | | ovex 6316 |
. . . . 5
           |
119 | | ovex 6316 |
. . . . 5
       |
120 | 118, 119 | elmap 7497 |
. . . 4
                 ![]_ ]_](_urbrack.gif) 
                                             
  
    
           ![]_ ]_](_urbrack.gif)  
                                                    |
121 | 117, 120 | sylibr 216 |
. . 3
                 ![]_ ]_](_urbrack.gif)  
                                            
     |
122 | | rneq 5059 |
. . . . . . . 8
     
           ![]_ ]_](_urbrack.gif)  
                             
                ![]_ ]_](_urbrack.gif)  
                                |
123 | 122 | mpteq1d 4483 |
. . . . . . 7
     
           ![]_ ]_](_urbrack.gif)  
                                     
           ![]_ ]_](_urbrack.gif)  
                                 |
124 | 123 | rneqd 5061 |
. . . . . 6
     
           ![]_ ]_](_urbrack.gif)  
                             
                   ![]_ ]_](_urbrack.gif) 
                                  |
125 | 124 | sseq2d 3459 |
. . . . 5
     
           ![]_ ]_](_urbrack.gif)  
                                      
                       ![]_ ]_](_urbrack.gif)  
                                  |
126 | 122 | rexeqdv 2993 |
. . . . 5
     
           ![]_ ]_](_urbrack.gif)  
                                                      ![]_ ]_](_urbrack.gif)  
                                      |
127 | 125, 126 | anbi12d 716 |
. . . 4
     
           ![]_ ]_](_urbrack.gif)  
                                     
        
                        ![]_ ]_](_urbrack.gif)  
                               
                ![]_ ]_](_urbrack.gif) 
                                        |
128 | 127 | ceqsrexv 3171 |
. . 3
                 ![]_ ]_](_urbrack.gif) 
                                             
    
                                    ![]_ ]_](_urbrack.gif) 
                                                                        ![]_ ]_](_urbrack.gif)  
                               
                ![]_ ]_](_urbrack.gif) 
                                        |
129 | 121, 128 | syl 17 |
. 2
                                       ![]_ ]_](_urbrack.gif) 
                                                                        ![]_ ]_](_urbrack.gif)  
                               
                ![]_ ]_](_urbrack.gif) 
                                        |
130 | | dfss3 3421 |
. . . 4
      
     
           ![]_ ]_](_urbrack.gif)  
                              
    
   
                ![]_ ]_](_urbrack.gif)  
                                 |
131 | | ovex 6316 |
. . . . . . . . . . . . 13
                                            |
132 | | poimirlem28.1 |
. . . . . . . . . . . . 13
                                           
  |
133 | 131, 132 | csbie 3388 |
. . . . . . . . . . . 12
                                             ![]_ ]_](_urbrack.gif)
 |
134 | 133 | csbeq2i 3781 |
. . . . . . . . . . 11
     ![]_ ]_](_urbrack.gif)                                              ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)  |
135 | | opex 4663 |
. . . . . . . . . . . . 13
    |
136 | 135 | a1i 11 |
. . . . . . . . . . . 12
      |
137 | | fveq2 5863 |
. . . . . . . . . . . . . . 15
                 |
138 | | fex 6136 |
. . . . . . . . . . . . . . . . 17
           ..^        |
139 | 45, 84, 138 | sylancl 667 |
. . . . . . . . . . . . . . . 16
   |
140 | | f1oexrnex 6739 |
. . . . . . . . . . . . . . . . 17
                     |
141 | 52, 84, 140 | sylancl 667 |
. . . . . . . . . . . . . . . 16
   |
142 | | op1stg 6802 |
. . . . . . . . . . . . . . . 16
 
          |
143 | 139, 141,
142 | syl2anc 666 |
. . . . . . . . . . . . . . 15
          |
144 | 137, 143 | sylan9eqr 2506 |
. . . . . . . . . . . . . 14
 
          |
145 | | fveq2 5863 |
. . . . . . . . . . . . . . . 16
                 |
146 | | op2ndg 6803 |
. . . . . . . . . . . . . . . . 17
 
          |
147 | 139, 141,
146 | syl2anc 666 |
. . . . . . . . . . . . . . . 16
          |
148 | 145, 147 | sylan9eqr 2506 |
. . . . . . . . . . . . . . 15
 
          |
149 | | imaeq1 5162 |
. . . . . . . . . . . . . . . . 17
                           |
150 | 149 | xpeq1d 4856 |
. . . . . . . . . . . . . . . 16
                                   |
151 | | imaeq1 5162 |
. . . . . . . . . . . . . . . . 17
                               |
152 | 151 | xpeq1d 4856 |
. . . . . . . . . . . . . . . 16
                                       |
153 | 150, 152 | uneq12d 3588 |
. . . . . . . . . . . . . . 15
                                                                       |
154 | 148, 153 | syl 17 |
. . . . . . . . . . . . . 14
 
                                                                      |
155 | 144, 154 | oveq12d 6306 |
. . . . . . . . . . . . 13
 
                                                                                |
156 | 155 | csbeq1d 3369 |
. . . . . . . . . . . 12
 
                                                 ![]_ ]_](_urbrack.gif)  
                               ![]_ ]_](_urbrack.gif)   |
157 | 136, 156 | csbied 3389 |
. . . . . . . . . . 11
      ![]_ ]_](_urbrack.gif)                                              ![]_ ]_](_urbrack.gif)
                                 ![]_ ]_](_urbrack.gif)   |
158 | 134, 157 | syl5eqr 2498 |
. . . . . . . . . 10
      ![]_ ]_](_urbrack.gif)   
                              ![]_ ]_](_urbrack.gif)   |
159 | 158 | csbeq2dv 3780 |
. . . . . . . . 9
          ![]_ ]_](_urbrack.gif)    
 ![]_ ]_](_urbrack.gif)
         ![]_ ]_](_urbrack.gif)                                  ![]_ ]_](_urbrack.gif)   |
160 | 159 | eqeq2d 2460 |
. . . . . . . 8
           ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
         ![]_ ]_](_urbrack.gif)   
                              ![]_ ]_](_urbrack.gif)    |
161 | 160 | rexbidv 2900 |
. . . . . . 7
      
            ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
    
            ![]_ ]_](_urbrack.gif)                                  ![]_ ]_](_urbrack.gif)    |
162 | | vex 3047 |
. . . . . . . . 9
 |
163 | | eqid 2450 |
. . . . . . . . . 10
                 ![]_ ]_](_urbrack.gif) 
                                                 ![]_ ]_](_urbrack.gif) 
                                 |
164 | 163 | elrnmpt 5080 |
. . . . . . . . 9
                   ![]_ ]_](_urbrack.gif) 
                               
     
           ![]_ ]_](_urbrack.gif)  
                                  |
165 | 162, 164 | ax-mp 5 |
. . . . . . . 8
                  ![]_ ]_](_urbrack.gif) 
                               
     
           ![]_ ]_](_urbrack.gif)  
                                 |
166 | | nfv 1760 |
. . . . . . . . 9
  |
167 | | nfcsb1v 3378 |
. . . . . . . . . 10
  
 ![]_ ]_](_urbrack.gif)  |
168 | 167 | nfeq2 2606 |
. . . . . . . . 9

  ![]_ ]_](_urbrack.gif)  |
169 | | csbeq1a 3371 |
. . . . . . . . . 10
   ![]_ ]_](_urbrack.gif)   |
170 | 169 | eqeq2d 2460 |
. . . . . . . . 9
 
  ![]_ ]_](_urbrack.gif)    |
171 | 166, 168,
170 | cbvrex 3015 |
. . . . . . . 8
                  ![]_ ]_](_urbrack.gif) 
                               
     
           ![]_ ]_](_urbrack.gif)  
                                 ![]_ ]_](_urbrack.gif)   |
172 | | ovex 6316 |
. . . . . . . . . . 11
                                |
173 | 172 | csbex 4537 |
. . . . . . . . . 10
         ![]_ ]_](_urbrack.gif) 
                               |
174 | 173 | rgenw 2748 |
. . . . . . . . 9
    
            ![]_ ]_](_urbrack.gif)                                 |
175 | | csbeq1 3365 |
. . . . . . . . . . . 12
          ![]_ ]_](_urbrack.gif)                               
  ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)                                 ![]_ ]_](_urbrack.gif)   |
176 | | vex 3047 |
. . . . . . . . . . . . . 14
 |
177 | 176, 99 | ifex 3948 |
. . . . . . . . . . . . 13
        |
178 | | csbnestg 3786 |
. . . . . . . . . . . . 13
                 ![]_ ]_](_urbrack.gif)   
                              ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)                                 ![]_ ]_](_urbrack.gif)   |
179 | 177, 178 | ax-mp 5 |
. . . . . . . . . . . 12
         ![]_ ]_](_urbrack.gif)                                  ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)                                 ![]_ ]_](_urbrack.gif)  |
180 | 175, 179 | syl6eqr 2502 |
. . . . . . . . . . 11
          ![]_ ]_](_urbrack.gif)                               
  ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)                                  ![]_ ]_](_urbrack.gif)   |
181 | 180 | eqeq2d 2460 |
. . . . . . . . . 10
          ![]_ ]_](_urbrack.gif)                               
   ![]_ ]_](_urbrack.gif)
         ![]_ ]_](_urbrack.gif)                                  ![]_ ]_](_urbrack.gif)    |
182 | 116, 181 | rexrnmpt 6030 |
. . . . . . . . 9
 
                ![]_ ]_](_urbrack.gif) 
                                    
           ![]_ ]_](_urbrack.gif)  
                                 ![]_ ]_](_urbrack.gif)
    
            ![]_ ]_](_urbrack.gif)                                  ![]_ ]_](_urbrack.gif)    |
183 | 174, 182 | ax-mp 5 |
. . . . . . . 8
                  ![]_ ]_](_urbrack.gif) 
                                  ![]_ ]_](_urbrack.gif)
    
            ![]_ ]_](_urbrack.gif)                                  ![]_ ]_](_urbrack.gif)   |
184 | 165, 171,
183 | 3bitri 275 |
. . . . . . 7
                  ![]_ ]_](_urbrack.gif) 
                               
    
            ![]_ ]_](_urbrack.gif)                                  ![]_ ]_](_urbrack.gif)   |
185 | 161, 184 | syl6bbr 267 |
. . . . . 6
      
            ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)
                 ![]_ ]_](_urbrack.gif)  
                                  |
186 | 24 | sselda 3431 |
. . . . . . . . . . . 12
 
   
         |
187 | 186 | adantr 467 |
. . . . . . . . . . 11
      
          |
188 | | elfzelz 11797 |
. . . . . . . . . . . . . 14
         |
189 | 188 | zred 11037 |
. . . . . . . . . . . . 13
         |
190 | 189 | adantl 468 |
. . . . . . . . . . . 12
 
   
     |
191 | | ltne 9727 |
. . . . . . . . . . . . 13
     |
192 | 191 | necomd 2678 |
. . . . . . . . . . . 12
     |
193 | 190, 192 | sylan 474 |
. . . . . . . . . . 11
      
      |
194 | | eldifsn 4096 |
. . . . . . . . . . 11
        
    
   |
195 | 187, 193,
194 | sylanbrc 669 |
. . . . . . . . . 10
      
              |
196 | 94 | adantr 467 |
. . . . . . . . . . 11
      
            |
197 | | poimirlem24.5 |
. . . . . . . . . . . . . . 15
       |
198 | | elfzelz 11797 |
. . . . . . . . . . . . . . 15
       |
199 | 197, 198 | syl 17 |
. . . . . . . . . . . . . 14
   |
200 | 199 | zred 11037 |
. . . . . . . . . . . . 13
   |
201 | 200 | ad2antrr 731 |
. . . . . . . . . . . 12
      
   
  |
202 | | zre 10938 |
. . . . . . . . . . . . . . . 16
   |
203 | | zre 10938 |
. . . . . . . . . . . . . . . 16
   |
204 | | lenlt 9709 |
. . . . . . . . . . . . . . . 16
 
     |
205 | 202, 203,
204 | syl2an 480 |
. . . . . . . . . . . . . . 15
 
     |
206 | | zleltp1 10984 |
. . . . . . . . . . . . . . 15
 
       |
207 | 205, 206 | bitr3d 259 |
. . . . . . . . . . . . . 14
 
 
     |
208 | 199, 188,
207 | syl2an 480 |
. . . . . . . . . . . . 13
 
   
   
     |
209 | 208 | biimpa 487 |
. . . . . . . . . . . 12
      
        |
210 | 201, 209 | gtned 9767 |
. . . . . . . . . . 11
      
        |
211 | | eldifsn 4096 |
. . . . . . . . . . 11
          
            |
212 | 196, 210,
211 | sylanbrc 669 |
. . . . . . . . . 10
      
                |
213 | 195, 212 | ifclda 3912 |
. . . . . . . . 9
 
   
                    |
214 | | nfcsb1v 3378 |
. . . . . . . . . . . 12
           ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)  |
215 | 214 | nfeq2 2606 |
. . . . . . . . . . 11
          ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)  |
216 | | csbeq1a 3371 |
. . . . . . . . . . . 12
             ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)    
 ![]_ ]_](_urbrack.gif)   |
217 | 216 | eqeq2d 2460 |
. . . . . . . . . . 11
              ![]_ ]_](_urbrack.gif)
         ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)    |
218 | 215, 217 | rspce 3144 |
. . . . . . . . . 10
             
            ![]_ ]_](_urbrack.gif)    
 ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)   |
219 | 218 | ex 436 |
. . . . . . . . 9
               
          ![]_ ]_](_urbrack.gif)    
 ![]_ ]_](_urbrack.gif)      
         ![]_ ]_](_urbrack.gif)    |
220 | 213, 219 | syl 17 |
. . . . . . . 8
 
   
             ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif) 
    
         ![]_ ]_](_urbrack.gif)    |
221 | 220 | rexlimdva 2878 |
. . . . . . 7
      
            ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif) 
    
         ![]_ ]_](_urbrack.gif)    |
222 | | nfv 1760 |
. . . . . . . 8
   |
223 | | nfcv 2591 |
. . . . . . . . 9
     
   |
224 | 223, 215 | nfrex 2849 |
. . . . . . . 8
                   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)  |
225 | | eldifi 3554 |
. . . . . . . . . . . . . . 15
               |
226 | 225, 57 | syl 17 |
. . . . . . . . . . . . . 14
           |
227 | 226 | nn0ge0d 10925 |
. . . . . . . . . . . . 13
        
  |
228 | 227 | ad2antlr 732 |
. . . . . . . . . . . 12
            
  |
229 | 226 | nn0red 10923 |
. . . . . . . . . . . . . . 15
           |
230 | 229 | ad2antlr 732 |
. . . . . . . . . . . . . 14
               |
231 | 200 | ad2antrr 731 |
. . . . . . . . . . . . . 14
            
  |
232 | 16 | zred 11037 |
. . . . . . . . . . . . . . 15
   |
233 | 232 | ad2antrr 731 |
. . . . . . . . . . . . . 14
            
  |
234 | | simpr 463 |
. . . . . . . . . . . . . 14
            
  |
235 | | elfzle2 11800 |
. . . . . . . . . . . . . . . 16
       |
236 | 197, 235 | syl 17 |
. . . . . . . . . . . . . . 15

  |
237 | 236 | ad2antrr 731 |
. . . . . . . . . . . . . 14
               |
238 | 230, 231,
233, 234, 237 | ltletrd 9792 |
. . . . . . . . . . . . 13
            
  |
239 | 226 | nn0zd 11035 |
. . . . . . . . . . . . . . 15
           |
240 | | zltlem1 10986 |
. . . . . . . . . . . . . . 15
 
       |
241 | 239, 16, 240 | syl2anr 481 |
. . . . . . . . . . . . . 14
 
               |
242 | 241 | adantr 467 |
. . . . . . . . . . . . 13
                   |
243 | 238, 242 | mpbid 214 |
. . . . . . . . . . . 12
            
    |
244 | | 0z 10945 |
. . . . . . . . . . . . . . 15
 |
245 | | elfz 11787 |
. . . . . . . . . . . . . . 15
 

         
      |
246 | 244, 245 | mp3an2 1351 |
. . . . . . . . . . . . . 14
  
      
  
      |
247 | 239, 18, 246 | syl2anr 481 |
. . . . . . . . . . . . 13
 
                
      |
248 | 247 | adantr 467 |
. . . . . . . . . . . 12
                    
      |
249 | 228, 243,
248 | mpbir2and 932 |
. . . . . . . . . . 11
                     |
250 | | 0red 9641 |
. . . . . . . . . . . . . . 15
           
   |
251 | 200 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
           
   |
252 | 229 | ad2antlr 732 |
. . . . . . . . . . . . . . 15
           
   |
253 | | elfzle1 11799 |
. . . . . . . . . . . . . . . . 17
       |
254 | 197, 253 | syl 17 |
. . . . . . . . . . . . . . . 16

  |
255 | 254 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
           
   |
256 | | lenlt 9709 |
. . . . . . . . . . . . . . . . . 18
 
     |
257 | 200, 229,
256 | syl2an 480 |
. . . . . . . . . . . . . . . . 17
 
             |
258 | 257 | biimpar 488 |
. . . . . . . . . . . . . . . 16
           
   |
259 | | eldifsni 4097 |
. . . . . . . . . . . . . . . . 17
           |
260 | 259 | ad2antlr 732 |
. . . . . . . . . . . . . . . 16
           
   |
261 | | ltlen 9732 |
. . . . . . . . . . . . . . . . . 18
 
  
    |
262 | 200, 229,
261 | syl2an 480 |
. . . . . . . . . . . . . . . . 17
 
          
    |
263 | 262 | adantr 467 |
. . . . . . . . . . . . . . . 16
           
  
    |
264 | 258, 260,
263 | mpbir2and 932 |
. . . . . . . . . . . . . . 15
           
   |
265 | 250, 251,
252, 255, 264 | lelttrd 9790 |
. . . . . . . . . . . . . 14
           
   |
266 | | zgt0ge1 10987 |
. . . . . . . . . . . . . . . 16
 
   |
267 | 239, 266 | syl 17 |
. . . . . . . . . . . . . . 15
             |
268 | 267 | ad2antlr 732 |
. . . . . . . . . . . . . 14
           
     |
269 | 265, 268 | mpbid 214 |
. . . . . . . . . . . . 13
           
   |
270 | | elfzle2 11800 |
. . . . . . . . . . . . . . 15
       |
271 | 225, 270 | syl 17 |
. . . . . . . . . . . . . 14
        
  |
272 | 271 | ad2antlr 732 |
. . . . . . . . . . . . 13
           
   |
273 | | 1z 10964 |
. . . . . . . . . . . . . . . 16
 |
274 | | elfz 11787 |
. . . . . . . . . . . . . . . 16
 
     
     |
275 | 273, 274 | mp3an2 1351 |
. . . . . . . . . . . . . . 15
 
      
    |
276 | 239, 16, 275 | syl2anr 481 |
. . . . . . . . . . . . . 14
 
              
    |
277 | 276 | adantr 467 |
. . . . . . . . . . . . 13
           
      
    |
278 | 269, 272,
277 | mpbir2and 932 |
. . . . . . . . . . . 12
           
       |
279 | | elfzmlbm 11897 |
. . . . . . . . . . . 12
               |
280 | 278, 279 | syl 17 |
. . . . . . . . . . 11
           
           |
281 | 249, 280 | ifclda 3912 |
. . . . . . . . . 10
 
                        |
282 | | breq1 4404 |
. . . . . . . . . . . . . . . 16
                   |
283 | | id 22 |
. . . . . . . . . . . . . . . 16
                 |
284 | | oveq1 6295 |
. . . . . . . . . . . . . . . 16
                     |
285 | 282, 283,
284 | ifbieq12d 3907 |
. . . . . . . . . . . . . . 15
                                             |
286 | 285 | eqeq2d 2460 |
. . . . . . . . . . . . . 14
                                               |
287 | | breq1 4404 |
. . . . . . . . . . . . . . . 16
                       |
288 | | id 22 |
. . . . . . . . . . . . . . . 16
                     |
289 | | oveq1 6295 |
. . . . . . . . . . . . . . . 16
                         |
290 | 287, 288,
289 | ifbieq12d 3907 |
. . . . . . . . . . . . . . 15
                                                     |
291 | 290 | eqeq2d 2460 |
. . . . . . . . . . . . . 14
                                                       |
292 | | iftrue 3886 |
. . . . . . . . . . . . . . . 16
          |
293 | 292 | eqcomd 2456 |
. . . . . . . . . . . . . . 15
          |
294 | 293 | adantl 468 |
. . . . . . . . . . . . . 14
                      |
295 | | zlem1lt 10985 |
. . . . . . . . . . . . . . . . . . 19
 
       |
296 | 239, 199,
295 | syl2anr 481 |
. . . . . . . . . . . . . . . . . 18
 
               |
297 | 259 | necomd 2678 |
. . . . . . . . . . . . . . . . . . . 20
           |
298 | 297 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
 
           |
299 | | ltlen 9732 |
. . . . . . . . . . . . . . . . . . . . 21
 
  |