Proof of Theorem jm2.26lem3
Step | Hyp | Ref
| Expression |
1 | | simplll 767 |
. . . . . . . . . 10
       
     
      
      |
2 | | elfzelz 11797 |
. . . . . . . . . . . 12
       |
3 | 2 | adantr 467 |
. . . . . . . . . . 11
     
       |
4 | 3 | ad2antlr 732 |
. . . . . . . . . 10
       
     
      
  |
5 | | rmyabs 35802 |
. . . . . . . . . 10
           Yrm    Yrm        |
6 | 1, 4, 5 | syl2anc 666 |
. . . . . . . . 9
       
     
           Yrm   
Yrm        |
7 | 3 | zred 11037 |
. . . . . . . . . . . 12
     
       |
8 | 7 | ad2antlr 732 |
. . . . . . . . . . 11
       
     
      
  |
9 | | elfzle1 11799 |
. . . . . . . . . . . . 13
       |
10 | 9 | adantr 467 |
. . . . . . . . . . . 12
     
       |
11 | 10 | ad2antlr 732 |
. . . . . . . . . . 11
       
     
      
  |
12 | 8, 11 | absidd 13477 |
. . . . . . . . . 10
       
     
             |
13 | 12 | oveq2d 6304 |
. . . . . . . . 9
       
     
       
Yrm       Yrm    |
14 | 6, 13 | eqtrd 2484 |
. . . . . . . 8
       
     
           Yrm   
Yrm    |
15 | | elfzelz 11797 |
. . . . . . . . . . . 12
       |
16 | 15 | adantl 468 |
. . . . . . . . . . 11
     
       |
17 | 16 | ad2antlr 732 |
. . . . . . . . . 10
       
     
      
  |
18 | | rmyabs 35802 |
. . . . . . . . . 10
           Yrm    Yrm        |
19 | 1, 17, 18 | syl2anc 666 |
. . . . . . . . 9
       
     
           Yrm   
Yrm        |
20 | 16 | zred 11037 |
. . . . . . . . . . . 12
     
       |
21 | 20 | ad2antlr 732 |
. . . . . . . . . . 11
       
     
      
  |
22 | | elfzle1 11799 |
. . . . . . . . . . . . 13
       |
23 | 22 | adantl 468 |
. . . . . . . . . . . 12
     
       |
24 | 23 | ad2antlr 732 |
. . . . . . . . . . 11
       
     
      
  |
25 | 21, 24 | absidd 13477 |
. . . . . . . . . 10
       
     
             |
26 | 25 | oveq2d 6304 |
. . . . . . . . 9
       
     
       
Yrm       Yrm    |
27 | 19, 26 | eqtrd 2484 |
. . . . . . . 8
       
     
           Yrm   
Yrm    |
28 | 14, 27 | oveq12d 6306 |
. . . . . . 7
       
     
            Yrm       Yrm      Yrm   Yrm     |
29 | | frmy 35756 |
. . . . . . . . . . . 12
Yrm
          |
30 | 29 | fovcl 6398 |
. . . . . . . . . . 11
        Yrm    |
31 | 1, 4, 30 | syl2anc 666 |
. . . . . . . . . 10
       
     
       
Yrm    |
32 | 31 | zred 11037 |
. . . . . . . . 9
       
     
       
Yrm    |
33 | 29 | fovcl 6398 |
. . . . . . . . . . 11
        Yrm    |
34 | 1, 17, 33 | syl2anc 666 |
. . . . . . . . . 10
       
     
       
Yrm    |
35 | 34 | zred 11037 |
. . . . . . . . 9
       
     
       
Yrm    |
36 | 32, 35 | readdcld 9667 |
. . . . . . . 8
       
     
         Yrm   Yrm     |
37 | | simpllr 768 |
. . . . . . . . . . . . 13
       
     
      
  |
38 | 37 | nnzd 11036 |
. . . . . . . . . . . 12
       
     
      
  |
39 | | peano2zm 10977 |
. . . . . . . . . . . 12
 
   |
40 | 38, 39 | syl 17 |
. . . . . . . . . . 11
       
     
           |
41 | 29 | fovcl 6398 |
. . . . . . . . . . 11
      
  
Yrm      |
42 | 1, 40, 41 | syl2anc 666 |
. . . . . . . . . 10
       
     
       
Yrm      |
43 | 42 | zred 11037 |
. . . . . . . . 9
       
     
       
Yrm      |
44 | 29 | fovcl 6398 |
. . . . . . . . . . 11
        Yrm    |
45 | 1, 38, 44 | syl2anc 666 |
. . . . . . . . . 10
       
     
       
Yrm    |
46 | 45 | zred 11037 |
. . . . . . . . 9
       
     
       
Yrm    |
47 | 43, 46 | readdcld 9667 |
. . . . . . . 8
       
     
         Yrm     Yrm     |
48 | | frmx 35755 |
. . . . . . . . . . 11
Xrm
          |
49 | 48 | fovcl 6398 |
. . . . . . . . . 10
        Xrm    |
50 | 1, 38, 49 | syl2anc 666 |
. . . . . . . . 9
       
     
       
Xrm    |
51 | 50 | nn0red 10923 |
. . . . . . . 8
       
     
       
Xrm    |
52 | | elfzle2 11800 |
. . . . . . . . . . . 12
           |
53 | 52 | adantl 468 |
. . . . . . . . . . 11
        


   
          
       |
54 | | lermy 35799 |
. . . . . . . . . . . . 13
           
 Yrm 
 Yrm       |
55 | 1, 4, 40, 54 | syl3anc 1267 |
. . . . . . . . . . . 12
       
     
        
 
Yrm  
Yrm       |
56 | 55 | adantr 467 |
. . . . . . . . . . 11
        


   
          
     
 Yrm 
 Yrm       |
57 | 53, 56 | mpbid 214 |
. . . . . . . . . 10
        


   
          
    Yrm   Yrm      |
58 | | simplrr 770 |
. . . . . . . . . . . . 13
       
     
      
      |
59 | | elfzle2 11800 |
. . . . . . . . . . . . 13
       |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
       
     
         |
61 | | lermy 35799 |
. . . . . . . . . . . . 13
       
 Yrm 
 Yrm     |
62 | 1, 17, 38, 61 | syl3anc 1267 |
. . . . . . . . . . . 12
       
     
         Yrm   Yrm     |
63 | 60, 62 | mpbid 214 |
. . . . . . . . . . 11
       
     
       
Yrm  
Yrm    |
64 | 63 | adantr 467 |
. . . . . . . . . 10
        


   
          
    Yrm   Yrm    |
65 | | le2add 10093 |
. . . . . . . . . . . 12
    Yrm   Yrm     Yrm    
Yrm       Yrm 
 Yrm     Yrm 
 Yrm    
Yrm  
Yrm     Yrm     Yrm      |
66 | 32, 35, 43, 46, 65 | syl22anc 1268 |
. . . . . . . . . . 11
       
     
          Yrm 
 Yrm     Yrm 
 Yrm    
Yrm  
Yrm     Yrm     Yrm      |
67 | 66 | adantr 467 |
. . . . . . . . . 10
        


   
          
      Yrm   Yrm     Yrm   Yrm  
  Yrm   Yrm     Yrm     Yrm      |
68 | 57, 64, 67 | mp2and 684 |
. . . . . . . . 9
        


   
          
    
Yrm  
Yrm     Yrm     Yrm     |
69 | 31 | zcnd 11038 |
. . . . . . . . . . . 12
       
     
       
Yrm    |
70 | 34 | zcnd 11038 |
. . . . . . . . . . . 12
       
     
       
Yrm    |
71 | 69, 70 | addcomd 9832 |
. . . . . . . . . . 11
       
     
         Yrm   Yrm     Yrm   Yrm     |
72 | 71 | adantr 467 |
. . . . . . . . . 10
        


   
         
Yrm  
Yrm     Yrm   Yrm     |
73 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
   |
74 | 73 | necomd 2678 |
. . . . . . . . . . . . . . . . . 18
   |
75 | 74 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
   |
76 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
 
   |
77 | 75, 76 | neeqtrd 2692 |
. . . . . . . . . . . . . . . 16
 
   |
78 | 77 | neneqd 2628 |
. . . . . . . . . . . . . . 15
 
   |
79 | 78 | adantll 719 |
. . . . . . . . . . . . . 14
        


   
       
  |
80 | | nnnn0 10873 |
. . . . . . . . . . . . . . . . 17
   |
81 | | nn0uz 11190 |
. . . . . . . . . . . . . . . . 17
     |
82 | 80, 81 | syl6eleq 2538 |
. . . . . . . . . . . . . . . 16
       |
83 | 82 | ad4antlr 738 |
. . . . . . . . . . . . . . 15
        


   
              |
84 | | simprr 765 |
. . . . . . . . . . . . . . . 16
      
                  |
85 | 84 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
        


   
              |
86 | | fzm1 11871 |
. . . . . . . . . . . . . . . 16
    
         
      |
87 | 86 | biimpa 487 |
. . . . . . . . . . . . . . 15
           
         |
88 | 83, 85, 87 | syl2anc 666 |
. . . . . . . . . . . . . 14
        


   
        
         |
89 | | orel2 385 |
. . . . . . . . . . . . . 14
      
      
     |
90 | 79, 88, 89 | sylc 62 |
. . . . . . . . . . . . 13
        


   
           
    |
91 | | elfzle2 11800 |
. . . . . . . . . . . . 13
           |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . 12
        


   
            |
93 | | lermy 35799 |
. . . . . . . . . . . . . 14
           
 Yrm 
 Yrm       |
94 | 1, 17, 40, 93 | syl3anc 1267 |
. . . . . . . . . . . . 13
       
     
        
 
Yrm  
Yrm       |
95 | 94 | adantr 467 |
. . . . . . . . . . . 12
        


   
          
 Yrm 
 Yrm       |
96 | 92, 95 | mpbid 214 |
. . . . . . . . . . 11
        


   
         Yrm   Yrm      |
97 | | simplrl 769 |
. . . . . . . . . . . . . 14
       
     
      
      |
98 | | elfzle2 11800 |
. . . . . . . . . . . . . 14
       |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . 13
       
     
         |
100 | | lermy 35799 |
. . . . . . . . . . . . . 14
       
 Yrm 
 Yrm     |
101 | 1, 4, 38, 100 | syl3anc 1267 |
. . . . . . . . . . . . 13
       
     
         Yrm   Yrm     |
102 | 99, 101 | mpbid 214 |
. . . . . . . . . . . 12
       
     
       
Yrm  
Yrm    |
103 | 102 | adantr 467 |
. . . . . . . . . . 11
        


   
         Yrm   Yrm    |
104 | | le2add 10093 |
. . . . . . . . . . . . 13
    Yrm   Yrm     Yrm    
Yrm       Yrm 
 Yrm     Yrm 
 Yrm    
Yrm  
Yrm     Yrm     Yrm      |
105 | 35, 32, 43, 46, 104 | syl22anc 1268 |
. . . . . . . . . . . 12
       
     
          Yrm 
 Yrm     Yrm 
 Yrm    
Yrm  
Yrm     Yrm     Yrm      |
106 | 105 | adantr 467 |
. . . . . . . . . . 11
        


   
           Yrm   Yrm     Yrm   Yrm  
  Yrm   Yrm     Yrm     Yrm      |
107 | 96, 103, 106 | mp2and 684 |
. . . . . . . . . 10
        


   
         
Yrm  
Yrm     Yrm     Yrm     |
108 | 72, 107 | eqbrtrd 4422 |
. . . . . . . . 9
        


   
         
Yrm  
Yrm     Yrm     Yrm     |
109 | 37 | nnnn0d 10922 |
. . . . . . . . . . 11
       
     
      
  |
110 | 109, 81 | syl6eleq 2538 |
. . . . . . . . . 10
       
     
      
      |
111 | | fzm1 11871 |
. . . . . . . . . . 11
    
         
      |
112 | 111 | biimpa 487 |
. . . . . . . . . 10
           
         |
113 | 110, 97, 112 | syl2anc 666 |
. . . . . . . . 9
       
     
                 |
114 | 68, 108, 113 | mpjaodan 794 |
. . . . . . . 8
       
     
         Yrm   Yrm  
  Yrm     Yrm     |
115 | | jm2.24 35807 |
. . . . . . . . 9
        
Yrm    
Yrm    Xrm    |
116 | 1, 38, 115 | syl2anc 666 |
. . . . . . . 8
       
     
         Yrm     Yrm    Xrm    |
