Step | Hyp | Ref
| Expression |
1 | | df-nq0 7257 |
. . . 4
Q0 ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
~Q0 ![) )](rp.gif) |
2 | | oveq2 5790 |
. . . . . . 7
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif)
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) +Q0 ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
3 | 2 | oveq1d 5797 |
. . . . . 6
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif) ![( (](lp.gif) +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) ![( (](lp.gif) +Q0 ![B B](_cb.gif) +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![) )](rp.gif) |
4 | | oveq1 5789 |
. . . . . . 7
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif)
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![) )](rp.gif) |
5 | 4 | oveq2d 5798 |
. . . . . 6
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif)
+Q0 ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![( (](lp.gif) +Q0 ![( (](lp.gif) +Q0 ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
6 | 3, 5 | eqeq12d 2155 |
. . . . 5
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif)
+Q0 ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) +Q0 ![B B](_cb.gif) +Q0 ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif)
+Q0 ![( (](lp.gif)
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | 6 | imbi2d 229 |
. . . 4
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif) ![( (](lp.gif) Q0 ![( (](lp.gif) ![( (](lp.gif)
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif)
+Q0 ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![)
)](rp.gif)
![( (](lp.gif) Q0 ![(
(](lp.gif) ![( (](lp.gif)
+Q0 ![B B](_cb.gif)
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) +Q0 ![( (](lp.gif) +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | | oveq2 5790 |
. . . . . 6
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif) ![( (](lp.gif) +Q0 ![B B](_cb.gif) +Q0 ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif) ![( (](lp.gif) +Q0 ![B B](_cb.gif) +Q0 ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
9 | | oveq2 5790 |
. . . . . . 7
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif)
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) +Q0 ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
10 | 9 | oveq2d 5798 |
. . . . . 6
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif)
+Q0 ![( (](lp.gif)
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![( (](lp.gif) +Q0 ![( (](lp.gif)
+Q0 ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
11 | 8, 10 | eqeq12d 2155 |
. . . . 5
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) +Q0 ![B B](_cb.gif)
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) +Q0 ![( (](lp.gif) +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) +Q0 ![B B](_cb.gif) +Q0 ![C C](_cc.gif) ![( (](lp.gif) +Q0 ![( (](lp.gif)
+Q0 ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | 11 | imbi2d 229 |
. . . 4
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif) ![( (](lp.gif) Q0 ![( (](lp.gif) ![( (](lp.gif)
+Q0 ![B B](_cb.gif)
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) +Q0 ![( (](lp.gif) +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) Q0 ![(
(](lp.gif) ![( (](lp.gif)
+Q0 ![B B](_cb.gif)
+Q0 ![C C](_cc.gif) ![( (](lp.gif) +Q0 ![( (](lp.gif)
+Q0 ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | | oveq1 5789 |
. . . . . . . . 9
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0 +Q0
![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 ![( (](lp.gif) +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) ![) )](rp.gif) |
14 | 13 | oveq1d 5797 |
. . . . . . . 8
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) ![( (](lp.gif) +Q0 ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) ![) )](rp.gif) |
15 | | oveq1 5789 |
. . . . . . . 8
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0 +Q0
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![( (](lp.gif) +Q0 ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | 14, 15 | eqeq12d 2155 |
. . . . . . 7
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0 +Q0
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) +Q0 ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![( (](lp.gif) +Q0 ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | 16 | imbi2d 229 |
. . . . . 6
![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif)
![N. N.](caln.gif)
![( (](lp.gif)
![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0 +Q0
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) +Q0 ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![( (](lp.gif) +Q0 ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
18 | | simp1l 1006 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![om om](omega.gif) ![) )](rp.gif) |
19 | | simp2r 1009 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![N. N.](caln.gif) ![) )](rp.gif) |
20 | | pinn 7141 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![om om](omega.gif) ![) )](rp.gif) |
21 | 19, 20 | syl 14 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![om om](omega.gif) ![) )](rp.gif) |
22 | | simp3r 1011 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![N. N.](caln.gif) ![) )](rp.gif) |
23 | | pinn 7141 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![om om](omega.gif) ![) )](rp.gif) |
24 | 22, 23 | syl 14 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![om om](omega.gif) ![) )](rp.gif) |
25 | | nnmcl 6385 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![om om](omega.gif) ![( (](lp.gif) ![u u](_u.gif) ![om om](omega.gif) ![) )](rp.gif) |
26 | 21, 24, 25 | syl2anc 409 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![u u](_u.gif) ![om om](omega.gif) ![) )](rp.gif) |
27 | | nnmcl 6385 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![om om](omega.gif) ![) )](rp.gif) |
28 | 18, 26, 27 | syl2anc 409 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![om om](omega.gif) ![) )](rp.gif) |
29 | | simp1r 1007 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![N. N.](caln.gif) ![) )](rp.gif) |
30 | | pinn 7141 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![om om](omega.gif) ![) )](rp.gif) |
31 | 29, 30 | syl 14 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![om om](omega.gif) ![) )](rp.gif) |
32 | | simp2l 1008 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![om om](omega.gif) ![) )](rp.gif) |
33 | | nnmcl 6385 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![om om](omega.gif) ![( (](lp.gif) ![u u](_u.gif) ![om om](omega.gif) ![) )](rp.gif) |
34 | 32, 24, 33 | syl2anc 409 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![u u](_u.gif) ![om om](omega.gif) ![) )](rp.gif) |
35 | | nnmcl 6385 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![om om](omega.gif) ![) )](rp.gif) |
36 | 31, 34, 35 | syl2anc 409 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![om om](omega.gif) ![) )](rp.gif) |
37 | | simp3l 1010 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![om om](omega.gif) ![) )](rp.gif) |
38 | | nnmcl 6385 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![om om](omega.gif) ![( (](lp.gif) ![v v](_v.gif) ![om om](omega.gif) ![) )](rp.gif) |
39 | 21, 37, 38 | syl2anc 409 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![v v](_v.gif) ![om om](omega.gif) ![) )](rp.gif) |
40 | | nnmcl 6385 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![om om](omega.gif) ![) )](rp.gif) |
41 | 31, 39, 40 | syl2anc 409 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![om om](omega.gif) ![) )](rp.gif) |
42 | | nnaass 6389 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
43 | 28, 36, 41, 42 | syl3anc 1217 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
44 | | nnmcom 6393 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![om om](omega.gif) ![( (](lp.gif) ![g g](_g.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) |
45 | 44 | adantl 275 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![N. N.](caln.gif)
![( (](lp.gif)
![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![om
om](omega.gif) ![) )](rp.gif) ![(
(](lp.gif) ![g g](_g.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) |
46 | | nndir 6394 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![om om](omega.gif) ![( (](lp.gif) ![(
(](lp.gif) ![g g](_g.gif) ![h h](_h.gif) ![( (](lp.gif) ![( (](lp.gif) ![h h](_h.gif) ![( (](lp.gif) ![h h](_h.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
47 | 46 | adantl 275 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![N. N.](caln.gif)
![( (](lp.gif)
![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif)
![om om](omega.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![g g](_g.gif) ![h h](_h.gif) ![( (](lp.gif) ![( (](lp.gif) ![h h](_h.gif) ![( (](lp.gif) ![h h](_h.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
48 | | nnmass 6391 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![om om](omega.gif) ![( (](lp.gif) ![(
(](lp.gif) ![g g](_g.gif) ![h h](_h.gif) ![( (](lp.gif) ![( (](lp.gif) ![h h](_h.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
49 | 48 | adantl 275 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![N. N.](caln.gif)
![( (](lp.gif)
![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif)
![om om](omega.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![g g](_g.gif) ![h h](_h.gif) ![( (](lp.gif) ![( (](lp.gif) ![h h](_h.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
50 | | nnmcl 6385 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![om om](omega.gif) ![( (](lp.gif) ![g g](_g.gif) ![om om](omega.gif) ![) )](rp.gif) |
51 | 50 | adantl 275 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![N. N.](caln.gif)
![( (](lp.gif)
![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![om
om](omega.gif) ![) )](rp.gif) ![(
(](lp.gif) ![g g](_g.gif) ![om om](omega.gif) ![) )](rp.gif) |
52 | 45, 47, 49, 51, 18, 31, 21, 32, 24 | caovdilemd 5970 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | | nnmass 6391 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![om om](omega.gif) ![( (](lp.gif) ![(
(](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
54 | 31, 21, 37, 53 | syl3anc 1217 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
55 | 52, 54 | oveq12d 5800 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
56 | | nndi 6390 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif)
![v v](_v.gif) ![om om](omega.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
57 | 31, 34, 39, 56 | syl3anc 1217 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
58 | 57 | oveq2d 5798 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
59 | 43, 55, 58 | 3eqtr4d 2183 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
60 | | nnmass 6391 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![om om](omega.gif) ![( (](lp.gif) ![(
(](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
61 | 31, 21, 24, 60 | syl3anc 1217 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
62 | | opeq12 3715 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![(
(](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![) )](rp.gif)
![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![) )](rp.gif) |
63 | 62 | eceq1d 6473 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![(
(](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) |
64 | 59, 61, 63 | syl2anc 409 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) |
65 | | addnnnq0 7281 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0 +Q0
![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) |
66 | 65 | oveq1d 5797 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ~Q0 +Q0
![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) ![) )](rp.gif) |
67 | 66 | adantr 274 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![N. N.](caln.gif)
![( (](lp.gif)
![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![N.
N.](caln.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ~Q0 +Q0
![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) ![) )](rp.gif) |
68 | | addassnq0lemcl 7293 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![w w](_w.gif) ![N. N.](caln.gif) ![) )](rp.gif) ![) )](rp.gif) |
69 | | addnnnq0 7281 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![( (](lp.gif) ![w w](_w.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ~Q0 +Q0
![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) |
70 | 68, 69 | sylan 281 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![N. N.](caln.gif)
![( (](lp.gif)
![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![N.
N.](caln.gif) ![) )](rp.gif) ![(
(](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![) )](rp.gif) ![>.
>.](rangle.gif) ~Q0 ![) )](rp.gif) |
71 | 67, 70 | eqtrd 2173 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![N. N.](caln.gif)
![( (](lp.gif)
![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![N.
N.](caln.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) |
72 | 71 | 3impa 1177 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0
![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![( (](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) |
73 | | addnnnq0 7281 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0
![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) |
74 | 73 | oveq2d 5798 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0 +Q0
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) ![) )](rp.gif) |
75 | 74 | adantl 275 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif)
![N. N.](caln.gif)
![( (](lp.gif)
![N. N.](caln.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ~Q0 +Q0 ![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) ![) )](rp.gif) |
76 | | addassnq0lemcl 7293 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![u u](_u.gif) ![N. N.](caln.gif) ![) )](rp.gif) ![) )](rp.gif) |
77 | | addnnnq0 7281 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![( (](lp.gif) ![u u](_u.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0 +Q0
![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) |
78 | 76, 77 | sylan2 284 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif)
![N. N.](caln.gif)
![( (](lp.gif)
![N. N.](caln.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) |
79 | 75, 78 | eqtrd 2173 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif)
![N. N.](caln.gif)
![( (](lp.gif)
![N. N.](caln.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ~Q0 +Q0 ![( (](lp.gif) ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) |
80 | 79 | 3impb 1178 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0 +Q0
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) |
81 | 64, 72, 80 | 3eqtr4d 2183 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0 +Q0
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
82 | 81 | 3expib 1185 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif)
![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ~Q0 +Q0
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
83 | 1, 17, 82 | ecoptocl 6524 |
. . . . 5
![( (](lp.gif) Q0 ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif)
![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) +Q0 ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![( (](lp.gif) +Q0 ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif)
~Q0 ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
84 | 83 | com12 30 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![N. N.](caln.gif) ![) )](rp.gif)
![( (](lp.gif) Q0 ![(
(](lp.gif) ![( (](lp.gif)
+Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ~Q0 +Q0 ![[ [](lbrack.gif) ![<.
<.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![( (](lp.gif)
+Q0 ![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif)
~Q0 +Q0 ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ~Q0 ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
85 | 1, 7, 12, 84 | 2ecoptocl 6525 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
Q0
Q0
![( (](lp.gif) Q0 ![(
(](lp.gif) ![( (](lp.gif)
+Q0 ![B B](_cb.gif)
+Q0 ![C C](_cc.gif) ![( (](lp.gif) +Q0 ![( (](lp.gif)
+Q0 ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
86 | 85 | com12 30 |
. 2
![( (](lp.gif) Q0 ![( (](lp.gif) ![( (](lp.gif) Q0 Q0 ![( (](lp.gif) ![( (](lp.gif) +Q0 ![B B](_cb.gif) +Q0 ![C C](_cc.gif) ![( (](lp.gif) +Q0 ![( (](lp.gif) +Q0 ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
87 | 86 | 3impib 1180 |
1
![( (](lp.gif) ![( (](lp.gif)
Q0
Q0
Q0
![( (](lp.gif) ![( (](lp.gif) +Q0 ![B B](_cb.gif) +Q0 ![C C](_cc.gif) ![( (](lp.gif) +Q0 ![( (](lp.gif)
+Q0 ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |