Description: Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro, 9-May-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | pilem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin | |
|
2 | sinf | |
|
3 | ffn | |
|
4 | fniniseg | |
|
5 | 2 3 4 | mp2b | |
6 | rpcn | |
|
7 | 6 | biantrurd | |
8 | 5 7 | bitr4id | |
9 | 8 | pm5.32i | |
10 | 1 9 | bitri | |