Proof of Theorem coseq0negpitopi
Step | Hyp | Ref
| Expression |
1 | | simplr 520 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) |
2 | | pire 12915 |
. . . . . . . . . . . . 13
![RR RR](bbr.gif) |
3 | 2 | renegcli 8048 |
. . . . . . . . . . . 12
![-u -u](shortminus.gif) ![RR RR](bbr.gif) |
4 | 3 | rexri 7847 |
. . . . . . . . . . 11
![-u -u](shortminus.gif) ![RR* RR*](_bbrast.gif) |
5 | | elioc2 9749 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
6 | 4, 2, 5 | mp2an 423 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | 6 | simp1bi 997 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
8 | 7 | adantr 274 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
9 | 8 | adantr 274 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
10 | | halfpire 12921 |
. . . . . . . . . 10
![( (](lp.gif) ![2 2](2.gif) ![RR RR](bbr.gif) |
11 | 10 | renegcli 8048 |
. . . . . . . . 9
![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![RR RR](bbr.gif) |
12 | 11 | a1i 9 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
13 | | 4re 8821 |
. . . . . . . . . . 11
![RR RR](bbr.gif) |
14 | | 4ap0 8843 |
. . . . . . . . . . 11
# ![0 0](0.gif) |
15 | 2, 13, 14 | redivclapi 8563 |
. . . . . . . . . 10
![( (](lp.gif) ![4 4](4.gif) ![RR RR](bbr.gif) |
16 | 15 | renegcli 8048 |
. . . . . . . . 9
![-u -u](shortminus.gif) ![( (](lp.gif)
![4 4](4.gif) ![RR RR](bbr.gif) |
17 | 16 | a1i 9 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![4 4](4.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
18 | | 2lt4 8917 |
. . . . . . . . . . 11
![4 4](4.gif) |
19 | | 2re 8814 |
. . . . . . . . . . . . 13
![RR RR](bbr.gif) |
20 | | 2pos 8835 |
. . . . . . . . . . . . 13
![2 2](2.gif) |
21 | 19, 20 | pm3.2i 270 |
. . . . . . . . . . . 12
![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) |
22 | | 4pos 8841 |
. . . . . . . . . . . . 13
![4 4](4.gif) |
23 | 13, 22 | pm3.2i 270 |
. . . . . . . . . . . 12
![( (](lp.gif) ![4 4](4.gif) ![) )](rp.gif) |
24 | | pipos 12917 |
. . . . . . . . . . . . 13
![pi pi](pi.gif) |
25 | 2, 24 | pm3.2i 270 |
. . . . . . . . . . . 12
![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) |
26 | | ltdiv2 8669 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![4
4](4.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | 21, 23, 25, 26 | mp3an 1316 |
. . . . . . . . . . 11
![( (](lp.gif)
![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
28 | 18, 27 | mpbi 144 |
. . . . . . . . . 10
![( (](lp.gif) ![4 4](4.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) |
29 | 15, 10 | ltnegi 8279 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif) ![2
2](2.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) ![) )](rp.gif) |
30 | 28, 29 | mpbi 144 |
. . . . . . . . 9
![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![) )](rp.gif) |
31 | 30 | a1i 9 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) ![) )](rp.gif) |
32 | | simpr 109 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![4 4](4.gif) ![A
A](_ca.gif) ![) )](rp.gif) |
33 | 12, 17, 9, 31, 32 | lttrd 7912 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![A
A](_ca.gif) ![) )](rp.gif) |
34 | 2 | a1i 9 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
35 | | 3re 8818 |
. . . . . . . . . 10
![RR RR](bbr.gif) |
36 | 35, 10 | remulcli 7804 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![RR RR](bbr.gif) |
37 | 36 | a1i 9 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
38 | 6 | simp3bi 999 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![pi pi](pi.gif) ![) )](rp.gif) |
39 | 38 | ad2antrr 480 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![pi pi](pi.gif) ![) )](rp.gif) |
40 | | 2lt3 8914 |
. . . . . . . . . . 11
![3 3](3.gif) |
41 | | 3pos 8838 |
. . . . . . . . . . . . 13
![3 3](3.gif) |
42 | 35, 41 | pm3.2i 270 |
. . . . . . . . . . . 12
![( (](lp.gif) ![3 3](3.gif) ![) )](rp.gif) |
43 | | ltdiv2 8669 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif) ![3 3](3.gif) ![( (](lp.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![3
3](3.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
44 | 21, 42, 25, 43 | mp3an 1316 |
. . . . . . . . . . 11
![( (](lp.gif)
![( (](lp.gif) ![3 3](3.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
45 | 40, 44 | mpbi 144 |
. . . . . . . . . 10
![( (](lp.gif) ![3 3](3.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) |
46 | | ltdivmul 8658 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![2 2](2.gif) ![( (](lp.gif) ![3 3](3.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif)
![3 3](3.gif) ![( (](lp.gif) ![2
2](2.gif)
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
47 | 2, 10, 42, 46 | mp3an 1316 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![3 3](3.gif) ![( (](lp.gif) ![2
2](2.gif)
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
48 | 45, 47 | mpbi 144 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) |
49 | 48 | a1i 9 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
50 | 9, 34, 37, 39, 49 | lelttrd 7911 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
51 | 11 | rexri 7847 |
. . . . . . . 8
![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![RR* RR*](_bbrast.gif) |
52 | 36 | rexri 7847 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![RR*
RR*](_bbrast.gif) |
53 | | elioo2 9734 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![RR* RR*](_bbrast.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
54 | 51, 52, 53 | mp2an 423 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![( (](lp.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
55 | 9, 33, 50, 54 | syl3anbrc 1166 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
56 | | coseq0q4123 12963 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![(,) (,)](_ioo.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
57 | 55, 56 | syl 14 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif)
![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
58 | 1, 57 | mpbid 146 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![( (](lp.gif)
![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) |
59 | | prid1g 3635 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![( (](lp.gif)
![2 2](2.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![-u
-u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
60 | | eleq1a 2212 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![-u
-u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif)
![{ {](lbrace.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
61 | 10, 59, 60 | mp2b 8 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![)
)](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
62 | 58, 61 | syl 14 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![A A](_ca.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
63 | 8 | recnd 7818 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif)
![CC CC](bbc.gif) ![) )](rp.gif) |
64 | 63 | adantr 274 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![CC CC](bbc.gif) ![) )](rp.gif) |
65 | | cosneg 11470 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
66 | 64, 65 | syl 14 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![) )](rp.gif) ![) )](rp.gif) |
67 | | simplr 520 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) |
68 | 66, 67 | eqtrd 2173 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) |
69 | 8 | renegcld 8166 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
70 | 69 | adantr 274 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![-u -u](shortminus.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
71 | | 0re 7790 |
. . . . . . . . . . 11
![RR RR](bbr.gif) |
72 | 71 | a1i 9 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
73 | | simpr 109 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![0 0](0.gif) ![) )](rp.gif) |
74 | 8 | adantr 274 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
75 | 74 | lt0neg1d 8301 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![)
)](rp.gif) ![) )](rp.gif) |
76 | 73, 75 | mpbid 146 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
77 | 72, 70, 76 | ltled 7905 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
78 | 2 | a1i 9 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![RR RR](bbr.gif) ![) )](rp.gif) |
79 | 2 | a1i 9 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![RR RR](bbr.gif) ![) )](rp.gif) |
80 | 6 | simp2bi 998 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
81 | 80 | adantr 274 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![) )](rp.gif) |
82 | 79, 8, 81 | ltnegcon1d 8311 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![) )](rp.gif) |
83 | 82 | adantr 274 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![-u -u](shortminus.gif) ![pi
pi](pi.gif) ![) )](rp.gif) |
84 | 70, 78, 83 | ltled 7905 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![-u -u](shortminus.gif) ![pi pi](pi.gif) ![) )](rp.gif) |
85 | 71, 2 | elicc2i 9752 |
. . . . . . . . 9
![( (](lp.gif) ![-u -u](shortminus.gif)
![( (](lp.gif) ![0 0](0.gif) ![[,] [,]](_icc.gif) ![pi pi](pi.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) |
86 | 70, 77, 84, 85 | syl3anbrc 1166 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![0 0](0.gif) ![[,] [,]](_icc.gif) ![pi pi](pi.gif) ![) )](rp.gif) ![) )](rp.gif) |
87 | | coseq00topi 12964 |
. . . . . . . 8
![( (](lp.gif) ![-u -u](shortminus.gif)
![( (](lp.gif) ![0 0](0.gif) ![[,] [,]](_icc.gif) ![pi pi](pi.gif) ![(
(](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
88 | 86, 87 | syl 14 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![( (](lp.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![A A](_ca.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
89 | 68, 88 | mpbid 146 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) |
90 | 64, 89 | negcon1ad 8092 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![A A](_ca.gif) ![) )](rp.gif) |
91 | 90 | eqcomd 2146 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![) )](rp.gif) |
92 | | prid2g 3636 |
. . . . 5
![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
93 | | eleq1a 2212 |
. . . . 5
![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![{ {](lbrace.gif) ![(
(](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
94 | 11, 92, 93 | mp2b 8 |
. . . 4
![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![)
)](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
95 | 91, 94 | syl 14 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![0 0](0.gif)
![{ {](lbrace.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
96 | | pirp 12918 |
. . . . . . 7
![RR+ RR+](_bbrplus.gif) |
97 | 13, 22 | elrpii 9473 |
. . . . . . 7
![RR+ RR+](_bbrplus.gif) |
98 | | rpdivcl 9496 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![RR+ RR+](_bbrplus.gif) ![( (](lp.gif)
![4 4](4.gif) ![RR+ RR+](_bbrplus.gif) ![) )](rp.gif) |
99 | 96, 97, 98 | mp2an 423 |
. . . . . 6
![( (](lp.gif) ![4 4](4.gif) ![RR+ RR+](_bbrplus.gif) |
100 | | rpgt0 9482 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif)
![(
(](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) ![) )](rp.gif) |
101 | 99, 100 | ax-mp 5 |
. . . . 5
![( (](lp.gif) ![4 4](4.gif) ![)
)](rp.gif) |
102 | | lt0neg2 8255 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![4 4](4.gif) ![( (](lp.gif)
![( (](lp.gif) ![4 4](4.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![4 4](4.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) |
103 | 15, 102 | ax-mp 5 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![4
4](4.gif)
![-u -u](shortminus.gif) ![( (](lp.gif) ![4 4](4.gif) ![0 0](0.gif) ![) )](rp.gif) |
104 | 101, 103 | mpbi 144 |
. . . 4
![-u -u](shortminus.gif) ![( (](lp.gif)
![4 4](4.gif) ![0 0](0.gif) |
105 | | axltwlin 7856 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![-u
-u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif)
![RR RR](bbr.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4 4](4.gif)
![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![4 4](4.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
106 | 16, 71, 8, 105 | mp3an12i 1320 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![(
(](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4 4](4.gif) ![0 0](0.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
107 | 104, 106 | mpi 15 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![(
(](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![4
4](4.gif)
![0 0](0.gif) ![)
)](rp.gif) ![) )](rp.gif) |
108 | 62, 95, 107 | mpjaodan 788 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif)
![{ {](lbrace.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
109 | | elpri 3555 |
. . . 4
![( (](lp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![-u
-u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
110 | | fveq2 5429 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
111 | | coshalfpi 12926 |
. . . . . 6
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![( (](lp.gif) ![2 2](2.gif) ![)
)](rp.gif) ![0 0](0.gif) |
112 | 110, 111 | eqtrdi 2189 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) |
113 | | fveq2 5429 |
. . . . . 6
![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
114 | | cosneghalfpi 12927 |
. . . . . 6
![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![0 0](0.gif) |
115 | 113, 114 | eqtrdi 2189 |
. . . . 5
![( (](lp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) |
116 | 112, 115 | jaoi 706 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![-u -u](shortminus.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) |
117 | 109, 116 | syl 14 |
. . 3
![( (](lp.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![2 2](2.gif) ![) )](rp.gif) ![-u
-u](shortminus.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) |
118 | 117 | adantl 275 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif)
![{ {](lbrace.gif) ![( (](lp.gif)
![2 2](2.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) |
119 | 108, 118 | impbida 586 |
1
![( (](lp.gif) ![( (](lp.gif) ![-u -u](shortminus.gif) ![pi pi](pi.gif) ![(,] (,]](_ioc.gif) ![pi pi](pi.gif) ![( (](lp.gif) ![(
(](lp.gif) ![cos cos](_cos.gif) ![` `](backtick.gif) ![A A](_ca.gif) ![{ {](lbrace.gif) ![( (](lp.gif) ![2
2](2.gif) ![) )](rp.gif) ![-u -u](shortminus.gif) ![( (](lp.gif)
![2 2](2.gif) ![)
)](rp.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |