Proof of Theorem xlemul1a
Step | Hyp | Ref
| Expression |
1 | | 0xr 9684 |
. . . . . 6
 |
2 | | simpr 463 |
. . . . . 6
   
   |
3 | | xrleloe 11440 |
. . . . . 6
   
     |
4 | 1, 2, 3 | sylancr 668 |
. . . . 5
   
  
    |
5 | | simpllr 768 |
. . . . . . . . . . . 12
    
  
    
  |
6 | | elxr 11413 |
. . . . . . . . . . . 12

    |
7 | 5, 6 | sylib 200 |
. . . . . . . . . . 11
    
  
     
   |
8 | | simplrr 770 |
. . . . . . . . . . . . . . 15
    
  
         |
9 | | simprll 771 |
. . . . . . . . . . . . . . . 16
    
  
      
  |
10 | | simprlr 772 |
. . . . . . . . . . . . . . . 16
    
  
      
  |
11 | | simprr 765 |
. . . . . . . . . . . . . . . 16
    
  
      
  |
12 | | simplrl 769 |
. . . . . . . . . . . . . . . 16
    
  
      
  |
13 | | lemul1 10454 |
. . . . . . . . . . . . . . . 16
 

          |
14 | 9, 10, 11, 12, 13 | syl112anc 1271 |
. . . . . . . . . . . . . . 15
    
  
               |
15 | 8, 14 | mpbid 214 |
. . . . . . . . . . . . . 14
    
  
        
    |
16 | | rexmul 11554 |
. . . . . . . . . . . . . . 15
 
          |
17 | 9, 11, 16 | syl2anc 666 |
. . . . . . . . . . . . . 14
    
  
                |
18 | | rexmul 11554 |
. . . . . . . . . . . . . . 15
 
          |
19 | 10, 11, 18 | syl2anc 666 |
. . . . . . . . . . . . . 14
    
  
                |
20 | 15, 17, 19 | 3brtr4d 4432 |
. . . . . . . . . . . . 13
    
  
                   |
21 | 20 | expr 619 |
. . . . . . . . . . . 12
    
  
                   |
22 | | simprl 763 |
. . . . . . . . . . . . . . 15
    
  
    
  |
23 | | 0re 9640 |
. . . . . . . . . . . . . . 15
 |
24 | | lttri4 9715 |
. . . . . . . . . . . . . . 15
 
 
   |
25 | 22, 23, 24 | sylancl 667 |
. . . . . . . . . . . . . 14
    
  
     
   |
26 | | simplll 767 |
. . . . . . . . . . . . . . . . . . 19
   
  
    |
27 | 26 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
    
  
    
  |
28 | | xmulpnf1n 11561 |
. . . . . . . . . . . . . . . . . 18
         |
29 | 27, 28 | sylan 474 |
. . . . . . . . . . . . . . . . 17
        
            |
30 | | simpllr 768 |
. . . . . . . . . . . . . . . . . . . . 21
   
  
    |
31 | 30 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
    
  
    
  |
32 | 31 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
        
     
  |
33 | | pnfxr 11409 |
. . . . . . . . . . . . . . . . . . 19
 |
34 | | xmulcl 11556 |
. . . . . . . . . . . . . . . . . . 19
         |
35 | 32, 33, 34 | sylancl 667 |
. . . . . . . . . . . . . . . . . 18
        
            |
36 | | mnfle 11432 |
. . . . . . . . . . . . . . . . . 18
    
      |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
        
            |
38 | 29, 37 | eqbrtrd 4422 |
. . . . . . . . . . . . . . . 16
        
                |
39 | 38 | ex 436 |
. . . . . . . . . . . . . . 15
    
  
                 |
40 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . 19
           |
41 | | xmul02 11551 |
. . . . . . . . . . . . . . . . . . . 20
      |
42 | 33, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
     |
43 | 40, 42 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . 18
       |
44 | 43 | adantl 468 |
. . . . . . . . . . . . . . . . 17
        
    
       |
45 | | simplrr 770 |
. . . . . . . . . . . . . . . . . . . . 21
    
  
       |
46 | | breq1 4404 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
47 | 45, 46 | syl5ibcom 224 |
. . . . . . . . . . . . . . . . . . . 20
    
  
         |
48 | | simprr 765 |
. . . . . . . . . . . . . . . . . . . . 21
    
  
    
  |
49 | | leloe 9717 |
. . . . . . . . . . . . . . . . . . . . 21
 
  
    |
50 | 23, 48, 49 | sylancr 668 |
. . . . . . . . . . . . . . . . . . . 20
    
  
      
    |
51 | 47, 50 | sylibd 218 |
. . . . . . . . . . . . . . . . . . 19
    
  
           |
52 | 51 | imp 431 |
. . . . . . . . . . . . . . . . . 18
        
    
     |
53 | | pnfge 11429 |
. . . . . . . . . . . . . . . . . . . . 21

  |
54 | 1, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
 |
55 | | xmulpnf1 11557 |
. . . . . . . . . . . . . . . . . . . . 21
         |
56 | 31, 55 | sylan 474 |
. . . . . . . . . . . . . . . . . . . 20
        
            |
57 | 54, 56 | syl5breqr 4438 |
. . . . . . . . . . . . . . . . . . 19
        
     
  
   |
58 | | xrleid 11446 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
59 | 1, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
 |
60 | 59, 42 | breqtrri 4427 |
. . . . . . . . . . . . . . . . . . . 20
     |
61 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . 21
        
    
   |
62 | 61 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . . . 20
        
    
           |
63 | 60, 62 | syl5breq 4437 |
. . . . . . . . . . . . . . . . . . 19
        
    

  
   |
64 | 57, 63 | jaodan 793 |
. . . . . . . . . . . . . . . . . 18
        
     
        |
65 | 52, 64 | syldan 473 |
. . . . . . . . . . . . . . . . 17
        
    
       |
66 | 44, 65 | eqbrtrd 4422 |
. . . . . . . . . . . . . . . 16
        
    
           |
67 | 66 | ex 436 |
. . . . . . . . . . . . . . 15
    
  
                 |
68 | | pnfge 11429 |
. . . . . . . . . . . . . . . . . 18
  |
69 | 33, 68 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
 |
70 | 26 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
    
  
      
  |
71 | | simprr 765 |
. . . . . . . . . . . . . . . . . . 19
    
  
      
  |
72 | | xmulpnf1 11557 |
. . . . . . . . . . . . . . . . . . 19
         |
73 | 70, 71, 72 | syl2anc 666 |
. . . . . . . . . . . . . . . . . 18
    
  
             |
74 | 30 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
    
  
      
  |
75 | | ltletr 9722 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
  
    |
76 | 23, 75 | mp3an1 1350 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  

   |
77 | 76 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
    
  
      

   |
78 | 45, 77 | mpan2d 679 |
. . . . . . . . . . . . . . . . . . . 20
    
  
         |
79 | 78 | impr 624 |
. . . . . . . . . . . . . . . . . . 19
    
  
      
  |
80 | 74, 79, 55 | syl2anc 666 |
. . . . . . . . . . . . . . . . . 18
    
  
             |
81 | 73, 80 | breq12d 4414 |
. . . . . . . . . . . . . . . . 17
    
  
               
   |
82 | 69, 81 | mpbiri 237 |
. . . . . . . . . . . . . . . 16
    
  
                 |
83 | 82 | expr 619 |
. . . . . . . . . . . . . . 15
    
  
                 |
84 | 39, 67, 83 | 3jaod 1331 |
. . . . . . . . . . . . . 14
    
  
                   |
85 | 25, 84 | mpd 15 |
. . . . . . . . . . . . 13
    
  
               |
86 | | oveq2 6296 |
. . . . . . . . . . . . . 14
            |
87 | | oveq2 6296 |
. . . . . . . . . . . . . 14
            |
88 | 86, 87 | breq12d 4414 |
. . . . . . . . . . . . 13
                       |
89 | 85, 88 | syl5ibrcom 226 |
. . . . . . . . . . . 12
    
  
                   |
90 | | nltmnf 11428 |
. . . . . . . . . . . . . . . . . 18

  |
91 | 1, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
 |
92 | | breq2 4405 |
. . . . . . . . . . . . . . . . 17
 
   |
93 | 91, 92 | mtbiri 305 |
. . . . . . . . . . . . . . . 16
   |
94 | 93 | con2i 124 |
. . . . . . . . . . . . . . 15

  |
95 | 94 | ad2antrl 733 |
. . . . . . . . . . . . . 14
   
  
 
  |
96 | 95 | adantr 467 |
. . . . . . . . . . . . 13
    
  
    
  |
97 | 96 | pm2.21d 110 |
. . . . . . . . . . . 12
    
  
                   |
98 | 21, 89, 97 | 3jaod 1331 |
. . . . . . . . . . 11
    
  
                     |
99 | 7, 98 | mpd 15 |
. . . . . . . . . 10
    
  
                 |
100 | 99 | anassrs 653 |
. . . . . . . . 9
        
                |
101 | | xmulcl 11556 |
. . . . . . . . . . . . . 14
          |
102 | 101 | adantlr 720 |
. . . . . . . . . . . . 13
   
        |
103 | 102 | ad2antrr 731 |
. . . . . . . . . . . 12
    
  
          |
104 | | pnfge 11429 |
. . . . . . . . . . . 12
          
  |
105 | 103, 104 | syl 17 |
. . . . . . . . . . 11
    
  
          |
106 | | oveq1 6295 |
. . . . . . . . . . . 12
            |
107 | | xmulpnf2 11558 |
. . . . . . . . . . . . 13
         |
108 | 107 | ad2ant2lr 753 |
. . . . . . . . . . . 12
   
  
        |
109 | 106, 108 | sylan9eqr 2506 |
. . . . . . . . . . 11
    
  
          |
110 | 105, 109 | breqtrrd 4428 |
. . . . . . . . . 10
    
  
               |
111 | 110 | adantlr 720 |
. . . . . . . . 9
        
                |
112 | | simplrr 770 |
. . . . . . . . . . . . 13
    
  
     |
113 | | simpr 463 |
. . . . . . . . . . . . . 14
    
  
     |
114 | 26 | adantr 467 |
. . . . . . . . . . . . . . 15
    
  
     |
115 | | mnfle 11432 |
. . . . . . . . . . . . . . 15

  |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . 14
    
  
  
  |
117 | 113, 116 | eqbrtrd 4422 |
. . . . . . . . . . . . 13
    
  
     |
118 | | xrletri3 11448 |
. . . . . . . . . . . . . 14
   
     |
119 | 118 | ad3antrrr 735 |
. . . . . . . . . . . . 13
    
  
         |
120 | 112, 117,
119 | mpbir2and 932 |
. . . . . . . . . . . 12
    
  
     |
121 | 120 | oveq1d 6303 |
. . . . . . . . . . 11
    
  
               |
122 | | xmulcl 11556 |
. . . . . . . . . . . . . 14
          |
123 | 122 | adantll 719 |
. . . . . . . . . . . . 13
   
        |
124 | 123 | ad2antrr 731 |
. . . . . . . . . . . 12
    
  
          |
125 | | xrleid 11446 |
. . . . . . . . . . . 12
          
       |
126 | 124, 125 | syl 17 |
. . . . . . . . . . 11
    
  
               |
127 | 121, 126 | eqbrtrd 4422 |
. . . . . . . . . 10
    
  
               |
128 | 127 | adantlr 720 |
. . . . . . . . 9
        
                |
129 | | elxr 11413 |
. . . . . . . . . . 11

    |
130 | 30, 129 | sylib 200 |
. . . . . . . . . 10
   
  
      |
131 | 130 | adantr 467 |
. . . . . . . . 9
    
  
       |
132 | 100, 111,
128, 131 | mpjao3dan 1334 |
. . . . . . . 8
    
  
               |
133 | | simplrr 770 |
. . . . . . . . . . 11
    
  
     |
134 | 30 | adantr 467 |
. . . . . . . . . . . . 13
    
  
     |
135 | | pnfge 11429 |
. . . . . . . . . . . . 13

  |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . 12
    
  
     |
137 | | simpr 463 |
. . . . . . . . . . . 12
    
  
     |
138 | 136, 137 | breqtrrd 4428 |
. . . . . . . . . . 11
    
  
     |
139 | 118 | ad3antrrr 735 |
. . . . . . . . . . 11
    
  
         |
140 | 133, 138,
139 | mpbir2and 932 |
. . . . . . . . . 10
    
  
     |
141 | 140 | oveq1d 6303 |
. . . . . . . . 9
    
  
               |
142 | 123, 125 | syl 17 |
. . . . . . . . . 10
   
             |
143 | 142 | ad2antrr 731 |
. . . . . . . . 9
    
  
               |
144 | 141, 143 | eqbrtrd 4422 |
. . . . . . . 8
    
  
               |
145 | | oveq1 6295 |
. . . . . . . . . 10
            |
146 | | xmulmnf2 11560 |
. . . . . . . . . . 11
         |
147 | 146 | ad2ant2lr 753 |
. . . . . . . . . 10
   
  
        |
148 | 145, 147 | sylan9eqr 2506 |
. . . . . . . . 9
    
  
          |
149 | 123 | ad2antrr 731 |
. . . . . . . . . 10
    
  
          |
150 | | mnfle 11432 |
. . . . . . . . . 10
             |
151 | 149, 150 | syl 17 |
. . . . . . . . 9
    
  
  
       |
152 | 148, 151 | eqbrtrd 4422 |
. . . . . . . 8
    
  
               |
153 | | elxr 11413 |
. . . . . . . . 9

    |
154 | 26, 153 | sylib 200 |
. . . . . . . 8
   
  
      |
155 | 132, 144,
152, 154 | mpjao3dan 1334 |
. . . . . . 7
   
  
              |
156 | 155 | exp32 609 |
. . . . . 6
   
                 |
157 | | xmul01 11550 |
. . . . . . . . . . 11

       |
158 | 157 | ad2antrr 731 |
. . . . . . . . . 10
   
        |
159 | | xmul01 11550 |
. . . . . . . . . . 11

       |
160 | 159 | ad2antlr 732 |
. . . . . . . . . 10
   
        |
161 | 158, 160 | breq12d 4414 |
. . . . . . . . 9
   
           
   |
162 | 59, 161 | mpbiri 237 |
. . . . . . . 8
   
             |
163 | | oveq2 6296 |
. . . . . . . . 9
             |
164 | | oveq2 6296 |
. . . . . . . . 9
             |
165 | 163, 164 | breq12d 4414 |
. . . . . . . 8
                         |
166 | 162, 165 | syl5ibcom 224 |
. . . . . . 7
   
               |
167 | 166 | a1dd 47 |
. . . . . 6
   
                 |
168 | 156, 167 | jaod 382 |
. . . . 5
   
                   |
169 | 4, 168 | sylbid 219 |
. . . 4
   
                 |
170 | 169 | expimpd 607 |
. . 3
    
                |
171 | 170 | 3impia 1204 |
. 2
  
                |
172 | 171 | imp 431 |
1
   
               |