Step | Hyp | Ref
| Expression |
1 | | caucvgsr.f |
. . . 4
![( (](lp.gif) ![F F](_cf.gif) ![: :](colon.gif) ![N. N.](caln.gif) ![--> -->](longrightarrow.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
2 | | caucvgsr.cau |
. . . 4
![( (](lp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![[
[](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![*Q *Q](_astq.gif) ![` `](backtick.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![n n](_n.gif) ![1o 1o](_1o.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![} }](rbrace.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![*Q *Q](_astq.gif) ![` `](backtick.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![n n](_n.gif) ![1o 1o](_1o.gif) ![>. >.](rangle.gif) ![u u](_u.gif) ![} }](rbrace.gif)
![1P 1P](_1p.gif) ![) )](rp.gif) ![1P 1P](_1p.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![n n](_n.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![*Q *Q](_astq.gif) ![` `](backtick.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![n n](_n.gif) ![1o 1o](_1o.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif)
![( (](lp.gif) ![*Q *Q](_astq.gif) ![` `](backtick.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![n n](_n.gif) ![1o 1o](_1o.gif) ![>. >.](rangle.gif) ![u u](_u.gif) ![} }](rbrace.gif) ![1P 1P](_1p.gif) ![) )](rp.gif)
![1P 1P](_1p.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
3 | | caucvgsrlembnd.bnd |
. . . 4
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) |
4 | | caucvgsrlembnd.offset |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![a a](_a.gif) ![1R
1R](_1cr.gif) ![( (](lp.gif) ![-1R -1R](_m1r.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | 1, 2, 3, 4 | caucvgsrlemofff 7629 |
. . 3
![( (](lp.gif) ![G G](_cg.gif) ![: :](colon.gif) ![N. N.](caln.gif) ![--> -->](longrightarrow.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
6 | 1, 2, 3, 4 | caucvgsrlemoffcau 7630 |
. . 3
![( (](lp.gif) ![A. A.](forall.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![n n](_n.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![[
[](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![<. <.](langle.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![*Q *Q](_astq.gif) ![` `](backtick.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![n n](_n.gif) ![1o 1o](_1o.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![} }](rbrace.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![*Q *Q](_astq.gif) ![` `](backtick.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![n n](_n.gif) ![1o 1o](_1o.gif) ![>. >.](rangle.gif) ![u u](_u.gif) ![} }](rbrace.gif)
![1P 1P](_1p.gif) ![) )](rp.gif) ![1P 1P](_1p.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![(
(](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![n n](_n.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![( (](lp.gif) ![<.
<.](langle.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![*Q *Q](_astq.gif) ![` `](backtick.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![n n](_n.gif) ![1o 1o](_1o.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif)
![( (](lp.gif) ![*Q *Q](_astq.gif) ![` `](backtick.gif) ![[ [](lbrack.gif) ![<. <.](langle.gif) ![n n](_n.gif) ![1o 1o](_1o.gif) ![>. >.](rangle.gif) ![u u](_u.gif) ![} }](rbrace.gif) ![1P 1P](_1p.gif) ![) )](rp.gif)
![1P 1P](_1p.gif) ![>. >.](rangle.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | 1, 2, 3, 4 | caucvgsrlemoffgt1 7631 |
. . 3
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![m m](_m.gif) ![) )](rp.gif) ![) )](rp.gif) |
8 | 5, 6, 7 | caucvgsrlemgt1 7627 |
. 2
![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![`
`](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
9 | | simprl 521 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
10 | 3 | caucvgsrlemasr 7622 |
. . . . . 6
![( (](lp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
11 | 10 | adantr 274 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
12 | | addclsr 7585 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
13 | 9, 11, 12 | syl2anc 409 |
. . . 4
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
14 | | m1r 7584 |
. . . 4
![R. R.](calr.gif) |
15 | | addclsr 7585 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R. R.](calr.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif)
![R. R.](calr.gif) ![) )](rp.gif) |
16 | 13, 14, 15 | sylancl 410 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
17 | | ltasrg 7602 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif)
![( (](lp.gif) ![f f](_f.gif) ![( (](lp.gif) ![g g](_g.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
18 | 17 | adantl 275 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![) )](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![f f](_f.gif) ![( (](lp.gif) ![g g](_g.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | 5 | ad3antrrr 484 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![G G](_cg.gif) ![: :](colon.gif) ![N. N.](caln.gif) ![--> -->](longrightarrow.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
20 | | simpr 109 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![N. N.](caln.gif) ![) )](rp.gif) |
21 | 19, 20 | ffvelrnd 5564 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
22 | | simpllr 524 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
23 | | simplr 520 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
24 | | addclsr 7585 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![x x](_x.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
25 | 22, 23, 24 | syl2anc 409 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![x x](_x.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
26 | 10 | ad3antrrr 484 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
27 | | addcomsrg 7587 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![g g](_g.gif) ![( (](lp.gif) ![f f](_f.gif) ![) )](rp.gif) ![) )](rp.gif) |
28 | 27 | adantl 275 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.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) |
29 | 18, 21, 25, 26, 28 | caovord2d 5948 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![(
(](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![x x](_x.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | 1, 2, 3, 4 | caucvgsrlemoffval 7628 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif)
![N. N.](caln.gif)
![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | 30 | adantlr 469 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![(
(](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R
1R](_1cr.gif) ![) )](rp.gif) ![) )](rp.gif) |
32 | 31 | adantlr 469 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![) )](rp.gif) ![)
)](rp.gif) |
33 | 32 | breq1d 3947 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![A A](_ca.gif) ![(
(](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R
1R](_1cr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![x x](_x.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
34 | 29, 33 | bitrd 187 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![(
(](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R
1R](_1cr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![x x](_x.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | | addasssrg 7588 |
. . . . . . . . . . . . . . . 16
![( (](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) |
36 | 35 | adantl 275 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.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) |
37 | 22, 23, 26, 28, 36 | caov32d 5959 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 37 | breq2d 3949 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![(
(](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R
1R](_1cr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
39 | 1 | ad2antrr 480 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![R. R.](calr.gif) ![F F](_cf.gif) ![: :](colon.gif) ![N. N.](caln.gif) ![--> -->](longrightarrow.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
40 | 39 | ffvelrnda 5563 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
41 | | 1sr 7583 |
. . . . . . . . . . . . . . . 16
![R. R.](calr.gif) |
42 | | addclsr 7585 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![R. R.](calr.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif)
![R. R.](calr.gif) ![) )](rp.gif) |
43 | 40, 41, 42 | sylancl 410 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R
1R](_1cr.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
44 | 22, 26, 12 | syl2anc 409 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![A A](_ca.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
45 | | addclsr 7585 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![x x](_x.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
46 | 44, 23, 45 | syl2anc 409 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![x x](_x.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
47 | 14 | a1i 9 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif)
![R. R.](calr.gif) ![) )](rp.gif) |
48 | 18, 43, 46, 47, 28 | caovord2d 5948 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![x x](_x.gif) ![-1R -1R](_m1r.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
49 | 41 | a1i 9 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif)
![R. R.](calr.gif) ![) )](rp.gif) |
50 | | addasssrg 7588 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![-1R -1R](_m1r.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
51 | 40, 49, 47, 50 | syl3anc 1217 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![-1R -1R](_m1r.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
52 | | addcomsrg 7587 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![(
(](lp.gif) ![-1R -1R](_m1r.gif)
![( (](lp.gif) ![1R
1R](_1cr.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | 41, 14, 52 | mp2an 423 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![1R 1R](_1cr.gif) ![) )](rp.gif) |
54 | | m1p1sr 7592 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![1R 1R](_1cr.gif) ![0R 0R](_0r.gif) |
55 | 53, 54 | eqtri 2161 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![-1R -1R](_m1r.gif) ![0R 0R](_0r.gif) |
56 | 55 | oveq2i 5793 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![-1R -1R](_m1r.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![0R 0R](_0r.gif) ![) )](rp.gif) |
57 | | 0idsr 7599 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![0R 0R](_0r.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![) )](rp.gif) ![) )](rp.gif) |
58 | 40, 57 | syl 14 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![0R 0R](_0r.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![) )](rp.gif) ![) )](rp.gif) |
59 | 56, 58 | syl5eq 2185 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![-1R -1R](_m1r.gif) ![) )](rp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![) )](rp.gif) ![) )](rp.gif) |
60 | 51, 59 | eqtrd 2173 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![) )](rp.gif) ![) )](rp.gif) |
61 | 44, 23, 47, 28, 36 | caov32d 5959 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![x x](_x.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
62 | 60, 61 | breq12d 3950 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![x x](_x.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
63 | 48, 62 | bitrd 187 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![x x](_x.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
64 | 34, 38, 63 | 3bitrd 213 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![(
(](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
65 | 64 | biimpd 143 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![(
(](lp.gif) ![x x](_x.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
66 | | addclsr 7585 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
67 | 21, 23, 66 | syl2anc 409 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
68 | 18, 22, 67, 26, 28 | caovord2d 5948 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
69 | 21, 23, 26, 28, 36 | caov32d 5959 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![A A](_ca.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
70 | 32 | oveq1d 5797 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![A A](_ca.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
71 | 69, 70 | eqtrd 2173 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
72 | 71 | breq2d 3949 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![A A](_ca.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
73 | 68, 72 | bitrd 187 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
74 | | addclsr 7585 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![x x](_x.gif) ![R.
R.](calr.gif) ![) )](rp.gif) |
75 | 43, 23, 74 | syl2anc 409 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![x x](_x.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
76 | 18, 44, 75, 47, 28 | caovord2d 5948 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R
1R](_1cr.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R
1R](_1cr.gif) ![x x](_x.gif) ![-1R -1R](_m1r.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
77 | 40, 49, 23, 28, 36 | caov32d 5959 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![1R 1R](_1cr.gif) ![) )](rp.gif) ![)
)](rp.gif) |
78 | 77 | oveq1d 5797 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![x x](_x.gif) ![-1R -1R](_m1r.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![1R 1R](_1cr.gif) ![-1R -1R](_m1r.gif) ![) )](rp.gif) ![) )](rp.gif) |
79 | | addclsr 7585 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif)
![R. R.](calr.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
80 | 40, 23, 79 | syl2anc 409 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![R. R.](calr.gif) ![) )](rp.gif) |
81 | | addasssrg 7588 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![1R 1R](_1cr.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![( (](lp.gif) ![-1R -1R](_m1r.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
82 | 80, 49, 47, 81 | syl3anc 1217 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![1R 1R](_1cr.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![( (](lp.gif) ![-1R -1R](_m1r.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
83 | 78, 82 | eqtrd 2173 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![x x](_x.gif) ![-1R -1R](_m1r.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![( (](lp.gif) ![-1R -1R](_m1r.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
84 | 55 | oveq2i 5793 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![( (](lp.gif) ![-1R -1R](_m1r.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![0R 0R](_0r.gif) ![) )](rp.gif) |
85 | 83, 84 | eqtrdi 2189 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![x x](_x.gif) ![-1R -1R](_m1r.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![0R 0R](_0r.gif) ![) )](rp.gif) ![) )](rp.gif) |
86 | | 0idsr 7599 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![0R 0R](_0r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
87 | 80, 86 | syl 14 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![0R 0R](_0r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
88 | 85, 87 | eqtrd 2173 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![x x](_x.gif) ![-1R -1R](_m1r.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
89 | 88 | breq2d 3949 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![1R 1R](_1cr.gif) ![x x](_x.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
90 | 73, 76, 89 | 3bitrd 213 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
91 | 90 | biimpd 143 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
92 | 65, 91 | anim12d 333 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
93 | 92 | imim2d 54 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![R. R.](calr.gif) ![N. N.](caln.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
94 | 93 | ralimdva 2502 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
95 | | breq2 3941 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) |
96 | | fveq2 5429 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![) )](rp.gif) ![) )](rp.gif) |
97 | 96 | breq1d 3947 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
98 | 96 | oveq1d 5797 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
99 | 98 | breq2d 3949 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
100 | 97, 99 | anbi12d 465 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
101 | 95, 100 | imbi12d 233 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
102 | 101 | cbvralv 2657 |
. . . . . . . 8
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif)
![A. A.](forall.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
103 | 94, 102 | syl6ib 160 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
104 | 103 | reximdv 2536 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![E. E.](exists.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
105 | 104 | imim2d 54 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![R. R.](calr.gif) ![R. R.](calr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
106 | 105 | ralimdva 2502 |
. . . 4
![( (](lp.gif) ![( (](lp.gif)
![R. R.](calr.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![`
`](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![A. A.](forall.gif)
![( (](lp.gif)
![E. E.](exists.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
107 | 106 | impr 377 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
108 | | oveq1 5789 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
109 | 108 | breq2d 3949 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![x x](_x.gif)
![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
110 | | breq1 3940 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
111 | 109, 110 | anbi12d 465 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
112 | 111 | imbi2d 229 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
113 | 112 | rexralbidv 2464 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![E. E.](exists.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif)
![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
114 | 113 | imbi2d 229 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![(
(](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
115 | 114 | ralbidv 2438 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif)
![E. E.](exists.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![A. A.](forall.gif)
![( (](lp.gif)
![E. E.](exists.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![x x](_x.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
116 | 115 | rspcev 2793 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif)
![A. A.](forall.gif)
![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R
-1R](_m1r.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![-1R -1R](_m1r.gif) ![(
(](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif)
![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
117 | 16, 107, 116 | syl2anc 409 |
. 2
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif) ![` `](backtick.gif) ![i i](_i.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
118 | 8, 117 | rexlimddv 2557 |
1
![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![`
`](backtick.gif) ![k k](_k.gif) ![( (](lp.gif) ![x x](_x.gif)
![( (](lp.gif) ![( (](lp.gif) ![F F](_cf.gif) ![` `](backtick.gif) ![k k](_k.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |