Step | Hyp | Ref
| Expression |
1 | | chpdifbnd.y |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)      |
2 | | ioossre 11721 |
. . . . . . . . . . 11
    |
3 | | chpdifbnd.x |
. . . . . . . . . . 11
      |
4 | 2, 3 | sseldi 3416 |
. . . . . . . . . 10
   |
5 | | chpdifbnd.a |
. . . . . . . . . . . 12
   |
6 | 5 | rpred 11364 |
. . . . . . . . . . 11
   |
7 | 6, 4 | remulcld 9689 |
. . . . . . . . . 10
     |
8 | | elicc2 11724 |
. . . . . . . . . 10
  
     ![[,] [,]](_icc.gif) 
   
     |
9 | 4, 7, 8 | syl2anc 673 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)    
      |
10 | 1, 9 | mpbid 215 |
. . . . . . . 8
 
     |
11 | 10 | simp1d 1042 |
. . . . . . 7
   |
12 | | chpcl 24130 |
. . . . . . 7
 ψ    |
13 | 11, 12 | syl 17 |
. . . . . 6
 ψ    |
14 | | chpcl 24130 |
. . . . . . 7
 ψ    |
15 | 4, 14 | syl 17 |
. . . . . 6
 ψ    |
16 | 13, 15 | resubcld 10068 |
. . . . 5
  ψ  ψ     |
17 | | 0red 9662 |
. . . . . . . 8
   |
18 | | 1re 9660 |
. . . . . . . . 9
 |
19 | 18 | a1i 11 |
. . . . . . . 8
   |
20 | | 0lt1 10157 |
. . . . . . . . 9
 |
21 | 20 | a1i 11 |
. . . . . . . 8
   |
22 | | eliooord 11719 |
. . . . . . . . . 10
   
    |
23 | 3, 22 | syl 17 |
. . . . . . . . 9
 
   |
24 | 23 | simpld 466 |
. . . . . . . 8
   |
25 | 17, 19, 4, 21, 24 | lttrd 9813 |
. . . . . . 7
   |
26 | 4, 25 | elrpd 11361 |
. . . . . 6
   |
27 | 26 | relogcld 23651 |
. . . . 5
       |
28 | 16, 27 | remulcld 9689 |
. . . 4
   ψ  ψ          |
29 | | 2re 10701 |
. . . . . . 7
 |
30 | 11, 4 | resubcld 10068 |
. . . . . . 7
     |
31 | | remulcl 9642 |
. . . . . . 7
  
        |
32 | 29, 30, 31 | sylancr 676 |
. . . . . 6
  
    |
33 | 32, 27 | remulcld 9689 |
. . . . 5
             |
34 | | chpdifbnd.b |
. . . . . . . 8
   |
35 | 34 | rpred 11364 |
. . . . . . 7
   |
36 | 11, 4 | readdcld 9688 |
. . . . . . 7
     |
37 | 35, 36 | remulcld 9689 |
. . . . . 6
  
    |
38 | 5 | relogcld 23651 |
. . . . . . . 8
       |
39 | | remulcl 9642 |
. . . . . . . 8
               |
40 | 29, 38, 39 | sylancr 676 |
. . . . . . 7
         |
41 | 40, 11 | remulcld 9689 |
. . . . . 6
           |
42 | 37, 41 | readdcld 9688 |
. . . . 5
   
             |
43 | 33, 42 | readdcld 9688 |
. . . 4
              
              |
44 | | chpdifbnd.c |
. . . . . . 7
  
            |
45 | | peano2re 9824 |
. . . . . . . . . 10
 
   |
46 | 6, 45 | syl 17 |
. . . . . . . . 9
     |
47 | 35, 46 | remulcld 9689 |
. . . . . . . 8
  
    |
48 | | remulcl 9642 |
. . . . . . . . . 10
 
     |
49 | 29, 6, 48 | sylancr 676 |
. . . . . . . . 9
     |
50 | 49, 38 | remulcld 9689 |
. . . . . . . 8
           |
51 | 47, 50 | readdcld 9688 |
. . . . . . 7
   
             |
52 | 44, 51 | syl5eqel 2553 |
. . . . . 6
   |
53 | 52, 4 | remulcld 9689 |
. . . . 5
     |
54 | 33, 53 | readdcld 9688 |
. . . 4
                 |
55 | 13, 27 | remulcld 9689 |
. . . . . . 7
  ψ         |
56 | | fzfid 12224 |
. . . . . . . 8
           |
57 | 10 | simp2d 1043 |
. . . . . . . . . . . 12

  |
58 | | flword2 12081 |
. . . . . . . . . . . 12
 
               |
59 | 4, 11, 57, 58 | syl3anc 1292 |
. . . . . . . . . . 11
               |
60 | | fzss2 11864 |
. . . . . . . . . . 11
                               |
61 | 59, 60 | syl 17 |
. . . . . . . . . 10
                   |
62 | 61 | sselda 3418 |
. . . . . . . . 9
 
        
          |
63 | | elfznn 11854 |
. . . . . . . . . . . 12
           |
64 | 63 | adantl 473 |
. . . . . . . . . . 11
 
        
  |
65 | | vmacl 24124 |
. . . . . . . . . . 11
 Λ    |
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
 
        
Λ    |
67 | | nndivre 10667 |
. . . . . . . . . . . 12
 
     |
68 | 4, 63, 67 | syl2an 485 |
. . . . . . . . . . 11
 
        
    |
69 | | chpcl 24130 |
. . . . . . . . . . 11
   ψ      |
70 | 68, 69 | syl 17 |
. . . . . . . . . 10
 
        
ψ      |
71 | 66, 70 | remulcld 9689 |
. . . . . . . . 9
 
        
 Λ  ψ       |
72 | 62, 71 | syldan 478 |
. . . . . . . 8
 
        
 Λ  ψ       |
73 | 56, 72 | fsumrecl 13877 |
. . . . . . 7
 
          Λ  ψ       |
74 | 55, 73 | readdcld 9688 |
. . . . . 6
   ψ                  Λ  ψ 
      |
75 | | remulcl 9642 |
. . . . . . . . 9
               |
76 | 29, 27, 75 | sylancr 676 |
. . . . . . . 8
         |
77 | 76, 35 | resubcld 10068 |
. . . . . . 7
           |
78 | 77, 4 | remulcld 9689 |
. . . . . 6
             |
79 | 5, 26 | rpmulcld 11380 |
. . . . . . . . . 10
     |
80 | 79 | relogcld 23651 |
. . . . . . . . 9
    
    |
81 | | remulcl 9642 |
. . . . . . . . 9
                   |
82 | 29, 80, 81 | sylancr 676 |
. . . . . . . 8
           |
83 | 35, 82 | readdcld 9688 |
. . . . . . 7
             |
84 | 83, 11 | remulcld 9689 |
. . . . . 6
               |
85 | 15, 27 | remulcld 9689 |
. . . . . . 7
  ψ         |
86 | 85, 73 | readdcld 9688 |
. . . . . 6
   ψ                  Λ  ψ 
      |
87 | 17, 4, 11, 25, 57 | ltletrd 9812 |
. . . . . . . . . . 11
   |
88 | 11, 87 | elrpd 11361 |
. . . . . . . . . 10
   |
89 | 88 | relogcld 23651 |
. . . . . . . . 9
       |
90 | 13, 89 | remulcld 9689 |
. . . . . . . 8
  ψ         |
91 | | fzfid 12224 |
. . . . . . . . 9
           |
92 | | nndivre 10667 |
. . . . . . . . . . . 12
 
     |
93 | 11, 63, 92 | syl2an 485 |
. . . . . . . . . . 11
 
        
    |
94 | | chpcl 24130 |
. . . . . . . . . . 11
   ψ      |
