Description: Computational part of ~? signwlemn . (Contributed by Thierry Arnoux, 29-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | signslema.1 | |
|
signslema.2 | |
||
signslema.3 | |
||
signslema.4 | |
||
signslema.5 | |
||
signslema.6 | |
||
Assertion | signslema | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | signslema.1 | |
|
2 | signslema.2 | |
|
3 | signslema.3 | |
|
4 | signslema.4 | |
|
5 | signslema.5 | |
|
6 | signslema.6 | |
|
7 | 5 | simpld | |
8 | 7 | adantr | |
9 | 4 | nn0cnd | |
10 | 2 | nn0cnd | |
11 | 9 10 | subcld | |
12 | 3 | nn0cnd | |
13 | 1 | nn0cnd | |
14 | 12 13 | subcld | |
15 | 11 14 | subeq0ad | |
16 | 15 | biimpa | |
17 | 16 | breq2d | |
18 | 2 | nn0red | |
19 | 4 | nn0red | |
20 | 18 19 | posdifd | |
21 | 20 | adantr | |
22 | 1 | nn0red | |
23 | 3 | nn0red | |
24 | 22 23 | posdifd | |
25 | 24 | adantr | |
26 | 17 21 25 | 3bitr4rd | |
27 | 8 26 | mpbid | |
28 | 0red | |
|
29 | 23 22 | resubcld | |
30 | 29 | adantr | |
31 | 19 18 | resubcld | |
32 | 31 | adantr | |
33 | 7 | adantr | |
34 | 24 | adantr | |
35 | 33 34 | mpbid | |
36 | 2pos | |
|
37 | breq2 | |
|
38 | 36 37 | mpbiri | |
39 | 29 31 | posdifd | |
40 | 39 | biimpar | |
41 | 38 40 | sylan2 | |
42 | 28 30 32 35 41 | lttrd | |
43 | 20 | adantr | |
44 | 42 43 | mpbird | |
45 | 9 12 10 13 | sub4d | |
46 | 45 6 | eqeltrrd | |
47 | ovex | |
|
48 | 47 | elpr | |
49 | 46 48 | sylib | |
50 | 27 44 49 | mpjaodan | |
51 | 5 | simprd | |
52 | 51 | adantr | |
53 | 16 | breq2d | |
54 | 52 53 | mtbird | |
55 | 2z | |
|
56 | 3 | nn0zd | |
57 | 1 | nn0zd | |
58 | 56 57 | zsubcld | |
59 | dvdsaddr | |
|
60 | 55 58 59 | sylancr | |
61 | 51 60 | mtbid | |
62 | 61 | adantr | |
63 | 2cnd | |
|
64 | 11 14 63 | subaddd | |
65 | 64 | biimpa | |
66 | 65 | breq2d | |
67 | 62 66 | mtbid | |
68 | 54 67 49 | mpjaodan | |
69 | 50 68 | jca | |