Step | Hyp | Ref
| Expression |
1 | | itg2split.a |
. . 3
   |
2 | | itg2split.b |
. . 3
   |
3 | | itg2split.i |
. . 3
     
    |
4 | | itg2split.u |
. . 3
     |
5 | | itg2split.c |
. . 3
 
      |
6 | | itg2split.f |
. . 3
        |
7 | | itg2split.g |
. . 3
        |
8 | | itg2split.h |
. . 3
        |
9 | | itg2split.sf |
. . 3
       |
10 | | itg2split.sg |
. . 3
       |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | itg2splitlem 19593 |
. 2
    
            |
12 | 10 | adantr 452 |
. . . . . . 7
 


 
      |
13 | 5 | adantlr 696 |
. . . . . . . . . . 11
          |
14 | | 0xr 9087 |
. . . . . . . . . . . . 13
 |
15 | | 0le0 10037 |
. . . . . . . . . . . . 13
 |
16 | | elxrge0 10964 |
. . . . . . . . . . . . 13
   

   |
17 | 14, 15, 16 | mpbir2an 887 |
. . . . . . . . . . . 12
    |
18 | 17 | a1i 11 |
. . . . . . . . . . 11
   
      |
19 | 13, 18 | ifclda 3726 |
. . . . . . . . . 10
 

   
      |
20 | 19, 8 | fmptd 5852 |
. . . . . . . . 9
          |
21 | 9, 10 | readdcld 9071 |
. . . . . . . . 9
             |
22 | | itg2lecl 19583 |
. . . . . . . . 9
                      
                 |
23 | 20, 21, 11, 22 | syl3anc 1184 |
. . . . . . . 8
       |
24 | 23 | adantr 452 |
. . . . . . 7
 


 
      |
25 | | itg1cl 19530 |
. . . . . . . 8
       |
26 | 25 | ad2antrl 709 |
. . . . . . 7
 


 
      |
27 | | simprll 739 |
. . . . . . . . . . . . . 14
 
           |
28 | | simprrl 741 |
. . . . . . . . . . . . . 14
 
           |
29 | 27, 28 | itg1add 19546 |
. . . . . . . . . . . . 13
 
                            |
30 | 20 | adantr 452 |
. . . . . . . . . . . . . 14
 
                  |
31 | 27, 28 | i1fadd 19540 |
. . . . . . . . . . . . . 14
 
              |
32 | | inss1 3521 |
. . . . . . . . . . . . . . . 16
   |
33 | | mblss 19380 |
. . . . . . . . . . . . . . . . 17
   |
34 | 1, 33 | syl 16 |
. . . . . . . . . . . . . . . 16

  |
35 | 32, 34 | syl5ss 3319 |
. . . . . . . . . . . . . . 15
  
  |
36 | 35 | adantr 452 |
. . . . . . . . . . . . . 14
 
          
  |
37 | 3 | adantr 452 |
. . . . . . . . . . . . . 14
 
                  |
38 | | nfv 1626 |
. . . . . . . . . . . . . . . . . 18
   |
39 | | nfv 1626 |
. . . . . . . . . . . . . . . . . . . 20

 |
40 | | nfcv 2540 |
. . . . . . . . . . . . . . . . . . . . 21
   |
41 | | nfcv 2540 |
. . . . . . . . . . . . . . . . . . . . 21
 
 |
42 | | nfmpt1 4258 |
. . . . . . . . . . . . . . . . . . . . . 22
          |
43 | 6, 42 | nfcxfr 2537 |
. . . . . . . . . . . . . . . . . . . . 21
   |
44 | 40, 41, 43 | nfbr 4216 |
. . . . . . . . . . . . . . . . . . . 20
   |
45 | 39, 44 | nfan 1842 |
. . . . . . . . . . . . . . . . . . 19
      |
46 | | nfv 1626 |
. . . . . . . . . . . . . . . . . . . 20

 |
47 | | nfcv 2540 |
. . . . . . . . . . . . . . . . . . . . 21
   |
48 | | nfmpt1 4258 |
. . . . . . . . . . . . . . . . . . . . . 22
          |
49 | 7, 48 | nfcxfr 2537 |
. . . . . . . . . . . . . . . . . . . . 21
   |