95 | 93, 94 | syl 17 |
. . . . . . . . . 10
 
        
ψ      |
96 | 66, 95 | remulcld 9689 |
. . . . . . . . 9
 
        
 Λ  ψ       |
97 | 91, 96 | fsumrecl 13877 |
. . . . . . . 8
 
          Λ  ψ       |
98 | 90, 97 | readdcld 9688 |
. . . . . . 7
   ψ                  Λ  ψ 
      |
99 | | chpge0 24132 |
. . . . . . . . . 10
 ψ    |
100 | 11, 99 | syl 17 |
. . . . . . . . 9

ψ    |
101 | 26, 88 | logled 23655 |
. . . . . . . . . 10
             |
102 | 57, 101 | mpbid 215 |
. . . . . . . . 9
    
      |
103 | 27, 89, 13, 100, 102 | lemul2ad 10569 |
. . . . . . . 8
  ψ        ψ         |
104 | 91, 71 | fsumrecl 13877 |
. . . . . . . . 9
 
          Λ  ψ       |
105 | | vmage0 24127 |
. . . . . . . . . . . 12
 Λ    |
106 | 64, 105 | syl 17 |
. . . . . . . . . . 11
 
        
Λ    |
107 | | chpge0 24132 |
. . . . . . . . . . . 12
   ψ      |
108 | 68, 107 | syl 17 |
. . . . . . . . . . 11
 
        
ψ      |
109 | 66, 70, 106, 108 | mulge0d 10211 |
. . . . . . . . . 10
 
        
 Λ  ψ       |
110 | 91, 71, 109, 61 | fsumless 13933 |
. . . . . . . . 9
 
          Λ  ψ                Λ  ψ 
     |
111 | 4 | adantr 472 |
. . . . . . . . . . . . 13
 
        
  |
112 | 11 | adantr 472 |
. . . . . . . . . . . . 13
 
        
  |
113 | 64 | nnrpd 11362 |
. . . . . . . . . . . . 13
 
        
  |
114 | 57 | adantr 472 |
. . . . . . . . . . . . 13
 
        
  |
115 | 111, 112,
113, 114 | lediv1dd 11419 |
. . . . . . . . . . . 12
 
        
      |
116 | | chpwordi 24163 |
. . . . . . . . . . . 12
    
 

   ψ    ψ      |
117 | 68, 93, 115, 116 | syl3anc 1292 |
. . . . . . . . . . 11
 
        
ψ    ψ      |
118 | 70, 95, 66, 106, 117 | lemul2ad 10569 |
. . . . . . . . . 10
 
        
 Λ  ψ      Λ  ψ       |
119 | 91, 71, 96, 118 | fsumle 13936 |
. . . . . . . . 9
 
          Λ  ψ                Λ  ψ 
     |
120 | 73, 104, 97, 110, 119 | letrd 9809 |
. . . . . . . 8
 
          Λ  ψ                Λ  ψ 
     |
121 | 55, 73, 90, 97, 103, 120 | le2addd 10253 |
. . . . . . 7
   ψ                  Λ  ψ 
      ψ                  Λ  ψ 
      |
122 | 98, 88 | rerpdivcld 11392 |
. . . . . . . . 9
    ψ                  Λ  ψ 
       |
123 | | remulcl 9642 |
. . . . . . . . . . 11
               |
124 | 29, 89, 123 | sylancr 676 |
. . . . . . . . . 10
         |
125 | 35, 124 | readdcld 9688 |
. . . . . . . . 9
           |
126 | 122, 124 | resubcld 10068 |
. . . . . . . . . . 11
     ψ                  Λ  ψ                |
127 | 126 | recnd 9687 |
. . . . . . . . . . . 12
     ψ                  Λ  ψ                |
128 | 127 | abscld 13575 |
. . . . . . . . . . 11
        ψ                  Λ  ψ 
               |
129 | 126 | leabsd 13553 |
. . . . . . . . . . 11
     ψ                  Λ  ψ             
       ψ                  Λ  ψ                 |
130 | 19, 4, 24 | ltled 9800 |
. . . . . . . . . . . . . 14

  |
131 | 19, 4, 11, 130, 57 | letrd 9809 |
. . . . . . . . . . . . 13

  |
132 | | elicopnf 11755 |
. . . . . . . . . . . . . 14
 
  
     |
133 | 18, 132 | ax-mp 5 |
. . . . . . . . . . . . 13
   
    |
134 | 11, 131, 133 | sylanbrc 677 |
. . . . . . . . . . . 12
      |
135 | | chpdifbnd.2 |
. . . . . . . . . . . 12
             ψ                  Λ  ψ                 |
136 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
 ψ  ψ    |
137 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
138 | 136, 137 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . 18
  ψ        ψ         |
139 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . 21
 Λ  Λ    |
140 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
141 | 140 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
 ψ    ψ      |
142 | 139, 141 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . 20
  Λ  ψ      Λ  ψ       |
143 | 142 | cbvsumv 13839 |
. . . . . . . . . . . . . . . . . . 19
           Λ  ψ     
          Λ  ψ      |
144 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . 21
           |
145 | 144 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . 20
                   |
146 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
           |
147 | 146 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . 22
 
               |
148 | 147 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . 21
 
         ψ    ψ 
    |
149 | 148 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . 20
 
          Λ  ψ      Λ  ψ 
     |
150 | 145, 149 | sumeq12rdv 13850 |
. . . . . . . . . . . . . . . . . . 19
            Λ  ψ     
          Λ  ψ       |
151 | 143, 150 | syl5eq 2517 |
. . . . . . . . . . . . . . . . . 18
            Λ  ψ     
          Λ  ψ       |
152 | 138, 151 | oveq12d 6326 |
. . . . . . . . . . . . . . . . 17
   ψ       
          Λ  ψ        ψ                  Λ  ψ        |
153 | | id 22 |
. . . . . . . . . . . . . . . . 17
   |
154 | 152, 153 | oveq12d 6326 |
. . . . . . . . . . . . . . . 16
    ψ                  Λ  ψ          ψ                  Λ  ψ 
       |
155 | 137 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
               |
156 | 154, 155 | oveq12d 6326 |
. . . . . . . . . . . . . . 15
     ψ                  Λ  ψ                  ψ                  Λ  ψ 
              |
157 | 156 | fveq2d 5883 |
. . . . . . . . . . . . . 14
        ψ       
          Λ  ψ                      ψ                  Λ  ψ 
               |
158 | 157 | breq1d 4405 |
. . . . . . . . . . . . 13
         ψ                  Λ  ψ                      ψ                  Λ  ψ 
                |
159 | 158 | rspcv 3132 |
. . . . . . . . . . . 12
   
 
           ψ                  Λ  ψ                      ψ                  Λ  ψ 
                |
160 | 134, 135,
159 | sylc 61 |
. . . . . . . . . . 11
        ψ                  Λ  ψ 
               |
161 | 126, 128,
35, 129, 160 | letrd 9809 |
. . . . . . . . . 10
     ψ                  Λ  ψ             
  |
162 | 122, 124,
35 | lesubaddd 10231 |
. . . . . . . . . 10
      ψ       
          Λ  ψ                 ψ                  Λ  ψ 
                |
163 | 161, 162 | mpbid 215 |
. . . . . . . . 9
    ψ                  Λ  ψ 
               |
164 | 10 | simp3d 1044 |
. . . . . . . . . . . 12

    |
165 | 88, 79 | logled 23655 |
. . . . . . . . . . . 12
  
        
     |
166 | 164, 165 | mpbid 215 |
. . . . . . . . . . 11
    
        |
167 | | 2pos 10723 |
. . . . . . . . . . . . . 14
 |
168 | 29, 167 | pm3.2i 462 |
. . . . . . . . . . . . 13
   |
169 | 168 | a1i 11 |
. . . . . . . . . . . 12
     |
170 | | lemul2 10480 |
. . . . . . . . . . . 12
                         
                 |
171 | 89, 80, 169, 170 | syl3anc 1292 |
. . . . . . . . . . 11
     
     
                 |
172 | 166, 171 | mpbid 215 |
. . . . . . . . . 10
           
     |
173 | 124, 82, 35, 172 | leadd2dd 10249 |
. . . . . . . . 9
                     |
174 | 122, 125,
83, 163, 173 | letrd 9809 |
. . . . . . . 8
    ψ                  Λ  ψ 
                 |
175 | 98, 83, 88 | ledivmul2d 11415 |
. . . . . . . 8
     ψ                  Λ  ψ                   ψ                  Λ  ψ 
          
        |
176 | 174, 175 | mpbid 215 |
. . . . . . 7
   ψ                  Λ  ψ 
          
       |
177 | 74, 98, 84, 121, 176 | letrd 9809 |
. . . . . 6
   ψ                  Λ  ψ 
          
       |
178 | | elicopnf 11755 |
. . . . . . . . . . . 12
 
  
     |
179 | 18, 178 | ax-mp 5 |
. . . . . . . . . . 11
   
    |
180 | 4, 130, 179 | sylanbrc 677 |
. . . . . . . . . 10
      |
181 | | fveq2 5879 |
. . . . . . . . . . . . . . . . 17
 ψ  ψ    |
182 | | fveq2 5879 |
. . . . . . . . . . . . . . . . 17
           |
183 | 181, 182 | oveq12d 6326 |
. . . . . . . . . . . . . . . 16
  ψ        ψ         |
184 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
185 | 184 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
                   |
186 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
187 | 186 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . 20
 
               |
188 | 187 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . 19
 
         ψ    ψ 
    |
189 | 188 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
 
          Λ  ψ      Λ  ψ 
     |
190 | 185, 189 | sumeq12rdv 13850 |
. . . . . . . . . . . . . . . . 17
            Λ  ψ     
          Λ  ψ       |
191 | 143, 190 | syl5eq 2517 |
. . . . . . . . . . . . . . . 16
            Λ  ψ     
          Λ  ψ       |
192 | 183, 191 | oveq12d 6326 |
. . . . . . . . . . . . . . 15
   ψ       
          Λ  ψ        ψ                  Λ  ψ        |
193 | | id 22 |
. . . . . . . . . . . . . . 15
   |
194 | 192, 193 | oveq12d 6326 |
. . . . . . . . . . . . . 14
    ψ                  Λ  ψ          ψ                  Λ  ψ 
       |
195 | 182 | oveq2d 6324 |
. . . . . . . . . . . . . 14
               |
196 | 194, 195 | oveq12d 6326 |
. . . . . . . . . . . . 13
     ψ                  Λ  ψ                  ψ                  Λ  ψ 
              |
197 | 196 | fveq2d 5883 |
. . . . . . . . . . . 12
        ψ       
          Λ  ψ                      ψ                  Λ  ψ 
               |
198 | 197 | breq1d 4405 |
. . . . . . . . . . 11
         ψ                  Λ  ψ                      ψ                  Λ  ψ 
                |
199 | 198 | rspcv 3132 |
. . . . . . . . . 10
   
 
           ψ                  Λ  ψ                      ψ                  Λ  ψ 
                |
200 | 180, 135,
199 | sylc 61 |
. . . . . . . . 9
        ψ                  Λ  ψ 
               |
201 | 86, 26 | rerpdivcld 11392 |
. . . . . . . . . 10
    ψ                  Λ  ψ 
       |
202 | 201, 76, 35 | absdifled 13573 |
. . . . . . . . 9
         ψ                  Λ  ψ 
                     
   ψ       
          Λ  ψ          ψ                  Λ  ψ                   |
203 | 200, 202 | mpbid 215 |
. . . . . . . 8
         
   ψ       
          Λ  ψ          ψ                  Λ  ψ                  |
204 | 203 | simpld 466 |
. . . . . . 7
        
   ψ       
          Λ  ψ         |
205 | 77, 86, 26 | lemuldivd 11410 |
. . . . . . 7
           
  ψ                  Λ  ψ             
   ψ       
          Λ  ψ          |
206 | 204, 205 | mpbird 240 |
. . . . . 6
             ψ                  Λ  ψ 
      |
207 | 74, 78, 84, 86, 177, 206 | le2subd 10254 |
. . . . 5
    ψ                  Λ  ψ 
      ψ                  Λ  ψ 
    
                          |
208 | 55 | recnd 9687 |
. . . . . . 7
  ψ         |
209 | 85 | recnd 9687 |
. . . . . . 7
  ψ         |
210 | 73 | recnd 9687 |
. . . . . . 7
 
          Λ  ψ       |
211 | 208, 209,
210 | pnpcan2d 10043 |
. . . . . 6
    ψ                  Λ  ψ 
      ψ                  Λ  ψ 
       ψ        ψ          |
212 | 13 | recnd 9687 |
. . . . . . 7
 ψ    |
213 | 15 | recnd 9687 |
. . . . . . 7
 ψ    |
214 | 27 | recnd 9687 |
. . . . . . 7
       |
215 | 212, 213,
214 | subdird 10096 |
. . . . . 6
   ψ  ψ          ψ        ψ          |
216 | 211, 215 | eqtr4d 2508 |
. . . . 5
    ψ                  Λ  ψ 
      ψ                  Λ  ψ 
       ψ  ψ          |
217 | 76, 11 | remulcld 9689 |
. . . . . . . 8
           |
218 | 217 | recnd 9687 |
. . . . . . 7
           |
219 | 35, 40 | readdcld 9688 |
. . . . . . . . 9
           |
220 | 219, 11 | remulcld 9689 |
. . . . . . . 8
             |
221 | 220 | recnd 9687 |
. . . . . . 7
             |
222 | 76, 4 | remulcld 9689 |
. . . . . . . 8
           |
223 | 222 | recnd 9687 |
. . . . . . 7
           |
224 | 35, 4 | remulcld 9689 |
. . . . . . . . 9
     |
225 | 224 | recnd 9687 |
. . . . . . . 8
     |
226 | 225 | negcld 9992 |
. . . . . . 7
      |
227 | 218, 221,
223, 226 | addsub4d 10052 |
. . . . . 6
                                
                                  
     |
228 | 5, 26 | relogmuld 23653 |
. . . . . . . . . . . . . 14
    
              |
229 | 38 | recnd 9687 |
. . . . . . . . . . . . . . 15
       |
230 | 229, 214 | addcomd 9853 |
. . . . . . . . . . . . . 14
                       |
231 | 228, 230 | eqtrd 2505 |
. . . . . . . . . . . . 13
    
              |
232 | 231 | oveq2d 6324 |
. . . . . . . . . . . 12
                       |
233 | | 2cnd 10704 |
. . . . . . . . . . . . 13
   |
234 | 233, 214,
229 | adddid 9685 |
. . . . . . . . . . . 12
                             |
235 | 232, 234 | eqtrd 2505 |
. . . . . . . . . . 11
                         |
236 | 235 | oveq2d 6324 |
. . . . . . . . . 10
                             |
237 | 35 | recnd 9687 |
. . . . . . . . . . 11
   |
238 | 76 | recnd 9687 |
. . . . . . . . . . 11
         |
239 | 40 | recnd 9687 |
. . . . . . . . . . 11
         |
240 | 237, 238,
239 | add12d 9876 |
. . . . . . . . . 10
                                   |
241 | 236, 240 | eqtrd 2505 |
. . . . . . . . 9
                             |
242 | 241 | oveq1d 6323 |
. . . . . . . 8
                                 |
243 | 219 | recnd 9687 |
. . . . . . . . 9
           |
244 | 11 | recnd 9687 |
. . . . . . . . 9
   |
245 | 238, 243,
244 | adddird 9686 |
. . . . . . . 8
                                         |
246 | 242, 245 | eqtrd 2505 |
. . . . . . 7
                                   |
247 | 4 | recnd 9687 |
. . . . . . . . 9
   |
248 | 238, 237,
247 | subdird 10096 |
. . . . . . . 8
                    
    |
249 | 223, 225 | negsubd 10011 |
. . . . . . . 8
           
           
    |
250 | 248, 249 | eqtr4d 2508 |
. . . . . . 7
                     
    |
251 | 246, 250 | oveq12d 6326 |
. . . . . 6
        
                                               
     |
252 | 30 | recnd 9687 |
. . . . . . . . 9
     |
253 | 233, 252,
214 | mul32d 9861 |
. . . . . . . 8
                  
    |
254 | 238, 244,
247 | subdid 10095 |
. . . . . . . 8
        
                      |
255 | 253, 254 | eqtrd 2505 |
. . . . . . 7
                               |
256 | 35, 11 | remulcld 9689 |
. . . . . . . . . . 11
     |
257 | 256 | recnd 9687 |
. . . . . . . . . 10
     |
258 | 41 | recnd 9687 |
. . . . . . . . . 10
           |
259 | 257, 225,
258 | add32d 9877 |
. . . . . . . . 9
                                   |
260 | 237, 244,
247 | adddid 9685 |
. . . . . . . . . 10
  
          |
261 | 260 | oveq1d 6323 |
. . . . . . . . 9
   
                             |
262 | 237, 239,
244 | adddird 9686 |
. . . . . . . . . 10
                         |
263 | 262 | oveq1d 6323 |
. . . . . . . . 9
                                 |
264 | 259, 261,
263 | 3eqtr4d 2515 |
. . . . . . . 8
   
                           |
265 | 221, 225 | subnegd 10012 |
. . . . . . . 8
             
                  |
266 | 264, 265 | eqtr4d 2508 |
. . . . . . 7
   
                       
    |
267 | 255, 266 | oveq12d 6326 |
. . . . . 6
              
                                                 |
268 | 227, 251,
267 | 3eqtr4d 2515 |
. . . . 5
        
                   
         
              |
269 | 207, 216,
268 | 3brtr3d 4425 |
. . . 4
   ψ  ψ                                    |
270 | 47, 4 | remulcld 9689 |
. . . . . . 7
   
     |
271 | 50, 4 | remulcld 9689 |
. . . . . . 7
             |
272 | 11, 7, 4, 164 | leadd1dd 10248 |
. . . . . . . . . 10
  
 
    |
273 | 6 | recnd 9687 |
. . . . . . . . . . . 12
   |
274 | 19 | recnd 9687 |
. . . . . . . . . . . 12
   |
275 | 273, 274,
247 | adddird 9686 |
. . . . . . . . . . 11
             |
276 | 247 | mulid2d 9679 |
. . . . . . . . . . . 12
     |
277 | 276 | oveq2d 6324 |
. . . . . . . . . . 11
             |
278 | 275, 277 | eqtrd 2505 |
. . . . . . . . . 10
           |
279 | 272, 278 | breqtrrd 4422 |
. . . . . . . . 9
  
 
    |
280 | 46, 4 | remulcld 9689 |
. . . . . . . . . 10
       |
281 | 36, 280, 34 | lemul2d 11405 |
. . . . . . . . 9
         
 
         |
282 | 279, 281 | mpbid 215 |
. . . . . . . 8
  
 
        |
283 | 46 | recnd 9687 |
. . . . . . . . 9
     |
284 | 237, 283,
247 | mulassd 9684 |
. . . . . . . 8
   
           |
285 | 282, 284 | breqtrrd 4422 |
. . . . . . 7
  
 
 
      |
286 | 29 | a1i 11 |
. . . . . . . . . 10
   |
287 | | 0le2 10722 |
. . . . . . . . . . 11
 |
288 | 287 | a1i 11 |
. . . . . . . . . 10

  |
289 | | log1 23614 |
. . . . . . . . . . 11
     |
290 | | chpdifbnd.1 |
. . . . . . . . . . . 12

  |
291 | | 1rp 11329 |
. . . . . . . . . . . . 13
 |
292 | | logleb 23631 |
. . . . . . . . . . . . 13
   
           |
293 | 291, 5, 292 | sylancr 676 |
. . . . . . . . . . . 12
             |
294 | 290, 293 | mpbid 215 |
. . . . . . . . . . 11
    
      |
295 | 289, 294 | syl5eqbrr 4430 |
. . . . . . . . . 10

      |
296 | 286, 38, 288, 295 | mulge0d 10211 |
. . . . . . . . 9

        |
297 | 11, 7, 40, 296, 164 | lemul2ad 10569 |
. . . . . . . 8
        
            |
298 | 49 | recnd 9687 |
. . . . . . . . . 10
     |
299 | 298, 229,
247 | mulassd 9684 |
. . . . . . . . 9
                       |
300 | 233, 273,
229, 247 | mul4d 9863 |
. . . . . . . . 9
                       |
301 | 299, 300 | eqtrd 2505 |
. . . . . . . 8
                       |
302 | 297, 301 | breqtrrd 4422 |
. . . . . . 7
        
            |
303 | 37, 41, 270, 271, 285, 302 | le2addd 10253 |
. . . . . 6
   
                               |
304 | 44 | oveq1i 6318 |
. . . . . . 7
                   |
305 | 47 | recnd 9687 |
. . . . . . . 8
  
    |
306 | 50 | recnd 9687 |
. . . . . . . 8
           |
307 | 305, 306,
247 | adddird 9686 |
. . . . . . 7
                                     |
308 | 304, 307 | syl5eq 2517 |
. . . . . 6
      
                |
309 | 303, 308 | breqtrrd 4422 |
. . . . 5
   
               |
310 | 42, 53, 33, 309 | leadd2dd 10249 |
. . . 4
              
                            |
311 | 28, 43, 54, 269, 310 | letrd 9809 |
. . 3
   ψ  ψ                        |
312 | 32 | recnd 9687 |
. . . . 5
  
    |
313 | 4, 24 | rplogcld 23657 |
. . . . . . . 8
       |
314 | 4, 313 | rerpdivcld 11392 |
. . . . . . 7
         |
315 | 52, 314 | remulcld 9689 |
. . . . . 6
           |
316 | 315 | recnd 9687 |
. . . . 5
           |
317 | 312, 316,
214 | adddird 9686 |
. . . 4
                                                 |
318 | 52 | recnd 9687 |
. . . . . . 7
   |
319 | 314 | recnd 9687 |
. . . . . . 7
         |
320 | 318, 319,
214 | mulassd 9684 |
. . . . . 6
   
                           |
321 | 313 | rpne0d 11369 |
. . . . . . . 8
       |
322 | 247, 214,
321 | divcan1d 10406 |
. . . . . . 7
               |
323 | 322 | oveq2d 6324 |
. . . . . 6
                   |
324 | 320, 323 | eqtrd 2505 |
. . . . 5
   
               |
325 | 324 | oveq2d 6324 |
. . . 4
                                           |
326 | 317, 325 | eqtrd 2505 |
. . 3
                                     |
327 | 311, 326 | breqtrrd 4422 |
. 2
   ψ  ψ                              |
328 | 32, 315 | readdcld 9688 |
. . 3
                 |
329 | 16, 328, 313 | lemul1d 11404 |
. 2
   ψ  ψ                   ψ  ψ                               |
330 | 327, 329 | mpbird 240 |
1
  ψ  ψ                   |