Step | Hyp | Ref
| Expression |
1 | | reccn2ap.t |
. . 3
inf                    |
2 | | 1red 7971 |
. . . . . 6
  #

  |
3 | | simp1 997 |
. . . . . . . . 9
  #

  |
4 | | simp2 998 |
. . . . . . . . 9
  #

#   |
5 | 3, 4 | absrpclapd 11196 |
. . . . . . . 8
  #

      |
6 | | simp3 999 |
. . . . . . . 8
  #

  |
7 | 5, 6 | rpmulcld 9712 |
. . . . . . 7
  #

        |
8 | 7 | rpred 9695 |
. . . . . 6
  #

        |
9 | | mincl 11238 |
. . . . . 6
         inf              |
10 | 2, 8, 9 | syl2anc 411 |
. . . . 5
  #

inf              |
11 | 7 | rpgt0d 9698 |
. . . . . . 7
  #

        |
12 | | 0lt1 8083 |
. . . . . . 7
 |
13 | 11, 12 | jctil 312 |
. . . . . 6
  #

          |
14 | | 0red 7957 |
. . . . . . 7
  #

  |
15 | | ltmininf 11242 |
. . . . . . 7
 
        inf                       |
16 | 14, 2, 8, 15 | syl3anc 1238 |
. . . . . 6
  #

 inf           
           |
17 | 13, 16 | mpbird 167 |
. . . . 5
  #

inf              |
18 | 10, 17 | elrpd 9692 |
. . . 4
  #

inf              |
19 | 5 | rphalfcld 9708 |
. . . 4
  #

        |
20 | 18, 19 | rpmulcld 9712 |
. . 3
  #

inf                     |
21 | 1, 20 | eqeltrid 2264 |
. 2
  #

  |
22 | 3 | adantr 276 |
. . . . . . . . 9
   #    #            |
23 | | simprl 529 |
. . . . . . . . . . 11
   #    #           #
   |
24 | | breq1 4006 |
. . . . . . . . . . . 12
  #
#    |
25 | 24 | elrab 2893 |
. . . . . . . . . . 11
  #   #    |
26 | 23, 25 | sylib 122 |
. . . . . . . . . 10
   #    #           #    |
27 | 26 | simpld 112 |
. . . . . . . . 9
   #    #            |
28 | 22, 27 | mulcld 7977 |
. . . . . . . . 9
   #    #          
   |
29 | 4 | adantr 276 |
. . . . . . . . . 10
   #    #          #   |
30 | 26 | simprd 114 |
. . . . . . . . . 10
   #    #          #   |
31 | 22, 27, 29, 30 | mulap0d 8614 |
. . . . . . . . 9
   #    #          
 #   |
32 | 22, 27, 28, 31 | divsubdirapd 8786 |
. . . . . . . 8
   #    #                      
     |
33 | 22 | mulridd 7973 |
. . . . . . . . . . 11
   #    #          
   |
34 | 33 | oveq1d 5889 |
. . . . . . . . . 10
   #    #                      |
35 | | 1cnd 7972 |
. . . . . . . . . . 11
   #    #            |
36 | 35, 27, 22, 30, 29 | divcanap5d 8773 |
. . . . . . . . . 10
   #    #                    |
37 | 34, 36 | eqtr3d 2212 |
. . . . . . . . 9
   #    #                  |
38 | 27 | mulridd 7973 |
. . . . . . . . . . 11
   #    #              |
39 | 27, 22 | mulcomd 7978 |
. . . . . . . . . . 11
   #    #                |
40 | 38, 39 | oveq12d 5892 |
. . . . . . . . . 10
   #    #                      |
41 | 35, 22, 27, 29, 30 | divcanap5d 8773 |
. . . . . . . . . 10
   #    #                    |
42 | 40, 41 | eqtr3d 2212 |
. . . . . . . . 9
   #    #                  |
43 | 37, 42 | oveq12d 5892 |
. . . . . . . 8
   #    #            
               |
44 | 32, 43 | eqtrd 2210 |
. . . . . . 7
   #    #                        |
45 | 44 | fveq2d 5519 |
. . . . . 6
   #    #                                |
46 | 22, 27 | subcld 8267 |
. . . . . . 7
   #    #          
   |
47 | 46, 28, 31 | absdivapd 11203 |
. . . . . 6
   #    #                        
           |
48 | 45, 47 | eqtr3d 2212 |
. . . . 5
   #    #                        
           |
49 | 46 | abscld 11189 |
. . . . . . 7
   #    #                  |
50 | 21 | adantr 276 |
. . . . . . . 8
   #    #            |
51 | 50 | rpred 9695 |
. . . . . . 7
   #    #            |
52 | 28 | abscld 11189 |
. . . . . . . 8
   #    #                  |
53 | 6 | rpred 9695 |
. . . . . . . . 9
  #

  |
54 | 53 | adantr 276 |
. . . . . . . 8
   #    #            |
55 | 52, 54 | remulcld 7987 |
. . . . . . 7
   #    #              
     |
56 | 22, 27 | abssubd 11201 |
. . . . . . . 8
   #    #                        |
57 | | simprr 531 |
. . . . . . . 8
   #    #                  |
58 | 56, 57 | eqbrtrd 4025 |
. . . . . . 7
   #    #                  |
59 | 7 | adantr 276 |
. . . . . . . . . 10
   #    #                  |
60 | 59 | rpred 9695 |
. . . . . . . . 9
   #    #                  |
61 | 19 | adantr 276 |
. . . . . . . . . 10
   #    #                  |
