Step | Hyp | Ref
| Expression |
1 | | dfcnqs 7673 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif) ![/. /.](diagup.gif) ![) )](rp.gif) |
2 | | mulcnsrec 7675 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) ![>.
>.](rangle.gif) ![] ]](rbrack.gif) ![) )](rp.gif) |
3 | | mulcnsrec 7675 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![w w](_w.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif) ![) )](rp.gif) |
4 | | mulcnsrec 7675 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![w w](_w.gif) ![)
)](rp.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![v v](_v.gif) ![u u](_u.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif) ![)
)](rp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif) ![)
)](rp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif) ![) )](rp.gif) |
5 | | mulcnsrec 7675 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![x x](_x.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif)
![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![>.
>.](rangle.gif) ![] ]](rbrack.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![>. >.](rangle.gif) ![] ]](rbrack.gif)
![) )](rp.gif) |
6 | | mulclsr 7586 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![z z](_z.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
7 | | m1r 7584 |
. . . . . 6
![R. R.](calr.gif) |
8 | | mulclsr 7586 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![w w](_w.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
9 | | mulclsr 7586 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
10 | 7, 8, 9 | sylancr 411 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
11 | | addclsr 7585 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![(
(](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
12 | 6, 10, 11 | syl2an 287 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
13 | 12 | an4s 578 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
14 | | mulclsr 7586 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![z z](_z.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
15 | | mulclsr 7586 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![w w](_w.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
16 | | addclsr 7585 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif)
![w w](_w.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
17 | 14, 15, 16 | syl2anr 288 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![z z](_z.gif) ![( (](lp.gif) ![w w](_w.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
18 | 17 | an42s 579 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![z z](_z.gif) ![( (](lp.gif) ![w w](_w.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
19 | 13, 18 | jca 304 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) ![) )](rp.gif) |
20 | | mulclsr 7586 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![v v](_v.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
21 | | mulclsr 7586 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![u u](_u.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
22 | | mulclsr 7586 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
23 | 7, 21, 22 | sylancr 411 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
24 | | addclsr 7585 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![(
(](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
25 | 20, 23, 24 | syl2an 287 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
26 | 25 | an4s 578 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
27 | | mulclsr 7586 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![v v](_v.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
28 | | mulclsr 7586 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![u u](_u.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
29 | | addclsr 7585 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
30 | 27, 28, 29 | syl2anr 288 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
31 | 30 | an42s 579 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
32 | 26, 31 | jca 304 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | | simp1l 1006 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![R. R.](calr.gif) ![) )](rp.gif) |
34 | | simp2l 1008 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![R. R.](calr.gif) ![) )](rp.gif) |
35 | | simp3l 1010 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![R. R.](calr.gif) ![) )](rp.gif) |
36 | 34, 35, 20 | syl2anc 409 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![v v](_v.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
37 | | mulclsr 7586 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
38 | 33, 36, 37 | syl2anc 409 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
39 | | simp2r 1009 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![R. R.](calr.gif) ![) )](rp.gif) |
40 | | simp3r 1011 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![R. R.](calr.gif) ![) )](rp.gif) |
41 | 39, 40, 21 | syl2anc 409 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![u u](_u.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
42 | 7, 41, 22 | sylancr 411 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
43 | | mulclsr 7586 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
44 | 33, 42, 43 | syl2anc 409 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
45 | | simp1r 1007 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![R. R.](calr.gif) ![) )](rp.gif) |
46 | 39, 35, 27 | syl2anc 409 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![v v](_v.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
47 | | mulclsr 7586 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
48 | 45, 46, 47 | syl2anc 409 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
49 | | mulclsr 7586 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
50 | 7, 48, 49 | sylancr 411 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![) )](rp.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
51 | | addcomsrg 7587 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![g g](_g.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) |
52 | 51 | adantl 275 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![R.
R.](calr.gif) ![) )](rp.gif) ![(
(](lp.gif) ![g g](_g.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | | addasssrg 7588 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.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) |
54 | 53 | adantl 275 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif)
![R. R.](calr.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) |
55 | 34, 40, 28 | syl2anc 409 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![u u](_u.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
56 | | mulclsr 7586 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
57 | 45, 55, 56 | syl2anc 409 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
58 | | mulclsr 7586 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
59 | 7, 57, 58 | sylancr 411 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
60 | | addclsr 7585 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![g g](_g.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
61 | 60 | adantl 275 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![R.
R.](calr.gif) ![) )](rp.gif) ![(
(](lp.gif) ![g g](_g.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
62 | 38, 44, 50, 52, 54, 59, 61 | caov42d 5965 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.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) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
63 | | distrsrg 7591 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
64 | 33, 36, 42, 63 | syl3anc 1217 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
65 | | distrsrg 7591 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
66 | 45, 46, 55, 65 | syl3anc 1217 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
67 | 66 | oveq2d 5798 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
68 | 7 | a1i 9 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![R. R.](calr.gif) ![) )](rp.gif) |
69 | | distrsrg 7591 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.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) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
70 | 68, 48, 57, 69 | syl3anc 1217 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.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) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
71 | 67, 70 | eqtrd 2173 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.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) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
72 | 64, 71 | oveq12d 5800 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.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) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
73 | | mulcomsrg 7589 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![g g](_g.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) |
74 | 73 | adantl 275 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![R.
R.](calr.gif) ![) )](rp.gif) ![(
(](lp.gif) ![g g](_g.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) |
75 | | distrsrg 7591 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif)
![( (](lp.gif) ![g g](_g.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![( (](lp.gif)
![g g](_g.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
76 | 75 | 3coml 1189 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif)
![( (](lp.gif) ![g g](_g.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![( (](lp.gif)
![g g](_g.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
77 | | simp3 984 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
78 | 60 | 3adant3 1002 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![g g](_g.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
79 | | mulcomsrg 7589 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![g g](_g.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif) ![g g](_g.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![g g](_g.gif) ![h h](_h.gif) ![) )](rp.gif) ![) )](rp.gif) |
80 | 77, 78, 79 | syl2anc 409 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif)
![( (](lp.gif) ![g g](_g.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![g g](_g.gif) ![h h](_h.gif) ![)
)](rp.gif) ![) )](rp.gif) |
81 | | simp1 982 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
82 | | mulcomsrg 7589 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![f f](_f.gif) ![( (](lp.gif) ![h h](_h.gif) ![) )](rp.gif) ![) )](rp.gif) |
83 | 77, 81, 82 | syl2anc 409 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif)
![f f](_f.gif) ![( (](lp.gif) ![h h](_h.gif) ![) )](rp.gif) ![) )](rp.gif) |
84 | | simp2 983 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
85 | | mulcomsrg 7589 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![g g](_g.gif) ![( (](lp.gif) ![h h](_h.gif) ![) )](rp.gif) ![) )](rp.gif) |
86 | 77, 84, 85 | syl2anc 409 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif)
![g g](_g.gif) ![( (](lp.gif) ![h h](_h.gif) ![) )](rp.gif) ![) )](rp.gif) |
87 | 83, 86 | oveq12d 5800 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![f f](_f.gif) ![( (](lp.gif) ![g g](_g.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![h h](_h.gif) ![( (](lp.gif) ![h h](_h.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
88 | 76, 80, 87 | 3eqtr3d 2181 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.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) |
89 | 88 | adantl 275 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif)
![R. R.](calr.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) |
90 | | mulasssrg 7590 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.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) |
91 | 90 | adantl 275 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif)
![R. R.](calr.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) |
92 | | mulclsr 7586 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![g g](_g.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
93 | 92 | adantl 275 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![R.
R.](calr.gif) ![) )](rp.gif) ![(
(](lp.gif) ![g g](_g.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
94 | 45, 39, 8 | syl2anc 409 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![w w](_w.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
95 | 74, 89, 91, 93, 33, 68, 34, 94, 35 | caovdilemd 5970 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
96 | | mulasssrg 7590 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.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) |
97 | 45, 39, 35, 96 | syl3anc 1217 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.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) |
98 | 97 | oveq2d 5798 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![v v](_v.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
99 | 98 | oveq2d 5798 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![w w](_w.gif)
![v v](_v.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
100 | 95, 99 | eqtrd 2173 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
101 | 74, 89, 91, 93, 45, 33, 34, 39, 40 | caovdilemd 5970 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![w w](_w.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) |
102 | 101 | oveq2d 5798 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![w w](_w.gif) ![)
)](rp.gif) ![u u](_u.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) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
103 | 93, 33, 41 | caovcld 5932 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
104 | | distrsrg 7591 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![R. R.](calr.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) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
105 | 68, 57, 103, 104 | syl3anc 1217 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.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) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
106 | 68, 33, 41, 74, 91 | caov12d 5960 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
107 | 106 | oveq2d 5798 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
108 | 102, 105,
107 | 3eqtrd 2177 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![w w](_w.gif) ![)
)](rp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
109 | 100, 108 | oveq12d 5800 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
110 | 62, 72, 109 | 3eqtr4rd 2184 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
111 | 93, 45, 36 | caovcld 5932 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
112 | 93, 45, 42 | caovcld 5932 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
113 | 93, 33, 46 | caovcld 5932 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
114 | 93, 33, 55 | caovcld 5932 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
115 | 111, 112,
113, 52, 54, 114, 61 | caov42d 5965 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.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) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
116 | | distrsrg 7591 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
117 | 45, 36, 42, 116 | syl3anc 1217 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
118 | | distrsrg 7591 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
119 | 33, 46, 55, 118 | syl3anc 1217 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
120 | 117, 119 | oveq12d 5800 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif)
![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
121 | 74, 89, 91, 93, 45, 33, 34, 39, 35 | caovdilemd 5970 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![v v](_v.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
122 | 74, 89, 91, 93, 33, 68, 34, 94, 40 | caovdilemd 5970 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) ![u u](_u.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
123 | | mulasssrg 7590 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.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) |
124 | 45, 39, 40, 123 | syl3anc 1217 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.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) |
125 | 124 | oveq2d 5798 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
126 | 68, 45, 41, 74, 91 | caov12d 5960 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![u u](_u.gif) ![) )](rp.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
127 | 125, 126 | eqtrd 2173 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
128 | 127 | oveq2d 5798 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![w w](_w.gif)
![u u](_u.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) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
129 | 122, 128 | eqtrd 2173 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) ![u u](_u.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) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
130 | 121, 129 | oveq12d 5800 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif)
![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif) ![)
)](rp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.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) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
131 | 115, 120,
130 | 3eqtr4rd 2184 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif)
![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif)
![w w](_w.gif) ![) )](rp.gif) ![)
)](rp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![( (](lp.gif) ![u u](_u.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![v v](_v.gif) ![( (](lp.gif) ![u u](_u.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
132 | 1, 2, 3, 4, 5, 19,
32, 110, 131 | ecoviass 6547 |
1
![( (](lp.gif) ![( (](lp.gif)
![CC CC](bbc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |