Step | Hyp | Ref
| Expression |
1 | | poimir.r |
. . . . . . . . . . . 12
                 |
2 | | fzfi 12223 |
. . . . . . . . . . . . 13
     |
3 | | retop 21860 |
. . . . . . . . . . . . . 14
     |
4 | 3 | fconst6 5786 |
. . . . . . . . . . . . 13
                     |
5 | | pttop 20674 |
. . . . . . . . . . . . 13
                                             |
6 | 2, 4, 5 | mp2an 686 |
. . . . . . . . . . . 12
                 |
7 | 1, 6 | eqeltri 2545 |
. . . . . . . . . . 11
 |
8 | | poimir.i |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)        |
9 | | ovex 6336 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif)        |
10 | 8, 9 | eqeltri 2545 |
. . . . . . . . . . 11
 |
11 | | elrest 15404 |
. . . . . . . . . . 11
 
   ↾t 

     |
12 | 7, 10, 11 | mp2an 686 |
. . . . . . . . . 10
  ↾t  
    |
13 | | eqid 2471 |
. . . . . . . . . . . . . 14
           |
14 | 1, 13 | ptrecube 32004 |
. . . . . . . . . . . . 13
 
                  
     
  |
15 | 14 | ex 441 |
. . . . . . . . . . . 12
 
                  
    
   |
16 | | inss1 3643 |
. . . . . . . . . . . . . . 15
   |
17 | | sseq1 3439 |
. . . . . . . . . . . . . . 15
   
     |
18 | 16, 17 | mpbiri 241 |
. . . . . . . . . . . . . 14
     |
19 | 18 | sseld 3417 |
. . . . . . . . . . . . 13
   
   |
20 | | ssrin 3648 |
. . . . . . . . . . . . . . 15
 
               
     
                 
       
   |
21 | | sseq2 3440 |
. . . . . . . . . . . . . . 15
                     
                        
       
    |
22 | 20, 21 | syl5ibr 229 |
. . . . . . . . . . . . . 14
                    
     
                 
          |
23 | 22 | reximdv 2857 |
. . . . . . . . . . . . 13
    
                 
    
                  
          |
24 | 19, 23 | imim12d 76 |
. . . . . . . . . . . 12
                      
     
                    
           |
25 | 15, 24 | syl5com 30 |
. . . . . . . . . . 11
                       
           |
26 | 25 | rexlimiv 2867 |
. . . . . . . . . 10
    
                  
          |
27 | 12, 26 | sylbi 200 |
. . . . . . . . 9
  ↾t  
                   
         |
28 | 27 | imp 436 |
. . . . . . . 8
   ↾t                      
        |
29 | 28 | adantl 473 |
. . . . . . 7
 
 
↾t    
                 
         |
30 | | resttop 20253 |
. . . . . . . . . . 11
 
 
↾t    |
31 | 7, 10, 30 | mp2an 686 |
. . . . . . . . . 10
 ↾t   |
32 | | reex 9648 |
. . . . . . . . . . . . . 14
 |
33 | | unitssre 11805 |
. . . . . . . . . . . . . 14
  ![[,] [,]](_icc.gif)   |
34 | | mapss 7532 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif) 
    ![[,] [,]](_icc.gif)               |
35 | 32, 33, 34 | mp2an 686 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)       
      |
36 | 8, 35 | eqsstri 3448 |
. . . . . . . . . . . 12

      |
37 | | ovex 6336 |
. . . . . . . . . . . . . 14
     |
38 | | uniretop 21861 |
. . . . . . . . . . . . . . 15
      |
39 | 1, 38 | ptuniconst 20690 |
. . . . . . . . . . . . . 14
                    |
40 | 37, 3, 39 | mp2an 686 |
. . . . . . . . . . . . 13
        |
41 | 40 | restuni 20255 |
. . . . . . . . . . . 12
        
  ↾t    |
42 | 7, 36, 41 | mp2an 686 |
. . . . . . . . . . 11
  ↾t   |
43 | 42 | eltopss 20014 |
. . . . . . . . . 10
  
↾t   ↾t     |
44 | 31, 43 | mpan 684 |
. . . . . . . . 9
  ↾t    |
45 | 44 | sselda 3418 |
. . . . . . . 8
   ↾t     |
46 | | 2rp 11330 |
. . . . . . . . . . . . . . . . 17
 |
47 | | rpdivcl 11348 |
. . . . . . . . . . . . . . . . 17
       |
48 | 46, 47 | mpan 684 |
. . . . . . . . . . . . . . . 16

    |
49 | 48 | rpred 11364 |
. . . . . . . . . . . . . . 15

    |
50 | | ceicl 12103 |
. . . . . . . . . . . . . . 15
             |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . 14

          |
52 | | 0red 9662 |
. . . . . . . . . . . . . . 15

  |
53 | 51 | zred 11063 |
. . . . . . . . . . . . . . 15

          |
54 | 48 | rpgt0d 11367 |
. . . . . . . . . . . . . . 15

    |
55 | | ceige 12105 |
. . . . . . . . . . . . . . . 16
               |
56 | 49, 55 | syl 17 |
. . . . . . . . . . . . . . 15

            |
57 | 52, 49, 53, 54, 56 | ltletrd 9812 |
. . . . . . . . . . . . . 14

          |
58 | | elnnz 10971 |
. . . . . . . . . . . . . 14
        
                    |
59 | 51, 57, 58 | sylanbrc 677 |
. . . . . . . . . . . . 13

          |
60 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
                           |
61 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . 18
                       |
62 | 61 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
                   
                  
                  |
63 | 62 | eleq2d 2534 |
. . . . . . . . . . . . . . . 16
                                            
                                        
                   |
64 | 63 | ralbidv 2829 |
. . . . . . . . . . . . . . 15
          
                                      
       
                                       
                   |
65 | 60, 64 | rexeqbidv 2988 |
. . . . . . . . . . . . . 14
          
     
                                      
       
                                                      
                  |
66 | 65 | rspcv 3132 |
. . . . . . . . . . . . 13
                                                        
       
                                                      
                  |
67 | 59, 66 | syl 17 |
. . . . . . . . . . . 12

 
      
                                      
        
             
                                      
                   |
68 | 67 | adantl 473 |
. . . . . . . . . . 11
      
                                             
       
                                                      
                  |
69 | | uznnssnn 11229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                       |
70 | 59, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

              |
71 | 70 | sseld 3417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

                |
72 | 71 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                     |
73 | 72 | imdistani 704 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   


               
     |
74 | 59 | nnrpd 11362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

          |
75 | 48, 74 | lerecd 11383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

          
                 |
76 | 56, 75 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

                |
77 | | rpcn 11333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
78 | | rpne0 11340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
79 | | 2cn 10702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
80 | | 2ne0 10724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
81 | | recdiv 10335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
               |
82 | 79, 80, 81 | mpanl12 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
83 | 77, 78, 82 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

        |
84 | 76, 83 | breqtrd 4420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

              |
85 | 84 | ad4antlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                           |
86 | | elmapi 7511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
    ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)    |
87 | 86, 8 | eleq2s 2567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           ![[,] [,]](_icc.gif)    |
88 | 87 | ad4antlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
            
          ![[,] [,]](_icc.gif)    |
89 | 88 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
                   ![[,] [,]](_icc.gif)    |
90 | 33, 89 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
                   |
91 | | simp-4l 784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
            
  |
92 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
            
  |
93 | 91, 92 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
            
    |
94 | | poimirlem30.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                             |
95 | 94 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 

                            |
96 | | xp1st 6842 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                                           |
97 | | elmapi 7511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                                 |
98 | 95, 96, 97 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 

                  |
99 | 98 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                       |
100 | 99 | nn0red 10950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                       |
101 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
           |
102 | 100, 101 | nndivred 10680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                         |
103 | 93, 102 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
                             |
104 | 90, 103 | resubcld 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
                                   |
105 | 104 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
                                   |
106 | 105 | abscld 13575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                                       |
107 | 59 | nnrecred 10677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

            |
108 | 107 | ad4antlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                         |
109 | | rphalfcl 11350 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

    |
110 | 109 | rpred 11364 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

    |
111 | 110 | ad4antlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                 |
112 | | ltletr 9743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                                                                                                     |
113 | 106, 108,
111, 112 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                                                                                           |
114 | 85, 113 | mpan2d 688 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
                                                                             |
115 | 73, 114 | sylanl1 662 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
                                                                                         |
116 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
   |
117 | 70 | sselda 3418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
              
  |
118 | 116, 117 | anim12i 576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                       |
119 | 118 | anassrs 660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   


             
   |
120 | | 1re 9660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 |
121 | | snssi 4107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  
  |
122 | 120, 121 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
 |
123 | | 0re 9661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 |
124 | | snssi 4107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  
  |
125 | 123, 124 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
 |
126 | 122, 125 | unssi 3600 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
127 | | 1ex 9656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 |
128 | 127 | fconst 5782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                                           |
129 | | c0ex 9655 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 |
130 | 129 | fconst 5782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                                               |
131 | 128, 130 | pm3.2i 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                                                                                           |
132 | | xp2nd 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
                                                   |
133 | 95, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 

                        |
134 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
         |
135 | | f1oeq1 5818 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
        
                                    |
136 | 134, 135 | elab 3173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                                             |
137 | 133, 136 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 

                      |
138 | | dff1o3 5834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                                         
            |
139 | 138 | simprbi 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                    
           |
140 | | imain 5669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
         
                                                              |
141 | 137, 139,
140 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 

                                                              |
142 | | elfznn0 11913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
       |
143 | 142 | nn0red 10950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
       |
144 | 143 | ltp1d 10559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
         |
145 | | fzdisj 11852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
       
         |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
         
         |
147 | 146 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                                           |
148 | | ima0 5189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
             |
149 | 147, 148 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                               |
150 | 141, 149 | sylan9req 2526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                                               |
151 | | fun 5758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                                                                                                                                                                                                                             |
152 | 131, 150,
151 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                                                                                                     |
153 | | imaundi 5254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                                                             |
154 | | nn0p1nn 10933 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42

    |
155 | 142, 154 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
         |
156 | | nnuz 11218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
     |
157 | 155, 156 | syl6eleq 2559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
             |
158 | | elfzuz3 11823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
           |
159 | | fzsplit2 11850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
            
                  |
160 | 157, 158,
159 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
                       |
161 | 160 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                                               |
162 | | f1ofo 5835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
                    
                      |
163 | | foima 5811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
                                           |
164 | 137, 162,
163 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 

                      |
165 | 161, 164 | sylan9req 2526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                                       |
166 | 165 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                                       |
167 | 153, 166 | syl5eqr 2519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                                                   |
168 | 167 | feq2d 5725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                                                                                                   
                                                             |
169 | 152, 168 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                                                     |
170 | 169 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   

         
                                                        |
171 | 126, 170 | sseldi 3416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   

         
                                                  |
172 | | simpllr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   

         
  |
173 | 171, 172 | nndivred 10680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   

         
                                                    |
174 | 173 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   

         
                                                    |
175 | 174 | absnegd 13588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   

         
                                                                                                               |
176 | 119, 175 | sylanl1 662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                                                                                                                                        |
177 | 119, 170 | sylanl1 662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
                                                                                 |
178 | | elun 3565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                                                      
                                                                                                        |
179 | 177, 178 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                                                                                                                                 |
180 | | nnrecre 10668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     |
181 | | nnrp 11334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
   |
182 | 181 | rpreccld 11374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     |
183 | 182 | rpge0d 11368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     |
184 | 180, 183 | absidd 13561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           |
185 | 117, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
              
          |
186 | 117 | nnrecred 10677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
              
    |
187 | 107 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
              
            |
188 | 110 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
              
    |
189 | | eluzle 11195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                       |
190 | 189 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
              
          |
191 | 59 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
              
          |
192 | 191 | nnrpd 11362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
              
          |
193 | 117 | nnrpd 11362 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
              
  |
194 | 192, 193 | lerecd 11383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
              
                        |
195 | 190, 194 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
              
              |
196 | 84 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
              
              |
197 | 186, 187,
188, 195, 196 | letrd 9809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
              
      |
198 | 185, 197 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
              
          |
199 | | elsni 3985 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                                                                                                     |
200 | 199 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                                                                                                         |
201 | 200 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                                                                                                 |
202 | 201 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                                                                                         
 
           |
203 | 198, 202 | syl5ibrcom 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              
                                                                                                        
     |
204 | 109 | rpge0d 11368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

    |
205 | | nncn 10639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
   |
206 | | nnne0 10664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
   |
207 | 205, 206 | div0d 10404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
     |
208 | 207 | abs00bd 13431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
         |
209 | 208 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       
 
     |
210 | 209 | biimparc 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
 
      
    |
211 | 204, 210 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
             |
212 | 117, 211 | syldan 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
              
          |
213 | | elsni 3985 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                                                                                                     |
214 | 213 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                                                                                                         |
215 | 214 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                                                                                                 |
216 | 215 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                                                                                         
 
           |
217 | 212, 216 | syl5ibrcom 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              
                                                                                                        
     |
218 | 203, 217 | jaod 387 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
              
                                                                                                                                                            
     |
219 | 218 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   


                                                                                                                                                                         
     |
220 | 219 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                                                                                                                                                                                     
     |
221 | 179, 220 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                                                                              
    |
222 | 176, 221 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
                                                                               
    |
223 | 73, 106 | sylanl1 662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                                                   |
224 | | simpll 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
225 | 224 | anim1i 578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   


 
   |
226 | 173 | renegcld 10067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   

         
                                                     |
227 | 225, 226 | sylanl1 662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
                                                                  |
228 | 227 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
                                                                  |
229 | 228 | abscld 13575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                                                                      |
230 | 73, 229 | sylanl1 662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                                                                                  |
231 | 110, 110 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

        |
232 | 231 | ad4antlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                                 |
233 | | ltleadd 10118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                                                                                                                                                            
                                                                                             |
234 | 223, 230,
232, 233 | syl21anc 1291 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
                                                                                                           
                                                                                             |
235 | 222, 234 | mpan2d 688 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
                                                                                                                                              |
236 | 105, 228 | abstrid 13595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                                                                                                                                                                             |
237 | 104, 227 | readdcld 9688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
                                                                                        |
238 | 237 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
                                                                                        |
239 | 238 | abscld 13575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                                                                                            |
240 | 106, 229 | readdcld 9688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                                                                                                |
241 | 110, 110 | readdcld 9688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

        |
242 | 241 | ad4antlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                     |
243 | | lelttr 9742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                                                                                                                                                                                                                                                                                                                                                                                                              
                                                                                      |
244 | 239, 240,
242, 243 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
                                                                                                                                                                                                                                                                    
                                                                                      |
245 | 236, 244 | mpand 689 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
                                                                                                                                                                                           |
246 | 73, 245 | sylanl1 662 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
 |