Step | Hyp | Ref
| Expression |
1 | | itgspltprt.1 |
. . . . . 6
   |
2 | 1 | peano2zd 11043 |
. . . . 5
     |
3 | | itgspltprt.2 |
. . . . . 6
    
    |
4 | | eluzelz 11168 |
. . . . . 6
    
 
  |
5 | 3, 4 | syl 17 |
. . . . 5
   |
6 | 2, 5, 5 | 3jca 1188 |
. . . 4
   
   |
7 | | eluzle 11171 |
. . . . 5
    
 
    |
8 | 3, 7 | syl 17 |
. . . 4
  
  |
9 | | eluzelre 11169 |
. . . . . 6
    
 
  |
10 | 3, 9 | syl 17 |
. . . . 5
   |
11 | 10 | leidd 10180 |
. . . 4

  |
12 | 6, 8, 11 | jca32 538 |
. . 3
        
    |
13 | | elfz2 11791 |
. . 3
      
   
   
    |
14 | 12, 13 | sylibr 216 |
. 2
         |
15 | | fveq2 5865 |
. . . . . . 7
          
    |
16 | 15 | oveq2d 6306 |
. . . . . 6
         ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)    
     |
17 | 16 | itgeq1d 37833 |
. . . . 5
          ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)    
       |
18 | | oveq2 6298 |
. . . . . 6
    ..^  ..^     |
19 | 18 | sumeq1d 13767 |
. . . . 5
     ..^         ![[,] [,]](_icc.gif)            ..^           ![[,] [,]](_icc.gif)            |
20 | 17, 19 | eqeq12d 2466 |
. . . 4
           ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)    
       ..^           ![[,] [,]](_icc.gif)             |
21 | 20 | imbi2d 318 |
. . 3
    
       ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)            ..^           ![[,] [,]](_icc.gif)              |
22 | | fveq2 5865 |
. . . . . . 7
           |
23 | 22 | oveq2d 6306 |
. . . . . 6
       ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)        |
24 | 23 | itgeq1d 37833 |
. . . . 5
        ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)          |
25 | | oveq2 6298 |
. . . . . 6
  ..^  ..^   |
26 | 25 | sumeq1d 13767 |
. . . . 5
   ..^         ![[,] [,]](_icc.gif)            ..^         ![[,] [,]](_icc.gif)            |
27 | 24, 26 | eqeq12d 2466 |
. . . 4
         ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)             |
28 | 27 | imbi2d 318 |
. . 3
  
       ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)              |
29 | | fveq2 5865 |
. . . . . . 7
               |
30 | 29 | oveq2d 6306 |
. . . . . 6
         ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)          |
31 | 30 | itgeq1d 37833 |
. . . . 5
          ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)            |
32 | | oveq2 6298 |
. . . . . 6
    ..^  ..^     |
33 | 32 | sumeq1d 13767 |
. . . . 5
     ..^         ![[,] [,]](_icc.gif)            ..^           ![[,] [,]](_icc.gif)            |
34 | 31, 33 | eqeq12d 2466 |
. . . 4
           ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)            ..^           ![[,] [,]](_icc.gif)             |
35 | 34 | imbi2d 318 |
. . 3
    
       ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)            ..^           ![[,] [,]](_icc.gif)              |
36 | | fveq2 5865 |
. . . . . . 7
           |
37 | 36 | oveq2d 6306 |
. . . . . 6
       ![[,] [,]](_icc.gif)            ![[,] [,]](_icc.gif)        |
38 | 37 | itgeq1d 37833 |
. . . . 5
        ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)          |
39 | | oveq2 6298 |
. . . . . 6
  ..^  ..^   |
40 | 39 | sumeq1d 13767 |
. . . . 5
   ..^         ![[,] [,]](_icc.gif)            ..^         ![[,] [,]](_icc.gif)            |
41 | 38, 40 | eqeq12d 2466 |
. . . 4
         ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)             |
42 | 41 | imbi2d 318 |
. . 3
  
       ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)              |
43 | 1 | adantl 468 |
. . . . . . . 8
     
     |
44 | | fzval3 11983 |
. . . . . . . 8
      ..^     |
45 | 43, 44 | syl 17 |
. . . . . . 7
     
        ..^     |
46 | 45 | eqcomd 2457 |
. . . . . 6
     
    ..^
        |
47 | 46 | sumeq1d 13767 |
. . . . 5
     
     ..^           ![[,] [,]](_icc.gif)                       ![[,] [,]](_icc.gif)            |
48 | | itgspltprt.3 |
. . . . . . . . . . . 12
           |
49 | 48 | adantr 467 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)                   |
50 | 1 | zred 11040 |
. . . . . . . . . . . . . . 15
   |
51 | | 1red 9658 |
. . . . . . . . . . . . . . . . 17
   |
52 | 50, 51 | readdcld 9670 |
. . . . . . . . . . . . . . . 16
     |
53 | 50 | ltp1d 10537 |
. . . . . . . . . . . . . . . 16
     |
54 | 50, 52, 10, 53, 8 | ltletrd 9795 |
. . . . . . . . . . . . . . 15
   |
55 | 50, 10, 54 | ltled 9783 |
. . . . . . . . . . . . . 14

  |
56 | | eluz 11172 |
. . . . . . . . . . . . . . 15
 
     
   |
57 | 1, 5, 56 | syl2anc 667 |
. . . . . . . . . . . . . 14
     
   |
58 | 55, 57 | mpbird 236 |
. . . . . . . . . . . . 13
       |
59 | | eluzfz1 11806 |
. . . . . . . . . . . . 13
    
      |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
       |
61 | 60 | adantr 467 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)               |
62 | 49, 61 | ffvelrnd 6023 |
. . . . . . . . . 10
 
      ![[,] [,]](_icc.gif)               |
63 | | elfz1 11789 |
. . . . . . . . . . . . . 14
 
      
    |
64 | 1, 5, 63 | syl2anc 667 |
. . . . . . . . . . . . 13
      
    |
65 | 5, 55, 11, 64 | mpbir3and 1191 |
. . . . . . . . . . . 12
       |
66 | 48, 65 | ffvelrnd 6023 |
. . . . . . . . . . 11
       |
67 | 66 | adantr 467 |
. . . . . . . . . 10
 
      ![[,] [,]](_icc.gif)               |
68 | 50 | lep1d 10538 |
. . . . . . . . . . . . . 14

    |
69 | | elfz1 11789 |
. . . . . . . . . . . . . . 15
 
          
  

    |
70 | 1, 5, 69 | syl2anc 667 |
. . . . . . . . . . . . . 14
          
  

    |
71 | 2, 68, 8, 70 | mpbir3and 1191 |
. . . . . . . . . . . . 13
         |
72 | 48, 71 | ffvelrnd 6023 |
. . . . . . . . . . . 12
    
    |
73 | 72 | adantr 467 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)                 |
74 | | simpr 463 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)          |
75 | | eliccre 37603 |
. . . . . . . . . . 11
                  ![[,] [,]](_icc.gif)           |
76 | 62, 73, 74, 75 | syl3anc 1268 |
. . . . . . . . . 10
 
      ![[,] [,]](_icc.gif)           |
77 | 48, 60 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
       |
78 | 77 | rexrd 9690 |
. . . . . . . . . . . 12
       |
79 | 78 | adantr 467 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)               |
80 | 73 | rexrd 9690 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)                 |
81 | | iccgelb 11691 |
. . . . . . . . . . 11
           
      ![[,] [,]](_icc.gif)               |
82 | 79, 80, 74, 81 | syl3anc 1268 |
. . . . . . . . . 10
 
      ![[,] [,]](_icc.gif)               |
83 | | iccleub 11690 |
. . . . . . . . . . . 12
           
      ![[,] [,]](_icc.gif)            
    |
84 | 79, 80, 74, 83 | syl3anc 1268 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)            
    |
85 | 48 | adantr 467 |
. . . . . . . . . . . . . 14
 
                 |
86 | | elfzelz 11800 |
. . . . . . . . . . . . . . . 16
         |
87 | 86 | adantl 468 |
. . . . . . . . . . . . . . 15
 
         |
88 | 50 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
         |
89 | 87 | zred 11040 |
. . . . . . . . . . . . . . . 16
 
         |
90 | 52 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
       
   |
91 | 53 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
           |
92 | | elfzle1 11802 |
. . . . . . . . . . . . . . . . . 18
       
   |
93 | 92 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 
       
   |
94 | 88, 90, 89, 91, 93 | ltletrd 9795 |
. . . . . . . . . . . . . . . 16
 
         |
95 | 88, 89, 94 | ltled 9783 |
. . . . . . . . . . . . . . 15
 
         |
96 | | elfzle2 11803 |
. . . . . . . . . . . . . . . 16
         |
97 | 96 | adantl 468 |
. . . . . . . . . . . . . . 15
 
         |
98 | 1, 5 | jca 535 |
. . . . . . . . . . . . . . . . 17
     |
99 | 98 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
       
   |
100 | | elfz1 11789 |
. . . . . . . . . . . . . . . 16
 
      
    |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . 15
 
           

    |
102 | 87, 95, 97, 101 | mpbir3and 1191 |
. . . . . . . . . . . . . 14
 
             |
103 | 85, 102 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
 
             |
104 | 48 | adantr 467 |
. . . . . . . . . . . . . . 15
 
     
             |
105 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . 17
           |
106 | 105 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
     
     |
107 | 50 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
     
     |
108 | 106 | zred 11040 |
. . . . . . . . . . . . . . . . 17
 
     
     |
109 | 52 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
     
   
   |
110 | 53 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
     
       |
111 | | elfzle1 11802 |
. . . . . . . . . . . . . . . . . . 19
         
   |
112 | 111 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 
     
   
   |
113 | 107, 109,
108, 110, 112 | ltletrd 9795 |
. . . . . . . . . . . . . . . . 17
 
     
     |
114 | 107, 108,
113 | ltled 9783 |
. . . . . . . . . . . . . . . 16
 
     
     |
115 | 10 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
     
     |
116 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . 19
 
     
     |
117 | 115, 116 | resubcld 10047 |
. . . . . . . . . . . . . . . . . 18
 
     
   
   |
118 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . . 19
             |
119 | 118 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 
     
       |
120 | 115 | ltm1d 10539 |
. . . . . . . . . . . . . . . . . 18
 
     
   
   |
121 | 108, 117,
115, 119, 120 | lelttrd 9793 |
. . . . . . . . . . . . . . . . 17
 
     
     |
122 | 108, 115,
121 | ltled 9783 |
. . . . . . . . . . . . . . . 16
 
     
     |
123 | 98 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
     
   
   |
124 | 123, 100 | syl 17 |
. . . . . . . . . . . . . . . 16
 
     
       

    |
125 | 106, 114,
122, 124 | mpbir3and 1191 |
. . . . . . . . . . . . . . 15
 
     
         |
126 | 104, 125 | ffvelrnd 6023 |
. . . . . . . . . . . . . 14
 
     
         |
127 | 106 | peano2zd 11043 |
. . . . . . . . . . . . . . . 16
 
     
       |
128 | 108, 116 | readdcld 9670 |
. . . . . . . . . . . . . . . . 17
 
     
       |
129 | 107, 108,
116, 113 | ltadd1dd 10224 |
. . . . . . . . . . . . . . . . . 18
 
     
   
     |
130 | 107, 109,
128, 110, 129 | lttrd 9796 |
. . . . . . . . . . . . . . . . 17
 
     
       |
131 | 107, 128,
130 | ltled 9783 |
. . . . . . . . . . . . . . . 16
 
     
       |
132 | | zltp1le 10986 |
. . . . . . . . . . . . . . . . . 18
 
       |
133 | 105, 5, 132 | syl2anr 481 |
. . . . . . . . . . . . . . . . 17
 
     
   
     |
134 | 121, 133 | mpbid 214 |
. . . . . . . . . . . . . . . 16
 
     
       |
135 | | elfz1 11789 |
. . . . . . . . . . . . . . . . 17
 
          
   
    |
136 | 123, 135 | syl 17 |
. . . . . . . . . . . . . . . 16
 
     
         
           |
137 | 127, 131,
134, 136 | mpbir3and 1191 |
. . . . . . . . . . . . . . 15
 
     
           |
138 | 104, 137 | ffvelrnd 6023 |
. . . . . . . . . . . . . 14
 
     
           |
139 | | eluz 11172 |
. . . . . . . . . . . . . . . . . 18
 
     
   |
140 | 1, 105, 139 | syl2an 480 |
. . . . . . . . . . . . . . . . 17
 
     
       
   |
141 | 114, 140 | mpbird 236 |
. . . . . . . . . . . . . . . 16
 
     
         |
142 | 5 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
     
     |
143 | | elfzo2 11923 |
. . . . . . . . . . . . . . . 16
  ..^     
   |
144 | 141, 142,
121, 143 | syl3anbrc 1192 |
. . . . . . . . . . . . . . 15
 
     
    ..^   |
145 | | itgspltprt.4 |
. . . . . . . . . . . . . . 15
 
 ..^              |
146 | 144, 145 | syldan 473 |
. . . . . . . . . . . . . 14
 
     
               |
147 | 126, 138,
146 | ltled 9783 |
. . . . . . . . . . . . 13
 
     
               |
148 | 3, 103, 147 | monoord 12243 |
. . . . . . . . . . . 12
    
 
      |
149 | 148 | adantr 467 |
. . . . . . . . . . 11
 
      ![[,] [,]](_icc.gif)                     |
150 | 76, 73, 67, 84, 149 | letrd 9792 |
. . . . . . . . . 10
 
      ![[,] [,]](_icc.gif)               |
151 | 62, 67, 76, 82, 150 | eliccd 37601 |
. . . . . . . . 9
 
      ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)        |
152 | | itgspltprt.5 |
. . . . . . . . 9
 
      ![[,] [,]](_icc.gif)         |
153 | 151, 152 | syldan 473 |
. . . . . . . 8
 
      ![[,] [,]](_icc.gif)           |
154 | | id 22 |
. . . . . . . . . 10
   |
155 | | fzolb 11926 |
. . . . . . . . . . 11
  ..^     |
156 | 1, 5, 54, 155 | syl3anbrc 1192 |
. . . . . . . . . 10
  ..^   |
157 | 154, 156 | jca 535 |
. . . . . . . . 9
   ..^    |
158 | | eleq1 2517 |
. . . . . . . . . . . 12
   ..^
 ..^    |
159 | 158 | anbi2d 710 |
. . . . . . . . . . 11
  
 ..^  
 ..^     |
160 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
161 | | oveq1 6297 |
. . . . . . . . . . . . . . 15
       |
162 | 161 | fveq2d 5869 |
. . . . . . . . . . . . . 14
          
    |
163 | 160, 162 | oveq12d 6308 |
. . . . . . . . . . . . 13
       ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)    
     |
164 | 163 | mpteq1d 4484 |
. . . . . . . . . . . 12
        ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)    
      |
165 | 164 | eleq1d 2513 |
. . . . . . . . . . 11
         ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)             |
166 | 159, 165 | imbi12d 322 |
. . . . . . . . . 10
   
 ..^         ![[,] [,]](_icc.gif)          
   ..^         ![[,] [,]](_icc.gif)              |
167 | | itgspltprt.6 |
. . . . . . . . . 10
 
 ..^         ![[,] [,]](_icc.gif)            |
168 | 166, 167 | vtoclg 3107 |
. . . . . . . . 9
  
 ..^ 
       ![[,] [,]](_icc.gif)             |
169 | 1, 157, 168 | sylc 62 |
. . . . . . . 8
        ![[,] [,]](_icc.gif)            |
170 | 153, 169 | itgcl 22741 |
. . . . . . 7
        ![[,] [,]](_icc.gif)    
       |
171 | 163 | itgeq1d 37833 |
. . . . . . . 8
        ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)    
       |
172 | 171 | fsum1 13808 |
. . . . . . 7
         ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)    
       |
173 | 1, 170, 172 | syl2anc 667 |
. . . . . 6
              ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)            |
174 | 173 | adantl 468 |
. . . . 5
     
                ![[,] [,]](_icc.gif)                 ![[,] [,]](_icc.gif)            |
175 | 47, 174 | eqtr2d 2486 |
. . . 4
     
          ![[,] [,]](_icc.gif)    
     
 ..^
          ![[,] [,]](_icc.gif)            |
176 | 175 | ex 436 |
. . 3
    
 
        ![[,] [,]](_icc.gif)    
       ..^           ![[,] [,]](_icc.gif)             |
177 | | simp3 1010 |
. . . . 5
     ..^         ![[,] [,]](_icc.gif)        
 ..^         ![[,] [,]](_icc.gif)              |
178 | | simp1 1008 |
. . . . 5
     ..^         ![[,] [,]](_icc.gif)        
 ..^         ![[,] [,]](_icc.gif)               ..^   |
179 | | simp2 1009 |
. . . . . 6
     ..^         ![[,] [,]](_icc.gif)        
 ..^         ![[,] [,]](_icc.gif)            
       ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)             |
180 | 177, 179 | mpd 15 |
. . . . 5
     ..^         ![[,] [,]](_icc.gif)        
 ..^         ![[,] [,]](_icc.gif)                   ![[,] [,]](_icc.gif)          ..^         ![[,] [,]](_icc.gif)            |
181 | 50 | adantr 467 |
. . . . . . . . . 10
 
   ..^ 
  |
182 | | elfzoelz 11920 |
. . . . . . . . . . . 12
    ..^
  |
183 | 182 | zred 11040 |
. . . . . . . . . . 11
    ..^
  |
184 | 183 | adantl 468 |
. . . . . . . . . 10
 
   ..^ 
  |
185 | 52 | adantr 467 |
. . . . . . . . . . 11
 
   ..^ 
    |
186 | 53 | adantr 467 |
. . . . . . . . . . 11
 
   ..^ 
    |
187 | | elfzole1 11928 |
. . . . . . . . . . . 12
    ..^
    |
188 | 187 | adantl 468 |
. . . . . . . . . . 11
 
   ..^ 
    |
189 | 181, 185,
184, 186, 188 | ltletrd 9795 |
. . . . . . . . . 10
 
   ..^ 
  |
190 | 181, 184,
189 | ltled 9783 |
. . . . . . . . 9
 
   ..^ 
  |
191 | | eluz 11172 |
. . . . . . . . . 10
 
     
   |
192 | 1, 182, 191 | syl2an 480 |
. . . . . . . . 9
 
   ..^ 
        |
193 | 190, 192 | mpbird 236 |
. . . . . . . 8
 
   ..^ 
      |
194 | | simplll 768 |
. . . . . . . . . 10
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)           |
195 | | eliccxr 37612 |
. . . . . . . . . . . 12
       ![[,] [,]](_icc.gif)          |
196 | 195 | adantl 468 |
. . . . . . . . . . 11
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)           |
197 | 194, 77 | syl 17 |
. . . . . . . . . . . 12
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)               |
198 | 194, 48 | syl 17 |
. . . . . . . . . . . . 13
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)                   |
199 | | elfzelz 11800 |
. . . . . . . . . . . . . . . 16
       |
200 | 199 | adantl 468 |
. . . . . . . . . . . . . . 15
      ..^         |
201 | | elfzle1 11802 |
. . . . . . . . . . . . . . . 16
       |
202 | 201 | adantl 468 |
. . . . . . . . . . . . . . 15
      ..^         |
203 | 200 | zred 11040 |
. . . . . . . . . . . . . . . 16
      ..^         |
204 | 10 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
      ..^         |
205 | 184 | adantr 467 |
. . . . . . . . . . . . . . . . 17
      ..^         |
206 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . 18
       |
207 | 206 | adantl 468 |
. . . . . . . . . . . . . . . . 17
      ..^         |
208 | | elfzolt2 11929 |
. . . . . . . . . . . . . . . . . 18
    ..^
  |