62 | 61 | rpred 9695 |
. . . . . . . . 9
   #    #                  |
63 | 60, 62 | remulcld 7987 |
. . . . . . . 8
   #    #                          |
64 | | 1re 7955 |
. . . . . . . . . . 11
 |
65 | | min2inf 11240 |
. . . . . . . . . . 11
         inf           
        |
66 | 64, 60, 65 | sylancr 414 |
. . . . . . . . . 10
   #    #          inf                    |
67 | 10 | adantr 276 |
. . . . . . . . . . 11
   #    #          inf              |
68 | 67, 60, 61 | lemul1d 9739 |
. . . . . . . . . 10
   #    #          inf           
     
inf                                    |
69 | 66, 68 | mpbid 147 |
. . . . . . . . 9
   #    #          inf                                   |
70 | 1, 69 | eqbrtrid 4038 |
. . . . . . . 8
   #    #                          |
71 | 27 | abscld 11189 |
. . . . . . . . . 10
   #    #                |
72 | 22 | abscld 11189 |
. . . . . . . . . . . . . 14
   #    #                |
73 | 72 | recnd 7985 |
. . . . . . . . . . . . 13
   #    #                |
74 | 73 | 2halvesd 9163 |
. . . . . . . . . . . 12
   #    #                              |
75 | 72, 71 | resubcld 8337 |
. . . . . . . . . . . . . 14
   #    #                      |
76 | 27, 22 | subcld 8267 |
. . . . . . . . . . . . . . . 16
   #    #              |
77 | 76 | abscld 11189 |
. . . . . . . . . . . . . . 15
   #    #                  |
78 | 56, 77 | eqeltrd 2254 |
. . . . . . . . . . . . . 14
   #    #                  |
79 | 22, 27 | abs2difd 11205 |
. . . . . . . . . . . . . 14
   #    #                       
    |
80 | | min1inf 11239 |
. . . . . . . . . . . . . . . . . . 19
         inf           
  |
81 | 64, 60, 80 | sylancr 414 |
. . . . . . . . . . . . . . . . . 18
   #    #          inf              |
82 | | 1red 7971 |
. . . . . . . . . . . . . . . . . . 19
   #    #            |
83 | 67, 82, 61 | lemul1d 9739 |
. . . . . . . . . . . . . . . . . 18
   #    #          inf           
inf                              |
84 | 81, 83 | mpbid 147 |
. . . . . . . . . . . . . . . . 17
   #    #          inf                             |
85 | 1, 84 | eqbrtrid 4038 |
. . . . . . . . . . . . . . . 16
   #    #                    |
86 | 62 | recnd 7985 |
. . . . . . . . . . . . . . . . 17
   #    #                  |
87 | 86 | mulid2d 7975 |
. . . . . . . . . . . . . . . 16
   #    #                          |
88 | 85, 87 | breqtrd 4029 |
. . . . . . . . . . . . . . 15
   #    #                  |
89 | 78, 51, 62, 58, 88 | ltletrd 8379 |
. . . . . . . . . . . . . 14
   #    #                        |
90 | 75, 78, 62, 79, 89 | lelttrd 8081 |
. . . . . . . . . . . . 13
   #    #                            |
91 | 72, 71, 62 | ltsubadd2d 8499 |
. . . . . . . . . . . . 13
   #    #                              
               |
92 | 90, 91 | mpbid 147 |
. . . . . . . . . . . 12
   #    #                            |
93 | 74, 92 | eqbrtrd 4025 |
. . . . . . . . . . 11
   #    #                                      |
94 | 62, 71, 62 | ltadd1d 8494 |
. . . . . . . . . . 11
   #    #                                                  |
95 | 93, 94 | mpbird 167 |
. . . . . . . . . 10
   #    #                      |
96 | 62, 71, 59, 95 | ltmul2dd 9752 |
. . . . . . . . 9
   #    #                                      |
97 | 22, 27 | absmuld 11202 |
. . . . . . . . . . 11
   #    #                            |
98 | 97 | oveq1d 5889 |
. . . . . . . . . 10
   #    #              
                 |
99 | 71 | recnd 7985 |
. . . . . . . . . . 11
   #    #                |
100 | 54 | recnd 7985 |
. . . . . . . . . . 11
   #    #            |
101 | 73, 99, 100 | mul32d 8109 |
. . . . . . . . . 10
   #    #                                    |
102 | 98, 101 | eqtrd 2210 |
. . . . . . . . 9
   #    #              
                 |
103 | 96, 102 | breqtrrd 4031 |
. . . . . . . 8
   #    #                            
     |
104 | 51, 63, 55, 70, 103 | lelttrd 8081 |
. . . . . . 7
   #    #              
     |
105 | 49, 51, 55, 58, 104 | lttrd 8082 |
. . . . . 6
   #    #                    
     |
106 | 28, 31 | absrpclapd 11196 |
. . . . . . 7
   #    #                  |
107 | 49, 54, 106 | ltdivmuld 9747 |
. . . . . 6
   #    #               
            
 
           |
108 | 105, 107 | mpbird 167 |
. . . . 5
   #    #              
           |
109 | 48, 108 | eqbrtrd 4025 |
. . . 4
   #    #                      |
110 | 109 | expr 375 |
. . 3
   #   #
 
      
             |
111 | 110 | ralrimiva 2550 |
. 2
  #

  #
                     |
112 | | breq2 4007 |
. . 3
       
         |
113 | 112 | rspceaimv 2849 |
. 2
  
 #                    
   #
                     |
114 | 21, 111, 113 | syl2anc 411 |
1
  #

   #
                     |