Proof of Theorem reccn2ap
Step | Hyp | Ref
| Expression |
1 | | reccn2ap.t |
. . 3
inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![)
)](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
2 | | 1red 7805 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
3 | | simp1 982 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![CC CC](bbc.gif) ![) )](rp.gif) |
4 | | simp2 983 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
# ![0 0](0.gif) ![) )](rp.gif) |
5 | 3, 4 | absrpclapd 10992 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
6 | | simp3 984 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
7 | 5, 6 | rpmulcld 9530 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
8 | 7 | rpred 9513 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
9 | | mincl 11034 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![RR RR](bbr.gif) inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
10 | 2, 8, 9 | syl2anc 409 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
11 | 7 | rpgt0d 9516 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | | 0lt1 7913 |
. . . . . . 7
![1 1](1.gif) |
13 | 11, 12 | jctil 310 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
14 | | 0red 7791 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
15 | | ltmininf 11038 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![RR RR](bbr.gif) ![(
(](lp.gif) inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | 14, 2, 8, 15 | syl3anc 1217 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![( (](lp.gif) inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![)
)](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | 13, 16 | mpbird 166 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![) )](rp.gif) ![) )](rp.gif) |
18 | 10, 17 | elrpd 9510 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
19 | 5 | rphalfcld 9526 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
20 | 18, 19 | rpmulcld 9530 |
. . 3
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
21 | 1, 20 | eqeltrid 2227 |
. 2
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
22 | 3 | adantr 274 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
23 | | simprl 521 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![{ {](lbrace.gif) #
![0 0](0.gif) ![} }](rbrace.gif) ![)
)](rp.gif) |
24 | | breq1 3940 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) #
# ![0 0](0.gif) ![)
)](rp.gif) ![) )](rp.gif) |
25 | 24 | elrab 2844 |
. . . . . . . . . . 11
![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | 23, 25 | sylib 121 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) # ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | 26 | simpld 111 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
28 | 22, 27 | mulcld 7810 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif)
![z z](_z.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
29 | 4 | adantr 274 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) # ![0 0](0.gif) ![) )](rp.gif) |
30 | 26 | simprd 113 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) # ![0 0](0.gif) ![) )](rp.gif) |
31 | 22, 27, 29, 30 | mulap0d 8443 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif)
![z z](_z.gif) # ![0 0](0.gif) ![) )](rp.gif) |
32 | 22, 27, 28, 31 | divsubdirapd 8614 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | 22 | mulid1d 7807 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif)
![1 1](1.gif) ![A A](_ca.gif) ![) )](rp.gif) |
34 | 33 | oveq1d 5797 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | | 1cnd 7806 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
36 | 35, 27, 22, 30, 29 | divcanap5d 8601 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![z
z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | 34, 36 | eqtr3d 2175 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) |
38 | 27 | mulid1d 7807 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![1 1](1.gif) ![z z](_z.gif) ![) )](rp.gif) |
39 | 27, 22 | mulcomd 7811 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) |
40 | 38, 39 | oveq12d 5800 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
41 | 35, 22, 27, 29, 30 | divcanap5d 8601 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
42 | 40, 41 | eqtr3d 2175 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
43 | 37, 42 | oveq12d 5800 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
44 | 32, 43 | eqtrd 2173 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
45 | 44 | fveq2d 5433 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![(
(](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
46 | 22, 27 | subcld 8097 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif)
![z z](_z.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
47 | 46, 28, 31 | absdivapd 10999 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![(
(](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
48 | 45, 47 | eqtr3d 2175 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
49 | 46 | abscld 10985 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
50 | 21 | adantr 274 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
51 | 50 | rpred 9513 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
52 | 28 | abscld 10985 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
53 | 6 | rpred 9513 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
54 | 53 | adantr 274 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
55 | 52, 54 | remulcld 7820 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![B B](_cb.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
56 | 22, 27 | abssubd 10997 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
57 | | simprr 522 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![T
T](_ct.gif) ![) )](rp.gif) |
58 | 56, 57 | eqbrtrd 3958 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![T
T](_ct.gif) ![) )](rp.gif) |
59 | 7 | adantr 274 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
60 | 59 | rpred 9513 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
61 | 19 | adantr 274 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
62 | 61 | rpred 9513 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
63 | 60, 62 | remulcld 7820 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
64 | | 1re 7789 |
. . . . . . . . . . 11
![RR RR](bbr.gif) |
65 | | min2inf 11036 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![RR RR](bbr.gif) inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif)
![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
66 | 64, 60, 65 | sylancr 411 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) |
67 | 10 | adantr 274 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
68 | 67, 60, 61 | lemul1d 9557 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif)
![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif)
inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
69 | 66, 68 | mpbid 146 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
70 | 1, 69 | eqbrtrid 3971 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
71 | 27 | abscld 10985 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
72 | 22 | abscld 10985 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
73 | 72 | recnd 7818 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
74 | 73 | 2halvesd 8989 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
75 | 72, 71 | resubcld 8167 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
76 | 27, 22 | subcld 8097 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
77 | 76 | abscld 10985 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
78 | 56, 77 | eqeltrd 2217 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
79 | 22, 27 | abs2difd 11001 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![) )](rp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
80 | | min1inf 11035 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![RR RR](bbr.gif) inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif)
![1 1](1.gif) ![) )](rp.gif) |
81 | 64, 60, 80 | sylancr 411 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![1 1](1.gif) ![) )](rp.gif) |
82 | | 1red 7805 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
83 | 67, 82, 61 | lemul1d 9557 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif)
inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
84 | 81, 83 | mpbid 146 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) inf![( (](lp.gif) ![{ {](lbrace.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
85 | 1, 84 | eqbrtrid 3971 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
86 | 62 | recnd 7818 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
87 | 86 | mulid2d 7808 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) |
88 | 85, 87 | breqtrd 3962 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
89 | 78, 51, 62, 58, 88 | ltletrd 8209 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
90 | 75, 78, 62, 79, 89 | lelttrd 7911 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
91 | 72, 71, 62 | ltsubadd2d 8329 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
92 | 90, 91 | mpbid 146 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
93 | 74, 92 | eqbrtrd 3958 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
94 | 62, 71, 62 | ltadd1d 8324 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
95 | 93, 94 | mpbird 166 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) |
96 | 62, 71, 59, 95 | ltmul2dd 9570 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
97 | 22, 27 | absmuld 10998 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
98 | 97 | oveq1d 5797 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![)
)](rp.gif) ![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) |
99 | 71 | recnd 7818 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
100 | 54 | recnd 7818 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
101 | 73, 99, 100 | mul32d 7939 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![) )](rp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
102 | 98, 101 | eqtrd 2173 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
103 | 96, 102 | breqtrrd 3964 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
104 | 51, 63, 55, 70, 103 | lelttrd 7911 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
105 | 49, 51, 55, 58, 104 | lttrd 7912 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
106 | 28, 31 | absrpclapd 10992 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
107 | 49, 54, 106 | ltdivmuld 9565 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
108 | 105, 107 | mpbird 166 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif)
![z z](_z.gif) ![) )](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![B
B](_cb.gif) ![) )](rp.gif) |
109 | 48, 108 | eqbrtrd 3958 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif) ![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![B
B](_cb.gif) ![) )](rp.gif) |
110 | 109 | expr 373 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) # ![RR+ RR+](_bbrplus.gif) ![{ {](lbrace.gif) #
![0 0](0.gif) ![} }](rbrace.gif)
![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![z
z](_z.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) |
111 | 110 | ralrimiva 2508 |
. 2
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![A. A.](forall.gif) ![{ {](lbrace.gif) #
![0 0](0.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
112 | | breq2 3941 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![T T](_ct.gif) ![)
)](rp.gif) ![) )](rp.gif) |
113 | 112 | rspceaimv 2801 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![{ {](lbrace.gif) # ![0 0](0.gif) ![( (](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif)
![E. E.](exists.gif) ![A. A.](forall.gif) ![{
{](lbrace.gif) #
![0 0](0.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
114 | 21, 111, 113 | syl2anc 409 |
1
![( (](lp.gif) ![( (](lp.gif) #
![RR+ RR+](_bbrplus.gif)
![E. E.](exists.gif) ![A. A.](forall.gif) ![{
{](lbrace.gif) #
![0 0](0.gif) ![(
(](lp.gif) ![( (](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![abs abs](_abs.gif) ![` `](backtick.gif) ![( (](lp.gif) ![(
(](lp.gif) ![z z](_z.gif) ![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |