Proof of Theorem gomaex4
Step | Hyp | Ref
| Expression |
1 | | go2n4.7 |
. . . . . . 7
|
2 | | go2n4.8 |
. . . . . . 7
|
3 | | go2n4.1 |
. . . . . . 7
|
4 | | go2n4.2 |
. . . . . . 7
|
5 | | go2n4.3 |
. . . . . . 7
|
6 | | go2n4.4 |
. . . . . . 7
|
7 | | go2n4.5 |
. . . . . . 7
|
8 | | go2n4.6 |
. . . . . . 7
|
9 | | gomaex4.9 |
. . . . . . 7
|
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | go2n4 899 |
. . . . . 6
|
11 | | an4 86 |
. . . . . . 7
|
12 | | ancom 74 |
. . . . . . . 8
|
13 | | ancom 74 |
. . . . . . . . 9
|
14 | 13 | ran 78 |
. . . . . . . 8
|
15 | 12, 14 | ax-r2 36 |
. . . . . . 7
|
16 | | an4 86 |
. . . . . . 7
|
17 | 11, 15, 16 | 3tr 65 |
. . . . . 6
|
18 | | ax-a2 31 |
. . . . . 6
|
19 | 10, 17, 18 | le3tr1 140 |
. . . . 5
|
20 | | ancom 74 |
. . . . . . . . 9
|
21 | 20 | lan 77 |
. . . . . . . 8
|
22 | | an4 86 |
. . . . . . . 8
|
23 | | ancom 74 |
. . . . . . . . 9
|
24 | 23 | lan 77 |
. . . . . . . 8
|
25 | 21, 22, 24 | 3tr 65 |
. . . . . . 7
|
26 | | ancom 74 |
. . . . . . . 8
|
27 | | ancom 74 |
. . . . . . . 8
|
28 | 26, 27 | 2an 79 |
. . . . . . 7
|
29 | | ancom 74 |
. . . . . . 7
|
30 | 25, 28, 29 | 3tr 65 |
. . . . . 6
|
31 | | gomaex4.10 |
. . . . . . 7
|
32 | 5, 6, 7, 8, 1, 2, 3, 4, 31 | go2n4 899 |
. . . . . 6
|
33 | 30, 32 | bltr 138 |
. . . . 5
|
34 | 19, 33 | ler2an 173 |
. . . 4
|
35 | 34 | leran 153 |
. . 3
|
36 | | go1 343 |
. . 3
|
37 | 35, 36 | lbtr 139 |
. 2
|
38 | | le0 147 |
. 2
|
39 | 37, 38 | lebi 145 |
1
|