Description: Lemma for fnwe2 . Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fnwe2.su | |
|
fnwe2.t | |
||
fnwe2.s | |
||
fnwe2.f | |
||
fnwe2.r | |
||
fnwe2lem3.a | |
||
fnwe2lem3.b | |
||
Assertion | fnwe2lem3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnwe2.su | |
|
2 | fnwe2.t | |
|
3 | fnwe2.s | |
|
4 | fnwe2.f | |
|
5 | fnwe2.r | |
|
6 | fnwe2lem3.a | |
|
7 | fnwe2lem3.b | |
|
8 | animorrl | |
|
9 | 1 2 | fnwe2val | |
10 | 8 9 | sylibr | |
11 | 10 | 3mix1d | |
12 | simplr | |
|
13 | simpr | |
|
14 | 12 13 | jca | |
15 | 14 | olcd | |
16 | 15 9 | sylibr | |
17 | 16 | 3mix1d | |
18 | 3mix2 | |
|
19 | 18 | adantl | |
20 | simplr | |
|
21 | 20 | eqcomd | |
22 | csbeq1 | |
|
23 | 22 | adantl | |
24 | 23 | breqd | |
25 | 24 | biimpa | |
26 | 21 25 | jca | |
27 | 26 | olcd | |
28 | 1 2 | fnwe2val | |
29 | 27 28 | sylibr | |
30 | 29 | 3mix3d | |
31 | 1 2 3 | fnwe2lem1 | |
32 | 6 31 | mpdan | |
33 | weso | |
|
34 | 32 33 | syl | |
35 | 34 | adantr | |
36 | fveqeq2 | |
|
37 | 6 | adantr | |
38 | eqidd | |
|
39 | 36 37 38 | elrabd | |
40 | fveqeq2 | |
|
41 | 7 | adantr | |
42 | simpr | |
|
43 | 42 | eqcomd | |
44 | 40 41 43 | elrabd | |
45 | solin | |
|
46 | 35 39 44 45 | syl12anc | |
47 | 17 19 30 46 | mpjao3dan | |
48 | animorrl | |
|
49 | 48 28 | sylibr | |
50 | 49 | 3mix3d | |
51 | weso | |
|
52 | 5 51 | syl | |
53 | 6 | fvresd | |
54 | 4 6 | ffvelrnd | |
55 | 53 54 | eqeltrrd | |
56 | 7 | fvresd | |
57 | 4 7 | ffvelrnd | |
58 | 56 57 | eqeltrrd | |
59 | solin | |
|
60 | 52 55 58 59 | syl12anc | |
61 | 11 47 50 60 | mpjao3dan | |