117 | 36, 47, 51, 114, 116 | lelttrd 9790 |
. . . . . . 7
       
     
         Yrm   Yrm    Xrm    |
118 | 28, 117 | eqbrtrd 4422 |
. . . . . 6
       
     
            Yrm       Yrm     Xrm    |
119 | | simpr 463 |
. . . . . . 7
       
     
         |
120 | | rmyeq 35798 |
. . . . . . . . 9
       
 Yrm   Yrm     |
121 | 120 | necon3bid 2667 |
. . . . . . . 8
       
 Yrm   Yrm     |
122 | 1, 4, 17, 121 | syl3anc 1267 |
. . . . . . 7
       
     
         Yrm   Yrm     |
123 | 119, 122 | mpbid 214 |
. . . . . 6
       
     
       
Yrm  
Yrm    |
124 | 7 | ad2antlr 732 |
. . . . . . . . . . . . 13
       
     
     
    |
125 | | 0red 9641 |
. . . . . . . . . . . . 13
       
     
     
    |
126 | | simpr 463 |
. . . . . . . . . . . . . 14
       
     
     
     |
127 | 22 | ad2antll 734 |
. . . . . . . . . . . . . . . 16
      
              |
128 | 20 | adantl 468 |
. . . . . . . . . . . . . . . . 17
      
              |
129 | 128 | le0neg2d 10183 |
. . . . . . . . . . . . . . . 16
      
            
    |
130 | 127, 129 | mpbid 214 |
. . . . . . . . . . . . . . 15
      
               |
131 | 130 | adantr 467 |
. . . . . . . . . . . . . 14
       
     
     
     |
132 | 126, 131 | eqbrtrd 4422 |
. . . . . . . . . . . . 13
       
     
     
    |
133 | 10 | ad2antlr 732 |
. . . . . . . . . . . . 13
       
     
     
    |
134 | | letri3 9716 |
. . . . . . . . . . . . . 14
 
  
    |
135 | 134 | biimpar 488 |
. . . . . . . . . . . . 13
    
    |
136 | 124, 125,
132, 133, 135 | syl22anc 1268 |
. . . . . . . . . . . 12
       
     
     
    |
137 | | simpr 463 |
. . . . . . . . . . . . 13
        


   
       
   |
138 | | simplr 761 |
. . . . . . . . . . . . . . 15
        


   
       
    |
139 | 138, 137 | eqtr3d 2486 |
. . . . . . . . . . . . . 14
        


   
       
    |
140 | 128 | recnd 9666 |
. . . . . . . . . . . . . . . 16
      
              |
141 | 140 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
        


   
       
   |
142 | 141 | negeq0d 9975 |
. . . . . . . . . . . . . 14
        


   
       
      |
143 | 139, 142 | mpbird 236 |
. . . . . . . . . . . . 13
        


   
       
   |
144 | 137, 143 | eqtr4d 2487 |
. . . . . . . . . . . 12
        


   
       
   |
145 | 136, 144 | mpdan 673 |
. . . . . . . . . . 11
       
     
     
    |
146 | 145 | ex 436 |
. . . . . . . . . 10
      
            

   |
147 | 146 | necon3d 2644 |
. . . . . . . . 9
      
                 |
148 | 147 | imp 431 |
. . . . . . . 8
       
     
          |
149 | 58, 15 | syl 17 |
. . . . . . . . . 10
       
     
      
  |
150 | 149 | znegcld 11039 |
. . . . . . . . 9
       
     
          |
151 | | rmyeq 35798 |
. . . . . . . . . 10
        

 Yrm   Yrm      |
152 | 151 | necon3bid 2667 |
. . . . . . . . 9
         
 Yrm   Yrm      |
153 | 1, 4, 150, 152 | syl3anc 1267 |
. . . . . . . 8
       
     
          Yrm   Yrm      |
154 | 148, 153 | mpbid 214 |
. . . . . . 7
       
     
       
Yrm  
Yrm     |
155 | | rmyneg 35770 |
. . . . . . . 8
        Yrm    
Yrm    |
156 | 1, 17, 155 | syl2anc 666 |
. . . . . . 7
       
     
       
Yrm     Yrm    |
157 | 154, 156 | neeqtrd 2692 |
. . . . . 6
       
     
       
Yrm   
Yrm    |
158 | 118, 123,
157 | 3jca 1187 |
. . . . 5
       
     
            
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     |
159 | 158 | ex 436 |
. . . 4
      
                   Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm      |
160 | | simplll 767 |
. . . . . . . . . . . . . 14
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm          |
161 | 3 | ad2antlr 732 |
. . . . . . . . . . . . . 14
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm      |
162 | 160, 161,
30 | syl2anc 666 |
. . . . . . . . . . . . 13
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     Yrm    |
163 | 162 | zcnd 11038 |
. . . . . . . . . . . 12
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     Yrm    |
164 | 16 | ad2antlr 732 |
. . . . . . . . . . . . . 14
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm      |
165 | 160, 164,
33 | syl2anc 666 |
. . . . . . . . . . . . 13
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     Yrm    |
166 | 165 | zcnd 11038 |
. . . . . . . . . . . 12
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     Yrm    |
167 | 163, 166 | negsubd 9989 |
. . . . . . . . . . 11
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     
Yrm    Yrm     Yrm   Yrm     |
168 | 167 | fveq2d 5867 |
. . . . . . . . . 10
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm    Yrm        
Yrm  
Yrm      |
169 | 166 | negcld 9970 |
. . . . . . . . . . . . 13
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm      Yrm    |
170 | 163, 169 | addcld 9659 |
. . . . . . . . . . . 12
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     
Yrm    Yrm     |
171 | 170 | abscld 13491 |
. . . . . . . . . . 11
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm    Yrm      |
172 | 163 | abscld 13491 |
. . . . . . . . . . . 12
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm        Yrm     |
173 | 166 | abscld 13491 |
. . . . . . . . . . . 12
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm        Yrm     |
174 | 172, 173 | readdcld 9667 |
. . . . . . . . . . 11
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm       Yrm      |
175 | | nnz 10956 |
. . . . . . . . . . . . . . 15
   |
176 | 175 | adantl 468 |
. . . . . . . . . . . . . 14
         |
177 | 176 | ad2antrr 731 |
. . . . . . . . . . . . 13
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm      |
178 | 49 | nn0zd 11035 |
. . . . . . . . . . . . 13
        Xrm    |
179 | 160, 177,
178 | syl2anc 666 |
. . . . . . . . . . . 12
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     Xrm    |
180 | 179 | zred 11037 |
. . . . . . . . . . 11
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     Xrm    |
181 | 163, 169 | abstrid 13511 |
. . . . . . . . . . . 12
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm    Yrm        
Yrm        Yrm      |
182 | | absneg 13333 |
. . . . . . . . . . . . . . 15
  Yrm       Yrm       Yrm     |
183 | 182 | eqcomd 2456 |
. . . . . . . . . . . . . 14
  Yrm      Yrm        Yrm     |
184 | 166, 183 | syl 17 |
. . . . . . . . . . . . 13
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm        Yrm        Yrm     |
185 | 184 | oveq2d 6304 |
. . . . . . . . . . . 12
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm       Yrm        
Yrm        Yrm      |
186 | 181, 185 | breqtrrd 4428 |
. . . . . . . . . . 11
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm    Yrm        
Yrm       Yrm      |
187 | | simpr1 1013 |
. . . . . . . . . . 11
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm       Yrm     Xrm    |
188 | 171, 174,
180, 186, 187 | lelttrd 9790 |
. . . . . . . . . 10
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm    Yrm     Xrm    |
189 | 168, 188 | eqbrtrrd 4424 |
. . . . . . . . 9
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm   Yrm    
Xrm    |
190 | 162, 165 | zsubcld 11042 |
. . . . . . . . . . . 12
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     
Yrm  
Yrm     |
191 | 190 | zcnd 11038 |
. . . . . . . . . . 11
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     
Yrm  
Yrm     |
192 | 191 | abscld 13491 |
. . . . . . . . . 10
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm   Yrm      |
193 | 192, 180 | ltnled 9779 |
. . . . . . . . 9
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         
Yrm  
Yrm     Xrm 
 Xrm 
     Yrm   Yrm       |
194 | 189, 193 | mpbid 214 |
. . . . . . . 8
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm    
Xrm      
Yrm  
Yrm      |
195 | | simpr2 1014 |
. . . . . . . . . 10
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     Yrm   Yrm    |
196 | 163, 166,
195 | subne0d 9992 |
. . . . . . . . 9
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     
Yrm  
Yrm     |
197 | | dvdsleabs 14344 |
. . . . . . . . 9
  
Xrm    Yrm   Yrm     Yrm   Yrm     
Xrm    Yrm   Yrm  
 Xrm 
     Yrm   Yrm       |
198 | 179, 190,
196, 197 | syl3anc 1267 |
. . . . . . . 8
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     
Xrm    Yrm   Yrm  
 Xrm 
     Yrm   Yrm       |
199 | 194, 198 | mtod 181 |
. . . . . . 7
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm    
Xrm    Yrm   Yrm     |
200 | 163, 166 | subnegd 9990 |
. . . . . . . . . . 11
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     
Yrm   
Yrm     Yrm   Yrm     |
201 | 200 | fveq2d 5867 |
. . . . . . . . . 10
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm    Yrm        
Yrm  
Yrm      |
202 | 163, 166 | addcld 9659 |
. . . . . . . . . . . 12
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     
Yrm  
Yrm     |
203 | 202 | abscld 13491 |
. . . . . . . . . . 11
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm   Yrm      |
204 | 163, 166 | abstrid 13511 |
. . . . . . . . . . 11
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm   Yrm         Yrm       Yrm      |
205 | 203, 174,
180, 204, 187 | lelttrd 9790 |
. . . . . . . . . 10
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm   Yrm    
Xrm    |
206 | 201, 205 | eqbrtrd 4422 |
. . . . . . . . 9
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm    Yrm     Xrm    |
207 | 165 | znegcld 11039 |
. . . . . . . . . . . . 13
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm      Yrm    |
208 | 162, 207 | zsubcld 11042 |
. . . . . . . . . . . 12
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     
Yrm   
Yrm     |
209 | 208 | zcnd 11038 |
. . . . . . . . . . 11
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     
Yrm   
Yrm     |
210 | 209 | abscld 13491 |
. . . . . . . . . 10
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         Yrm    Yrm      |
211 | 210, 180 | ltnled 9779 |
. . . . . . . . 9
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm         
Yrm   
Yrm     Xrm 
 Xrm 
     Yrm    Yrm       |
212 | 206, 211 | mpbid 214 |
. . . . . . . 8
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm    
Xrm      
Yrm   
Yrm      |
213 | | simpr3 1015 |
. . . . . . . . . 10
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     Yrm    Yrm    |
214 | 163, 169,
213 | subne0d 9992 |
. . . . . . . . 9
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     
Yrm   
Yrm     |
215 | | dvdsleabs 14344 |
. . . . . . . . 9
  
Xrm    Yrm    Yrm     Yrm    Yrm     
Xrm    Yrm    Yrm  
 Xrm 
     Yrm    Yrm       |
216 | 179, 208,
214, 215 | syl3anc 1267 |
. . . . . . . 8
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     
Xrm    Yrm    Yrm  
 Xrm 
     Yrm    Yrm       |
217 | 212, 216 | mtod 181 |
. . . . . . 7
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm    
Xrm    Yrm    Yrm     |
218 | 199, 217 | jca 535 |
. . . . . 6
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm     
Xrm    Yrm   Yrm    Xrm   
Yrm   
Yrm      |
219 | | pm4.56 498 |
. . . . . 6
   Xrm    Yrm   Yrm   
Xrm    Yrm    Yrm   
 
Xrm    Yrm   Yrm    Xrm    Yrm    Yrm      |
220 | 218, 219 | sylib 200 |
. . . . 5
       
     
           
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm      Xrm    Yrm   Yrm    Xrm   
Yrm   
Yrm      |
221 | 220 | ex 436 |
. . . 4
      
                  
Yrm       Yrm     Xrm   Yrm   Yrm   Yrm    Yrm  
 
Xrm    Yrm   Yrm    Xrm    Yrm    Yrm       |
222 | 159, 221 | syld 45 |
. . 3
      
               Xrm    Yrm   Yrm    Xrm   
Yrm   
Yrm       |
223 | 222 | necon4ad 2642 |
. 2
      
               Xrm    Yrm   Yrm    Xrm   
Yrm   
Yrm   
   |
224 | 223 | 3impia 1204 |
1
      
             Xrm   
Yrm  
Yrm    Xrm    Yrm    Yrm    
  |