Step | Hyp | Ref
| Expression |
1 | | 0xr 8035 |
. . . . . . . . 9
 |
2 | | 1re 7987 |
. . . . . . . . 9
 |
3 | | elioc2 9968 |
. . . . . . . . 9
   
  ![(,] (,]](_ioc.gif) 

    |
4 | 1, 2, 3 | mp2an 426 |
. . . . . . . 8
   ![(,] (,]](_ioc.gif) 

   |
5 | 4 | simp1bi 1014 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)    |
6 | | eqid 2189 |
. . . . . . . 8

                            |
7 | 6 | resin4p 11761 |
. . . . . . 7
                                             |
8 | 5, 7 | syl 14 |
. . . . . 6
   ![(,] (,]](_ioc.gif)                                              |
9 | 8 | eqcomd 2195 |
. . . . 5
   ![(,] (,]](_ioc.gif)                                              |
10 | 5 | resincld 11766 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)        |
11 | 10 | recnd 8017 |
. . . . . 6
   ![(,] (,]](_ioc.gif)        |
12 | | 3nn0 9225 |
. . . . . . . . . 10
 |
13 | | reexpcl 10571 |
. . . . . . . . . 10
 
       |
14 | 5, 12, 13 | sylancl 413 |
. . . . . . . . 9
   ![(,] (,]](_ioc.gif)        |
15 | | 6nn 9115 |
. . . . . . . . 9
 |
16 | | nndivre 8986 |
. . . . . . . . 9
     
         |
17 | 14, 15, 16 | sylancl 413 |
. . . . . . . 8
   ![(,] (,]](_ioc.gif)          |
18 | 5, 17 | resubcld 8369 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)  
         |
19 | 18 | recnd 8017 |
. . . . . 6
   ![(,] (,]](_ioc.gif)  
         |
20 | | ax-icn 7937 |
. . . . . . . . . 10
 |
21 | 5 | recnd 8017 |
. . . . . . . . . 10
   ![(,] (,]](_ioc.gif)    |
22 | | mulcl 7969 |
. . . . . . . . . 10
 
     |
23 | 20, 21, 22 | sylancr 414 |
. . . . . . . . 9
   ![(,] (,]](_ioc.gif)  
   |
24 | | 4nn0 9226 |
. . . . . . . . 9
 |
25 | 6 | eftlcl 11731 |
. . . . . . . . 9
   
                           |
26 | 23, 24, 25 | sylancl 413 |
. . . . . . . 8
   ![(,] (,]](_ioc.gif)                            |
27 | 26 | imcld 10983 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)                                |
28 | 27 | recnd 8017 |
. . . . . 6
   ![(,] (,]](_ioc.gif)                                |
29 | 11, 19, 28 | subaddd 8317 |
. . . . 5
   ![(,] (,]](_ioc.gif)                                                                                          |
30 | 9, 29 | mpbird 167 |
. . . 4
   ![(,] (,]](_ioc.gif)                                              |
31 | 30 | fveq2d 5538 |
. . 3
   ![(,] (,]](_ioc.gif)          
               
                           |
32 | 28 | abscld 11225 |
. . . 4
   ![(,] (,]](_ioc.gif)                                    |
33 | 26 | abscld 11225 |
. . . 4
   ![(,] (,]](_ioc.gif)                                |
34 | | absimle 11128 |
. . . . 5
 
                      
      
                        
                              |
35 | 26, 34 | syl 14 |
. . . 4
   ![(,] (,]](_ioc.gif)                                 
                              |
36 | | reexpcl 10571 |
. . . . . . 7
 
       |
37 | 5, 24, 36 | sylancl 413 |
. . . . . 6
   ![(,] (,]](_ioc.gif)        |
38 | | nndivre 8986 |
. . . . . 6
     
         |
39 | 37, 15, 38 | sylancl 413 |
. . . . 5
   ![(,] (,]](_ioc.gif)          |
40 | 6 | ef01bndlem 11799 |
. . . . 5
   ![(,] (,]](_ioc.gif)                                      |
41 | 12 | a1i 9 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)    |
42 | | 4z 9314 |
. . . . . . . . 9
 |
43 | | 3re 9024 |
. . . . . . . . . 10
 |
44 | | 4re 9027 |
. . . . . . . . . 10
 |
45 | | 3lt4 9122 |
. . . . . . . . . 10
 |
46 | 43, 44, 45 | ltleii 8091 |
. . . . . . . . 9
 |
47 | | 3z 9313 |
. . . . . . . . . 10
 |
48 | 47 | eluz1i 9566 |
. . . . . . . . 9
         |
49 | 42, 46, 48 | mpbir2an 944 |
. . . . . . . 8
     |
50 | 49 | a1i 9 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)        |
51 | 4 | simp2bi 1015 |
. . . . . . . 8
   ![(,] (,]](_ioc.gif)    |
52 | | 0re 7988 |
. . . . . . . . 9
 |
53 | | ltle 8076 |
. . . . . . . . 9
 
 
   |
54 | 52, 5, 53 | sylancr 414 |
. . . . . . . 8
   ![(,] (,]](_ioc.gif)  
   |
55 | 51, 54 | mpd 13 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)    |
56 | 4 | simp3bi 1016 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)    |
57 | 5, 41, 50, 55, 56 | leexp2rd 10718 |
. . . . . 6
   ![(,] (,]](_ioc.gif)            |
58 | | 6re 9031 |
. . . . . . . 8
 |
59 | 58 | a1i 9 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)    |
60 | | 6pos 9051 |
. . . . . . . 8
 |
61 | 60 | a1i 9 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)    |
62 | | lediv1 8857 |
. . . . . . 7
                                     |
63 | 37, 14, 59, 61, 62 | syl112anc 1253 |
. . . . . 6
   ![(,] (,]](_ioc.gif)      
   
               |
64 | 57, 63 | mpbid 147 |
. . . . 5
   ![(,] (,]](_ioc.gif)                |
65 | 33, 39, 17, 40, 64 | ltletrd 8411 |
. . . 4
   ![(,] (,]](_ioc.gif)                                      |
66 | 32, 33, 17, 35, 65 | lelttrd 8113 |
. . 3
   ![(,] (,]](_ioc.gif)                                          |
67 | 31, 66 | eqbrtrd 4040 |
. 2
   ![(,] (,]](_ioc.gif)          
                 |
68 | 10, 18, 17 | absdifltd 11222 |
. . 3
   ![(,] (,]](_ioc.gif)                          
                    
                        |
69 | 17 | recnd 8017 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)          |
70 | 21, 69, 69 | subsub4d 8330 |
. . . . . 6
   ![(,] (,]](_ioc.gif)                                    |
71 | 14 | recnd 8017 |
. . . . . . . . . . 11
   ![(,] (,]](_ioc.gif)        |
72 | | 3cn 9025 |
. . . . . . . . . . . . 13
 |
73 | | 3ap0 9046 |
. . . . . . . . . . . . 13
#  |
74 | 72, 73 | pm3.2i 272 |
. . . . . . . . . . . 12
 #   |
75 | | 2cn 9021 |
. . . . . . . . . . . . 13
 |
76 | | 2ap0 9043 |
. . . . . . . . . . . . 13
#  |
77 | 75, 76 | pm3.2i 272 |
. . . . . . . . . . . 12
 #   |
78 | | divdivap1 8711 |
. . . . . . . . . . . 12
       #   #                     |
79 | 74, 77, 78 | mp3an23 1340 |
. . . . . . . . . . 11
                       |
80 | 71, 79 | syl 14 |
. . . . . . . . . 10
   ![(,] (,]](_ioc.gif)                    |
81 | | 3t2e6 9106 |
. . . . . . . . . . 11
   |
82 | 81 | oveq2i 5908 |
. . . . . . . . . 10
               |
83 | 80, 82 | eqtr2di 2239 |
. . . . . . . . 9
   ![(,] (,]](_ioc.gif)                  |
84 | 83, 83 | oveq12d 5915 |
. . . . . . . 8
   ![(,] (,]](_ioc.gif)                                    |
85 | | 3nn 9112 |
. . . . . . . . . . 11
 |
86 | | nndivre 8986 |
. . . . . . . . . . 11
     
         |
87 | 14, 85, 86 | sylancl 413 |
. . . . . . . . . 10
   ![(,] (,]](_ioc.gif)          |
88 | 87 | recnd 8017 |
. . . . . . . . 9
   ![(,] (,]](_ioc.gif)          |
89 | 88 | 2halvesd 9195 |
. . . . . . . 8
   ![(,] (,]](_ioc.gif)                            |
90 | 84, 89 | eqtrd 2222 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)                        |
91 | 90 | oveq2d 5913 |
. . . . . 6
   ![(,] (,]](_ioc.gif)  
                         |
92 | 70, 91 | eqtrd 2222 |
. . . . 5
   ![(,] (,]](_ioc.gif)                            |
93 | 92 | breq1d 4028 |
. . . 4
   ![(,] (,]](_ioc.gif)                      
               |
94 | 21, 69 | npcand 8303 |
. . . . 5
   ![(,] (,]](_ioc.gif)                    |
95 | 94 | breq2d 4030 |
. . . 4
   ![(,] (,]](_ioc.gif)      
 
             
       |
96 | 93, 95 | anbi12d 473 |
. . 3
   ![(,] (,]](_ioc.gif)                                            
 
          
        |
97 | 68, 96 | bitrd 188 |
. 2
   ![(,] (,]](_ioc.gif)                          
 
          
        |
98 | 67, 97 | mpbid 147 |
1
   ![(,] (,]](_ioc.gif)                      |