Step | Hyp | Ref
| Expression |
1 | | iblspltprt.3 |
. . . 4
    
    |
2 | | eluzelz 11192 |
. . . 4
    
 
  |
3 | 1, 2 | syl 17 |
. . 3
   |
4 | | eluzle 11195 |
. . . 4
    
 
    |
5 | 1, 4 | syl 17 |
. . 3
  
  |
6 | 3 | zred 11063 |
. . . 4
   |
7 | 6 | leidd 10201 |
. . 3

  |
8 | | iblspltprt.2 |
. . . . 5
   |
9 | 8 | peano2zd 11066 |
. . . 4
     |
10 | | elfz1 11815 |
. . . 4
   
          
    |
11 | 9, 3, 10 | syl2anc 673 |
. . 3
          
    |
12 | 3, 5, 7, 11 | mpbir3and 1213 |
. 2
         |
13 | | fveq2 5879 |
. . . . . . 7
          
    |
14 | 13 | oveq2d 6324 |
. . . . . 6
         ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)    
     |
15 | 14 | mpteq1d 4477 |
. . . . 5
          ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)    
      |
16 | 15 | eleq1d 2533 |
. . . 4
           ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)             |
17 | 16 | imbi2d 323 |
. . 3
    
       ![[,] [,]](_icc.gif)         
       ![[,] [,]](_icc.gif)    
         |
18 | | fveq2 5879 |
. . . . . . 7
           |
19 | 18 | oveq2d 6324 |
. . . . . 6
       ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)        |
20 | 19 | mpteq1d 4477 |
. . . . 5
        ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)         |
21 | 20 | eleq1d 2533 |
. . . 4
         ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)           |
22 | 21 | imbi2d 323 |
. . 3
  
       ![[,] [,]](_icc.gif)         
       ![[,] [,]](_icc.gif)            |
23 | | fveq2 5879 |
. . . . . . 7
               |
24 | 23 | oveq2d 6324 |
. . . . . 6
         ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)          |
25 | 24 | mpteq1d 4477 |
. . . . 5
          ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)           |
26 | 25 | eleq1d 2533 |
. . . 4
           ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)             |
27 | 26 | imbi2d 323 |
. . 3
    
       ![[,] [,]](_icc.gif)         
       ![[,] [,]](_icc.gif)              |
28 | | fveq2 5879 |
. . . . . . 7
           |
29 | 28 | oveq2d 6324 |
. . . . . 6
       ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)        |
30 | 29 | mpteq1d 4477 |
. . . . 5
        ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)         |
31 | 30 | eleq1d 2533 |
. . . 4
         ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)           |
32 | 31 | imbi2d 323 |
. . 3
  
       ![[,] [,]](_icc.gif)         
       ![[,] [,]](_icc.gif)            |
33 | | uzid 11197 |
. . . . . . 7
       |
34 | 8, 33 | syl 17 |
. . . . . 6
       |
35 | 8 | zred 11063 |
. . . . . . 7
   |
36 | | 1red 9676 |
. . . . . . . 8
   |
37 | 35, 36 | readdcld 9688 |
. . . . . . 7
     |
38 | 35 | ltp1d 10559 |
. . . . . . 7
     |
39 | 35, 37, 6, 38, 5 | ltletrd 9812 |
. . . . . 6
   |
40 | | elfzo2 11950 |
. . . . . 6
  ..^     
   |
41 | 34, 3, 39, 40 | syl3anbrc 1214 |
. . . . 5
  ..^   |
42 | | fveq2 5879 |
. . . . . . . . . 10
           |
43 | | oveq1 6315 |
. . . . . . . . . . 11
       |
44 | 43 | fveq2d 5883 |
. . . . . . . . . 10
          
    |
45 | 42, 44 | oveq12d 6326 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)    
     |
46 | 45 | mpteq1d 4477 |
. . . . . . . 8
        ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)    
      |
47 | 46 | eleq1d 2533 |
. . . . . . 7
         ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)             |
48 | 47 | imbi2d 323 |
. . . . . 6
  
       ![[,] [,]](_icc.gif)           
       ![[,] [,]](_icc.gif)    
         |
49 | | iblspltprt.7 |
. . . . . . 7
 
 ..^         ![[,] [,]](_icc.gif)            |
50 | 49 | expcom 442 |
. . . . . 6
  ..^
        ![[,] [,]](_icc.gif)             |
51 | 48, 50 | vtoclga 3099 |
. . . . 5
  ..^
        ![[,] [,]](_icc.gif)             |
52 | 41, 51 | mpcom 36 |
. . . 4
        ![[,] [,]](_icc.gif)            |
53 | 52 | a1i 11 |
. . 3
    
 
        ![[,] [,]](_icc.gif)             |
54 | | nfv 1769 |
. . . . . 6
    ..^  |
55 | | iblspltprt.1 |
. . . . . . 7
   |
56 | | nfmpt1 4485 |
. . . . . . . 8
         ![[,] [,]](_icc.gif)        |
57 | 56 | nfel1 2626 |
. . . . . . 7
         ![[,] [,]](_icc.gif)         |
58 | 55, 57 | nfim 2023 |
. . . . . 6
          ![[,] [,]](_icc.gif)          |
59 | 54, 58, 55 | nf3an 2033 |
. . . . 5
      ..^ 
       ![[,] [,]](_icc.gif)           |
60 | | simp3 1032 |
. . . . . 6
     ..^         ![[,] [,]](_icc.gif)         
  |
61 | | simp1 1030 |
. . . . . 6
     ..^         ![[,] [,]](_icc.gif)         
   ..^   |
62 | 35 | leidd 10201 |
. . . . . . . . . . . . 13

  |
63 | 35, 6, 39 | ltled 9800 |
. . . . . . . . . . . . 13

  |
64 | | elfz1 11815 |
. . . . . . . . . . . . . 14
 
      
    |
65 | 8, 3, 64 | syl2anc 673 |
. . . . . . . . . . . . 13
      
    |
66 | 8, 62, 63, 65 | mpbir3and 1213 |
. . . . . . . . . . . 12
       |
67 | 66 | ancli 560 |
. . . . . . . . . . . 12
         |
68 | | eleq1 2537 |
. . . . . . . . . . . . . . 15
     
       |
69 | 68 | anbi2d 718 |
. . . . . . . . . . . . . 14
  
    
         |
70 | 42 | eleq1d 2533 |
. . . . . . . . . . . . . 14
     
       |
71 | 69, 70 | imbi12d 327 |
. . . . . . . . . . . . 13
   
           
             |
72 | | iblspltprt.4 |
. . . . . . . . . . . . 13
 
    
      |
73 | 71, 72 | vtoclg 3093 |
. . . . . . . . . . . 12
      
            |
74 | 66, 67, 73 | sylc 61 |
. . . . . . . . . . 11
       |
75 | 74 | adantr 472 |
. . . . . . . . . 10
 
   ..^ 
      |
76 | 75 | rexrd 9708 |
. . . . . . . . 9
 
   ..^ 
      |
77 | | simpl 464 |
. . . . . . . . . . 11
 
   ..^ 
  |
78 | | elfzoelz 11947 |
. . . . . . . . . . . . 13
    ..^
  |
79 | 78 | adantl 473 |
. . . . . . . . . . . 12
 
   ..^ 
  |
80 | 35 | adantr 472 |
. . . . . . . . . . . . 13
 
   ..^ 
  |
81 | 79 | zred 11063 |
. . . . . . . . . . . . 13
 
   ..^ 
  |
82 | 37 | adantr 472 |
. . . . . . . . . . . . . 14
 
   ..^ 
    |
83 | 38 | adantr 472 |
. . . . . . . . . . . . . 14
 
   ..^ 
    |
84 | | elfzole1 11955 |
. . . . . . . . . . . . . . 15
    ..^
    |
85 | 84 | adantl 473 |
. . . . . . . . . . . . . 14
 
   ..^ 
    |
86 | 80, 82, 81, 83, 85 | ltletrd 9812 |
. . . . . . . . . . . . 13
 
   ..^ 
  |
87 | 80, 81, 86 | ltled 9800 |
. . . . . . . . . . . 12
 
   ..^ 
  |
88 | 6 | adantr 472 |
. . . . . . . . . . . . 13
 
   ..^ 
  |
89 | | elfzolt2 11956 |
. . . . . . . . . . . . . 14
    ..^
  |
90 | 89 | adantl 473 |
. . . . . . . . . . . . 13
 
   ..^ 
  |
91 | 81, 88, 90 | ltled 9800 |
. . . . . . . . . . . 12
 
   ..^ 
  |
92 | 8, 3 | jca 541 |
. . . . . . . . . . . . . 14
     |
93 | 92 | adantr 472 |
. . . . . . . . . . . . 13
 
   ..^ 
    |
94 | | elfz1 11815 |
. . . . . . . . . . . . 13
 
      
    |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . 12
 
   ..^ 
     
    |
96 | 79, 87, 91, 95 | mpbir3and 1213 |
. . . . . . . . . . 11
 
   ..^ 
      |
97 | | eleq1 2537 |
. . . . . . . . . . . . . 14
     
       |
98 | 97 | anbi2d 718 |
. . . . . . . . . . . . 13
  
    
         |
99 | | fveq2 5879 |
. . . . . . . . . . . . . 14
           |
100 | 99 | eleq1d 2533 |
. . . . . . . . . . . . 13
     
       |
101 | 98, 100 | imbi12d 327 |
. . . . . . . . . . . 12
   
           
             |
102 | 101, 72 | chvarv 2120 |
. . . . . . . . . . 11
 
    
      |
103 | 77, 96, 102 | syl2anc 673 |
. . . . . . . . . 10
 
   ..^ 
      |
104 | 103 | rexrd 9708 |
. . . . . . . . 9
 
   ..^ 
      |
