Proof of Theorem grothprim
Step | Hyp | Ref
| Expression |
1 | | axgroth4 9654 |
. 2
|
2 | | 3anass 1042 |
. . . 4
|
3 | | dfss2 3591 |
. . . . . . . . . . . . 13
|
4 | | elin 3796 |
. . . . . . . . . . . . 13
|
5 | 3, 4 | imbi12i 340 |
. . . . . . . . . . . 12
|
6 | 5 | albii 1747 |
. . . . . . . . . . 11
|
7 | 6 | rexbii 3041 |
. . . . . . . . . 10
|
8 | | df-rex 2918 |
. . . . . . . . . 10
|
9 | 7, 8 | bitri 264 |
. . . . . . . . 9
|
10 | 9 | ralbii 2980 |
. . . . . . . 8
|
11 | | df-ral 2917 |
. . . . . . . 8
|
12 | 10, 11 | bitri 264 |
. . . . . . 7
|
13 | | dfss2 3591 |
. . . . . . . . . . 11
|
14 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
15 | | difexg 4808 |
. . . . . . . . . . . . . . 15
|
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
17 | | vex 3203 |
. . . . . . . . . . . . . 14
|
18 | | incom 3805 |
. . . . . . . . . . . . . . 15
|
19 | | disjdif 4040 |
. . . . . . . . . . . . . . 15
|
20 | 18, 19 | eqtri 2644 |
. . . . . . . . . . . . . 14
|
21 | 16, 17, 20 | brdom6disj 9354 |
. . . . . . . . . . . . 13
|
22 | 21 | orbi1i 542 |
. . . . . . . . . . . 12
|
23 | | 19.44v 1912 |
. . . . . . . . . . . 12
|
24 | 22, 23 | bitr4i 267 |
. . . . . . . . . . 11
|
25 | 13, 24 | imbi12i 340 |
. . . . . . . . . 10
|
26 | | 19.35 1805 |
. . . . . . . . . 10
|
27 | 25, 26 | bitr4i 267 |
. . . . . . . . 9
|
28 | | grothprimlem 9655 |
. . . . . . . . . . . . . . . . . 18
|
29 | 28 | mobii 2493 |
. . . . . . . . . . . . . . . . 17
|
30 | | mo2v 2477 |
. . . . . . . . . . . . . . . . 17
|
31 | 29, 30 | bitri 264 |
. . . . . . . . . . . . . . . 16
|
32 | 31 | ralbii 2980 |
. . . . . . . . . . . . . . 15
|
33 | | df-ral 2917 |
. . . . . . . . . . . . . . 15
|
34 | 32, 33 | bitri 264 |
. . . . . . . . . . . . . 14
|
35 | | df-ral 2917 |
. . . . . . . . . . . . . . 15
|
36 | | eldif 3584 |
. . . . . . . . . . . . . . . . . 18
|
37 | | grothprimlem 9655 |
. . . . . . . . . . . . . . . . . . . 20
|
38 | 37 | rexbii 3041 |
. . . . . . . . . . . . . . . . . . 19
|
39 | | df-rex 2918 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 38, 39 | bitri 264 |
. . . . . . . . . . . . . . . . . 18
|
41 | 36, 40 | imbi12i 340 |
. . . . . . . . . . . . . . . . 17
|
42 | | pm5.6 951 |
. . . . . . . . . . . . . . . . 17
|
43 | 41, 42 | bitri 264 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | albii 1747 |
. . . . . . . . . . . . . . 15
|
45 | 35, 44 | bitri 264 |
. . . . . . . . . . . . . 14
|
46 | 34, 45 | anbi12i 733 |
. . . . . . . . . . . . 13
|
47 | | 19.26 1798 |
. . . . . . . . . . . . 13
|
48 | 46, 47 | bitr4i 267 |
. . . . . . . . . . . 12
|
49 | 48 | orbi1i 542 |
. . . . . . . . . . 11
|
50 | 49 | imbi2i 326 |
. . . . . . . . . 10
|
51 | 50 | exbii 1774 |
. . . . . . . . 9
|
52 | 27, 51 | bitri 264 |
. . . . . . . 8
|
53 | 52 | albii 1747 |
. . . . . . 7
|
54 | 12, 53 | anbi12i 733 |
. . . . . 6
|
55 | | 19.26 1798 |
. . . . . 6
|
56 | 54, 55 | bitr4i 267 |
. . . . 5
|
57 | 56 | anbi2i 730 |
. . . 4
|
58 | 2, 57 | bitri 264 |
. . 3
|
59 | 58 | exbii 1774 |
. 2
|
60 | 1, 59 | mpbi 220 |
1
|