Description: Transitivity of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | acongtr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | congtr | |
|
2 | 1 | 3expa | |
3 | 2 | orcd | |
4 | 3 | ex | |
5 | simpll | |
|
6 | znegcl | |
|
7 | znegcl | |
|
8 | 6 7 | anim12i | |
9 | 8 | ad2antlr | |
10 | simplll | |
|
11 | simplrl | |
|
12 | simplrr | |
|
13 | simpr | |
|
14 | congsym | |
|
15 | 10 11 12 13 14 | syl22anc | |
16 | 15 | ex | |
17 | zcn | |
|
18 | 17 | adantr | |
19 | zcn | |
|
20 | 19 | adantl | |
21 | 18 20 | neg2subd | |
22 | 21 | adantl | |
23 | 22 | eqcomd | |
24 | 23 | breq2d | |
25 | 16 24 | sylibd | |
26 | 25 | anim2d | |
27 | 26 | imp | |
28 | congtr | |
|
29 | 5 9 27 28 | syl3anc | |
30 | 29 | olcd | |
31 | 30 | ex | |
32 | simpll | |
|
33 | 7 | anim2i | |
34 | 33 | ad2antlr | |
35 | simpr | |
|
36 | congtr | |
|
37 | 32 34 35 36 | syl3anc | |
38 | 37 | olcd | |
39 | 38 | ex | |
40 | simpll | |
|
41 | 6 | anim1i | |
42 | 41 | ad2antlr | |
43 | simpl | |
|
44 | simpr | |
|
45 | 43 44 | anim12i | |
46 | 45 | an42s | |
47 | 46 | adantr | |
48 | 7 | adantl | |
49 | 48 | ad2antlr | |
50 | simpr | |
|
51 | congsym | |
|
52 | 47 49 50 51 | syl12anc | |
53 | 52 | ex | |
54 | 18 | negnegd | |
55 | 54 | oveq2d | |
56 | zcn | |
|
57 | 56 | adantr | |
58 | 8 57 | syl | |
59 | 20 58 | neg2subd | |
60 | 55 59 | eqtr3d | |
61 | 60 | adantl | |
62 | 61 | breq2d | |
63 | 53 62 | sylibd | |
64 | 63 | anim2d | |
65 | 64 | imp | |
66 | congtr | |
|
67 | 40 42 65 66 | syl3anc | |
68 | 67 | orcd | |
69 | 68 | ex | |
70 | 4 31 39 69 | ccased | |
71 | 70 | 3impia | |