Proof of Theorem sgn3da
Step | Hyp | Ref
| Expression |
1 | | sgn3da.0 |
. . . . . . . . 9
|
2 | | sgnval 13828 |
. . . . . . . . 9
sgn
|
3 | 1, 2 | syl 17 |
. . . . . . . 8
sgn |
4 | 3 | eqeq2d 2632 |
. . . . . . 7
sgn
|
5 | 4 | pm5.32i 669 |
. . . . . 6
sgn
|
6 | | sgn3da.1 |
. . . . . . . . 9
sgn
|
7 | 6 | eqcoms 2630 |
. . . . . . . 8
sgn
|
8 | 7 | bicomd 213 |
. . . . . . 7
sgn
|
9 | 8 | adantl 482 |
. . . . . 6
sgn
|
10 | 5, 9 | sylbir 225 |
. . . . 5
|
11 | 10 | expcom 451 |
. . . 4
|
12 | 11 | pm5.74d 262 |
. . 3
|
13 | 3 | eqeq2d 2632 |
. . . . . . 7
sgn |
14 | 13 | pm5.32i 669 |
. . . . . 6
sgn
|
15 | | eqeq1 2626 |
. . . . . . . . 9
sgn sgn |
16 | 15 | imbi1d 331 |
. . . . . . . 8
sgn
sgn
|
17 | | eqeq1 2626 |
. . . . . . . . 9
sgn sgn |
18 | 17 | imbi1d 331 |
. . . . . . . 8
sgn
sgn
|
19 | | sgn3da.6 |
. . . . . . . . . . . . . . 15
|
20 | 19 | adantr 481 |
. . . . . . . . . . . . . 14
|
21 | | simp2 1062 |
. . . . . . . . . . . . . . 15
|
22 | 21 | 3expia 1267 |
. . . . . . . . . . . . . 14
|
23 | 20, 22 | impbida 877 |
. . . . . . . . . . . . 13
|
24 | | pm3.24 926 |
. . . . . . . . . . . . . . . . 17
|
25 | 24 | pm2.21i 116 |
. . . . . . . . . . . . . . . 16
|
26 | 25 | adantl 482 |
. . . . . . . . . . . . . . 15
|
27 | 26 | expr 643 |
. . . . . . . . . . . . . 14
|
28 | | tbtru 1494 |
. . . . . . . . . . . . . 14
|
29 | 27, 28 | sylib 208 |
. . . . . . . . . . . . 13
|
30 | 23, 29 | anbi12d 747 |
. . . . . . . . . . . 12
|
31 | | ancom 466 |
. . . . . . . . . . . . 13
|
32 | | truan 1501 |
. . . . . . . . . . . . 13
|
33 | 31, 32 | bitri 264 |
. . . . . . . . . . . 12
|
34 | 30, 33 | syl6bb 276 |
. . . . . . . . . . 11
|
35 | 34 | 3adant3 1081 |
. . . . . . . . . 10
sgn
|
36 | | sgn3da.3 |
. . . . . . . . . . . 12
sgn |
37 | 36 | eqcoms 2630 |
. . . . . . . . . . 11
sgn |
38 | 37 | 3ad2ant3 1084 |
. . . . . . . . . 10
sgn
|
39 | 35, 38 | bitr4d 271 |
. . . . . . . . 9
sgn
|
40 | 39 | 3expia 1267 |
. . . . . . . 8
sgn
|
41 | 19 | 3adant2 1080 |
. . . . . . . . . . . . . . 15
|
42 | 41 | 3expia 1267 |
. . . . . . . . . . . . . 14
|
43 | | tbtru 1494 |
. . . . . . . . . . . . . 14
|
44 | 42, 43 | sylib 208 |
. . . . . . . . . . . . 13
|
45 | | pm3.35 611 |
. . . . . . . . . . . . . . 15
|
46 | 45 | adantll 750 |
. . . . . . . . . . . . . 14
|
47 | | simp2 1062 |
. . . . . . . . . . . . . . 15
|
48 | 47 | 3expia 1267 |
. . . . . . . . . . . . . 14
|
49 | 46, 48 | impbida 877 |
. . . . . . . . . . . . 13
|
50 | 44, 49 | anbi12d 747 |
. . . . . . . . . . . 12
|
51 | | truan 1501 |
. . . . . . . . . . . 12
|
52 | 50, 51 | syl6bb 276 |
. . . . . . . . . . 11
|
53 | 52 | 3adant3 1081 |
. . . . . . . . . 10
sgn
|
54 | | sgn3da.2 |
. . . . . . . . . . . 12
sgn
|
55 | 54 | eqcoms 2630 |
. . . . . . . . . . 11
sgn
|
56 | 55 | 3ad2ant3 1084 |
. . . . . . . . . 10
sgn
|
57 | 53, 56 | bitr4d 271 |
. . . . . . . . 9
sgn
|
58 | 57 | 3expia 1267 |
. . . . . . . 8
sgn
|
59 | 16, 18, 40, 58 | ifbothda 4123 |
. . . . . . 7
sgn
|
60 | 59 | imp 445 |
. . . . . 6
sgn
|
61 | 14, 60 | sylbir 225 |
. . . . 5
|
62 | 61 | expcom 451 |
. . . 4
|
63 | 62 | pm5.74d 262 |
. . 3
|
64 | | sgn3da.4 |
. . . . 5
|
65 | 64 | expcom 451 |
. . . 4
|
66 | 65 | adantl 482 |
. . 3
|
67 | 19 | ex 450 |
. . . . . . 7
|
68 | 67 | adantr 481 |
. . . . . 6
|
69 | | simp1 1061 |
. . . . . . . 8
|
70 | | df-ne 2795 |
. . . . . . . . . . . 12
|
71 | | 0xr 10086 |
. . . . . . . . . . . . 13
|
72 | | xrlttri2 11975 |
. . . . . . . . . . . . 13
|
73 | 1, 71, 72 | sylancl 694 |
. . . . . . . . . . . 12
|
74 | 70, 73 | syl5bbr 274 |
. . . . . . . . . . 11
|
75 | 74 | biimpa 501 |
. . . . . . . . . 10
|
76 | 75 | ord 392 |
. . . . . . . . 9
|
77 | 76 | 3impia 1261 |
. . . . . . . 8
|
78 | | sgn3da.5 |
. . . . . . . 8
|
79 | 69, 77, 78 | syl2anc 693 |
. . . . . . 7
|
80 | 79 | 3expia 1267 |
. . . . . 6
|
81 | 68, 80 | jca 554 |
. . . . 5
|
82 | 81 | expcom 451 |
. . . 4
|
83 | 82 | adantl 482 |
. . 3
|
84 | 12, 63, 66, 83 | ifbothda 4123 |
. 2
|
85 | 84 | trud 1493 |
1
|