Step | Hyp | Ref
| Expression |
1 | | simpr 463 |
. 2
 
           |
2 | | simpl 459 |
. 2
 
       |
3 | | fveq2 5870 |
. . . . 5
                           |
4 | | csbeq1 3368 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
5 | 4 | oveq1d 6310 |
. . . . . 6
  
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
6 | 5 | mpteq2dv 4493 |
. . . . 5
     ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)
    |
7 | 3, 6 | eqeq12d 2468 |
. . . 4
                  ![]_ ]_](_urbrack.gif)  
                ![]_ ]_](_urbrack.gif)      |
8 | 7 | imbi2d 318 |
. . 3
  
                ![]_ ]_](_urbrack.gif)    
                ![]_ ]_](_urbrack.gif)       |
9 | | fveq2 5870 |
. . . . 5
                           |
10 | | csbeq1 3368 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
11 | 10 | oveq1d 6310 |
. . . . . 6
  
 ![]_ ]_](_urbrack.gif)
    ![]_ ]_](_urbrack.gif)    |
12 | 11 | mpteq2dv 4493 |
. . . . 5
     ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)
    |
13 | 9, 12 | eqeq12d 2468 |
. . . 4
                  ![]_ ]_](_urbrack.gif)  
                ![]_ ]_](_urbrack.gif)      |
14 | 13 | imbi2d 318 |
. . 3
  
                ![]_ ]_](_urbrack.gif)    
                ![]_ ]_](_urbrack.gif)       |
15 | | fveq2 5870 |
. . . . 5
                               |
16 | | csbeq1 3368 |
. . . . . . 7
     ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
17 | 16 | oveq1d 6310 |
. . . . . 6
    
 ![]_ ]_](_urbrack.gif)
      ![]_ ]_](_urbrack.gif)    |
18 | 17 | mpteq2dv 4493 |
. . . . 5
       ![]_ ]_](_urbrack.gif)
        ![]_ ]_](_urbrack.gif)
    |
19 | 15, 18 | eqeq12d 2468 |
. . . 4
                    ![]_ ]_](_urbrack.gif)  
                    ![]_ ]_](_urbrack.gif)      |
20 | 19 | imbi2d 318 |
. . 3
    
                ![]_ ]_](_urbrack.gif)    
                    ![]_ ]_](_urbrack.gif)       |
21 | | fveq2 5870 |
. . . . 5
                           |
22 | | equcomi 1863 |
. . . . . . . . 9
   |
23 | | csbeq1a 3374 |
. . . . . . . . 9
   ![]_ ]_](_urbrack.gif)   |
24 | 22, 23 | syl 17 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)   |
25 | 24 | eqcomd 2459 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)   |
26 | 25 | oveq1d 6310 |
. . . . . 6
  
 ![]_ ]_](_urbrack.gif)
     |
27 | 26 | mpteq2dv 4493 |
. . . . 5
     ![]_ ]_](_urbrack.gif)
        |
28 | 21, 27 | eqeq12d 2468 |
. . . 4
                  ![]_ ]_](_urbrack.gif)  
                   |
29 | 28 | imbi2d 318 |
. . 3
  
                ![]_ ]_](_urbrack.gif)    
                    |
30 | | dvnmptdivc.s |
. . . . . . 7
      |
31 | | recnprss 22871 |
. . . . . . 7
   
  |
32 | 30, 31 | syl 17 |
. . . . . 6

  |
33 | | cnex 9625 |
. . . . . . . 8
 |
34 | 33 | a1i 11 |
. . . . . . 7
   |
35 | | dvnmptdivc.a |
. . . . . . . . 9
 
   |
36 | | dvnmptdivc.c |
. . . . . . . . . 10
   |
37 | 36 | adantr 467 |
. . . . . . . . 9
 
   |
38 | | dvnmptdivc.cne0 |
. . . . . . . . . 10
   |
39 | 38 | adantr 467 |
. . . . . . . . 9
 
   |
40 | 35, 37, 39 | divcld 10390 |
. . . . . . . 8
 
     |
41 | | eqid 2453 |
. . . . . . . 8
         |
42 | 40, 41 | fmptd 6051 |
. . . . . . 7
           |
43 | | dvnmptdivc.x |
. . . . . . 7

  |
44 | | elpm2r 7494 |
. . . . . . 7
                      
   |
45 | 34, 30, 42, 43, 44 | syl22anc 1270 |
. . . . . 6
     
   |
46 | | dvn0 22890 |
. . . . . 6
 
                         |
47 | 32, 45, 46 | syl2anc 667 |
. . . . 5
                   |
48 | | id 22 |
. . . . . . . . . . . 12
   |
49 | | dvnmptdivc.8 |
. . . . . . . . . . . . . 14
   |
50 | | nn0uz 11200 |
. . . . . . . . . . . . . 14
     |
51 | 49, 50 | syl6eleq 2541 |
. . . . . . . . . . . . 13
       |
52 | | eluzfz1 11813 |
. . . . . . . . . . . . 13
    
      |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . 12
       |
54 | | nfv 1763 |
. . . . . . . . . . . . . 14
  
      |
55 | | nfcv 2594 |
. . . . . . . . . . . . . . 15
             |
56 | | nfcv 2594 |
. . . . . . . . . . . . . . . 16
   |
57 | | nfcsb1v 3381 |
. . . . . . . . . . . . . . . 16
  
 ![]_ ]_](_urbrack.gif)  |
58 | 56, 57 | nfmpt 4494 |
. . . . . . . . . . . . . . 15
     ![]_ ]_](_urbrack.gif)   |
59 | 55, 58 | nfeq 2605 |
. . . . . . . . . . . . . 14
               ![]_ ]_](_urbrack.gif)   |
60 | 54, 59 | nfim 2005 |
. . . . . . . . . . . . 13
   
                  ![]_ ]_](_urbrack.gif)    |
61 | | c0ex 9642 |
. . . . . . . . . . . . 13
 |
62 | | eleq1 2519 |
. . . . . . . . . . . . . . 15
     
       |
63 | 62 | anbi2d 711 |
. . . . . . . . . . . . . 14
  
    
         |
64 | | fveq2 5870 |
. . . . . . . . . . . . . . 15
                       |
65 | | csbeq1a 3374 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)   |
66 | 65 | mpteq2dv 4493 |
. . . . . . . . . . . . . . 15
      ![]_ ]_](_urbrack.gif)    |
67 | 64, 66 | eqeq12d 2468 |
. . . . . . . . . . . . . 14
             
             ![]_ ]_](_urbrack.gif)     |
68 | 63, 67 | imbi12d 322 |
. . . . . . . . . . . . 13
   
                   
                  ![]_ ]_](_urbrack.gif)      |
69 | | dvnmptdivc.dvn |
. . . . . . . . . . . . 13
 
                   |
70 | 60, 61, 68, 69 | vtoclf 3101 |
. . . . . . . . . . . 12
 
                  ![]_ ]_](_urbrack.gif)    |
71 | 48, 53, 70 | syl2anc 667 |
. . . . . . . . . . 11
              ![]_ ]_](_urbrack.gif)    |
72 | 71 | fveq1d 5872 |
. . . . . . . . . 10
                   ![]_ ]_](_urbrack.gif)       |
73 | 72 | adantr 467 |
. . . . . . . . 9
 
                   ![]_ ]_](_urbrack.gif)       |
74 | | simpr 463 |
. . . . . . . . . 10
 
   |
75 | | simpl 459 |
. . . . . . . . . . 11
 
   |
76 | 53 | adantr 467 |
. . . . . . . . . . 11
 
       |
77 | | 0re 9648 |
. . . . . . . . . . . 12
 |
78 | | nfcv 2594 |
. . . . . . . . . . . . 13
   |
79 | | nfv 1763 |
. . . . . . . . . . . . . 14
  
      |
80 | | nfcv 2594 |
. . . . . . . . . . . . . . 15
   |
81 | 57, 80 | nfel 2606 |
. . . . . . . . . . . . . 14
  
 ![]_ ]_](_urbrack.gif)
 |
82 | 79, 81 | nfim 2005 |
. . . . . . . . . . . . 13
   
       ![]_ ]_](_urbrack.gif)
  |
83 | 62 | 3anbi3d 1347 |
. . . . . . . . . . . . . 14
  
    

        |
84 | 65 | eleq1d 2515 |
. . . . . . . . . . . . . 14
 
  ![]_ ]_](_urbrack.gif)    |
85 | 83, 84 | imbi12d 322 |
. . . . . . . . . . . . 13
   
       
       ![]_ ]_](_urbrack.gif)
    |
86 | | dvnmptdivc.b |
. . . . . . . . . . . . 13
 
    
  |
87 | 78, 82, 85, 86 | vtoclgf 3107 |
. . . . . . . . . . . 12
  
       ![]_ ]_](_urbrack.gif)    |
88 | 77, 87 | ax-mp 5 |
. . . . . . . . . . 11
 
    
  ![]_ ]_](_urbrack.gif)   |
89 | 75, 74, 76, 88 | syl3anc 1269 |
. . . . . . . . . 10
 
   ![]_ ]_](_urbrack.gif)   |
90 | | eqid 2453 |
. . . . . . . . . . 11
   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)   |
91 | 90 | fvmpt2 5962 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)
     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
92 | 74, 89, 91 | syl2anc 667 |
. . . . . . . . 9
 
     ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)   |
93 | 73, 92 | eqtr2d 2488 |
. . . . . . . 8
 
   ![]_ ]_](_urbrack.gif)                 |
94 | | eqid 2453 |
. . . . . . . . . . . . 13
     |
95 | 35, 94 | fmptd 6051 |
. . . . . . . . . . . 12
         |
96 | | elpm2r 7494 |
. . . . . . . . . . . 12
                  
   |
97 | 34, 30, 95, 43, 96 | syl22anc 1270 |
. . . . . . . . . . 11
   
   |
98 | | dvn0 22890 |
. . . . . . . . . . 11
 
                   |
99 | 32, 97, 98 | syl2anc 667 |
. . . . . . . . . 10
               |
100 | 99 | fveq1d 5872 |
. . . . . . . . 9
                       |
101 | 100 | adantr 467 |
. . . . . . . 8
 
                       |
102 | 94 | fvmpt2 5962 |
. . . . . . . . 9
 
         |
103 | 74, 35, 102 | syl2anc 667 |
. . . . . . . 8
 
         |
104 | 93, 101, 103 | 3eqtrrd 2492 |
. . . . . . 7
 
   ![]_ ]_](_urbrack.gif)   |
105 | 104 | oveq1d 6310 |
. . . . . 6
 
      ![]_ ]_](_urbrack.gif)    |
106 | 105 | mpteq2dva 4492 |
. . . . 5
         ![]_ ]_](_urbrack.gif)
    |
107 | 47, 106 | eqtrd 2487 |
. . . 4
                 ![]_ ]_](_urbrack.gif)     |
108 | 107 | a1i 11 |
. . 3
    
                 ![]_ ]_](_urbrack.gif)      |
109 | | simp3 1011 |
. . . . 5
   ..^                  ![]_ ]_](_urbrack.gif)       |
110 | | simp1 1009 |
. . . . 5
   ..^                  ![]_ ]_](_urbrack.gif)      ..^   |
111 | | simpr 463 |
. . . . . . 7
                   ![]_ ]_](_urbrack.gif)
   
  |
112 | | simpl 459 |
. . . . . . 7
                   ![]_ ]_](_urbrack.gif)
   
                 ![]_ ]_](_urbrack.gif)      |
113 | 111, 112 | mpd 15 |
. . . . . 6
                   ![]_ ]_](_urbrack.gif)
   
                ![]_ ]_](_urbrack.gif)     |
114 | 113 | 3adant1 1027 |
. . . . 5
   ..^                  ![]_ ]_](_urbrack.gif)                     ![]_ ]_](_urbrack.gif)     |
115 | 32 | ad2antrr 733 |
. . . . . . 7
    ..^                  ![]_ ]_](_urbrack.gif)      |
116 | 45 | ad2antrr 733 |
. . . . . . 7
    ..^                  ![]_ ]_](_urbrack.gif)            |
117 | | elfzofz 11942 |
. . . . . . . 8
  ..^
      |
118 | | elfznn0 11894 |
. . . . . . . . 9
       |
119 | 118 | ad2antlr 734 |
. . . . . . . 8
                        ![]_ ]_](_urbrack.gif)
     |
120 | 117, 119 | sylanl2 657 |
. . . . . . 7
    ..^                  ![]_ ]_](_urbrack.gif)      |
121 | | dvnp1 22891 |
. . . . . . 7
 
     
                               |
122 | 115, 116,
120, 121 | syl3anc 1269 |
. . . . . 6
    ..^                  ![]_ ]_](_urbrack.gif)                                  |
123 | | oveq2 6303 |
. . . . . . 7
                 ![]_ ]_](_urbrack.gif)
                     ![]_ ]_](_urbrack.gif)      |
124 | 123 | adantl 468 |
. . . . . 6
    ..^                  ![]_ ]_](_urbrack.gif)                   
   ![]_ ]_](_urbrack.gif)      |
125 | 32 | adantr 467 |
. . . . . . . . . . 11
 
 ..^    |
126 | 45 | adantr 467 |
. . . . . . . . . . 11
 
 ..^          |
127 | | simpr 463 |
. . . . . . . . . . . . 13
 
           |
128 | 127, 118 | syl 17 |
. . . . . . . . . . . 12
 
       |
129 | 117, 128 | sylan2 477 |
. . . . . . . . . . 11
 
 ..^    |
130 | 125, 126,
129, 121 | syl3anc 1269 |
. . . . . . . . . 10
 
 ..^                                |
131 | 130 | adantr 467 |
. . . . . . . . 9
    ..^                  ![]_ ]_](_urbrack.gif)                                  |
132 | 30 | adantr 467 |
. . . . . . . . . . 11
 
 ..^   
   |
133 | | simplr 763 |
. . . . . . . . . . . . 13
               |
134 | 48 | ad2antrr 733 |
. . . . . . . . . . . . . 14
           |
135 | | simpr 463 |
. . . . . . . . . . . . . 14
           |
136 | 134, 135,
133 | 3jca 1189 |
. . . . . . . . . . . . 13
         
       |
137 | | nfcv 2594 |
. . . . . . . . . . . . . 14
   |
138 | | nfv 1763 |
. . . . . . . . . . . . . . 15
  
      |
139 | 137 | nfcsb1 3380 |
. . . . . . . . . . . . . . . 16
  
 ![]_ ]_](_urbrack.gif)  |
140 | 139, 80 | nfel 2606 |
. . . . . . . . . . . . . . 15
  
 ![]_ ]_](_urbrack.gif)
 |
141 | 138, 140 | nfim 2005 |
. . . . . . . . . . . . . 14
   
       ![]_ ]_](_urbrack.gif)
  |
142 | | eleq1 2519 |
. . . . . . . . . . . . . . . 16
     
       |
143 | 142 | 3anbi3d 1347 |
. . . . . . . . . . . . . . 15
  
    

        |
144 | | csbeq1a 3374 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)   |
145 | 144 | eleq1d 2515 |
. . . . . . . . . . . . . . 15
 
  ![]_ ]_](_urbrack.gif)    |
146 | 143, 145 | imbi12d 322 |
. . . . . . . . . . . . . 14
   
       
       ![]_ ]_](_urbrack.gif)
    |
147 | 137, 141,
146, 86 | vtoclgf 3107 |
. . . . . . . . . . . . 13
      
       ![]_ ]_](_urbrack.gif)    |
148 | 133, 136,
147 | sylc 62 |
. . . . . . . . . . . 12
           ![]_ ]_](_urbrack.gif)   |
149 | 117, 148 | sylanl2 657 |
. . . . . . . . . . 11
    ..^     ![]_ ]_](_urbrack.gif)   |
150 | | fzofzp1 12015 |
. . . . . . . . . . . . 13
  ..^
        |
151 | 150 | ad2antlr 734 |
. . . . . . . . . . . 12
    ..^           |
152 | 117, 134 | sylanl2 657 |
. . . . . . . . . . . . 13
    ..^     |
153 | | simpr 463 |
. . . . . . . . . . . . 13
    ..^     |
154 | 152, 153,
151 | 3jca 1189 |
. . . . . . . . . . . 12
    ..^             |
155 | | nfcv 2594 |
. . . . . . . . . . . . 13
     |
156 | | nfv 1763 |
. . . . . . . . . . . . . 14
  
        |
157 | 155 | nfcsb1 3380 |
. . . . . . . . . . . . . . 15
      ![]_ ]_](_urbrack.gif)  |
158 | 157, 80 | nfel 2606 |
. . . . . . . . . . . . . 14
      ![]_ ]_](_urbrack.gif)
 |
159 | 156, 158 | nfim 2005 |
. . . . . . . . . . . . 13
   
           ![]_ ]_](_urbrack.gif)
  |
160 | | eleq1 2519 |
. . . . . . . . . . . . . . 15
       
         |
161 | 160 | 3anbi3d 1347 |
. . . . . . . . . . . . . 14
    
    
           |
162 | | csbeq1a 3374 |
. . . . . . . . . . . . . . 15
       ![]_ ]_](_urbrack.gif)   |
163 | 162 | eleq1d 2515 |
. . . . . . . . . . . . . 14
   
    ![]_ ]_](_urbrack.gif)    |
164 | 161, 163 | imbi12d 322 |
. . . . . . . . . . . . 13
     
       
           ![]_ ]_](_urbrack.gif)
    |
165 | 155, 159,
164, 86 | vtoclgf 3107 |
. . . . . . . . . . . 12
        
           ![]_ ]_](_urbrack.gif)
   |
166 | 151, 154,
165 | sylc 62 |
. . . . . . . . . . 11
    ..^       ![]_ ]_](_urbrack.gif)   |
167 | | simpl 459 |
. . . . . . . . . . . . . . 15
 
 ..^    |
168 | 117 | adantl 468 |
. . . . . . . . . . . . . . 15
 
 ..^        |
169 | | nfv 1763 |
. . . . . . . . . . . . . . . . 17
  
      |
170 | | nfcv 2594 |
. . . . . . . . . . . . . . . . . 18
             |
171 | 56, 139 | nfmpt 4494 |
. . . . . . . . . . . . . . . . . 18
     ![]_ ]_](_urbrack.gif)   |
172 | 170, 171 | nfeq 2605 |
. . . . . . . . . . . . . . . . 17
               ![]_ ]_](_urbrack.gif)   |
173 | 169, 172 | nfim 2005 |
. . . . . . . . . . . . . . . 16
   
                  ![]_ ]_](_urbrack.gif)    |
174 | 142 | anbi2d 711 |
. . . . . . . . . . . . . . . . 17
  
    
         |
175 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . 18
                       |
176 | 144 | mpteq2dv 4493 |
. . . . . . . . . . . . . . . . . 18
      ![]_ ]_](_urbrack.gif)    |
177 | 175, 176 | eqeq12d 2468 |
. . . . . . . . . . . . . . . . 17
             
             ![]_ ]_](_urbrack.gif)     |
178 | 174, 177 | imbi12d 322 |
. . . . . . . . . . . . . . . 16
   
                   
                  ![]_ ]_](_urbrack.gif)      |
179 | 173, 178,
69 | chvar 2108 |
. . . . . . . . . . . . . . 15
 
                  ![]_ ]_](_urbrack.gif)    |
180 | 167, 168,
179 | syl2anc 667 |
. . . . . . . . . . . . . 14
 
 ..^               ![]_ ]_](_urbrack.gif)    |
181 | 180 | eqcomd 2459 |
. . . . . . . . . . . . 13
 
 ..^     ![]_ ]_](_urbrack.gif)              |
182 | 181 | oveq2d 6311 |
. . . . . . . . . . . 12
 
 ..^   
  ![]_ ]_](_urbrack.gif)                 |
183 | 167, 97 | syl 17 |
. . . . . . . . . . . . . 14
 
 ..^        |
184 | | dvnp1 22891 |
. . . . . . . . . . . . . 14
 
   
                           |
185 | 125, 183,
129, 184 | syl3anc 1269 |
. . . . . . . . . . . . 13
 
 ..^                            |
186 | 185 | eqcomd 2459 |
. . . . . . . . . . . 12
 
 ..^                            |
187 | 150 | adantl 468 |
. . . . . . . . . . . . 13
 
 ..^          |
188 | 167, 187 | jca 535 |
. . . . . . . . . . . . 13
 
 ..^            |
189 | | nfv 1763 |
. . . . . . . . . . . . . . 15
  
        |
190 | | nfcv 2594 |
. . . . . . . . . . . . . . . 16
               |
191 | 56, 157 | nfmpt 4494 |
. . . . . . . . . . . . . . . 16
       ![]_ ]_](_urbrack.gif)   |
192 | 190, 191 | nfeq 2605 |
. . . . . . . . . . . . . . 15
                   ![]_ ]_](_urbrack.gif)   |
193 | 189, 192 | nfim 2005 |
. . . . . . . . . . . . . 14
                            ![]_ ]_](_urbrack.gif)    |
194 | 160 | anbi2d 711 |
. . . . . . . . . . . . . . 15
    
    
           |
195 | | fveq2 5870 |
. . . . . . . . . . . . . . . 16
                           |
196 | 162 | mpteq2dv 4493 |
. . . . . . . . . . . . . . . 16
          ![]_ ]_](_urbrack.gif)    |
197 | 195, 196 | eqeq12d 2468 |
. . . . . . . . . . . . . . 15
               
                 ![]_ ]_](_urbrack.gif)     |
198 | 194, 197 | imbi12d 322 |
. . . . . . . . . . . . . 14
     
                                            ![]_ ]_](_urbrack.gif)      |
199 | 155, 193,
198, 69 | vtoclgf 3107 |
. . . . . . . . . . . . 13
        
                        ![]_ ]_](_urbrack.gif)     |
200 | 187, 188,
199 | sylc 62 |
. . . . . . . . . . . 12
 
 ..^                   ![]_ ]_](_urbrack.gif)    |
201 | 182, 186,
200 | 3eqtrd 2491 |
. . . . . . . . . . 11
 
 ..^   
  ![]_ ]_](_urbrack.gif)        ![]_ ]_](_urbrack.gif)    |
202 | 36 | adantr 467 |
. . . . . . . . . . 11
 
 ..^    |
203 | 38 | adantr 467 |
. . . . . . . . . . 11
 
 ..^    |
204 | 132, 149,
166, 201, 202, 203 | dvmptdivc 22931 |
. . . . . . . . . 10
 
 ..^   
   ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)     |
205 | 204 | adantr 467 |
. . . . . . . . 9
    ..^                  ![]_ ]_](_urbrack.gif)     
   ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)     |
206 | 131, 124,
205 | 3eqtrd 2491 |
. . . . . . . 8
    ..^                  ![]_ ]_](_urbrack.gif)                        ![]_ ]_](_urbrack.gif)     |
207 | 206 | eqcomd 2459 |
. . . . . . 7
    ..^                  ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)                   |
208 | 207, 122,
124 | 3eqtrrd 2492 |
. . . . . 6
    ..^                  ![]_ ]_](_urbrack.gif)     
   ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)     |
209 | 122, 124,
208 | 3eqtrd 2491 |
. . . . 5
    ..^                  ![]_ ]_](_urbrack.gif)                        ![]_ ]_](_urbrack.gif)     |
210 | 109, 110,
114, 209 | syl21anc 1268 |
. . . 4
   ..^                  ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)     |
211 | 210 | 3exp 1208 |
. . 3
  ..^
                  ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)
      |
212 | 8, 14, 20, 29, 108, 211 | fzind2 12030 |
. 2
                         |
213 | 1, 2, 212 | sylc 62 |
1
 
                       |