Proof of Theorem pntibndlem2
Step | Hyp | Ref
| Expression |
1 | | pntibndlem2.10 |
. . 3
   |
2 | 1 | nnrpd 11362 |
. 2
   |
3 | | pntibndlem2.11 |
. . . . 5
  
                    |
4 | 3 | simpld 466 |
. . . 4
 
       |
5 | 4 | simpld 466 |
. . 3
   |
6 | | 1red 9676 |
. . . . . 6
   |
7 | | ioossre 11721 |
. . . . . . . 8
     |
8 | | pntibnd.r |
. . . . . . . . 9
  ψ     |
9 | | pntibndlem1.1 |
. . . . . . . . 9
   |
10 | | pntibndlem1.l |
. . . . . . . . 9
   
   |
11 | 8, 9, 10 | pntibndlem1 24506 |
. . . . . . . 8
       |
12 | 7, 11 | sseldi 3416 |
. . . . . . 7
   |
13 | | pntibndlem3.4 |
. . . . . . . 8
       |
14 | 7, 13 | sseldi 3416 |
. . . . . . 7
   |
15 | 12, 14 | remulcld 9689 |
. . . . . 6
     |
16 | 6, 15 | readdcld 9688 |
. . . . 5
       |
17 | 1 | nnred 10646 |
. . . . 5
   |
18 | 16, 17 | remulcld 9689 |
. . . 4
         |
19 | | 2re 10701 |
. . . . 5
 |
20 | | remulcl 9642 |
. . . . 5
 
     |
21 | 19, 17, 20 | sylancr 676 |
. . . 4
     |
22 | | pntibndlem3.c |
. . . . . . . . . 10
         |
23 | | pntibndlem3.3 |
. . . . . . . . . . . . 13
   |
24 | 23 | rpred 11364 |
. . . . . . . . . . . 12
   |
25 | | remulcl 9642 |
. . . . . . . . . . . 12
 
     |
26 | 19, 24, 25 | sylancr 676 |
. . . . . . . . . . 11
     |
27 | | 2rp 11330 |
. . . . . . . . . . . . 13
 |
28 | 27 | a1i 11 |
. . . . . . . . . . . 12
   |
29 | 28 | relogcld 23651 |
. . . . . . . . . . 11
       |
30 | 26, 29 | readdcld 9688 |
. . . . . . . . . 10
           |
31 | 22, 30 | syl5eqel 2553 |
. . . . . . . . 9
   |
32 | | eliooord 11719 |
. . . . . . . . . . . 12
     
   |
33 | 13, 32 | syl 17 |
. . . . . . . . . . 11
 
   |
34 | 33 | simpld 466 |
. . . . . . . . . 10
   |
35 | 14, 34 | elrpd 11361 |
. . . . . . . . 9
   |
36 | 31, 35 | rerpdivcld 11392 |
. . . . . . . 8
     |
37 | 36 | reefcld 14219 |
. . . . . . 7
         |
38 | | pnfxr 11435 |
. . . . . . 7
 |
39 | | icossre 11740 |
. . . . . . 7
                    |
40 | 37, 38, 39 | sylancl 675 |
. . . . . 6
            |
41 | | pntibndlem2.8 |
. . . . . 6
            |
42 | 40, 41 | sseldd 3419 |
. . . . 5
   |
43 | | ioossre 11721 |
. . . . . 6
    |
44 | | pntibndlem2.9 |
. . . . . 6
      |
45 | 43, 44 | sseldi 3416 |
. . . . 5
   |
46 | 42, 45 | remulcld 9689 |
. . . 4
     |
47 | 19 | a1i 11 |
. . . . 5
   |
48 | | eliooord 11719 |
. . . . . . . . . . . . 13
     
   |
49 | 11, 48 | syl 17 |
. . . . . . . . . . . 12
 
   |
50 | 49 | simpld 466 |
. . . . . . . . . . 11
   |
51 | 12, 50 | elrpd 11361 |
. . . . . . . . . 10
   |
52 | 51 | rpge0d 11368 |
. . . . . . . . 9

  |
53 | 49 | simprd 470 |
. . . . . . . . 9
   |
54 | 35 | rpge0d 11368 |
. . . . . . . . 9

  |
55 | 33 | simprd 470 |
. . . . . . . . 9
   |
56 | 12, 6, 14, 6, 52, 53, 54, 55 | ltmul12ad 10570 |
. . . . . . . 8
  
    |
57 | | 1t1e1 10780 |
. . . . . . . 8
   |
58 | 56, 57 | syl6breq 4435 |
. . . . . . 7
  
  |
59 | 15, 6, 6, 58 | ltadd2dd 9811 |
. . . . . 6
         |
60 | | df-2 10690 |
. . . . . 6
   |
61 | 59, 60 | syl6breqr 4436 |
. . . . 5
       |
62 | 16, 47, 2, 61 | ltmul1dd 11416 |
. . . 4
      
    |
63 | 4 | simprd 470 |
. . . . . 6

      |
64 | 42 | recnd 9687 |
. . . . . . 7
   |
65 | 45 | recnd 9687 |
. . . . . . 7
   |
66 | | rpcnne0 11342 |
. . . . . . . 8

    |
67 | 27, 66 | mp1i 13 |
. . . . . . 7
     |
68 | | div23 10311 |
. . . . . . 7
 
             |
69 | 64, 65, 67, 68 | syl3anc 1292 |
. . . . . 6
           |
70 | 63, 69 | breqtrrd 4422 |
. . . . 5

 
    |
71 | 17, 46, 28 | lemuldiv2d 11411 |
. . . . 5
    
        |
72 | 70, 71 | mpbird 240 |
. . . 4
  
    |
73 | 18, 21, 46, 62, 72 | ltletrd 9812 |
. . 3
      
    |
74 | | pntibndlem3.2 |
. . . . . . . . . . . 12
              |
75 | | pntibndlem3.k |
. . . . . . . . . . . 12
         |
76 | 8, 9, 10, 74, 23, 75, 22, 13, 9, 1 | pntibndlem2a 24507 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
          |
77 | 76 | simp1d 1042 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
  |
78 | 2 | adantr 472 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
  |
79 | 76 | simp2d 1043 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
  |
80 | 77, 78, 79 | rpgecld 11400 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)        
  |
81 | 8 | pntrf 24480 |
. . . . . . . . . 10
     |
82 | 81 | ffvelrni 6036 |
. . . . . . . . 9

      |
83 | 80, 82 | syl 17 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)        
      |
84 | 83, 80 | rerpdivcld 11392 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)        
        |
85 | 84 | recnd 9687 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)        
        |
86 | 85 | abscld 13575 |
. . . . 5
 
  ![[,] [,]](_icc.gif)        
            |
87 | 81 | ffvelrni 6036 |
. . . . . . . . . . . 12

      |
88 | 2, 87 | syl 17 |
. . . . . . . . . . 11
       |
89 | 88, 1 | nndivred 10680 |
. . . . . . . . . 10
         |
90 | 89 | adantr 472 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)        
        |
91 | 90 | recnd 9687 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)        
        |
92 | 85, 91 | subcld 10005 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)        
                |
93 | 92 | abscld 13575 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)        
                    |
94 | 91 | abscld 13575 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)        
            |
95 | 93, 94 | readdcld 9688 |
. . . . 5
 
  ![[,] [,]](_icc.gif)        
                                |
96 | 14 | adantr 472 |
. . . . 5
 
  ![[,] [,]](_icc.gif)        
  |
97 | 85, 91 | abs2difd 13596 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)        
                     
                    |
98 | 86, 94, 93 | lesubaddd 10231 |
. . . . . 6
 
  ![[,] [,]](_icc.gif)        
                                                  
                                 |
99 | 97, 98 | mpbid 215 |
. . . . 5
 
  ![[,] [,]](_icc.gif)        
                                          |
100 | 96 | rehalfcld 10882 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)        
    |
101 | 17 | adantr 472 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
  |
102 | 77, 101 | resubcld 10068 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
    |
103 | 102, 78 | rerpdivcld 11392 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
      |
104 | | 3re 10705 |
. . . . . . . . . . . 12
 |
105 | 104 | a1i 11 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
  |
106 | 86, 105 | readdcld 9688 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
              |
107 | 103, 106 | remulcld 9689 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)        
                    |
108 | | pntibndlem2.5 |
. . . . . . . . . . . 12
   |
109 | 108 | rpred 11364 |
. . . . . . . . . . 11
   |
110 | 109 | adantr 472 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
  |
111 | | 1red 9676 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
  |
112 | | 4nn 10792 |
. . . . . . . . . . . . . . . . . 18
 |
113 | | nnrp 11334 |
. . . . . . . . . . . . . . . . . 18
   |
114 | 112, 113 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
   |
115 | 35, 114 | rpdivcld 11381 |
. . . . . . . . . . . . . . . 16
     |
116 | 108, 115 | rpdivcld 11381 |
. . . . . . . . . . . . . . 15
       |
117 | 116 | rpred 11364 |
. . . . . . . . . . . . . 14
       |
118 | 117 | reefcld 14219 |
. . . . . . . . . . . . 13
           |
119 | 118 | adantr 472 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
          |
120 | | efgt1 14247 |
. . . . . . . . . . . . . 14
    
          |
121 | 116, 120 | syl 17 |
. . . . . . . . . . . . 13
           |
122 | 121 | adantr 472 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
          |
123 | | pntibndlem2.7 |
. . . . . . . . . . . . . . . 16
           |
124 | | pntibndlem3.6 |
. . . . . . . . . . . . . . . . . 18
   |
125 | 124 | rpred 11364 |
. . . . . . . . . . . . . . . . 17
   |
126 | 118, 125 | readdcld 9688 |
. . . . . . . . . . . . . . . 16
             |
127 | 123, 126 | syl5eqel 2553 |
. . . . . . . . . . . . . . 15
   |
128 | 118, 124 | ltaddrpd 11394 |
. . . . . . . . . . . . . . . 16
                     |
129 | 128, 123 | syl6breqr 4436 |
. . . . . . . . . . . . . . 15
           |
130 | | eliooord 11719 |
. . . . . . . . . . . . . . . . 17
   
    |
131 | 44, 130 | syl 17 |
. . . . . . . . . . . . . . . 16
 
   |
132 | 131 | simpld 466 |
. . . . . . . . . . . . . . 15
   |
133 | 118, 127,
45, 129, 132 | lttrd 9813 |
. . . . . . . . . . . . . 14
           |
134 | 118, 45, 17, 133, 5 | lttrd 9813 |
. . . . . . . . . . . . 13
           |
135 | 134 | adantr 472 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
          |
136 | 111, 119,
101, 122, 135 | lttrd 9813 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
  |
137 | 101, 136 | rplogcld 23657 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
      |
138 | 110, 137 | rerpdivcld 11392 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)        
        |
139 | 107, 138 | readdcld 9688 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)        
                            |
140 | | peano2re 9824 |
. . . . . . . . . . . 12
                         |
141 | 86, 140 | syl 17 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
              |
142 | 103, 141 | remulcld 9689 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
                    |
143 | | chpcl 24130 |
. . . . . . . . . . . . 13
 ψ    |
144 | 77, 143 | syl 17 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
ψ    |
145 | | chpcl 24130 |
. . . . . . . . . . . . 13
 ψ    |
146 | 101, 145 | syl 17 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
ψ    |
147 | 144, 146 | resubcld 10068 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
 ψ  ψ     |
148 | 147, 78 | rerpdivcld 11392 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
  ψ  ψ      |
149 | 142, 148 | readdcld 9688 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)        
                     ψ  ψ       |
150 | 103, 86 | remulcld 9689 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
                  |
151 | 88 | adantr 472 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
      |
152 | 83, 151 | resubcld 10068 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
            |
153 | 152 | recnd 9687 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
            |
154 | 153 | abscld 13575 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
                |
155 | 154, 78 | rerpdivcld 11392 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
                  |
156 | 150, 155 | readdcld 9688 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
                                    |
157 | 103, 84 | remulcld 9689 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
              |
158 | 157 | renegcld 10067 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
               |
159 | 158 | recnd 9687 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
               |
160 | 152, 78 | rerpdivcld 11392 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
              |
161 | 160 | recnd 9687 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
              |
162 | 159, 161 | abstrid 13595 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
                                                                    |
163 | 77 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . 20
 
  ![[,] [,]](_icc.gif)        
  |
164 | 101 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . 20
 
  ![[,] [,]](_icc.gif)        
  |
165 | 78 | rpne0d 11369 |
. . . . . . . . . . . . . . . . . . . 20
 
  ![[,] [,]](_icc.gif)        
  |
166 | 163, 164,
164, 165 | divsubdird 10444 |
. . . . . . . . . . . . . . . . . . 19
 
  ![[,] [,]](_icc.gif)        
            |
167 | 164, 165 | dividd 10403 |
. . . . . . . . . . . . . . . . . . . 20
 
  ![[,] [,]](_icc.gif)        
    |
168 | 167 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . 19
 
  ![[,] [,]](_icc.gif)        
            |
169 | 166, 168 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)        
          |
170 | 169 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
                          |
171 | 77, 78 | rerpdivcld 11392 |
. . . . . . . . . . . . . . . . . . 19
 
  ![[,] [,]](_icc.gif)        
    |
172 | 171 | recnd 9687 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)        
    |
173 | | 1cnd 9677 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)        
  |
174 | 172, 173,
85 | subdird 10096 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
                                  |
175 | 80 | rpcnne0d 11373 |
. . . . . . . . . . . . . . . . . . 19
 
  ![[,] [,]](_icc.gif)        
    |
176 | 78 | rpcnne0d 11373 |
. . . . . . . . . . . . . . . . . . 19
 
  ![[,] [,]](_icc.gif)        
    |
177 | 83 | recnd 9687 |
. . . . . . . . . . . . . . . . . . 19
 
  ![[,] [,]](_icc.gif)        
      |
178 | | dmdcan 10339 |
. . . . . . . . . . . . . . . . . . 19
                             |
179 | 175, 176,
177, 178 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)        
                  |
180 | 85 | mulid2d 9679 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)        
                |
181 | 179, 180 | oveq12d 6326 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
                                    |
182 | 170, 174,
181 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
                            |
183 | 182 | negeqd 9889 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
                              |
184 | 83, 78 | rerpdivcld 11392 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
        |
185 | 184 | recnd 9687 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
        |
186 | 185, 85 | negsubdi2d 10021 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
                               |
187 | 183, 186 | eqtrd 2505 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
                             |
188 | 151 | recnd 9687 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
      |
189 | 177, 188,
164, 165 | divsubdird 10444 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
                            |
190 | 187, 189 | oveq12d 6326 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                                                           |
191 | 85, 185, 91 | npncand 10029 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                                              |
192 | 190, 191 | eqtrd 2505 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
                                           |
193 | 192 | fveq2d 5883 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
                                                   |
194 | 157 | recnd 9687 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
              |
195 | 194 | absnegd 13588 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                                   |
196 | 103 | recnd 9687 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
      |
197 | 196, 85 | absmuld 13593 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                                      |
198 | 77, 101 | subge0d 10224 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
  
   |
199 | 79, 198 | mpbird 240 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
    |
200 | 102, 78, 199 | divge0d 11401 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
      |
201 | 103, 200 | absidd 13561 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
              |
202 | 201 | oveq1d 6323 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                                      |
203 | 195, 197,
202 | 3eqtrd 2509 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
                                   |
204 | 153, 164,
165 | absdivd 13594 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                                      |
205 | 78 | rprege0d 11371 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
    |
206 | | absid 13436 |
. . . . . . . . . . . . . . 15
         |
207 | 205, 206 | syl 17 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
      |
208 | 207 | oveq2d 6324 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                                      |
209 | 204, 208 | eqtrd 2505 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
                                  |
210 | 203, 209 | oveq12d 6326 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
                                                                       |
211 | 162, 193,
210 | 3brtr3d 4425 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
                                                      |
212 | 102, 147 | readdcld 9688 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
    ψ  ψ      |
213 | 212, 78 | rerpdivcld 11392 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
     ψ  ψ       |
214 | 147 | recnd 9687 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
 ψ  ψ     |
215 | 164, 163 | subcld 10005 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
    |
216 | 214, 215 | abstrid 13595 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
     ψ  ψ            ψ  ψ             |
217 | 8 | pntrval 24479 |
. . . . . . . . . . . . . . . . . 18

     ψ     |
218 | 80, 217 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
     ψ     |
219 | 8 | pntrval 24479 |
. . . . . . . . . . . . . . . . . 18

     ψ     |
220 | 78, 219 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
     ψ     |
221 | 218, 220 | oveq12d 6326 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
            ψ    ψ      |
222 | 144 | recnd 9687 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
ψ    |
223 | 146 | recnd 9687 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
ψ    |
224 | | subadd4 9938 |
. . . . . . . . . . . . . . . . . 18
   ψ  ψ   
 
  ψ  ψ        ψ    ψ      |
225 | | sub4 9939 |
. . . . . . . . . . . . . . . . . 18
   ψ  ψ   
 
  ψ  ψ        ψ    ψ      |
226 | | addsub4 9937 |
. . . . . . . . . . . . . . . . . . 19
   ψ 
  ψ 
 
  ψ    ψ      ψ  ψ        |
227 | 226 | an42s 843 |
. . . . . . . . . . . . . . . . . 18
   ψ  ψ   
 
  ψ    ψ      ψ  ψ        |
228 | 224, 225,
227 | 3eqtr3d 2513 |
. . . . . . . . . . . . . . . . 17
   ψ  ψ   
 
  ψ    ψ      ψ  ψ        |
229 | 222, 223,
163, 164, 228 | syl22anc 1293 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
  ψ    ψ      ψ  ψ        |
230 | 221, 229 | eqtr2d 2506 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
  ψ  ψ                  |
231 | 230 | fveq2d 5883 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
     ψ  ψ                       |
232 | | chpwordi 24163 |
. . . . . . . . . . . . . . . . . 18
 
 ψ  ψ    |
233 | 101, 77, 79, 232 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
ψ 
ψ    |
234 | 146, 144,
233 | abssubge0d 13570 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
    ψ  ψ     ψ  ψ     |
235 | 101, 77, 79 | abssuble0d 13571 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
          |
236 | 234, 235 | oveq12d 6326 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
     ψ  ψ       
     ψ  ψ        |
237 | 102 | recnd 9687 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
    |
238 | 214, 237 | addcomd 9853 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
  ψ  ψ          ψ  ψ      |
239 | 236, 238 | eqtrd 2505 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
     ψ  ψ       
       ψ  ψ      |
240 | 216, 231,
239 | 3brtr3d 4425 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                  ψ  ψ      |
241 | 154, 212,
78, 240 | lediv1dd 11419 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
               
     ψ  ψ       |
242 | 155, 213,
150, 241 | leadd2dd 10249 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
                                 
                      ψ  ψ        |
243 | 150 | recnd 9687 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                  |
244 | 148 | recnd 9687 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
  ψ  ψ      |
245 | 243, 196,
244 | addassd 9683 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
                         ψ  ψ                             ψ  ψ        |
246 | 86 | recnd 9687 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
            |
247 | 196, 246,
173 | adddid 9685 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
                                            |
248 | 196 | mulid1d 9678 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
            |
249 | 248 | oveq2d 6324 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
                                                |
250 | 247, 249 | eqtrd 2505 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                                          |
251 | 250 | oveq1d 6323 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
                     ψ  ψ                              ψ  ψ       |
252 | 237, 214,
164, 165 | divdird 10443 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
     ψ  ψ            ψ  ψ       |
253 | 252 | oveq2d 6324 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
                      ψ  ψ                              ψ  ψ        |
254 | 245, 251,
253 | 3eqtr4d 2515 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
                     ψ  ψ                           ψ  ψ        |
255 | 242, 254 | breqtrrd 4422 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
                                 
                     ψ  ψ       |
256 | 93, 156, 149, 211, 255 | letrd 9809 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)        
                                       ψ  ψ       |
257 | | remulcl 9642 |
. . . . . . . . . . . . 13
               |
258 | 19, 103, 257 | sylancr 676 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
        |
259 | 258, 138 | readdcld 9688 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
                |
260 | | remulcl 9642 |
. . . . . . . . . . . . . . 15
  
        |
261 | 19, 102, 260 | sylancr 676 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
      |
262 | 101, 137 | rerpdivcld 11392 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
        |
263 | 110, 262 | remulcld 9689 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
          |
264 | 261, 263 | readdcld 9688 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
      
         |
265 | 18 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
        |
266 | 21 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
    |
267 | 76 | simp3d 1044 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
        |
268 | | ltle 9740 |
. . . . . . . . . . . . . . . . . . . 20
     
         
   |
269 | 16, 19, 268 | sylancl 675 |
. . . . . . . . . . . . . . . . . . 19
         
   |
270 | 61, 269 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
    
  |
271 | 270 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
      |
272 | 16 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)        
      |
273 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
 
  ![[,] [,]](_icc.gif)        
  |
274 | 272, 273,
78 | lemul1d 11404 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
    
           |
275 | 271, 274 | mpbid 215 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
          |
276 | 77, 265, 266, 267, 275 | letrd 9809 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
    |
277 | | elicc2 11724 |
. . . . . . . . . . . . . . . 16
        ![[,] [,]](_icc.gif)           |
278 | 101, 266,
277 | syl2anc 673 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
   ![[,] [,]](_icc.gif)           |
279 | 77, 79, 276, 278 | mpbir3and 1213 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
  ![[,] [,]](_icc.gif)      |
280 | | 1re 9660 |
. . . . . . . . . . . . . . . . . 18
 |
281 | 280 | rexri 9711 |
. . . . . . . . . . . . . . . . 17
 |
282 | | elioopnf 11753 |
. . . . . . . . . . . . . . . . 17

   
     |
283 | 281, 282 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
   
    |
284 | 101, 136,
283 | sylanbrc 677 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
     |
285 | | pntibndlem2.6 |
. . . . . . . . . . . . . . . 16
      
  ![[,] [,]](_icc.gif)      ψ  ψ                   |
286 | 285 | adantr 472 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
        ![[,] [,]](_icc.gif)      ψ  ψ                   |
287 | | id 22 |
. . . . . . . . . . . . . . . . . 18
   |
288 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . 18
       |
289 | 287, 288 | oveq12d 6326 |
. . . . . . . . . . . . . . . . 17
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)      |
290 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
 ψ  ψ    |
291 | 290 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
  ψ  ψ    ψ  ψ     |
292 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . 20
       |
293 | 292 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . 19
           |
294 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . 21
           |
295 | 287, 294 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . 20
               |
296 | 295 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . 19
 
                 |
297 | 293, 296 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . 18
                               |
298 | 291, 297 | breq12d 4408 |
. . . . . . . . . . . . . . . . 17
   ψ  ψ                  ψ  ψ                    |
299 | 289, 298 | raleqbidv 2987 |
. . . . . . . . . . . . . . . 16
  
  ![[,] [,]](_icc.gif)      ψ  ψ                 
  ![[,] [,]](_icc.gif)      ψ  ψ  
      
          |
300 | 299 | rspcv 3132 |
. . . . . . . . . . . . . . 15
   
 
    
  ![[,] [,]](_icc.gif)      ψ  ψ                    ![[,] [,]](_icc.gif)      ψ  ψ                    |
301 | 284, 286,
300 | sylc 61 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
   ![[,] [,]](_icc.gif)      ψ  ψ                   |
302 | | fveq2 5879 |
. . . . . . . . . . . . . . . . 17
 ψ  ψ    |
303 | 302 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16
  ψ  ψ    ψ  ψ     |
304 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . 18
       |
305 | 304 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
           |
306 | 305 | oveq1d 6323 |
. . . . . . . . . . . . . . . 16
                               |
307 | 303, 306 | breq12d 4408 |
. . . . . . . . . . . . . . 15
   ψ  ψ                  ψ  ψ                    |
308 | 307 | rspcv 3132 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)     
  ![[,] [,]](_icc.gif)      ψ  ψ  
      
        ψ  ψ  
      
          |
309 | 279, 301,
308 | sylc 61 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
 ψ  ψ                   |
310 | 147, 264,
78, 309 | lediv1dd 11419 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
  ψ  ψ           
          |
311 | 261 | recnd 9687 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
      |
312 | 108 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
  |
313 | 312 | rpred 11364 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
  |
314 | 313, 262 | remulcld 9689 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
          |
315 | 314 | recnd 9687 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
          |
316 | | divdir 10315 |
. . . . . . . . . . . . . 14
      
                                              |
317 | 311, 315,
176, 316 | syl3anc 1292 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                                    |
318 | | 2cnd 10704 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
  |
319 | 318, 237,
164, 165 | divassd 10440 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
              |
320 | 110 | recnd 9687 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
  |
321 | 137 | rpcnne0d 11373 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
            |
322 | | div12 10314 |
. . . . . . . . . . . . . . . . 17
 
            
                |
323 | 320, 164,
321, 322 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
                  |
324 | 323 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
 
                    |
325 | 312, 137 | rpdivcld 11381 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
        |
326 | 325 | rpcnd 11366 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
        |
327 | 326, 164,
165 | divcan3d 10410 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
 
                |
328 | 324, 327 | eqtrd 2505 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
 
                |
329 | 319, 328 | oveq12d 6326 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                                  |
330 | 317, 329 | eqtrd 2505 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
                                |
331 | 310, 330 | breqtrd 4420 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
  ψ  ψ                    |
332 | 148, 259,
142, 331 | leadd2dd 10249 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
                     ψ  ψ                                         |
333 | 142 | recnd 9687 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
                    |
334 | 258 | recnd 9687 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
        |
335 | 138 | recnd 9687 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
        |
336 | 333, 334,
335 | addassd 9683 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
                                                                      |
337 | | 2cn 10702 |
. . . . . . . . . . . . . . 15
 |
338 | | mulcom 9643 |
. . . . . . . . . . . . . . 15
                     |
339 | 337, 196,
338 | sylancr 676 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
              |
340 | 339 | oveq2d 6324 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                                                      |
341 | 141 | recnd 9687 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
              |
342 | 196, 341,
318 | adddid 9685 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                                                |
343 | 246, 173,
318 | addassd 9683 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
                              |
344 | | 1p2e3 10757 |
. . . . . . . . . . . . . . . 16
   |
345 | 344 | oveq2i 6319 |
. . . . . . . . . . . . . . 15
                           |
346 | 343, 345 | syl6eq 2521 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
                            |
347 | 346 | oveq2d 6324 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
                                        |
348 | 340, 342,
347 | 3eqtr2d 2511 |
. . . . . . . . . . . 12
 
  ![[,] [,]](_icc.gif)        
                                              |
349 | 348 | oveq1d 6323 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)        
                                                              |
350 | 336, 349 | eqtr3d 2507 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
                                                              |
351 | 332, 350 | breqtrd 4420 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)        
                     ψ  ψ                                 |
352 | 93, 149, 139, 256, 351 | letrd 9809 |
. . . . . . . 8
 
  ![[,] [,]](_icc.gif)        
                                              |
353 | 100 | rehalfcld 10882 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)        
      |
354 | 77, 272, 78 | ledivmul2d 11415 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
      
         |
355 | 267, 354 | mpbird 240 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
        |
356 | | ax-1cn 9615 |
. . . . . . . . . . . . . . . 16
 |
357 | 15 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
  ![[,] [,]](_icc.gif)        
    |
358 | 357 | recnd 9687 |
. . . . . . . . . . . . . . . 16
 
  ![[,] [,]](_icc.gif)        
    |
359 | | addcom 9837 |
. . . . . . . . . . . . . . . 16
  
            |
360 | 356, 358,
359 | sylancr 676 |
. . . . . . . . . . . . . . 15
 
  ![[,] [,]](_icc.gif)        
          |
361 | 355, 360 | breqtrd 4420 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
        |
362 | 171, 111,
357 | lesubaddd 10231 |
. . . . . . . . . . . . . 14
 
  ![[,] [,]](_icc.gif)        
      
         |
363 | 361, 362 | mpbird 240 |
. . . . . . . . . . . . 13
 
  ![[,] [,]](_icc.gif)        
        |
364 | 169, 363 | eqbrtrd 4416 |
. . . . . . . . . . . 12
 
   |