Description: Lemma derived from modular law. (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pmodl42.s | |
|
pmodl42.p | |
||
Assertion | pmodl42N | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pmodl42.s | |
|
2 | pmodl42.p | |
|
3 | simpl1 | |
|
4 | simpl3 | |
|
5 | eqid | |
|
6 | 5 1 | psubssat | |
7 | 3 4 6 | syl2anc | |
8 | simpl2 | |
|
9 | 5 1 | psubssat | |
10 | 3 8 9 | syl2anc | |
11 | simprl | |
|
12 | 5 1 | psubssat | |
13 | 3 11 12 | syl2anc | |
14 | 5 2 | paddssat | |
15 | 3 10 13 14 | syl3anc | |
16 | simprr | |
|
17 | 1 2 | paddclN | |
18 | 3 4 16 17 | syl3anc | |
19 | 5 1 | psubssat | |
20 | 3 16 19 | syl2anc | |
21 | 5 2 | sspadd1 | |
22 | 3 7 20 21 | syl3anc | |
23 | 5 1 2 | pmod1i | |
24 | 23 | 3impia | |
25 | 3 7 15 18 22 24 | syl131anc | |
26 | incom | |
|
27 | 25 26 | eqtr3di | |
28 | 27 | oveq2d | |
29 | ssinss1 | |
|
30 | 15 29 | syl | |
31 | 5 2 | paddass | |
32 | 3 10 7 30 31 | syl13anc | |
33 | 5 2 | paddass | |
34 | 3 10 7 13 33 | syl13anc | |
35 | 5 2 | padd12N | |
36 | 3 10 7 13 35 | syl13anc | |
37 | 34 36 | eqtrd | |
38 | 5 2 | paddass | |
39 | 3 10 7 20 38 | syl13anc | |
40 | 37 39 | ineq12d | |
41 | incom | |
|
42 | 40 41 | eqtrdi | |
43 | 5 1 | psubssat | |
44 | 3 18 43 | syl2anc | |
45 | 1 2 | paddclN | |
46 | 3 8 11 45 | syl3anc | |
47 | 1 2 | paddclN | |
48 | 3 4 46 47 | syl3anc | |
49 | 5 2 | sspadd1 | |
50 | 3 10 13 49 | syl3anc | |
51 | 5 2 | sspadd2 | |
52 | 3 15 7 51 | syl3anc | |
53 | 50 52 | sstrd | |
54 | 5 1 2 | pmod1i | |
55 | 54 | 3impia | |
56 | 3 10 44 48 53 55 | syl131anc | |
57 | 42 56 | eqtrd | |
58 | 28 32 57 | 3eqtr4rd | |