105 | 79 | peano2zd 11066 |
. . . . . . . . . . . 12
 
   ..^ 
    |
106 | 105 | zred 11063 |
. . . . . . . . . . . . 13
 
   ..^ 
    |
107 | | 1red 9676 |
. . . . . . . . . . . . . . 15
 
   ..^ 
  |
108 | 80, 81, 107, 86 | ltadd1dd 10245 |
. . . . . . . . . . . . . 14
 
   ..^ 
      |
109 | 80, 82, 106, 83, 108 | lttrd 9813 |
. . . . . . . . . . . . 13
 
   ..^ 
    |
110 | 80, 106, 109 | ltled 9800 |
. . . . . . . . . . . 12
 
   ..^ 
    |
111 | | zltp1le 11010 |
. . . . . . . . . . . . . 14
 
       |
112 | 78, 3, 111 | syl2anr 486 |
. . . . . . . . . . . . 13
 
   ..^ 
      |
113 | 90, 112 | mpbid 215 |
. . . . . . . . . . . 12
 
   ..^ 
    |
114 | | elfz1 11815 |
. . . . . . . . . . . . 13
 
          
   
    |
115 | 93, 114 | syl 17 |
. . . . . . . . . . . 12
 
   ..^ 
      
           |
116 | 105, 110,
113, 115 | mpbir3and 1213 |
. . . . . . . . . . 11
 
   ..^ 
        |
117 | 77, 116 | jca 541 |
. . . . . . . . . . 11
 
   ..^ 
          |
118 | | eleq1 2537 |
. . . . . . . . . . . . . 14
       
         |
119 | 118 | anbi2d 718 |
. . . . . . . . . . . . 13
    
    
           |
120 | | fveq2 5879 |
. . . . . . . . . . . . . 14
               |
121 | 120 | eleq1d 2533 |
. . . . . . . . . . . . 13
       
         |
122 | 119, 121 | imbi12d 327 |
. . . . . . . . . . . 12
     
                             |
123 | 122, 72 | vtoclg 3093 |
. . . . . . . . . . 11
        
                |
124 | 116, 117,
123 | sylc 61 |
. . . . . . . . . 10
 
   ..^ 
        |
125 | 124 | rexrd 9708 |
. . . . . . . . 9
 
   ..^ 
        |
126 | | eluz 11196 |
. . . . . . . . . . . 12
 
     
   |
127 | 8, 78, 126 | syl2an 485 |
. . . . . . . . . . 11
 
   ..^ 
        |
128 | 87, 127 | mpbird 240 |
. . . . . . . . . 10
 
   ..^ 
      |
129 | | simpll 768 |
. . . . . . . . . . 11
      ..^         |
130 | | elfzelz 11826 |
. . . . . . . . . . . . 13
       |
131 | 130 | adantl 473 |
. . . . . . . . . . . 12
      ..^         |
132 | | elfzle1 11828 |
. . . . . . . . . . . . 13
       |
133 | 132 | adantl 473 |
. . . . . . . . . . . 12
      ..^         |
134 | 131 | zred 11063 |
. . . . . . . . . . . . 13
      ..^         |
135 | 129, 6 | syl 17 |
. . . . . . . . . . . . 13
      ..^         |
136 | 81 | adantr 472 |
. . . . . . . . . . . . . 14
      ..^         |
137 | | elfzle2 11829 |
. . . . . . . . . . . . . . 15
       |
138 | 137 | adantl 473 |
. . . . . . . . . . . . . 14
      ..^         |
139 | 90 | adantr 472 |
. . . . . . . . . . . . . 14
      ..^         |
140 | 134, 136,
135, 138, 139 | lelttrd 9810 |
. . . . . . . . . . . . 13
      ..^         |
141 | 134, 135,
140 | ltled 9800 |
. . . . . . . . . . . 12
      ..^         |
142 | | elfz1 11815 |
. . . . . . . . . . . . 13
 
      
    |
143 | 129, 92, 142 | 3syl 18 |
. . . . . . . . . . . 12
      ..^           

    |
144 | 131, 133,
141, 143 | mpbir3and 1213 |
. . . . . . . . . . 11
      ..^             |
145 | 129, 144,
72 | syl2anc 673 |
. . . . . . . . . 10
      ..^             |
146 | | simpll 768 |
. . . . . . . . . . . 12
      ..^           |
147 | | elfzelz 11826 |
. . . . . . . . . . . . . 14
         |
148 | 147 | adantl 473 |
. . . . . . . . . . . . 13
      ..^           |
149 | | elfzle1 11828 |
. . . . . . . . . . . . . 14
         |
150 | 149 | adantl 473 |
. . . . . . . . . . . . 13
      ..^           |
151 | 148 | zred 11063 |
. . . . . . . . . . . . . 14
      ..^           |
152 | 146, 6 | syl 17 |
. . . . . . . . . . . . . 14
      ..^           |
153 | 81 | adantr 472 |
. . . . . . . . . . . . . . . 16
      ..^           |
