Proof of Theorem jm2.24nn
Step | Hyp | Ref
| Expression |
1 | | nnz 10259 |
. . . . . 6
   |
2 | | 1z 10267 |
. . . . . 6
 |
3 | | zsubcl 10275 |
. . . . . 6
 
     |
4 | 1, 2, 3 | sylancl 644 |
. . . . 5
 
   |
5 | | frmy 26867 |
. . . . . 6
Yrm
          |
6 | 5 | fovcl 6134 |
. . . . 5
      
  
Yrm      |
7 | 4, 6 | sylan2 461 |
. . . 4
        Yrm      |
8 | 7 | zred 10331 |
. . 3
        Yrm      |
9 | 5 | fovcl 6134 |
. . . . 5
        Yrm    |
10 | 1, 9 | sylan2 461 |
. . . 4
        Yrm    |
11 | 10 | zred 10331 |
. . 3
        Yrm    |
12 | 8, 11 | readdcld 9071 |
. 2
        
Yrm    
Yrm     |
13 | | 2re 10025 |
. . . 4
 |
14 | | remulcl 9031 |
. . . 4
  
Yrm     Yrm     |
15 | 13, 11, 14 | sylancr 645 |
. . 3
         Yrm     |
16 | 15, 8 | resubcld 9421 |
. 2
          Yrm   
Yrm       |
17 | | frmx 26866 |
. . . . 5
Xrm
          |
18 | 17 | fovcl 6134 |
. . . 4
        Xrm    |
19 | 1, 18 | sylan2 461 |
. . 3
        Xrm    |
20 | 19 | nn0red 10231 |
. 2
        Xrm    |
21 | 11, 8 | resubcld 9421 |
. . . 4
        
Yrm  
Yrm       |
22 | | remulcl 9031 |
. . . . . . . 8
  
Yrm       Yrm       |
23 | 13, 8, 22 | sylancr 645 |
. . . . . . 7
         Yrm       |
24 | | eluzelre 10453 |
. . . . . . . . 9
    
  |
25 | 24 | adantr 452 |
. . . . . . . 8
         |
26 | 25, 8 | remulcld 9072 |
. . . . . . 7
       
 Yrm       |
27 | 8, 25 | remulcld 9072 |
. . . . . . . 8
        
Yrm       |
28 | 17 | fovcl 6134 |
. . . . . . . . . 10
      
  
Xrm      |
29 | 4, 28 | sylan2 461 |
. . . . . . . . 9
        Xrm      |
30 | 29 | nn0red 10231 |
. . . . . . . 8
        Xrm      |
31 | 27, 30 | readdcld 9071 |
. . . . . . 7
          Yrm     
Xrm       |
32 | 13 | a1i 11 |
. . . . . . . 8
         |
33 | | nnm1nn0 10217 |
. . . . . . . . 9
 
   |
34 | | rmxypos 26902 |
. . . . . . . . . 10
      
    Xrm    
Yrm       |
35 | 34 | simprd 450 |
. . . . . . . . 9
      
 
 Yrm      |
36 | 33, 35 | sylan2 461 |
. . . . . . . 8
       
Yrm      |
37 | | eluzle 10454 |
. . . . . . . . 9
    
  |
38 | 37 | adantr 452 |
. . . . . . . 8
         |
39 | 32, 25, 8, 36, 38 | lemul1ad 9906 |
. . . . . . 7
         Yrm     
 Yrm       |
40 | 25 | recnd 9070 |
. . . . . . . . 9
         |
41 | 8 | recnd 9070 |
. . . . . . . . 9
        Yrm      |
42 | 40, 41 | mulcomd 9065 |
. . . . . . . 8
       
 Yrm      
Yrm       |
43 | 34 | simpld 446 |
. . . . . . . . . 10
      
 
 Xrm      |
44 | 33, 43 | sylan2 461 |
. . . . . . . . 9
       
Xrm      |
45 | 30, 27 | ltaddposd 9566 |
. . . . . . . . 9
       
 Xrm      Yrm        Yrm      Xrm        |
46 | 44, 45 | mpbid 202 |
. . . . . . . 8
        
Yrm        Yrm     
Xrm       |
47 | 42, 46 | eqbrtrd 4192 |
. . . . . . 7
       
 Yrm        Yrm     
Xrm       |
48 | 23, 26, 31, 39, 47 | lelttrd 9184 |
. . . . . 6
         Yrm        Yrm     
Xrm       |
49 | 41 | 2timesd 10166 |
. . . . . 6
         Yrm      
Yrm    
Yrm       |
50 | | rmyp1 26886 |
. . . . . . . 8
      
  
Yrm         Yrm      Xrm       |
51 | 4, 50 | sylan2 461 |
. . . . . . 7
        Yrm         Yrm     
Xrm       |
52 | | nnre 9963 |
. . . . . . . . . . 11
   |
53 | 52 | adantl 453 |
. . . . . . . . . 10
         |
54 | 53 | recnd 9070 |
. . . . . . . . 9
         |
55 | | ax-1cn 9004 |
. . . . . . . . 9
 |
56 | | npcan 9270 |
. . . . . . . . 9
 
       |
57 | 54, 55, 56 | sylancl 644 |
. . . . . . . 8
             |
58 | 57 | oveq2d 6056 |
. . . . . . 7
        Yrm       Yrm    |
59 | 51, 58 | eqtr3d 2438 |
. . . . . 6
          Yrm     
Xrm      Yrm    |
60 | 48, 49, 59 | 3brtr3d 4201 |
. . . . 5
        
Yrm    
Yrm      Yrm    |
61 | 8, 8, 11 | ltaddsubd 9582 |
. . . . 5
          Yrm     Yrm      Yrm   Yrm      Yrm   Yrm        |
62 | 60, 61 | mpbid 202 |
. . . 4
        Yrm     
Yrm  
Yrm       |
63 | 8, 21, 11, 62 | ltadd1dd 9593 |
. . 3
        
Yrm    
Yrm      Yrm   Yrm     
Yrm     |
64 | 11 | recnd 9070 |
. . . . . 6
        Yrm    |
65 | 64 | 2timesd 10166 |
. . . . 5
         Yrm    
Yrm  
Yrm     |
66 | 65 | oveq1d 6055 |
. . . 4
          Yrm   
Yrm        Yrm   Yrm   
Yrm       |
67 | 64, 64, 41 | addsubd 9388 |
. . . 4
          Yrm   Yrm    Yrm        Yrm   Yrm      Yrm     |
68 | 66, 67 | eqtrd 2436 |
. . 3
          Yrm   
Yrm        Yrm   Yrm     
Yrm     |
69 | 63, 68 | breqtrrd 4198 |
. 2
        
Yrm    
Yrm      Yrm    Yrm       |
70 | 25, 11 | remulcld 9072 |
. . . 4
       
 Yrm     |
71 | | rmy0 26882 |
. . . . . . . 8
    
 Yrm    |
72 | 71 | adantr 452 |
. . . . . . 7
        Yrm    |
73 | | nngt0 9985 |
. . . . . . . . 9
   |
74 | 73 | adantl 453 |
. . . . . . . 8
         |
75 | | simpl 444 |
. . . . . . . . 9
             |
76 | | 0z 10249 |
. . . . . . . . . 10
 |
77 | 76 | a1i 11 |
. . . . . . . . 9
         |
78 | 1 | adantl 453 |
. . . . . . . . 9
         |
79 | | ltrmy 26907 |
. . . . . . . . 9
       
 Yrm   Yrm     |
80 | 75, 77, 78, 79 | syl3anc 1184 |
. . . . . . . 8
       
 Yrm   Yrm     |
81 | 74, 80 | mpbid 202 |
. . . . . . 7
        Yrm   Yrm    |
82 | 72, 81 | eqbrtrrd 4194 |
. . . . . 6
       
Yrm    |
83 | | lemul1 9818 |
. . . . . 6
 
 
Yrm  
Yrm   

  Yrm  
 
Yrm      |
84 | 32, 25, 11, 82, 83 | syl112anc 1188 |
. . . . 5
       
  Yrm  
 
Yrm      |
85 | 38, 84 | mpbid 202 |
. . . 4
         Yrm   
 Yrm     |
86 | 15, 70, 8, 85 | lesub1dd 9598 |
. . 3
          Yrm   
Yrm        Yrm    Yrm       |
87 | | rmym1 26888 |
. . . . . 6
        Yrm       Yrm   
Xrm     |
88 | 1, 87 | sylan2 461 |
. . . . 5
        Yrm       Yrm   
Xrm     |
89 | 64, 40 | mulcomd 9065 |
. . . . . 6
        
Yrm     Yrm     |
90 | 89 | oveq1d 6055 |
. . . . 5
          Yrm   
Xrm      Yrm    Xrm     |
91 | 88, 90 | eqtr2d 2437 |
. . . 4
          Yrm   
Xrm    Yrm      |
92 | 70 | recnd 9070 |
. . . . 5
       
 Yrm     |
93 | 20 | recnd 9070 |
. . . . 5
        Xrm    |
94 | | subsub23 9266 |
. . . . 5
    Yrm    Xrm  
Yrm        
Yrm    Xrm    Yrm       Yrm    Yrm      Xrm     |
95 | 92, 93, 41, 94 | syl3anc 1184 |
. . . 4
          
Yrm    Xrm    Yrm       Yrm    Yrm      Xrm     |
96 | 91, 95 | mpbid 202 |
. . 3
          Yrm   
Yrm      Xrm    |
97 | 86, 96 | breqtrd 4196 |
. 2
          Yrm   
Yrm      Xrm    |
98 | 12, 16, 20, 69, 97 | ltletrd 9186 |
1
        
Yrm    
Yrm    Xrm    |