Step | Hyp | Ref
| Expression |
1 | | zfpow 4844 |
. . . 4
|
2 | | 19.8a 2052 |
. . . . . . . 8
|
3 | | sp 2053 |
. . . . . . . 8
|
4 | 2, 3 | imim12i 62 |
. . . . . . 7
|
5 | 4 | alimi 1739 |
. . . . . 6
|
6 | 5 | imim1i 63 |
. . . . 5
|
7 | 6 | alimi 1739 |
. . . 4
|
8 | 1, 7 | eximii 1764 |
. . 3
|
9 | | nfnae 2318 |
. . . . 5
|
10 | | nfnae 2318 |
. . . . 5
|
11 | 9, 10 | nfan 1828 |
. . . 4
|
12 | | nfnae 2318 |
. . . . . 6
|
13 | | nfnae 2318 |
. . . . . 6
|
14 | 12, 13 | nfan 1828 |
. . . . 5
|
15 | | nfv 1843 |
. . . . . . 7
|
16 | | nfnae 2318 |
. . . . . . . . . 10
|
17 | | nfcvd 2765 |
. . . . . . . . . . 11
|
18 | | nfcvf 2788 |
. . . . . . . . . . 11
|
19 | 17, 18 | nfeld 2773 |
. . . . . . . . . 10
|
20 | 16, 19 | nfexd 2167 |
. . . . . . . . 9
|
21 | 20 | adantr 481 |
. . . . . . . 8
|
22 | | nfcvd 2765 |
. . . . . . . . . . 11
|
23 | | nfcvf 2788 |
. . . . . . . . . . 11
|
24 | 22, 23 | nfeld 2773 |
. . . . . . . . . 10
|
25 | 13, 24 | nfald 2165 |
. . . . . . . . 9
|
26 | 25 | adantl 482 |
. . . . . . . 8
|
27 | 21, 26 | nfimd 1823 |
. . . . . . 7
|
28 | 15, 27 | nfald 2165 |
. . . . . 6
|
29 | 18, 17 | nfeld 2773 |
. . . . . . 7
|
30 | 29 | adantr 481 |
. . . . . 6
|
31 | 28, 30 | nfimd 1823 |
. . . . 5
|
32 | 14, 31 | nfald 2165 |
. . . 4
|
33 | | nfeqf2 2297 |
. . . . . . . . 9
|
34 | 33 | naecoms 2313 |
. . . . . . . 8
|
35 | 34 | adantr 481 |
. . . . . . 7
|
36 | 14, 35 | nfan1 2068 |
. . . . . 6
|
37 | | nfnae 2318 |
. . . . . . . . . . . . . 14
|
38 | | nfeqf2 2297 |
. . . . . . . . . . . . . . 15
|
39 | 38 | naecoms 2313 |
. . . . . . . . . . . . . 14
|
40 | 37, 39 | nfan1 2068 |
. . . . . . . . . . . . 13
|
41 | | elequ1 1997 |
. . . . . . . . . . . . . 14
|
42 | 41 | adantl 482 |
. . . . . . . . . . . . 13
|
43 | 40, 42 | exbid 2091 |
. . . . . . . . . . . 12
|
44 | 43 | adantll 750 |
. . . . . . . . . . 11
|
45 | 12, 34 | nfan1 2068 |
. . . . . . . . . . . . 13
|
46 | | elequ1 1997 |
. . . . . . . . . . . . . 14
|
47 | 46 | adantl 482 |
. . . . . . . . . . . . 13
|
48 | 45, 47 | albid 2090 |
. . . . . . . . . . . 12
|
49 | 48 | adantlr 751 |
. . . . . . . . . . 11
|
50 | 44, 49 | imbi12d 334 |
. . . . . . . . . 10
|
51 | 50 | ex 450 |
. . . . . . . . 9
|
52 | 11, 27, 51 | cbvald 2277 |
. . . . . . . 8
|
53 | 52 | adantr 481 |
. . . . . . 7
|
54 | | elequ2 2004 |
. . . . . . . 8
|
55 | 54 | adantl 482 |
. . . . . . 7
|
56 | 53, 55 | imbi12d 334 |
. . . . . 6
|
57 | 36, 56 | albid 2090 |
. . . . 5
|
58 | 57 | ex 450 |
. . . 4
|
59 | 11, 32, 58 | cbvexd 2278 |
. . 3
|
60 | 8, 59 | mpbii 223 |
. 2
|
61 | 60 | ex 450 |
1
|