Proof of Theorem tangtx
Step | Hyp | Ref
| Expression |
1 | | elioore 9725 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
2 | 1 | recoscld 11467 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
3 | 1, 2 | remulcld 7820 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
4 | | 1re 7789 |
. . . . . . 7
![RR RR](bbr.gif) |
5 | | rehalfcl 8971 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
6 | 1, 5 | syl 14 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
7 | 6 | resqcld 10481 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
8 | | 3nn 8906 |
. . . . . . . 8
![NN NN](bbn.gif) |
9 | | nndivre 8780 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif)
![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
10 | 7, 8, 9 | sylancl 410 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
11 | | resubcl 8050 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
12 | 4, 10, 11 | sylancr 411 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
13 | 1, 12 | remulcld 7820 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
14 | | 2re 8814 |
. . . . . . 7
![RR RR](bbr.gif) |
15 | | remulcl 7772 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
16 | 14, 10, 15 | sylancr 411 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
17 | | resubcl 8050 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
18 | 4, 16, 17 | sylancr 411 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
19 | 13, 18 | remulcld 7820 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
20 | 1 | resincld 11466 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
21 | 12 | resqcld 10481 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
22 | | remulcl 7772 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
23 | 14, 21, 22 | sylancr 411 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
24 | | resubcl 8050 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif)
![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
25 | 23, 4, 24 | sylancl 410 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
26 | 12, 18 | remulcld 7820 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
27 | 1 | recnd 7818 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
28 | | 2cn 8815 |
. . . . . . . . . . . 12
![CC CC](bbc.gif) |
29 | 28 | a1i 9 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
30 | | 2ap0 8837 |
. . . . . . . . . . . 12
# ![0 0](0.gif) |
31 | 30 | a1i 9 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) # ![0 0](0.gif) ![) )](rp.gif) |
32 | 27, 29, 31 | divcanap2d 8576 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
33 | 32 | fveq2d 5433 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
34 | 6 | recnd 7818 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2 2](2.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
35 | | cos2t 11493 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
36 | 34, 35 | syl 14 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | 33, 36 | eqtr3d 2175 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | 6 | recoscld 11467 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
39 | 38 | resqcld 10481 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
40 | | remulcl 7772 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
41 | 14, 39, 40 | sylancr 411 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
42 | 4 | a1i 9 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
43 | 14 | a1i 9 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
44 | | eliooord 9741 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
45 | 44 | simpld 111 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![A A](_ca.gif) ![) )](rp.gif) |
46 | | 2pos 8835 |
. . . . . . . . . . . . . . . 16
![2 2](2.gif) |
47 | 46 | a1i 9 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![2 2](2.gif) ![) )](rp.gif) |
48 | 1, 43, 45, 47 | divgt0d 8717 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) |
49 | | pire 12915 |
. . . . . . . . . . . . . . . . . . 19
![RR RR](bbr.gif) |
50 | | rehalfcl 8971 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif)
![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
51 | 49, 50 | mp1i 10 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif)
![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
52 | 44 | simprd 113 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) |
53 | | pigt2lt4 12913 |
. . . . . . . . . . . . . . . . . . . . . 22
![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) |
54 | 53 | simpri 112 |
. . . . . . . . . . . . . . . . . . . . 21
![4 4](4.gif) |
55 | | 2t2e4 8898 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![2 2](2.gif) ![4 4](4.gif) |
56 | 54, 55 | breqtrri 3963 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) |
57 | 14, 46 | pm3.2i 270 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) |
58 | | ltdivmul 8658 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif)
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
59 | 49, 14, 57, 58 | mp3an 1316 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif)
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
60 | 56, 59 | mpbir 145 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![2 2](2.gif) ![2 2](2.gif) |
61 | 60 | a1i 9 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif)
![2 2](2.gif) ![2 2](2.gif) ![) )](rp.gif) |
62 | 1, 51, 43, 52, 61 | lttrd 7912 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![2 2](2.gif) ![) )](rp.gif) |
63 | 28 | mulid2i 7793 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![2 2](2.gif) ![2 2](2.gif) |
64 | 62, 63 | breqtrrdi 3978 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
65 | | ltdivmul2 8660 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif)
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
66 | 1, 42, 43, 47, 65 | syl112anc 1221 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif)
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
67 | 64, 66 | mpbird 166 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2 2](2.gif) ![1 1](1.gif) ![) )](rp.gif) |
68 | 6, 42, 67 | ltled 7905 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2 2](2.gif) ![1
1](1.gif) ![) )](rp.gif) |
69 | | 0xr 7836 |
. . . . . . . . . . . . . . 15
![RR* RR*](_bbrast.gif) |
70 | | elioc2 9749 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,] (,]](_ioc.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![(
(](lp.gif) ![2 2](2.gif)
![( (](lp.gif) ![2 2](2.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
71 | 69, 4, 70 | mp2an 423 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,] (,]](_ioc.gif) ![1 1](1.gif)
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![(
(](lp.gif) ![2 2](2.gif)
![( (](lp.gif) ![2 2](2.gif) ![1
1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
72 | 6, 48, 68, 71 | syl3anbrc 1166 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,] (,]](_ioc.gif) ![1 1](1.gif) ![)
)](rp.gif) ![) )](rp.gif) |
73 | | cos01bnd 11501 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,] (,]](_ioc.gif) ![1 1](1.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
74 | 72, 73 | syl 14 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
75 | 74 | simprd 113 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
76 | | cos01gt0 11505 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,] (,]](_ioc.gif) ![1 1](1.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
77 | 72, 76 | syl 14 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
78 | | 0re 7790 |
. . . . . . . . . . . . . 14
![RR RR](bbr.gif) |
79 | | ltle 7875 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![(
(](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif)
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
80 | 78, 38, 79 | sylancr 411 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
81 | 77, 80 | mpd 13 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
82 | 78 | a1i 9 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
83 | 82, 38, 12, 77, 75 | lttrd 7912 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
84 | 82, 12, 83 | ltled 7905 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
85 | 38, 12, 81, 84 | lt2sqd 10486 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
86 | 75, 85 | mpbid 146 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
87 | | ltmul2 8638 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
88 | 39, 21, 43, 47, 87 | syl112anc 1221 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
89 | 86, 88 | mpbid 146 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
90 | 41, 23, 42, 89 | ltsub1dd 8343 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
91 | 37, 90 | eqbrtrd 3958 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
92 | | 3re 8818 |
. . . . . . . . . 10
![RR RR](bbr.gif) |
93 | | remulcl 7772 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
94 | 92, 10, 93 | sylancr 411 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
95 | | 4re 8821 |
. . . . . . . . . 10
![RR RR](bbr.gif) |
96 | | remulcl 7772 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
97 | 95, 10, 96 | sylancr 411 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
98 | 10 | resqcld 10481 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
99 | | remulcl 7772 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
100 | 14, 98, 99 | sylancr 411 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
101 | | readdcl 7770 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
102 | 4, 100, 101 | sylancr 411 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
103 | | 3lt4 8916 |
. . . . . . . . . 10
![4 4](4.gif) |
104 | 92 | a1i 9 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
105 | 95 | a1i 9 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
106 | 6, 48 | gt0ap0d 8415 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![2 2](2.gif) # ![0 0](0.gif) ![) )](rp.gif) |
107 | 6, 106 | sqgt0apd 10483 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
108 | | 3pos 8838 |
. . . . . . . . . . . . 13
![3 3](3.gif) |
109 | 108 | a1i 9 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![3 3](3.gif) ![) )](rp.gif) |
110 | 7, 104, 107, 109 | divgt0d 8717 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) |
111 | | ltmul1 8378 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
112 | 104, 105,
10, 110, 111 | syl112anc 1221 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
113 | 103, 112 | mpbii 147 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
114 | 94, 97, 102, 113 | ltsub2dd 8344 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
115 | 42 | recnd 7818 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
116 | | ax-1cn 7737 |
. . . . . . . . . . 11
![CC CC](bbc.gif) |
117 | 100 | recnd 7818 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
118 | | addcl 7769 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
119 | 116, 117,
118 | sylancr 411 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
120 | 97 | recnd 7818 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
121 | 119, 120 | subcld 8097 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
122 | | sq1 10417 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![1 1](1.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![1 1](1.gif) |
123 | 122 | a1i 9 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![1
1](1.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![1 1](1.gif) ![) )](rp.gif) |
124 | 10 | recnd 7818 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
125 | 124 | mulid2d 7808 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) |
126 | 125 | oveq2d 5798 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
127 | 123, 126 | oveq12d 5800 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
128 | 127 | oveq1d 5797 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
129 | | binom2sub 10436 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
130 | 116, 124,
129 | sylancr 411 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
131 | 98 | recnd 7818 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
132 | 16 | recnd 7818 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
133 | 115, 131,
132 | addsubd 8118 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
134 | 128, 130,
133 | 3eqtr4d 2183 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
135 | 134 | oveq2d 5798 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
136 | | addcl 7769 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
137 | 116, 131,
136 | sylancr 411 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
138 | 29, 137, 132 | subdid 8200 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
139 | 29, 115, 131 | adddid 7814 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
140 | 116 | 2timesi 8874 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) |
141 | 140 | oveq1i 5792 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
142 | 115, 115,
117 | addassd 7812 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
143 | 141, 142 | syl5eq 2185 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
144 | 139, 143 | eqtrd 2173 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
145 | 55 | oveq1i 5792 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) |
146 | 29, 29, 124 | mulassd 7813 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
147 | 145, 146 | syl5reqr 2188 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
148 | 144, 147 | oveq12d 5800 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
149 | 115, 119,
120, 148 | assraddsubd 8154 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
150 | 135, 138,
149 | 3eqtrd 2177 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
151 | 115, 121,
150 | mvrladdd 8153 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
152 | | subcl 7985 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![CC CC](bbc.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
153 | 116, 124,
152 | sylancr 411 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
154 | 153, 115,
132 | subdid 8200 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
155 | 153 | mulid1d 7807 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
156 | 115, 124,
132 | subdird 8201 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
157 | 132 | mulid2d 7808 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
158 | 124, 29, 124 | mul12d 7938 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
159 | 124 | sqvald 10452 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
160 | 159 | oveq2d 5798 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
161 | 158, 160 | eqtr4d 2176 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
162 | 157, 161 | oveq12d 5800 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
163 | 156, 162 | eqtrd 2173 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
164 | 155, 163 | oveq12d 5800 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
165 | 115, 124,
132, 117 | subadd4d 8145 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
166 | | df-3 8804 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) |
167 | 28, 116 | addcomi 7930 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) |
168 | 166, 167 | eqtri 2161 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) |
169 | 168 | oveq1i 5792 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) |
170 | 125 | oveq1d 5797 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
171 | 115, 124,
29, 170 | joinlmuladdmuld 7817 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
172 | 169, 171 | syl5eq 2185 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
173 | 172 | oveq2d 5798 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
174 | 165, 173 | eqtr4d 2176 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
175 | 154, 164,
174 | 3eqtrd 2177 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
176 | 114, 151,
175 | 3brtr4d 3968 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
177 | 2, 25, 26, 91, 176 | lttrd 7912 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
178 | | ltmul2 8638 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif)
![A A](_ca.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
179 | 2, 26, 1, 45, 178 | syl112anc 1221 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
180 | 177, 179 | mpbid 146 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
181 | 18 | recnd 7818 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
182 | 27, 153, 181 | mulassd 7813 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
183 | 180, 182 | breqtrrd 3964 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
184 | 13, 38 | remulcld 7820 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
185 | 74 | simpld 111 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
186 | 1, 12, 45, 83 | mulgt0d 7909 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
187 | | ltmul2 8638 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
188 | 18, 38, 13, 186, 187 | syl112anc 1221 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
189 | 185, 188 | mpbid 146 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
190 | 29, 34, 153 | mulassd 7813 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
191 | 32 | oveq1d 5797 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
192 | 34, 115, 124 | subdid 8200 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
193 | 34 | mulid1d 7807 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![1 1](1.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
194 | 166 | oveq2i 5793 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![) )](rp.gif) |
195 | | 2nn0 9018 |
. . . . . . . . . . . . . . . . 17
![NN0 NN0](_bbn0.gif) |
196 | | expp1 10331 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif)
![NN0 NN0](_bbn0.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
197 | 34, 195, 196 | sylancl 410 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
198 | 194, 197 | syl5eq 2185 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
199 | 7 | recnd 7818 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
200 | 199, 34 | mulcomd 7811 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
201 | 198, 200 | eqtrd 2173 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
202 | 201 | oveq1d 5797 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![) )](rp.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) |
203 | | 3cn 8819 |
. . . . . . . . . . . . . . 15
![CC CC](bbc.gif) |
204 | 203 | a1i 9 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
205 | 104, 109 | gt0ap0d 8415 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) # ![0 0](0.gif) ![) )](rp.gif) |
206 | 34, 199, 204, 205 | divassapd 8610 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![) )](rp.gif) ![3 3](3.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
207 | 202, 206 | eqtr2d 2174 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) |
208 | 193, 207 | oveq12d 5800 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3
3](3.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
209 | 192, 208 | eqtrd 2173 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3
3](3.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
210 | 209 | oveq2d 5798 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
211 | 190, 191,
210 | 3eqtr3d 2181 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
212 | | sin01bnd 11500 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,] (,]](_ioc.gif) ![1 1](1.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
213 | 72, 212 | syl 14 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
214 | 213 | simpld 111 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
215 | | 3nn0 9019 |
. . . . . . . . . . . . 13
![NN0 NN0](_bbn0.gif) |
216 | | reexpcl 10341 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif)
![NN0 NN0](_bbn0.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
217 | 6, 215, 216 | sylancl 410 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
218 | | nndivre 8780 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif)
![NN NN](bbn.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3
3](3.gif) ![3 3](3.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
219 | 217, 8, 218 | sylancl 410 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3 3](3.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
220 | 6, 219 | resubcld 8167 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3 3](3.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
221 | 6 | resincld 11466 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
222 | | ltmul2 8638 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3
3](3.gif) ![) )](rp.gif) ![(
(](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
223 | 220, 221,
43, 47, 222 | syl112anc 1221 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3 3](3.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3
3](3.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
224 | 214, 223 | mpbid 146 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![3 3](3.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
225 | 211, 224 | eqbrtrd 3958 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3
3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
226 | | remulcl 7772 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![(
(](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
227 | 14, 221, 226 | sylancr 411 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
228 | | ltmul1 8378 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
229 | 13, 227, 38, 77, 228 | syl112anc 1221 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
230 | 225, 229 | mpbid 146 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
231 | 221 | recnd 7818 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
232 | 38 | recnd 7818 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![CC CC](bbc.gif) ![) )](rp.gif) |
233 | 29, 231, 232 | mulassd 7813 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
234 | | sin2t 11492 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
235 | 34, 234 | syl 14 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
236 | 32 | fveq2d 5433 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
237 | 233, 235,
236 | 3eqtr2rd 2180 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
238 | 230, 237 | breqtrrd 3964 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
239 | 19, 184, 20, 189, 238 | lttrd 7912 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![^ ^](uparrow.gif) ![2 2](2.gif) ![3 3](3.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![^ ^](uparrow.gif) ![2
2](2.gif) ![3 3](3.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
240 | 3, 19, 20, 183, 239 | lttrd 7912 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![(
(](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
241 | | sincosq1sgn 12955 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif)
![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
242 | 241 | simprd 113 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
243 | | ltmuldiv 8656 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![(
(](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
244 | 1, 20, 2, 242, 243 | syl112anc 1221 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
245 | 240, 244 | mpbid 146 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
246 | 2, 242 | gt0ap0d 8415 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) # ![0 0](0.gif) ![) )](rp.gif) |
247 | | tanvalap 11451 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) # ![0 0](0.gif) ![( (](lp.gif) ![tan tan](_tan.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
248 | 27, 246, 247 | syl2anc 409 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![tan tan](_tan.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![sin sin](_sin.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
249 | 245, 248 | breqtrrd 3964 |
1
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![( (](lp.gif) ![tan tan](_tan.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |