Proof of Theorem pntlemb
Step | Hyp | Ref
| Expression |
1 | | pntlem1.z |
. . . . 5
      |
2 | | pntlem1.r |
. . . . . . . 8
  ψ     |
3 | | pntlem1.a |
. . . . . . . 8
   |
4 | | pntlem1.b |
. . . . . . . 8
   |
5 | | pntlem1.l |
. . . . . . . 8
       |
6 | | pntlem1.d |
. . . . . . . 8
   |
7 | | pntlem1.f |
. . . . . . . 8
       ;          |
8 | | pntlem1.u |
. . . . . . . 8
   |
9 | | pntlem1.u2 |
. . . . . . . 8

  |
10 | | pntlem1.e |
. . . . . . . 8
   |
11 | | pntlem1.k |
. . . . . . . 8
       |
12 | | pntlem1.y |
. . . . . . . 8
 
   |
13 | | pntlem1.x |
. . . . . . . 8
     |
14 | | pntlem1.c |
. . . . . . . 8
   |
15 | | pntlem1.w |
. . . . . . . 8
                           ;                      |
16 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 | pntlema 22988 |
. . . . . . 7
   |
17 | 16 | rpred 11142 |
. . . . . 6
   |
18 | | pnfxr 11207 |
. . . . . 6
 |
19 | | elico2 11474 |
. . . . . 6
   
  
     |
20 | 17, 18, 19 | sylancl 662 |
. . . . 5
          |
21 | 1, 20 | mpbid 210 |
. . . 4
 
   |
22 | 21 | simp1d 1000 |
. . 3
   |
23 | 21 | simp2d 1001 |
. . 3

  |
24 | 22, 16, 23 | rpgecld 11177 |
. 2
   |
25 | | 1re 9500 |
. . . . . . 7
 |
26 | 25 | a1i 11 |
. . . . . 6
   |
27 | | ere 13496 |
. . . . . . 7
 |
28 | 27 | a1i 11 |
. . . . . 6
   |
29 | 24 | rpsqrcld 13020 |
. . . . . . 7
       |
30 | 29 | rpred 11142 |
. . . . . 6
       |
31 | | 1lt2 10603 |
. . . . . . . 8
 |
32 | | egt2lt3 13610 |
. . . . . . . . 9
   |
33 | 32 | simpli 458 |
. . . . . . . 8
 |
34 | | 2re 10506 |
. . . . . . . . 9
 |
35 | 25, 34, 27 | lttri 9615 |
. . . . . . . 8
     |
36 | 31, 33, 35 | mp2an 672 |
. . . . . . 7
 |
37 | 36 | a1i 11 |
. . . . . 6
   |
38 | | 4re 10513 |
. . . . . . . 8
 |
39 | 38 | a1i 11 |
. . . . . . 7
   |
40 | 32 | simpri 462 |
. . . . . . . . 9
 |
41 | | 3lt4 10606 |
. . . . . . . . 9
 |
42 | | 3re 10510 |
. . . . . . . . . 10
 |
43 | 27, 42, 38 | lttri 9615 |
. . . . . . . . 9
     |
44 | 40, 41, 43 | mp2an 672 |
. . . . . . . 8
 |
45 | 44 | a1i 11 |
. . . . . . 7
   |
46 | | 4nn 10596 |
. . . . . . . . . . 11
 |
47 | | nnrp 11115 |
. . . . . . . . . . 11
   |
48 | 46, 47 | ax-mp 5 |
. . . . . . . . . 10
 |
49 | 2, 3, 4, 5, 6, 7 | pntlemd 22986 |
. . . . . . . . . . . 12
     |
50 | 49 | simp1d 1000 |
. . . . . . . . . . 11
   |
51 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 | pntlemc 22987 |
. . . . . . . . . . . 12
  
    
     |
52 | 51 | simp1d 1000 |
. . . . . . . . . . 11
   |
53 | 50, 52 | rpmulcld 11158 |
. . . . . . . . . 10
     |
54 | | rpdivcl 11128 |
. . . . . . . . . 10
  
        |
55 | 48, 53, 54 | sylancr 663 |
. . . . . . . . 9
  
    |
56 | 55 | rpred 11142 |
. . . . . . . 8
  
    |
57 | 53 | rpred 11142 |
. . . . . . . . . . . 12
     |
58 | 52 | rpred 11142 |
. . . . . . . . . . . 12
   |
59 | 50 | rpred 11142 |
. . . . . . . . . . . . . 14
   |
60 | | eliooord 11470 |
. . . . . . . . . . . . . . . 16
     
   |
61 | 5, 60 | syl 16 |
. . . . . . . . . . . . . . 15
 
   |
62 | 61 | simprd 463 |
. . . . . . . . . . . . . 14
   |
63 | 59, 26, 52, 62 | ltmul1dd 11193 |
. . . . . . . . . . . . 13
  
    |
64 | 52 | rpcnd 11144 |
. . . . . . . . . . . . . 14
   |
65 | 64 | mulid2d 9519 |
. . . . . . . . . . . . 13
     |
66 | 63, 65 | breqtrd 4427 |
. . . . . . . . . . . 12
  
  |
67 | 51 | simp3d 1002 |
. . . . . . . . . . . . . . 15
           |
68 | 67 | simp1d 1000 |
. . . . . . . . . . . . . 14
       |
69 | | eliooord 11470 |
. . . . . . . . . . . . . 14
     
   |
70 | 68, 69 | syl 16 |
. . . . . . . . . . . . 13
 
   |
71 | 70 | simprd 463 |
. . . . . . . . . . . 12
   |
72 | 57, 58, 26, 66, 71 | lttrd 9647 |
. . . . . . . . . . 11
  
  |
73 | | 4pos 10532 |
. . . . . . . . . . . . 13
 |
74 | 39, 73 | jctir 538 |
. . . . . . . . . . . 12
     |
75 | | ltmul2 10295 |
. . . . . . . . . . . 12
   
               |
76 | 57, 26, 74, 75 | syl3anc 1219 |
. . . . . . . . . . 11
             |
77 | 72, 76 | mpbid 210 |
. . . . . . . . . 10
  
 
    |
78 | | 4cn 10514 |
. . . . . . . . . . 11
 |
79 | 78 | mulid1i 9503 |
. . . . . . . . . 10
   |
80 | 77, 79 | syl6breq 4442 |
. . . . . . . . 9
  
 
  |
81 | 39, 39, 53 | ltmuldivd 11185 |
. . . . . . . . 9
             |
82 | 80, 81 | mpbid 210 |
. . . . . . . 8
       |
83 | 12 | simpld 459 |
. . . . . . . . . . 11
   |
84 | 83, 55 | rpaddcld 11157 |
. . . . . . . . . 10
         |
85 | 84 | rpred 11142 |
. . . . . . . . 9
         |
86 | 56, 83 | ltaddrp2d 11172 |
. . . . . . . . 9
  
 
        |
87 | 85 | resqcld 12155 |
. . . . . . . . . . . 12
    
        |
88 | 13 | simpld 459 |
. . . . . . . . . . . . . . . . 17
   |
89 | 51 | simp2d 1001 |
. . . . . . . . . . . . . . . . . 18
   |
90 | | 2z 10793 |
. . . . . . . . . . . . . . . . . 18
 |
91 | | rpexpcl 12005 |
. . . . . . . . . . . . . . . . . 18
         |
92 | 89, 90, 91 | sylancl 662 |
. . . . . . . . . . . . . . . . 17
       |
93 | 88, 92 | rpmulcld 11158 |
. . . . . . . . . . . . . . . 16
         |
94 | 46 | nnzi 10785 |
. . . . . . . . . . . . . . . 16
 |
95 | | rpexpcl 12005 |
. . . . . . . . . . . . . . . 16
       
             |
96 | 93, 94, 95 | sylancl 662 |
. . . . . . . . . . . . . . 15
             |
97 | | 3nn0 10712 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
98 | | 2nn 10594 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
99 | 97, 98 | decnncl 10883 |
. . . . . . . . . . . . . . . . . . . . 21
;  |
100 | | nnrp 11115 |
. . . . . . . . . . . . . . . . . . . . 21
; ;   |
101 | 99, 100 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
;  |
102 | | rpmulcl 11127 |
. . . . . . . . . . . . . . . . . . . 20
 ;  ;    |
103 | 101, 4, 102 | sylancr 663 |
. . . . . . . . . . . . . . . . . . 19
 ;    |
104 | 67 | simp3d 1002 |
. . . . . . . . . . . . . . . . . . . 20
     |
105 | | rpexpcl 12005 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
106 | 52, 90, 105 | sylancl 662 |
. . . . . . . . . . . . . . . . . . . . 21
       |
107 | 50, 106 | rpmulcld 11158 |
. . . . . . . . . . . . . . . . . . . 20
         |
108 | 104, 107 | rpmulcld 11158 |
. . . . . . . . . . . . . . . . . . 19
    
        |
109 | 103, 108 | rpdivcld 11159 |
. . . . . . . . . . . . . . . . . 18
  ;               |
110 | | 3nn 10595 |
. . . . . . . . . . . . . . . . . . . . 21
 |
111 | | nnrp 11115 |
. . . . . . . . . . . . . . . . . . . . 21
   |
112 | 110, 111 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
 |
113 | | rpmulcl 11127 |
. . . . . . . . . . . . . . . . . . . 20
   
   |
114 | 8, 112, 113 | sylancl 662 |
. . . . . . . . . . . . . . . . . . 19
     |
115 | 114, 14 | rpaddcld 11157 |
. . . . . . . . . . . . . . . . . 18
       |
116 | 109, 115 | rpmulcld 11158 |
. . . . . . . . . . . . . . . . 17
   ;                    |
117 | 116 | rpred 11142 |
. . . . . . . . . . . . . . . 16
   ;                    |
118 | 117 | rpefcld 13511 |
. . . . . . . . . . . . . . 15
      ;                     |
119 | 96, 118 | rpaddcld 11157 |
. . . . . . . . . . . . . 14
                 ;                      |
120 | 87, 119 | ltaddrpd 11171 |
. . . . . . . . . . . . 13
    
                                 ;                       |
121 | 120, 15 | syl6breqr 4443 |
. . . . . . . . . . . 12
    
        |
122 | 87, 17, 22, 121, 23 | ltletrd 9646 |
. . . . . . . . . . 11
    
        |
123 | 24 | rprege0d 11149 |
. . . . . . . . . . . 12
 
   |
124 | | resqrth 12867 |
. . . . . . . . . . . 12
             |
125 | 123, 124 | syl 16 |
. . . . . . . . . . 11
           |
126 | 122, 125 | breqtrrd 4429 |
. . . . . . . . . 10
    
                |
127 | 84 | rprege0d 11149 |
. . . . . . . . . . 11
    
  
         |
128 | 29 | rprege0d 11149 |
. . . . . . . . . . 11
             |
129 | | lt2sq 12060 |
. . . . . . . . . . 11
     
  
           
                                      |
130 | 127, 128,
129 | syl2anc 661 |
. . . . . . . . . 10
    
      
 
                   |
131 | 126, 130 | mpbird 232 |
. . . . . . . . 9
             |
132 | 56, 85, 30, 86, 131 | lttrd 9647 |
. . . . . . . 8
  
 
      |
133 | 39, 56, 30, 82, 132 | lttrd 9647 |
. . . . . . 7
       |
134 | 28, 39, 30, 45, 133 | lttrd 9647 |
. . . . . 6
       |
135 | 26, 28, 30, 37, 134 | lttrd 9647 |
. . . . 5
       |
136 | | 0le1 9978 |
. . . . . . 7
 |
137 | 136 | a1i 11 |
. . . . . 6

  |
138 | | lt2sq 12060 |
. . . . . 6
  
     
                          |
139 | 26, 137, 128, 138 | syl21anc 1218 |
. . . . 5
     
               |
140 | 135, 139 | mpbid 210 |
. . . 4
               |
141 | | sq1 12081 |
. . . . 5
     |
142 | 141 | a1i 11 |
. . . 4
       |
143 | 140, 142,
125 | 3brtr3d 4432 |
. . 3
   |
144 | 28, 30, 134 | ltled 9637 |
. . 3

      |
145 | 22, 83 | rerpdivcld 11169 |
. . . 4
     |
146 | 83 | rpred 11142 |
. . . . . . 7
   |
147 | 146, 55 | ltaddrpd 11171 |
. . . . . . . 8
         |
148 | 146, 85, 30, 147, 131 | lttrd 9647 |
. . . . . . 7
       |
149 | 146, 30, 29, 148 | ltmul2dd 11194 |
. . . . . 6
                   |
150 | | remsqsqr 12868 |
. . . . . . 7
               |
151 | 123, 150 | syl 16 |
. . . . . 6
             |
152 | 149, 151 | breqtrd 4427 |
. . . . 5
         |
153 | 30, 22, 83 | ltmuldivd 11185 |
. . . . 5
       
         |
154 | 152, 153 | mpbid 210 |
. . . 4
    
    |
155 | 30, 145, 154 | ltled 9637 |
. . 3
    
    |
156 | 143, 144,
155 | 3jca 1168 |
. 2
 
             |
157 | 56, 30, 132 | ltled 9637 |
. . 3
  
 
      |
158 | 88 | relogcld 22215 |
. . . . . 6
       |
159 | 89 | rpred 11142 |
. . . . . . 7
   |
160 | 67 | simp2d 1001 |
. . . . . . 7
   |
161 | 159, 160 | rplogcld 22221 |
. . . . . 6
       |
162 | 158, 161 | rerpdivcld 11169 |
. . . . 5
             |
163 | | readdcl 9480 |
. . . . 5
                           |
164 | 162, 34, 163 | sylancl 662 |
. . . 4
               |
165 | 24 | relogcld 22215 |
. . . . . 6
       |
166 | 165, 161 | rerpdivcld 11169 |
. . . . 5
             |
167 | | nndivre 10472 |
. . . . 5
                           |
168 | 166, 46, 167 | sylancl 662 |
. . . 4
               |
169 | 93 | relogcld 22215 |
. . . . . 6
    
        |
170 | | nndivre 10472 |
. . . . . . 7
     
         |
171 | 165, 46, 170 | sylancl 662 |
. . . . . 6
         |
172 | | relogexp 22187 |
. . . . . . . . 9
       
                             |
173 | 93, 94, 172 | sylancl 662 |
. . . . . . . 8
                   
         |
174 | 96 | rpred 11142 |
. . . . . . . . . 10
             |
175 | 119 | rpred 11142 |
. . . . . . . . . 10
                 ;                      |
176 | 174, 118 | ltaddrpd 11171 |
. . . . . . . . . 10
                           ;                      |
177 | | rpexpcl 12005 |
. . . . . . . . . . . . . 14
                     |
178 | 84, 90, 177 | sylancl 662 |
. . . . . . . . . . . . 13
    
        |
179 | 175, 178 | ltaddrpd 11171 |
. . . . . . . . . . . 12
                 ;                                     ;                                 |
180 | 87 | recnd 9527 |
. . . . . . . . . . . . . 14
    
        |
181 | 119 | rpcnd 11144 |
. . . . . . . . . . . . . 14
                 ;                      |
182 | 180, 181 | addcomd 9686 |
. . . . . . . . . . . . 13
                            ;                                      ;                                 |
183 | 15, 182 | syl5eq 2507 |
. . . . . . . . . . . 12
                  ;                                 |
184 | 179, 183 | breqtrrd 4429 |
. . . . . . . . . . 11
                 ;                      |
185 | 175, 17, 22, 184, 23 | ltletrd 9646 |
. . . . . . . . . 10
                 ;                      |
186 | 174, 175,
22, 176, 185 | lttrd 9647 |
. . . . . . . . 9
             |
187 | | logltb 22191 |
. . . . . . . . . 10
           

                                |
188 | 96, 24, 187 | syl2anc 661 |
. . . . . . . . 9
                                 |
189 | 186, 188 | mpbid 210 |
. . . . . . . 8
                     |
190 | 173, 189 | eqbrtrrd 4425 |
. . . . . . 7
                   |
191 | | ltmuldiv2 10318 |
. . . . . . . 8
     
                  
          
                   |
192 | 169, 165,
74, 191 | syl3anc 1219 |
. . . . . . 7
      
          
                   |
193 | 190, 192 | mpbid 210 |
. . . . . 6
    
              |
194 | 169, 171,
161, 193 | ltdiv1dd 11195 |
. . . . 5
     
                         |
195 | 88, 92 | relogmuld 22217 |
. . . . . . . 8
    
                      |
196 | | relogexp 22187 |
. . . . . . . . . 10
                   |
197 | 89, 90, 196 | sylancl 662 |
. . . . . . . . 9
                 |
198 | 197 | oveq2d 6219 |
. . . . . . . 8
                             |
199 | 195, 198 | eqtrd 2495 |
. . . . . . 7
    
                    |
200 | 199 | oveq1d 6218 |
. . . . . 6
     
                               |
201 | 158 | recnd 9527 |
. . . . . . 7
       |
202 | | 2cnd 10509 |
. . . . . . . 8
   |
203 | 161 | rpcnd 11144 |
. . . . . . . 8
       |
204 | 202, 203 | mulcld 9521 |
. . . . . . 7
         |
205 | 161 | rpcnne0d 11151 |
. . . . . . 7
             |
206 | | divdir 10132 |
. . . . . . 7
                                                                   |
207 | 201, 204,
205, 206 | syl3anc 1219 |
. . . . . 6
                                             |
208 | 205 | simprd 463 |
. . . . . . . 8
       |
209 | 202, 203,
208 | divcan4d 10228 |
. . . . . . 7
               |
210 | 209 | oveq2d 6219 |
. . . . . 6
                                       |
211 | 200, 207,
210 | 3eqtrd 2499 |
. . . . 5
     
                         |
212 | 165 | recnd 9527 |
. . . . . 6
       |
213 | | rpcnne0 11123 |
. . . . . . 7

    |
214 | 48, 213 | mp1i 12 |
. . . . . 6
     |
215 | | divdiv32 10154 |
. . . . . 6
                  
                          |
216 | 212, 214,
205, 215 | syl3anc 1219 |
. . . . 5
                           |
217 | 194, 211,
216 | 3brtr3d 4432 |
. . . 4
                           |
218 | 164, 168,
217 | ltled 9637 |
. . 3
                           |
219 | 115 | rpred 11142 |
. . . . 5
       |
220 | 108, 103 | rpdivcld 11159 |
. . . . . . 7
            ;     |
221 | 220 | rpred 11142 |
. . . . . 6
            ;     |
222 | 221, 165 | remulcld 9529 |
. . . . 5
             ;          |
223 | 115 | rpcnd 11144 |
. . . . . . . . 9
       |
224 | 108 | rpcnne0d 11151 |
. . . . . . . . 9
               
         |
225 | 103 | rpcnne0d 11151 |
. . . . . . . . 9
  ;  ;     |
226 | | divdiv2 10158 |
. . . . . . . . 9
                    
        ;  ;                    ;          ;                |
227 | 223, 224,
225, 226 | syl3anc 1219 |
. . . . . . . 8
          
      ;          ;                |
228 | 103 | rpcnd 11144 |
. . . . . . . . . 10
 ;    |
229 | 223, 228 | mulcomd 9522 |
. . . . . . . . 9
      ;    ;         |
230 | 229 | oveq1d 6218 |
. . . . . . . 8
       ;                ;                    |
231 | | div23 10128 |
. . . . . . . . 9
  ;                    
       
  ;                    ;                    |
232 | 228, 223,
224, 231 | syl3anc 1219 |
. . . . . . . 8
   ;                    ;                    |
233 | 227, 230,
232 | 3eqtrd 2499 |
. . . . . . 7
          
      ;      ;                    |
234 | 117 | reefcld 13495 |
. . . . . . . . . 10
      ;                     |
235 | 234, 96 | ltaddrp2d 11172 |
. . . . . . . . . 10
      ;                                   ;                      |
236 | 234, 175,
22, 235, 185 | lttrd 9647 |
. . . . . . . . 9
      ;                     |
237 | 24 | reeflogd 22216 |
. . . . . . . . 9
           |
238 | 236, 237 | breqtrrd 4429 |
. . . . . . . 8
      ;                             |
239 | | eflt 13523 |
. . . . . . . . 9
    ;                          ;                     
     ;                              |
240 | 117, 165,
239 | syl2anc 661 |
. . . . . . . 8
    ;                     
     ;                              |
241 | 238, 240 | mpbird 232 |
. . . . . . 7
   ;                        |
242 | 233, 241 | eqbrtrd 4423 |
. . . . . 6
          
      ;          |
243 | 219, 165,
220 | ltdivmuld 11189 |
. . . . . 6
                  ;                        ;           |
244 | 242, 243 | mpbid 210 |
. . . . 5
    
     
      ;          |
245 | 219, 222,
244 | ltled 9637 |
. . . 4
    
     
      ;          |
246 | 104 | rpcnd 11144 |
. . . . . 6
     |
247 | 107 | rpcnd 11144 |
. . . . . 6
         |
248 | | divass 10127 |
. . . . . 6
    
      ;  ;               ;             ;      |
249 | 246, 247,
225, 248 | syl3anc 1219 |
. . . . 5
            ;             ;      |
250 | 249 | oveq1d 6218 |
. . . 4
             ;                   ;           |
251 | 245, 250 | breqtrd 4427 |
. . 3
    
           ;           |
252 | 157, 218,
251 | 3jca 1168 |
. 2
                                     
           ;            |
253 | 24, 156, 252 | 3jca 1168 |
1
  
             
 
                                           ;             |