154 | | 1red 9676 |
. . . . . . . . . . . . . . . 16
      ..^           |
155 | 153, 154 | resubcld 10068 |
. . . . . . . . . . . . . . 15
      ..^             |
156 | | elfzle2 11829 |
. . . . . . . . . . . . . . . 16
           |
157 | 156 | adantl 473 |
. . . . . . . . . . . . . . 15
      ..^             |
158 | 78 | zred 11063 |
. . . . . . . . . . . . . . . . . 18
    ..^
  |
159 | | 1red 9676 |
. . . . . . . . . . . . . . . . . 18
    ..^
  |
160 | 158, 159 | resubcld 10068 |
. . . . . . . . . . . . . . . . 17
    ..^
    |
161 | | elfzoel2 11946 |
. . . . . . . . . . . . . . . . . 18
    ..^
  |
162 | 161 | zred 11063 |
. . . . . . . . . . . . . . . . 17
    ..^
  |
163 | 158 | ltm1d 10561 |
. . . . . . . . . . . . . . . . 17
    ..^
    |
164 | 160, 158,
162, 163, 89 | lttrd 9813 |
. . . . . . . . . . . . . . . 16
    ..^
    |
165 | 164 | ad2antlr 741 |
. . . . . . . . . . . . . . 15
      ..^             |
166 | 151, 155,
152, 157, 165 | lelttrd 9810 |
. . . . . . . . . . . . . 14
      ..^           |
167 | 151, 152,
166 | ltled 9800 |
. . . . . . . . . . . . 13
      ..^           |
168 | 146, 92, 142 | 3syl 18 |
. . . . . . . . . . . . 13
      ..^             

    |
169 | 148, 150,
167, 168 | mpbir3and 1213 |
. . . . . . . . . . . 12
      ..^               |
170 | 146, 169,
72 | syl2anc 673 |
. . . . . . . . . . 11
      ..^               |
171 | 148 | peano2zd 11066 |
. . . . . . . . . . . . 13
      ..^             |
172 | | elfzel1 11825 |
. . . . . . . . . . . . . . . 16
         |
173 | 172 | zred 11063 |
. . . . . . . . . . . . . . 15
         |
174 | 147 | zred 11063 |
. . . . . . . . . . . . . . . 16
         |
175 | | 1red 9676 |
. . . . . . . . . . . . . . . 16
         |
176 | 174, 175 | readdcld 9688 |
. . . . . . . . . . . . . . 15
           |
177 | 174 | ltp1d 10559 |
. . . . . . . . . . . . . . . 16
           |
178 | 173, 174,
176, 149, 177 | lelttrd 9810 |
. . . . . . . . . . . . . . 15
           |
179 | 173, 176,
178 | ltled 9800 |
. . . . . . . . . . . . . 14
           |
180 | 179 | adantl 473 |
. . . . . . . . . . . . 13
      ..^             |
181 | 146, 1, 2 | 3syl 18 |
. . . . . . . . . . . . . . 15
      ..^           |
182 | | zltp1le 11010 |
. . . . . . . . . . . . . . 15
 
       |
183 | 148, 181,
182 | syl2anc 673 |
. . . . . . . . . . . . . 14
      ..^         
     |
184 | 166, 183 | mpbid 215 |
. . . . . . . . . . . . 13
      ..^             |
185 | | elfz1 11815 |
. . . . . . . . . . . . . 14
 
          
   
    |
186 | 146, 92, 185 | 3syl 18 |
. . . . . . . . . . . . 13
      ..^               
           |
187 | 171, 180,
184, 186 | mpbir3and 1213 |
. . . . . . . . . . . 12
      ..^                 |
188 | 146, 187 | jca 541 |
. . . . . . . . . . . 12
      ..^                   |
189 | | eleq1 2537 |
. . . . . . . . . . . . . . 15
       
         |
190 | 189 | anbi2d 718 |
. . . . . . . . . . . . . 14
    
    
           |
191 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
               |
192 | 191 | eleq1d 2533 |
. . . . . . . . . . . . . 14
       
         |
193 | 190, 192 | imbi12d 327 |
. . . . . . . . . . . . 13
     
                             |
194 | 193, 102 | vtoclg 3093 |
. . . . . . . . . . . 12
        
                |
195 | 187, 188,
194 | sylc 61 |
. . . . . . . . . . 11
      ..^                 |
196 | | elfzuz 11822 |
. . . . . . . . . . . . . 14
             |
197 | 196 | adantl 473 |
. . . . . . . . . . . . 13
      ..^               |
198 | | elfzo2 11950 |
. . . . . . . . . . . . 13
  ..^     
   |
199 | 197, 181,
166, 198 | syl3anbrc 1214 |
. . . . . . . . . . . 12
      ..^          ..^   |
200 | | iblspltprt.5 |
. . . . . . . . . . . 12
 
 ..^              |
201 | 146, 199,
200 | syl2anc 673 |
. . . . . . . . . . 11
      ..^                     |