209 | 208 | ad2antlr 733 |
. . . . . . . . . . . . . . . . 17
      ..^         |
210 | 203, 205,
204, 207, 209 | lelttrd 9793 |
. . . . . . . . . . . . . . . 16
      ..^         |
211 | 203, 204,
210 | ltled 9783 |
. . . . . . . . . . . . . . 15
      ..^         |
212 | 98 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
      ..^       
   |
213 | 212, 100 | syl 17 |
. . . . . . . . . . . . . . 15
      ..^           

    |
214 | 200, 202,
211, 213 | mpbir3and 1191 |
. . . . . . . . . . . . . 14
      ..^             |
215 | 214 | adantr 467 |
. . . . . . . . . . . . 13
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)               |
216 | 198, 215 | ffvelrnd 6023 |
. . . . . . . . . . . 12
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)               |
217 | 200 | peano2zd 11043 |
. . . . . . . . . . . . . . . 16
      ..^           |
218 | 50 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
      ..^         |
219 | 217 | zred 11040 |
. . . . . . . . . . . . . . . . 17
      ..^           |
220 | 50 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
221 | 199 | zred 11040 |
. . . . . . . . . . . . . . . . . . . 20
       |
222 | 221 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
223 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . 20
 
    
  |
224 | 222, 223 | readdcld 9670 |
. . . . . . . . . . . . . . . . . . 19
 
    
    |
225 | 201 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
226 | 222 | ltp1d 10537 |
. . . . . . . . . . . . . . . . . . 19
 
    
    |
227 | 220, 222,
224, 225, 226 | lelttrd 9793 |
. . . . . . . . . . . . . . . . . 18
 
    
    |
228 | 227 | adantlr 721 |
. . . . . . . . . . . . . . . . 17
      ..^           |
229 | 218, 219,
228 | ltled 9783 |
. . . . . . . . . . . . . . . 16
      ..^           |
230 | 5, 199 | anim12ci 571 |
. . . . . . . . . . . . . . . . . . 19
 
    
    |
231 | 230 | adantlr 721 |
. . . . . . . . . . . . . . . . . 18
      ..^       
   |
232 | 231, 132 | syl 17 |
. . . . . . . . . . . . . . . . 17
      ..^       
     |
233 | 210, 232 | mpbid 214 |
. . . . . . . . . . . . . . . 16
      ..^           |
234 | 212, 135 | syl 17 |
. . . . . . . . . . . . . . . 16
      ..^             
           |
235 | 217, 229,
233, 234 | mpbir3and 1191 |
. . . . . . . . . . . . . . 15
      ..^               |
236 | 235 | adantr 467 |
. . . . . . . . . . . . . 14
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)                 |
237 | 198, 236 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)                 |
238 | | simpr 463 |
. . . . . . . . . . . . 13
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)               ![[,] [,]](_icc.gif)          |
239 | | eliccre 37603 |
. . . . . . . . . . . . 13
                  ![[,] [,]](_icc.gif)           |
240 | 216, 237,
238, 239 | syl3anc 1268 |
. . . . . . . . . . . 12
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)           |
241 | | elfzuz 11796 |
. . . . . . . . . . . . . . 15
           |
242 | 241 | adantl 468 |
. . . . . . . . . . . . . 14
      ..^             |
243 | 48 | ad3antrrr 736 |
. . . . . . . . . . . . . . 15
   
 
 ..^ 
    
               |
244 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . 17
       |
245 | 244 | adantl 468 |
. . . . . . . . . . . . . . . 16
   
 
 ..^ 
    
       |
246 | | elfzle1 11802 |
. . . . . . . . . . . . . . . . 17
       |
247 | 246 | adantl 468 |
. . . . . . . . . . . . . . . 16
   
 
 ..^ 
    
       |
248 | 245 | zred 11040 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
       |
249 | 204 | adantr 467 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
    
  |
250 | 203 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
   
 
 ..^ 
    
       |
251 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . . 19
       |
252 | 251 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
   
 
 ..^ 
    
    
  |
253 | 210 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
   
 
 ..^ 
    
    
  |
254 | 248, 250,
249, 252, 253 | lelttrd 9793 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
    
  |
255 | 248, 249,
254 | ltled 9783 |
. . . . . . . . . . . . . . . 16
   
 
 ..^ 
    
    
  |
256 | 212 | adantr 467 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
         |
257 | | elfz1 11789 |
. . . . . . . . . . . . . . . . 17
 
      
    |
258 | 256, 257 | syl 17 |
. . . . . . . . . . . . . . . 16
   
 
 ..^ 
    
          
    |
259 | 245, 247,
255, 258 | mpbir3and 1191 |
. . . . . . . . . . . . . . 15
   
 
 ..^ 
    
           |
260 | 243, 259 | ffvelrnd 6023 |
. . . . . . . . . . . . . 14
   
 
 ..^ 
    
           |
261 | 48 | ad3antrrr 736 |
. . . . . . . . . . . . . . . 16
   
 
 ..^ 
    
                 |
262 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . . 18
         |
263 | 262 | adantl 468 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
         |
264 | | elfzle1 11802 |
. . . . . . . . . . . . . . . . . 18
         |
265 | 264 | adantl 468 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
         |
266 | 263 | zred 11040 |
. . . . . . . . . . . . . . . . . 18
   
 
 ..^ 
    
         |
267 | 204 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
   
 
 ..^ 
    
      
  |
268 | 203 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   
 
 ..^ 
    
         |
269 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . 21
   
 
 ..^ 
    
         |
270 | 268, 269 | resubcld 10047 |
. . . . . . . . . . . . . . . . . . . 20
   
 
 ..^ 
    
           |
271 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . . . . 21
           |
272 | 271 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
   
 
 ..^ 
    
      
    |
273 | 268 | ltm1d 10539 |
. . . . . . . . . . . . . . . . . . . 20
   
 
 ..^ 
    
           |
274 | 266, 270,
268, 272, 273 | lelttrd 9793 |
. . . . . . . . . . . . . . . . . . 19
   
 
 ..^ 
    
      
  |
275 | 210 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   
 
 ..^ 
    
      
  |
276 | 266, 268,
267, 274, 275 | lttrd 9796 |
. . . . . . . . . . . . . . . . . 18
   
 
 ..^ 
    
      
  |
277 | 266, 267,
276 | ltled 9783 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
      
  |
278 | 212 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
   
 
 ..^ 
    
           |
279 | 278, 257 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
            
    |
280 | 263, 265,
277, 279 | mpbir3and 1191 |
. . . . . . . . . . . . . . . 16
   
 
 ..^ 
    
             |
281 | 261, 280 | ffvelrnd 6023 |
. . . . . . . . . . . . . . 15
   
 
 ..^ 
    
             |
282 | 263 | peano2zd 11043 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
           |
283 | 181 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . 18
   
 
 ..^ 
    
      
  |
284 | 266, 269 | readdcld 9670 |
. . . . . . . . . . . . . . . . . 18
   
 
 ..^ 
    
           |
285 | 50 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
      
  |
286 | 262 | zred 11040 |
. . . . . . . . . . . . . . . . . . . . 21
         |
287 | 286 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 
      
  |
288 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
  |
289 | 287, 288 | readdcld 9670 |
. . . . . . . . . . . . . . . . . . . 20
 
      
    |
290 | 264 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 
      
  |
291 | 287 | ltp1d 10537 |
. . . . . . . . . . . . . . . . . . . 20
 
      
    |
292 | 285, 287,
289, 290, 291 | lelttrd 9793 |
. . . . . . . . . . . . . . . . . . 19
 
      
    |
293 | 292 | adant423 37367 |
. . . . . . . . . . . . . . . . . 18
   
 
 ..^ 
    
           |
294 | 283, 284,
293 | ltled 9783 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
           |
295 | | zltp1le 10986 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
296 | 262, 200,
295 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . 20
   
 
 ..^ 
    
             |
297 | 274, 296 | mpbid 214 |
. . . . . . . . . . . . . . . . . . 19
   
 
 ..^ 
    
        
  |
298 | 284, 268,
267, 297, 275 | lelttrd 9793 |
. . . . . . . . . . . . . . . . . 18
   
 
 ..^ 
    
           |
299 | 284, 267,
298 | ltled 9783 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
        
  |
300 | | elfz1 11789 |
. . . . . . . . . . . . . . . . . 18
 
          
   
    |
301 | 278, 300 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
                
   
    |
302 | 282, 294,
299, 301 | mpbir3and 1191 |
. . . . . . . . . . . . . . . 16
   
 
 ..^ 
    
               |
303 | 261, 302 | ffvelrnd 6023 |
. . . . . . . . . . . . . . 15
   
 
 ..^ 
    
               |
304 | | simplll 768 |
. . . . . . . . . . . . . . . 16
   
 
 ..^ 
    
         |
305 | | elfzuz 11796 |
. . . . . . . . . . . . . . . . . 18
             |
306 | 305 | adantl 468 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
             |
307 | 304, 5 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
      
  |
308 | | elfzo2 11923 |
. . . . . . . . . . . . . . . . 17
  ..^     
   |
309 | 306, 307,
276, 308 | syl3anbrc 1192 |
. . . . . . . . . . . . . . . 16
   
 
 ..^ 
    
        ..^   |
310 | | eleq1 2517 |
. . . . . . . . . . . . . . . . . . 19
   ..^
 ..^    |
311 | 310 | anbi2d 710 |
. . . . . . . . . . . . . . . . . 18
  
 ..^  
 ..^     |
312 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . 19
           |
313 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . 20
       |
314 | 313 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . 19
               |
315 | 312, 314 | breq12d 4415 |
. . . . . . . . . . . . . . . . . 18
     
     
             |
316 | 311, 315 | imbi12d 322 |
. . . . . . . . . . . . . . . . 17
   
 ..^     
      
   ..^                |
317 | 316, 145 | chvarv 2107 |
. . . . . . . . . . . . . . . 16
 
 ..^              |
318 | 304, 309,
317 | syl2anc 667 |
. . . . . . . . . . . . . . 15
   
 
 ..^ 
    
          
        |
319 | 281, 303,
318 | ltled 9783 |
. . . . . . . . . . . . . 14
   
 
 ..^ 
    
          
        |
320 | 242, 260,
319 | monoord 12243 |
. . . . . . . . . . . . 13
      ..^                 |
321 | 320 | adantr 467 |
. . . . . . . . . . . 12
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)            
      |
322 | 216 | rexrd 9690 |
. . . . . . . . . . . . 13
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)               |
323 | 237 | rexrd 9690 |
. . . . . . . . . . . . 13
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)                 |
324 | | iccgelb 11691 |
. . . . . . . . . . . . 13
           
      ![[,] [,]](_icc.gif)               |
325 | 322, 323,
238, 324 | syl3anc 1268 |
. . . . . . . . . . . 12
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)            
  |
326 | 197, 216,
240, 321, 325 | letrd 9792 |
. . . . . . . . . . 11
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)            
  |
327 | 194, 66 | syl 17 |
. . . . . . . . . . . 12
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)               |
328 | | iccleub 11690 |
. . . . . . . . . . . . 13
           
      ![[,] [,]](_icc.gif)                 |
329 | 322, 323,
238, 328 | syl3anc 1268 |
. . . . . . . . . . . 12
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)        
        |
330 | 5 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
      ..^         |
331 | | eluz 11172 |
. . . . . . . . . . . . . . . 16
   
       
     |
332 | 217, 330,
331 | syl2anc 667 |
. . . . . . . . . . . . . . 15
      ..^       
     
     |
333 | 233, 332 | mpbird 236 |
. . . . . . . . . . . . . 14
      ..^               |
334 | 333 | adantr 467 |
. . . . . . . . . . . . 13
   
 
 ..^ 
    
      ![[,] [,]](_icc.gif)        
        |
335 | 48 | ad3antrrr 736 |
. . . . . . . . . . . . . . 15
   
 
 ..^ 
    
                 |
336 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . 17
         |
337 | 336 | adantl 468 |
. . . . . . . . . . . . . . . 16
   
 
 ..^ 
    
         |
338 | | elfzel1 11799 |
. . . . . . . . . . . . . . . . . . . 20
       |
339 | 338 | zred 11040 |
. . . . . . . . . . . . . . . . . . 19
       |
340 | 339 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
     
         |
341 | 336 | zred 11040 |
. . . . . . . . . . . . . . . . . . 19
         |
342 | 341 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
     
         |
343 | 221 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
     
         |
344 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . 20
     
         |
345 | 343, 344 | readdcld 9670 |
. . . . . . . . . . . . . . . . . . 19
     
           |
346 | 201 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
     
         |
347 | 343 | ltp1d 10537 |
. . . . . . . . . . . . . . . . . . . 20
     
           |
348 | 340, 343,
345, 346, 347 | lelttrd 9793 |
. . . . . . . . . . . . . . . . . . 19
     
           |
349 | | elfzle1 11802 |
. . . . . . . . . . . . . . . . . . . 20
           |
350 | 349 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
     
           |
351 | 340, 345,
342, 348, 350 | ltletrd 9795 |
. . . . . . . . . . . . . . . . . 18
     
         |
352 | 340, 342,
351 | ltled 9783 |
. . . . . . . . . . . . . . . . 17
     
         |
353 | 352 | adantll 720 |
. . . . . . . . . . . . . . . 16
   
 
 ..^ 
    
         |
354 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . 17
         |
355 | 354 | adantl 468 |
. . . . . . . . . . . . . . . 16
   
 
 ..^ 
    
         |
356 | 212 | adantr 467 |
. . . . . . . . . . . . . . . . 17
   
 
 ..^ 
    
           |
357 | 356, 257 | syl 17 |
. . . . . . . . . . . . . . . 16
   
 
 ..^ 
    
            
    |
358 | 337, 353,
355, 357 | mpbir3and 1191 |
. . . . . . . . . . . . . . 15
   
 
 ..^ 
    
             |
359 | 335, 358 | ffvelrnd 6023 |
. . . . . . . . . . . . . 14
   
 
 ..^ 
    
             |
360 | 359 | adantlr 721 |
. . . . . . . . . . . . 13
        ..^ 
    
      ![[,] [,]](_icc.gif)        
             |
361 | | simplll 768 |
. . . . . . . . . . . . . . 15
   
 
 ..^ 
    
           |
362 | | simplr 762 |
. . . . . . . . . . . . . . 15
   
 
 ..^ 
    
               |
363 | | simpr 463 |
. . . . . . . . . . . . . . 15
   
 
 ..^ 
    
                   |
364 | 48 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . 17
 
            
          |
365 | | elfzelz 11800 |
. . . . . . . . . . . . . . . . . . 19
           |
366 | 365 | 3ad2ant3 1031 |
. . . . . . . . . . . . . . . . . 18
 
            
  |
367 | 50 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . 19
 
            
  |
368 | 366 | zred 11040 |
. . . . . . . . . . . . . . . . . . 19
 
            
  |
369 | 224 | 3adant3 1028 |
. . . . . . . . . . . . . . . . . . . 20
 
            
    |
370 | 227 | 3adant3 1028 |
. . . . . . . . . . . . . . . . . . . 20
 
            
    |
371 | | elfzle1 11802 |
. . . . . . . . . . . . . . . . . . . . 21
             |
372 | 371 | 3ad2ant3 1031 |
. . . . . . . . . . . . . . . . . . . 20
 
            
    |
373 | 367, 369,
368, 370, 372 | ltletrd 9795 |
. . . . . . . . . . . . . . . . . . 19
 
            
  |
374 | 367, 368,
373 | ltled 9783 |
. . . . . . . . . . . . . . . . . 18
 
            
  |
375 | 365 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
 
     
     |
376 | 375 | zred 11040 |
. . . . . . . . . . . . . . . . . . . 20
 
     
     |
377 | 10 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
     
     |
378 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     
     |
379 | 377, 378 | resubcld 10047 |
. . . . . . . . . . . . . . . . . . . . 21
 
     
   
   |
380 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
381 | 380 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
 
     
       |
382 | 377 | ltm1d 10539 |
. . . . . . . . . . . . . . . . . . . . 21
 
     
   
   |
383 | 376, 379,
377, 381, 382 | lelttrd 9793 |
. . . . . . . . . . . . . . . . . . . 20
 
     
     |
384 | 376, 377,
383 | ltled 9783 |
. . . . . . . . . . . . . . . . . . 19
 
     
     |
385 | 384 | 3adant2 1027 |
. . . . . . . . . . . . . . . . . 18
 
            
  |
386 | 98 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . 19
 
            
    |
387 | 386, 257 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
            
     
    |
388 | 366, 374,
385, 387 | mpbir3and 1191 |
. . . . . . . . . . . . . . . . 17
 
            
      |
389 | 364, 388 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . 16
 
            
      |
390 | 366 | peano2zd 11043 |
. . . . . . . . . . . . . . . . . 18
 
            
    |
391 | 390 | zred 11040 |
. . . . . . . . . . . . . . . . . . 19
 
            
    |
392 | 221 | 3ad2ant2 1030 |
. . . . . . . . . . . . . . . . . . . . 21
 
            
  |
393 | | 1red 9658 |
. . . . . . . . . . . . . . . . . . . . 21
 
            
  |
394 | 226 | 3adant3 1028 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
            
    |
395 | 392, 369,
368, 394, 372 | ltletrd 9795 |
. . . . . . . . . . . . . . . . . . . . . 22
 
            
  |
396 | 392, 368,
395 | ltled 9783 |
. . . . . . . . . . . . . . . . . . . . 21
 
            
  |
397 | 392, 368,
393, 396 | leadd1dd 10227 |
. . . . . . . . . . . . . . . . . . . 20
 
            
      |
398 | 367, 369,
391, 370, 397 | ltletrd 9795 |
. . . . . . . . . . . . . . . . . . 19
 
            
    |
399 | 367, 391,
398 | ltled 9783 |
. . . . . . . . . . . . . . . . . 18
 
            
    |
400 | | zltp1le 10986 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
401 | 365, 5, 400 | syl2anr 481 |
. . . . . . . . . . . . . . . . . . . 20
 
     
   
     |
402 | 383, 401 | mpbid 214 |
. . . . . . . . . . . . . . . . . . 19
 
     
       |
403 | 402 | 3adant2 1027 |
. . . . . . . . . . . . . . . . . 18
 
            
    |
404 | 386, 300 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
            
      
           |
405 | 390, 399,
403, 404 | mpbir3and 1191 |
. . . . . . . . . . . . . . . . 17
 
            
        |
406 | 364, 405 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . 16
 
            
        |
407 | | simp1 1008 |
. . . . . . . . . . . . . . . . 17
 
            
  |
408 | 1 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . 20
 
            
  |
409 | | eluz 11172 |
. . . . . . . . . . . . . . . . . . . 20
 
     
   |
410 | 408, 366,
409 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
 
            
        |
411 | 374, 410 | mpbird 236 |
. . . . . . . . . . . . . . . . . 18
 
            
      |
412 | 5 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . 18
 
            
  |
413 | 383 | 3adant2 1027 |
. . . . . . . . . . . . . . . . . 18
 
            
  |
414 | 411, 412,
413, 308 | syl3anbrc 1192 |
. . . . . . . . . . . . . . . . 17
 
            
 ..^   |
415 | 407, 414,
317 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
 
            
            |
416 | 389, 406,
415 | ltled 9783 |
. . . . . . . . . . . . . . 15
 
            
            |
417 | 361, 362,
363, 416 | syl3anc 1268 |
. . . . . . . . . . . . . 14
   
 
 ..^ 
    
                     |
418 | 417 | adantlr 721 |
. . . . . . . . . . . . 13
        ..^ 
    
      ![[,] [,]](_icc.gif)        
                     |
419 | 334, 360,
418 | monoord 12243 |
. . . . . . . . . . . 12
 |