Proof of Theorem testmod2expanded
Step | Hyp | Ref
| Expression |
1 | | orass 75 |
. . . . . . . . . . . . 13
|
2 | 1 | lan 77 |
. . . . . . . . . . . 12
|
3 | 2 | cm 61 |
. . . . . . . . . . 11
|
4 | | leo 158 |
. . . . . . . . . . . . 13
|
5 | 4 | ler 149 |
. . . . . . . . . . . 12
|
6 | 5 | mlduali 1126 |
. . . . . . . . . . 11
|
7 | 3, 6 | tr 62 |
. . . . . . . . . 10
|
8 | | leo 158 |
. . . . . . . . . . . . . . 15
|
9 | | leor 159 |
. . . . . . . . . . . . . . 15
|
10 | 8, 9 | ler2an 173 |
. . . . . . . . . . . . . 14
|
11 | 10 | df2le2 136 |
. . . . . . . . . . . . 13
|
12 | 11 | ran 78 |
. . . . . . . . . . . 12
|
13 | 12 | cm 61 |
. . . . . . . . . . 11
|
14 | 13 | lor 70 |
. . . . . . . . . 10
|
15 | 7, 14 | tr 62 |
. . . . . . . . 9
|
16 | | anass 76 |
. . . . . . . . . 10
|
17 | 16 | lor 70 |
. . . . . . . . 9
|
18 | 15, 17 | tr 62 |
. . . . . . . 8
|
19 | | an32 83 |
. . . . . . . . . 10
|
20 | 19 | lan 77 |
. . . . . . . . 9
|
21 | 20 | lor 70 |
. . . . . . . 8
|
22 | 18, 21 | tr 62 |
. . . . . . 7
|
23 | | leor 159 |
. . . . . . . . . . 11
|
24 | 23 | mldual2i 1125 |
. . . . . . . . . 10
|
25 | 24 | ran 78 |
. . . . . . . . 9
|
26 | 25 | lan 77 |
. . . . . . . 8
|
27 | 26 | lor 70 |
. . . . . . 7
|
28 | 22, 27 | tr 62 |
. . . . . 6
|
29 | | ancom 74 |
. . . . . . . . . 10
|
30 | 29 | ror 71 |
. . . . . . . . 9
|
31 | 30 | ran 78 |
. . . . . . . 8
|
32 | 31 | lan 77 |
. . . . . . 7
|
33 | 32 | lor 70 |
. . . . . 6
|
34 | 28, 33 | tr 62 |
. . . . 5
|
35 | | lea 160 |
. . . . . . . . . . . 12
|
36 | 35 | leror 152 |
. . . . . . . . . . 11
|
37 | 36 | df2le2 136 |
. . . . . . . . . 10
|
38 | 37 | ran 78 |
. . . . . . . . 9
|
39 | 38 | cm 61 |
. . . . . . . 8
|
40 | | anass 76 |
. . . . . . . 8
|
41 | 39, 40 | tr 62 |
. . . . . . 7
|
42 | 41 | lan 77 |
. . . . . 6
|
43 | 42 | lor 70 |
. . . . 5
|
44 | 34, 43 | tr 62 |
. . . 4
|
45 | | l42modlem1 1147 |
. . . . . . 7
|
46 | 45 | lan 77 |
. . . . . 6
|
47 | 46 | lan 77 |
. . . . 5
|
48 | 47 | lor 70 |
. . . 4
|
49 | 44, 48 | tr 62 |
. . 3
|
50 | | orcom 73 |
. . . . . . . . 9
|
51 | | orcom 73 |
. . . . . . . . 9
|
52 | 50, 51 | 2an 79 |
. . . . . . . 8
|
53 | | ancom 74 |
. . . . . . . 8
|
54 | 52, 53 | tr 62 |
. . . . . . 7
|
55 | 54 | lor 70 |
. . . . . 6
|
56 | 55 | lan 77 |
. . . . 5
|
57 | 56 | lan 77 |
. . . 4
|
58 | 57 | lor 70 |
. . 3
|
59 | 49, 58 | tr 62 |
. 2
|
60 | | leao1 162 |
. . . . 5
|
61 | 60 | mlduali 1126 |
. . . 4
|
62 | 61 | lan 77 |
. . 3
|
63 | 62 | lor 70 |
. 2
|
64 | 59, 63 | tr 62 |
1
|