50 | 47, 41, 49 | nfbr 4216 |
. . . . . . . . . . . . . . . . . . . 20
   |
51 | 46, 50 | nfan 1842 |
. . . . . . . . . . . . . . . . . . 19
      |
52 | 45, 51 | nfan 1842 |
. . . . . . . . . . . . . . . . . 18
    
      |
53 | 38, 52 | nfan 1842 |
. . . . . . . . . . . . . . . . 17
  
          |
54 | | eldifi 3429 |
. . . . . . . . . . . . . . . . . . . 20
       |
55 | | i1ff 19521 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
56 | 27, 55 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
 
               |
57 | | ffn 5550 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
58 | 56, 57 | syl 16 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
59 | | i1ff 19521 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
60 | 28, 59 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
 
               |
61 | | ffn 5550 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
62 | 60, 61 | syl 16 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
63 | | reex 9037 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
 
           |
65 | | inidm 3510 |
. . . . . . . . . . . . . . . . . . . . 21
   |
66 | | eqidd 2405 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
67 | | eqidd 2405 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
68 | 58, 62, 64, 64, 65, 66, 67 | ofval 6273 |
. . . . . . . . . . . . . . . . . . . 20
                                |
69 | 54, 68 | sylan2 461 |
. . . . . . . . . . . . . . . . . . 19
                
                   |
70 | | ffvelrn 5827 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
       |
71 | 56, 54, 70 | syl2an 464 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                
      |
72 | | ffvelrn 5827 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
       |
73 | 60, 54, 72 | syl2an 464 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                
      |
74 | 71, 73 | readdcld 9071 |
. . . . . . . . . . . . . . . . . . . . . . 23
                
            |
75 | 74 | rexrd 9090 |
. . . . . . . . . . . . . . . . . . . . . 22
                
            |
76 | 75 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . 21
      
                        |
77 | 71 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                  |
78 | 77 | rexrd 9090 |
. . . . . . . . . . . . . . . . . . . . 21
      
                  |
79 | | iccssxr 10949 |
. . . . . . . . . . . . . . . . . . . . . . 23
    |
80 | | ffvelrn 5827 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
81 | 30, 54, 80 | syl2an 464 |
. . . . . . . . . . . . . . . . . . . . . . 23
                
         |
82 | 79, 81 | sseldi 3306 |
. . . . . . . . . . . . . . . . . . . . . 22
                
      |
83 | 82 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . 21
      
                  |
84 | 73 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
                  |
85 | | 0re 9047 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
              |
87 | | simprrr 742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
            |
88 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

  |
89 | | fvex 5701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     |
90 | 89 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
91 | | ssun2 3471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36

  |
92 | 91, 4 | syl5sseqr 3357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35

  |
93 | 92 | sselda 3308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   |
94 | 93 | adantlr 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
95 | 94, 13 | syldan 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
          |
96 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
      |
97 | 95, 96 | ifclda 3726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 

   
      |
98 | 97 | adantlr 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
      
        |
99 | | simpr 448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 

  |
100 | | dffn5 5731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31


       |
101 | 99, 100 | sylib 189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

        |
102 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

         |
103 | 88, 90, 98, 101, 102 | ofrfval2 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

               |
104 | 62, 103 | syldan 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
          
      
      |
105 | 87, 104 | mpbid 202 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
             
   
   |
106 | 105 | r19.21bi 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                        |
107 | 54, 106 | sylan2 461 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                
     
     |
108 | 107 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
                       |
109 | | eldifn 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
    |
110 | 109 | adantl 453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                
    |
111 | | elin 3490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
112 | 110, 111 | sylnib 296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                

   |
113 | | imnan 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 


   |
114 | 112, 113 | sylibr 204 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                

   |
115 | 114 | imp 419 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
           
  |
116 | | iffalse 3706 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        |
117 | 115, 116 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
             
     |
118 | 108, 117 | breqtrd 4196 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
                  |
119 | 84, 86, 77, 118 | leadd2dd 9597 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                              |
120 | 77 | recnd 9070 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
                  |
121 | 120 | addid1d 9222 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                        |
122 | 119, 121 | breqtrd 4196 |
. . . . . . . . . . . . . . . . . . . . 21
      
                            |
123 | | simprlr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
            |
124 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

  |
125 | | fvex 5701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
126 | 125 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
127 | | ssun1 3470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34

  |
128 | 127, 4 | syl5sseqr 3357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33

  |
129 | 128 | sselda 3308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   |
130 | 129 | adantlr 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
131 | 130, 13 | syldan 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          |
132 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
      |
133 | 131, 132 | ifclda 3726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

   
      |
134 | 133 | adantlr 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
        |
135 | | simpr 448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

  |
136 | | dffn5 5731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29


       |
137 | 135, 136 | sylib 189 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

        |
138 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

         |
139 | 124, 126,
134, 137, 138 | ofrfval2 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 

               |
140 | 58, 139 | syldan 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
          
      
      |
141 | 123, 140 | mpbid 202 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
             
   
   |
142 | 141 | r19.21bi 2764 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                        |
143 | 54, 142 | sylan2 461 |
. . . . . . . . . . . . . . . . . . . . . . 23
                
     
     |
144 | 143 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                       |
145 | 128 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                
  |
146 | 145 | sselda 3308 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
              |
147 | | iftrue 3705 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
     |
148 | 146, 147 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
             
     |
149 | | simpr 448 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               |
150 | 19 | adantlr 696 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
              
        |
151 | 8 | fvmpt2 5771 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                  
   |
152 | 149, 150,
151 | syl2anc 643 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                        |
153 | 54, 152 | sylan2 461 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                
           |
154 | 153 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
                       |
155 | | iftrue 3705 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
     |
156 | 155 | adantl 453 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
             
     |
157 | 148, 154,
156 | 3eqtr4d 2446 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                       |
158 | 144, 157 | breqtrrd 4198 |
. . . . . . . . . . . . . . . . . . . . 21
      
                      |
159 | 76, 78, 83, 122, 158 | xrletrd 10708 |
. . . . . . . . . . . . . . . . . . . 20
      
                            |
160 | 75 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . 21
      
                        |
161 | 73 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                  |
162 | 161 | rexrd 9090 |
. . . . . . . . . . . . . . . . . . . . 21
      
                  |
163 | 82 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . 21
      
                  |
164 | 71 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
                  |
165 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
              |
166 | 143 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
                       |
167 | | iffalse 3706 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        |
168 | 167 | adantl 453 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
             
     |
169 | 166, 168 | breqtrd 4196 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
                  |
170 | 164, 165,
161, 169 | leadd1dd 9596 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                              |
171 | 161 | recnd 9070 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
                  |
172 | 171 | addid2d 9223 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                        |
173 | 170, 172 | breqtrd 4196 |
. . . . . . . . . . . . . . . . . . . . 21
      
                            |
174 | 107 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                       |
175 | 153 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
                       |
176 | 4 | ad3antrrr 711 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
                |
177 | 176 | eleq2d 2471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
            

    |
178 | | biorf 395 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
    |
179 | | elun 3448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  

   |
180 | 178, 179 | syl6rbbr 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
181 | 180 | adantl 453 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
              
   |
182 | 177, 181 | bitrd 245 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
            
   |
183 | 182 | ifbid 3717 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
             
          |
184 | 175, 183 | eqtrd 2436 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                       |
185 | 174, 184 | breqtrrd 4198 |
. . . . . . . . . . . . . . . . . . . . 21
      
                      |
186 | 160, 162,
163, 173, 185 | xrletrd 10708 |
. . . . . . . . . . . . . . . . . . . 20
      
                            |
187 | 159, 186 | pm2.61dan 767 |
. . . . . . . . . . . . . . . . . . 19
                
                |
188 | 69, 187 | eqbrtrd 4192 |
. . . . . . . . . . . . . . . . . 18
                
      
      |
189 | 188 | ex 424 |
. . . . . . . . . . . . . . . . 17
 
                            |
190 | 53, 189 | ralrimi 2747 |
. . . . . . . . . . . . . . . 16
 
                            |
191 | | nfv 1626 |
. . . . . . . . . . . . . . . . 17
              |
192 | | nfcv 2540 |
. . . . . . . . . . . . . . . . . 18
          |
193 | | nfcv 2540 |
. . . . . . . . . . . . . . . . . 18
  |
194 | | nfmpt1 4258 |
. . . . . . . . . . . . . . . . . . . 20
          |
195 | 8, 194 | nfcxfr 2537 |
. . . . . . . . . . . . . . . . . . 19
   |
196 | | nfcv 2540 |
. . . . . . . . . . . . . . . . . . 19
   |
197 | 195, 196 | nffv 5694 |
. . . . . . . . . . . . . . . . . 18
       |
198 | 192, 193,
197 | nfbr 4216 |
. . . . . . . . . . . . . . . . 17
              |
199 | | fveq2 5687 |
. . . . . . . . . . . . . . . . . 18
                 |
200 | | fveq2 5687 |
. . . . . . . . . . . . . . . . . 18
           |
201 | 199, 200 | breq12d 4185 |
. . . . . . . . . . . . . . . . 17
                           |
202 | 191, 198,
201 | cbvral 2888 |
. . . . . . . . . . . . . . . 16
 
           
   
                   |
203 | 190, 202 | sylib 189 |
. . . . . . . . . . . . . . 15
 
                            |
204 | 203 | r19.21bi 2764 |
. . . . . . . . . . . . . 14
                
      
      |
205 | 30, 31, 36, 37, 204 | itg2uba 19588 |
. . . . . . . . . . . . 13
 
                      |
206 | 29, 205 | eqbrtrrd 4194 |
. . . . . . . . . . . 12
 
                  
      |
207 | 26 | adantrr 698 |
. . . . . . . . . . . . 13
 
               |
208 | | itg1cl 19530 |
. . . . . . . . . . . . . 14
       |
209 | 28, 208 | syl 16 |
. . . . . . . . . . . . 13
 
               |
210 | 23 | adantr 452 |
. . . . . . . . . . . . 13
 
               |
211 | 207, 209,
210 | leaddsub2d 9584 |
. . . . . . . . . . . 12
 
                       
                 |
212 | 206, 211 | mpbid 202 |
. . . . . . . . . . 11
 
            
            |
213 | 212 | anassrs 630 |
. . . . . . . . . 10
              
            |
214 | 213 | expr 599 |
. . . . . . . . 9
      
                    |
215 | 214 | ralrimiva 2749 |
. . . . . . . 8
 


 
   
                 |
216 | 97, 7 | fmptd 5852 |
. . . . . . . . . 10
          |
217 | 216 | adantr 452 |
. . . . . . . . 9
 


 
         |
218 | 24, 26 | resubcld 9421 |
. . . . . . . . . 10
 


 
            |
219 | 218 | rexrd 9090 |
. . . . . . . . 9
 


 
            |
220 | | itg2leub 19579 |
. . . . . . . . 9
                                  
   
                  |
221 | 217, 219,
220 | syl2anc 643 |
. . . . . . . 8
 


 
              
   
                  |
222 | 215, 221 | mpbird 224 |
. . . . . . 7
 


 
                |
223 | 12, 24, 26, 222 | lesubd 9586 |
. . . . . 6
 


 
                |
224 | 223 | expr 599 |
. . . . 5
 
      
             |
225 | 224 | ralrimiva 2749 |
. . . 4
                      |
226 | 133, 6 | fmptd 5852 |
. . . . 5
          |
227 | 23, 10 | resubcld 9421 |
. . . . . 6
             |
228 | 227 | rexrd 9090 |
. . . . 5
             |
229 | | itg2leub 19579 |
. . . . 5
                                  
   
                  |
230 | 226, 228,
229 | syl2anc 643 |
. . . 4
     
                                |
231 | 225, 230 | mpbird 224 |
. . 3
    
            |
232 | | leaddsub 9460 |
. . . 4
                                               |
233 | 9, 10, 23, 232 | syl3anc 1184 |
. . 3
           
   
                 |
234 | 231, 233 | mpbird 224 |
. 2
                 |
235 | | itg2cl 19577 |
. . . 4
              |
236 | 20, 235 | syl 16 |
. . 3
       |
237 | 21 | rexrd 9090 |
. . 3
             |
238 | | xrletri3 10701 |
. . 3
                               
                                 |
239 | 236, 237,
238 | syl2anc 643 |
. 2
               
                                 |
240 | 11, 234, 239 | mpbir2and 889 |
1
                 |