202 | 170, 195,
201 | ltled 9800 |
. . . . . . . . . 10
      ..^                     |
203 | 128, 145,
202 | monoord 12281 |
. . . . . . . . 9
 
   ..^ 
          |
204 | 161 | adantl 473 |
. . . . . . . . . . . 12
 
   ..^ 
  |
205 | | elfzo2 11950 |
. . . . . . . . . . . 12
  ..^     
   |
206 | 128, 204,
90, 205 | syl3anbrc 1214 |
. . . . . . . . . . 11
 
   ..^ 
 ..^   |
207 | | eleq1 2537 |
. . . . . . . . . . . . . 14
   ..^
 ..^    |
208 | 207 | anbi2d 718 |
. . . . . . . . . . . . 13
  
 ..^  
 ..^     |
209 | | oveq1 6315 |
. . . . . . . . . . . . . . 15
       |
210 | 209 | fveq2d 5883 |
. . . . . . . . . . . . . 14
               |
211 | 99, 210 | breq12d 4408 |
. . . . . . . . . . . . 13
     
     
             |
212 | 208, 211 | imbi12d 327 |
. . . . . . . . . . . 12
   
 ..^     
      
   ..^                |
213 | 212, 200 | chvarv 2120 |
. . . . . . . . . . 11
 
 ..^              |
214 | 77, 206, 213 | syl2anc 673 |
. . . . . . . . . 10
 
   ..^ 
            |
215 | 103, 124,
214 | ltled 9800 |
. . . . . . . . 9
 
   ..^ 
            |
216 | | iccintsng 37720 |
. . . . . . . . 9
                      
                       ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)                 |
217 | 76, 104, 125, 203, 215, 216 | syl32anc 1300 |
. . . . . . . 8
 
   ..^ 
       ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)                 |
218 | 217 | fveq2d 5883 |
. . . . . . 7
 
   ..^ 
           ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)                       |
219 | | ovolsn 22526 |
. . . . . . . 8
                  |
220 | 103, 219 | syl 17 |
. . . . . . 7
 
   ..^ 
             |
221 | 218, 220 | eqtrd 2505 |
. . . . . 6
 
   ..^ 
           ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)            |
222 | 60, 61, 221 | syl2anc 673 |
. . . . 5
     ..^         ![[,] [,]](_icc.gif)         
           ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)            |
223 | 75, 124, 103, 203, 215 | eliccd 37697 |
. . . . . . . 8
 
   ..^ 
          ![[,] [,]](_icc.gif)          |
224 | 75, 124, 223 | 3jca 1210 |
. . . . . . 7
 
   ..^ 
                     ![[,] [,]](_icc.gif)           |
225 | 60, 61, 224 | syl2anc 673 |
. . . . . 6
     ..^         ![[,] [,]](_icc.gif)         
                     ![[,] [,]](_icc.gif)           |
226 | | iccsplit 11791 |
. . . . . 6
                      ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)           |
227 | 225, 226 | syl 17 |
. . . . 5
     ..^         ![[,] [,]](_icc.gif)         
      ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)           |
228 | | simpl3 1035 |
. . . . . 6
      ..^ 
       ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)           |
229 | | simpl1 1033 |
. . . . . 6
      ..^ 
       ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)            ..^   |
230 | | simpr 468 |
. . . . . 6
      ..^ 
       ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)          |
231 | | simp1 1030 |
. . . . . . 7
 
   ..^       ![[,] [,]](_icc.gif)        
  |
232 | | eliccxr 37708 |
. . . . . . . . 9
       ![[,] [,]](_icc.gif)          |
233 | 232 | 3ad2ant3 1053 |
. . . . . . . 8
 
   ..^       ![[,] [,]](_icc.gif)        
  |
234 | 74 | rexrd 9708 |
. . . . . . . . . 10
       |
235 | 234 | 3ad2ant1 1051 |
. . . . . . . . 9
 
   ..^       ![[,] [,]](_icc.gif)        
      |
236 | 125 | 3adant3 1050 |
. . . . . . . . 9
 
   ..^       ![[,] [,]](_icc.gif)        
        |
237 | | simp3 1032 |
. . . . . . . . 9
 
   ..^       ![[,] [,]](_icc.gif)        
      ![[,] [,]](_icc.gif)          |
238 | | iccgelb 11716 |
. . . . . . . . 9
           
      ![[,] [,]](_icc.gif)               |
239 | 235, 236,
237, 238 | syl3anc 1292 |
. . . . . . . 8
 
   ..^       ![[,] [,]](_icc.gif)        
      |
240 | 75, 124 | jca 541 |
. . . . . . . . . . 11
 
   ..^ 
              |
241 | 240 | 3adant3 1050 |
. . . . . . . . . 10
 
   ..^       ![[,] [,]](_icc.gif)        
              |
242 | | iccssre 11741 |
. . . . . . . . . . 11
                   ![[,] [,]](_icc.gif)       
  |
243 | 242 | sseld 3417 |
. . . . . . . . . 10
                    ![[,] [,]](_icc.gif)           |
