Step |
Hyp |
Ref |
Expression |
1 |
|
gpg3kgrtriex.n |
|
2 |
|
gpg3kgrtriex.g |
Could not format G = ( N gPetersenGr K ) : No typesetting found for |- G = ( N gPetersenGr K ) with typecode |- |
3 |
|
gpg3kgrtriex.e |
|
4 |
|
nnz |
|
5 |
|
3nn |
|
6 |
5
|
a1i |
|
7 |
|
id |
|
8 |
6 7
|
nnmulcld |
|
9 |
1 8
|
eqeltrid |
|
10 |
|
zmodfzo |
|
11 |
4 9 10
|
syl2anc |
|
12 |
|
opeq2 |
|
13 |
|
oveq1 |
|
14 |
13
|
oveq1d |
|
15 |
14
|
opeq2d |
|
16 |
12 15
|
preq12d |
|
17 |
16
|
eqeq2d |
|
18 |
|
opeq2 |
|
19 |
12 18
|
preq12d |
|
20 |
19
|
eqeq2d |
|
21 |
|
oveq1 |
|
22 |
21
|
oveq1d |
|
23 |
22
|
opeq2d |
|
24 |
18 23
|
preq12d |
|
25 |
24
|
eqeq2d |
|
26 |
17 20 25
|
3orbi123d |
|
27 |
26
|
adantl |
|
28 |
1
|
gpg3kgrtriexlem2 |
|
29 |
28
|
opeq2d |
|
30 |
29
|
preq2d |
|
31 |
3 30
|
eqtrid |
|
32 |
31
|
3mix3d |
|
33 |
11 27 32
|
rspcedvd |
|
34 |
|
3z |
|
35 |
34
|
a1i |
|
36 |
35 4
|
zmulcld |
|
37 |
|
3t1e3 |
|
38 |
|
nnge1 |
|
39 |
|
1red |
|
40 |
|
nnre |
|
41 |
|
3re |
|
42 |
|
3pos |
|
43 |
41 42
|
pm3.2i |
|
44 |
43
|
a1i |
|
45 |
|
lemul2 |
|
46 |
39 40 44 45
|
syl3anc |
|
47 |
38 46
|
mpbid |
|
48 |
37 47
|
eqbrtrrid |
|
49 |
|
eluz2 |
|
50 |
35 36 48 49
|
syl3anbrc |
|
51 |
1 50
|
eqeltrid |
|
52 |
41
|
a1i |
|
53 |
52 40
|
remulcld |
|
54 |
1 53
|
eqeltrid |
|
55 |
54
|
rehalfcld |
|
56 |
55
|
ceilcld |
|
57 |
56
|
zred |
|
58 |
53
|
rehalfcld |
|
59 |
58
|
ceilcld |
|
60 |
59
|
zred |
|
61 |
|
gpg3kgrtriexlem1 |
|
62 |
40 60 61
|
ltled |
|
63 |
1
|
oveq1i |
|
64 |
63
|
fveq2i |
|
65 |
62 64
|
breqtrrdi |
|
66 |
39 40 57 38 65
|
letrd |
|
67 |
|
elnnz1 |
|
68 |
56 66 67
|
sylanbrc |
|
69 |
61 64
|
breqtrrdi |
|
70 |
|
elfzo1 |
|
71 |
7 68 69 70
|
syl3anbrc |
|
72 |
|
eqid |
|
73 |
|
eqid |
|
74 |
|
eqid |
|
75 |
72 73 2 74
|
gpgedgel |
|
76 |
51 71 75
|
syl2anc |
|
77 |
33 76
|
mpbird |
|