244 | 241, 237,
243 | sylc 61 |
. . . . . . . . 9
 
   ..^       ![[,] [,]](_icc.gif)        
  |
245 | 124 | 3adant3 1050 |
. . . . . . . . 9
 
   ..^       ![[,] [,]](_icc.gif)        
        |
246 | | elfz1 11815 |
. . . . . . . . . . . . . 14
 
      
    |
247 | 8, 3, 246 | syl2anc 673 |
. . . . . . . . . . . . 13
      
    |
248 | 3, 63, 7, 247 | mpbir3and 1213 |
. . . . . . . . . . . 12
       |
249 | 248 | ancli 560 |
. . . . . . . . . . 11
         |
250 | | eleq1 2537 |
. . . . . . . . . . . . . 14
     
       |
251 | 250 | anbi2d 718 |
. . . . . . . . . . . . 13
  
    
         |
252 | | fveq2 5879 |
. . . . . . . . . . . . . 14
           |
253 | 252 | eleq1d 2533 |
. . . . . . . . . . . . 13
     
       |
254 | 251, 253 | imbi12d 327 |
. . . . . . . . . . . 12
   
           
             |
255 | 254, 72 | vtoclg 3093 |
. . . . . . . . . . 11
  
            |
256 | 3, 249, 255 | sylc 61 |
. . . . . . . . . 10
       |
257 | 256 | 3ad2ant1 1051 |
. . . . . . . . 9
 
   ..^       ![[,] [,]](_icc.gif)        
      |
258 | | elicc1 11705 |
. . . . . . . . . . . 12
                    ![[,] [,]](_icc.gif)       
    
          |
259 | 235, 236,
258 | syl2anc 673 |
. . . . . . . . . . 11
 
   ..^       ![[,] [,]](_icc.gif)        
       ![[,] [,]](_icc.gif)        
   
          |
260 | 237, 259 | mpbid 215 |
. . . . . . . . . 10
 
   ..^       ![[,] [,]](_icc.gif)        
    
         |
261 | 260 | simp3d 1044 |
. . . . . . . . 9
 
   ..^       ![[,] [,]](_icc.gif)        
        |
262 | | elfzop1le2 37592 |
. . . . . . . . . . . . 13
    ..^
    |
263 | 78 | peano2zd 11066 |
. . . . . . . . . . . . . 14
    ..^
    |
264 | | eluz 11196 |
. . . . . . . . . . . . . 14
   
       
     |
265 | 263, 161,
264 | syl2anc 673 |
. . . . . . . . . . . . 13
    ..^
        
   |
266 | 262, 265 | mpbird 240 |
. . . . . . . . . . . 12
    ..^
        |
267 | 266 | adantl 473 |
. . . . . . . . . . 11
 
   ..^ 
        |
268 | | simpll 768 |
. . . . . . . . . . . 12
      ..^           |
269 | | elfzelz 11826 |
. . . . . . . . . . . . . 14
         |
270 | 269 | adantl 473 |
. . . . . . . . . . . . 13
      ..^           |
271 | 268, 35 | syl 17 |
. . . . . . . . . . . . . 14
      ..^           |
272 | 270 | zred 11063 |
. . . . . . . . . . . . . 14
      ..^           |
273 | 81 | adantr 472 |
. . . . . . . . . . . . . . 15
      ..^           |
274 | 86 | adantr 472 |
. . . . . . . . . . . . . . 15
      ..^           |
275 | 158 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     ..^          |
276 | | 1red 9676 |
. . . . . . . . . . . . . . . . . 18
     ..^          |
277 | 275, 276 | readdcld 9688 |
. . . . . . . . . . . . . . . . 17
     ..^            |
278 | 269 | zred 11063 |
. . . . . . . . . . . . . . . . . 18
         |
279 | 278 | adantl 473 |
. . . . . . . . . . . . . . . . 17
     ..^          |
280 | 275 | ltp1d 10559 |
. . . . . . . . . . . . . . . . 17
     ..^            |
281 | | elfzle1 11828 |
. . . . . . . . . . . . . . . . . 18
           |
282 | 281 | adantl 473 |
. . . . . . . . . . . . . . . . 17
     ..^            |
283 | 275, 277,
279, 280, 282 | ltletrd 9812 |
. . . . . . . . . . . . . . . 16
     ..^          |
284 | 283 | adantll 728 |
. . . . . . . . . . . . . . 15
      ..^           |
285 | 271, 273,
272, 274, 284 | lttrd 9813 |
. . . . . . . . . . . . . 14
      ..^           |
286 | 271, 272,
285 | ltled 9800 |
. . . . . . . . . . . . 13
      ..^           |
287 | | elfzle2 11829 |
. . . . . . . . . . . . . 14
         |
288 | 287 | adantl 473 |
. . . . . . . . . . . . 13
      ..^           |
289 | 268, 92, 142 | 3syl 18 |
. . . . . . . . . . . . 13
      ..^             

    |
290 | 270, 286,
288, 289 | mpbir3and 1213 |
. . . . . . . . . . . 12
      ..^               |
291 | 268, 290,
72 | syl2anc 673 |
. . . . . . . . . . 11
      ..^               |
292 | | simpll 768 |
. . . . . . . . . . . . 13
      ..^       
     |
293 | | elfzelz 11826 |
. . . . . . . . . . . . . . 15
           |
294 | 293 | adantl 473 |
. . . . . . . . . . . . . 14
      ..^       
     |
295 | 292, 35 | syl 17 |
. . . . . . . . . . . . . . 15
      ..^       
     |
296 | 294 | zred 11063 |
. . . . . . . . . . . . . . 15
      ..^       
     |
297 | 81 | adantr 472 |
. . . . . . . . . . . . . . . 16
      ..^       
     |
298 | 86 | adantr 472 |
. . . . . . . . . . . . . . . 16
      ..^       
     |
299 | 158 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
     ..^      
     |
300 | | 1red 9676 |
. . . . . . . . . . . . . . . . . . 19
     ..^      
     |
301 | 299, 300 | readdcld 9688 |
. . . . . . . . . . . . . . . . . 18
     ..^      
       |
302 | 293 | zred 11063 |
. . . . . . . . . . . . . . . . . . 19
           |
303 | 302 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
     ..^      
     |
304 | 299 | ltp1d 10559 |
. . . . . . . . . . . . . . . . . 18
     ..^      
       |
305 | | elfzle1 11828 |
. . . . . . . . . . . . . . . . . . 19
             |
306 | 305 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
     ..^      
       |
307 | 299, 301,
303, 304, 306 | ltletrd 9812 |
. . . . . . . . . . . . . . . . 17
     ..^      
     |
308 | 307 | adantll 728 |
. . . . . . . . . . . . . . . 16
      ..^       
     |
309 | 295, 297,
296, 298, 308 | lttrd 9813 |
. . . . . . . . . . . . . . 15
      ..^       
     |
310 | 295, 296,
309 | ltled 9800 |
. . . . . . . . . . . . . 14
      ..^       
     |
311 | 302 | adantl 473 |
. . . . . . . . . . . . . . . 16
 
     
     |
312 | 6 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
     
     |
313 | | 1red 9676 |
. . . . . . . . . . . . . . . . . 18
 
     
     |
314 | 312, 313 | resubcld 10068 |
. . . . . . . . . . . . . . . . 17
 
     
   
   |
315 | | elfzle2 11829 |
. . . . . . . . . . . . . . . . . 18
             |
316 | 315 | adantl 473 |
. . . . . . . . . . . . . . . . 17
 
     
       |
317 | 312 | ltm1d 10561 |
. . . . . . . . . . . . . . . . 17
 
     
   
   |
318 | 311, 314,
312, 316, 317 | lelttrd 9810 |
. . . . . . . . . . . . . . . 16
 
     
     |
319 | 311, 312,
318 | ltled 9800 |
. . . . . . . . . . . . . . 15
 
     
     |
320 | 319 | adantlr 729 |
. . . . . . . . . . . . . 14
      ..^       
     |
321 | 292, 92, 142 | 3syl 18 |
. . . . . . . . . . . . . 14
      ..^       
       

    |
322 | 294, 310,
320, 321 | mpbir3and 1213 |
. . . . . . . . . . . . 13
      ..^       
         |
323 | 292, 322,
72 | syl2anc 673 |
. . . . . . . . . . . 12
      ..^       
         |
324 | 294 | peano2zd 11066 |
. . . . . . . . . . . . . 14
      ..^       
       |
325 | 324 | zred 11063 |
. . . . . . . . . . . . . . 15
      ..^       
       |
326 | 303, 300 | readdcld 9688 |
. . . . . . . . . . . . . . . . . 18
     ..^      
       |
327 | 299, 303,
307 | ltled 9800 |
. . . . . . . . . . . . . . . . . . 19
     ..^      
     |
328 | 299, 303,
300, 327 | leadd1dd 10248 |
. . . . . . . . . . . . . . . . . 18
     ..^      
         |
329 | 299, 301,
326, 304, 328 | ltletrd 9812 |
. . . . . . . . . . . . . . . . 17
     ..^      
       |
330 | 329 | adantll 728 |
. . . . . . . . . . . . . . . 16
      ..^       
       |
331 | 295, 297,
325, 298, 330 | lttrd 9813 |
. . . . . . . . . . . . . . 15
      ..^       
       |
332 | 295, 325,
331 | ltled 9800 |
. . . . . . . . . . . . . 14
      ..^       
       |
333 | 293, 3, 182 | syl2anr 486 |
. . . . . . . . . . . . . . . 16
 
     
   
     |
334 | 318, 333 | mpbid 215 |
. . . . . . . . . . . . . . 15
 
     
       |
335 | 334 | adantlr 729 |
. . . . . . . . . . . . . 14
      ..^       
       |
336 | 292, 92, 185 | 3syl 18 |
. . . . . . . . . . . . . 14
      ..^       
         
           |
337 | 324, 332,
335, 336 | mpbir3and 1213 |
. . . . . . . . . . . . 13
      ..^       
           |
338 | 292, 337 | jca 541 |
. . . . . . . . . . . . 13
      ..^       
             |
339 | 337, 338,
194 | sylc 61 |
. . . . . . . . . . . 12
      ..^       
           |
340 | 292, 8 | syl 17 |
. . . . . . . . . . . . . . . 16
      ..^       
     |
341 | | eluz 11196 |
. . . . . . . . . . . . . . . 16
 
     
   |
342 | 340, 294,
341 | syl2anc 673 |
. . . . . . . . . . . . . . 15
      ..^       
       
   |
343 | 310, 342 | mpbird 240 |
. . . . . . . . . . . . . 14
      ..^       
         |
344 | 292, 1, 2 | 3syl 18 |
. . . . . . . . . . . . . 14
      ..^       
     |
345 | 318 | adantlr 729 |
. . . . . . . . . . . . . 14
      ..^       
     |
346 | 343, 344,
345, 198 | syl3anbrc 1214 |
. . . . . . . . . . . . 13
      ..^       
    ..^   |
347 | 292, 346,
200 | syl2anc 673 |
. . . . . . . . . . . 12
      ..^       
               |
348 | 323, 339,
347 | ltled 9800 |
. . . . . . . . . . 11
      ..^       
               |
349 | 267, 291,
348 | monoord 12281 |
. . . . . . . . . 10
 
   ..^ 
            |
350 | 349 | 3adant3 1050 |
. . . . . . . . 9
 
   ..^       ![[,] [,]](_icc.gif)        
            |
351 | 244, 245,
257, 261, 350 | letrd 9809 |
. . . . . . . 8
 
   ..^       ![[,] [,]](_icc.gif)        
      |
352 | 257 | rexrd 9708 |
. . . . . . . . 9
 
   ..^       ![[,] [,]](_icc.gif)        
      |
353 | | elicc1 11705 |
. . . . . . . . 9
                  ![[,] [,]](_icc.gif)     
    
        |
354 | 235, 352,
353 | syl2anc 673 |
. . . . . . . 8
 
   ..^       ![[,] [,]](_icc.gif)        
       ![[,] [,]](_icc.gif)      
   
        |
355 | 233, 239,
351, 354 | mpbir3and 1213 |
. . . . . . 7
 
   ..^       ![[,] [,]](_icc.gif)        
      ![[,] [,]](_icc.gif)        |
356 | | iblspltprt.6 |
. . . . . . 7
 
      ![[,] [,]](_icc.gif)         |
357 | 231, 355,
356 | syl2anc 673 |
. . . . . 6
 
   ..^       ![[,] [,]](_icc.gif)        
  |
358 | 228, 229,
230, 357 | syl3anc 1292 |
. . . . 5
      ..^ 
       ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)           |
359 | | simp2 1031 |
. . . . . 6
     ..^         ![[,] [,]](_icc.gif)         
        ![[,] [,]](_icc.gif)           |
360 | 60, 359 | mpd 15 |
. . . . 5
     ..^         ![[,] [,]](_icc.gif)         
       ![[,] [,]](_icc.gif)          |
361 | 60, 61 | jca 541 |
. . . . . 6
     ..^         ![[,] [,]](_icc.gif)         
    ..^    |
362 | 77, 206 | jca 541 |
. . . . . 6
 
   ..^ 
  ..^    |
363 | 99, 210 | oveq12d 6326 |
. . . . . . . . . 10
       ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)          |
364 | 363 | mpteq1d 4477 |
. . . . . . . . 9
        ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)           |
365 | 364 | eleq1d 2533 |
. . . . . . . 8
         ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)             |
366 | 208, 365 | imbi12d 327 |
. . . . . . 7
   
 ..^         ![[,] [,]](_icc.gif)          
   ..^         ![[,] [,]](_icc.gif)              |
367 | 366, 49 | chvarv 2120 |
. . . . . 6
 
 ..^         ![[,] [,]](_icc.gif)            |
368 | 361, 362,
367 | 3syl 18 |
. . . . 5
     ..^         ![[,] [,]](_icc.gif)         
       ![[,] [,]](_icc.gif)            |
369 | 59, 222, 227, 358, 360, 368 | iblsplitf 37944 |
. . . 4
     ..^         ![[,] [,]](_icc.gif)         
       ![[,] [,]](_icc.gif)            |
370 | 369 | 3exp 1230 |
. . 3
    ..^
         ![[,] [,]](_icc.gif)         
       ![[,] [,]](_icc.gif)              |
371 | 17, 22, 27, 32, 53, 370 | fzind2 12054 |
. 2
               ![[,] [,]](_icc.gif)           |
372 | 12, 371 | mpcom 36 |
1
        ![[,] [,]](_icc.gif)          |