Proof of Theorem crctcsh
Step | Hyp | Ref
| Expression |
1 | | crctcsh.v |
. . . 4
Vtx |
2 | | crctcsh.i |
. . . 4
iEdg |
3 | | crctcsh.d |
. . . 4
Circuits |
4 | | crctcsh.n |
. . . 4
|
5 | | crctcsh.s |
. . . 4
..^ |
6 | | crctcsh.h |
. . . 4
cyclShift
|
7 | | crctcsh.q |
. . . 4
|
8 | 1, 2, 3, 4, 5, 6, 7 | crctcshlem4 26712 |
. . 3
|
9 | | breq12 4658 |
. . . . 5
Circuits
Circuits |
10 | 3, 9 | syl5ibrcom 237 |
. . . 4
Circuits |
11 | 10 | adantr 481 |
. . 3
Circuits |
12 | 8, 11 | mpd 15 |
. 2
Circuits |
13 | 1, 2, 3, 4, 5, 6, 7 | crctcshtrl 26715 |
. . . 4
Trails |
14 | 13 | adantr 481 |
. . 3
Trails |
15 | 7 | a1i 11 |
. . . . 5
|
16 | | breq1 4656 |
. . . . . . 7
|
17 | | oveq1 6657 |
. . . . . . . 8
|
18 | 17 | fveq2d 6195 |
. . . . . . 7
|
19 | 17 | oveq1d 6665 |
. . . . . . . 8
|
20 | 19 | fveq2d 6195 |
. . . . . . 7
|
21 | 16, 18, 20 | ifbieq12d 4113 |
. . . . . 6
|
22 | | elfzo0le 12511 |
. . . . . . . . . 10
..^
|
23 | 5, 22 | syl 17 |
. . . . . . . . 9
|
24 | 1, 2, 3, 4 | crctcshlem1 26709 |
. . . . . . . . . . 11
|
25 | 24 | nn0red 11352 |
. . . . . . . . . 10
|
26 | | elfzoelz 12470 |
. . . . . . . . . . . 12
..^
|
27 | 5, 26 | syl 17 |
. . . . . . . . . . 11
|
28 | 27 | zred 11482 |
. . . . . . . . . 10
|
29 | 25, 28 | subge0d 10617 |
. . . . . . . . 9
|
30 | 23, 29 | mpbird 247 |
. . . . . . . 8
|
31 | 30 | adantr 481 |
. . . . . . 7
|
32 | 31 | iftrued 4094 |
. . . . . 6
|
33 | 21, 32 | sylan9eqr 2678 |
. . . . 5
|
34 | 3 | adantr 481 |
. . . . . . 7
Circuits |
35 | 1, 2, 34, 4 | crctcshlem1 26709 |
. . . . . 6
|
36 | | 0elfz 12436 |
. . . . . 6
|
37 | 35, 36 | syl 17 |
. . . . 5
|
38 | | fvexd 6203 |
. . . . 5
|
39 | 15, 33, 37, 38 | fvmptd 6288 |
. . . 4
|
40 | | breq1 4656 |
. . . . . . . 8
|
41 | | oveq1 6657 |
. . . . . . . . 9
|
42 | 41 | fveq2d 6195 |
. . . . . . . 8
|
43 | 41 | oveq1d 6665 |
. . . . . . . . 9
|
44 | 43 | fveq2d 6195 |
. . . . . . . 8
|
45 | 40, 42, 44 | ifbieq12d 4113 |
. . . . . . 7
|
46 | | elfzoel2 12469 |
. . . . . . . . . . . 12
..^
|
47 | | elfzonn0 12512 |
. . . . . . . . . . . 12
..^
|
48 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
49 | 48 | anim1i 592 |
. . . . . . . . . . . . . . . 16
|
50 | | elnnne0 11306 |
. . . . . . . . . . . . . . . 16
|
51 | 49, 50 | sylibr 224 |
. . . . . . . . . . . . . . 15
|
52 | 51 | nngt0d 11064 |
. . . . . . . . . . . . . 14
|
53 | | zre 11381 |
. . . . . . . . . . . . . . . . 17
|
54 | | nn0re 11301 |
. . . . . . . . . . . . . . . . 17
|
55 | 53, 54 | anim12ci 591 |
. . . . . . . . . . . . . . . 16
|
56 | 55 | adantr 481 |
. . . . . . . . . . . . . . 15
|
57 | | ltsubpos 10520 |
. . . . . . . . . . . . . . . 16
|
58 | 57 | bicomd 213 |
. . . . . . . . . . . . . . 15
|
59 | 56, 58 | syl 17 |
. . . . . . . . . . . . . 14
|
60 | 52, 59 | mpbird 247 |
. . . . . . . . . . . . 13
|
61 | 60 | ex 450 |
. . . . . . . . . . . 12
|
62 | 46, 47, 61 | syl2anc 693 |
. . . . . . . . . . 11
..^
|
63 | 5, 62 | syl 17 |
. . . . . . . . . 10
|
64 | 63 | imp 445 |
. . . . . . . . 9
|
65 | 5 | adantr 481 |
. . . . . . . . . . . . 13
..^ |
66 | 1, 2, 34, 4, 65, 6 | crctcshlem2 26710 |
. . . . . . . . . . . 12
|
67 | 66 | breq1d 4663 |
. . . . . . . . . . 11
|
68 | 67 | notbid 308 |
. . . . . . . . . 10
|
69 | 25, 28 | resubcld 10458 |
. . . . . . . . . . . . 13
|
70 | 69, 25 | jca 554 |
. . . . . . . . . . . 12
|
71 | 70 | adantr 481 |
. . . . . . . . . . 11
|
72 | | ltnle 10117 |
. . . . . . . . . . 11
|
73 | 71, 72 | syl 17 |
. . . . . . . . . 10
|
74 | 68, 73 | bitr4d 271 |
. . . . . . . . 9
|
75 | 64, 74 | mpbird 247 |
. . . . . . . 8
|
76 | 75 | iffalsed 4097 |
. . . . . . 7
|
77 | 45, 76 | sylan9eqr 2678 |
. . . . . 6
|
78 | 1, 2, 3, 4, 5, 6 | crctcshlem2 26710 |
. . . . . . . . . . . . 13
|
79 | 78, 24 | eqeltrd 2701 |
. . . . . . . . . . . 12
|
80 | 79 | nn0cnd 11353 |
. . . . . . . . . . 11
|
81 | 27 | zcnd 11483 |
. . . . . . . . . . 11
|
82 | 24 | nn0cnd 11353 |
. . . . . . . . . . 11
|
83 | 80, 81, 82 | addsubd 10413 |
. . . . . . . . . 10
|
84 | 78 | oveq1d 6665 |
. . . . . . . . . . . 12
|
85 | 82 | subidd 10380 |
. . . . . . . . . . . 12
|
86 | 84, 85 | eqtrd 2656 |
. . . . . . . . . . 11
|
87 | 86 | oveq1d 6665 |
. . . . . . . . . 10
|
88 | 83, 87 | eqtrd 2656 |
. . . . . . . . 9
|
89 | 88 | fveq2d 6195 |
. . . . . . . 8
|
90 | 89 | adantr 481 |
. . . . . . 7
|
91 | 90 | adantr 481 |
. . . . . 6
|
92 | 77, 91 | eqtrd 2656 |
. . . . 5
|
93 | 78 | adantr 481 |
. . . . . 6
|
94 | | nn0fz0 12437 |
. . . . . . . 8
|
95 | 24, 94 | sylib 208 |
. . . . . . 7
|
96 | 95 | adantr 481 |
. . . . . 6
|
97 | 93, 96 | eqeltrd 2701 |
. . . . 5
|
98 | 15, 92, 97, 38 | fvmptd 6288 |
. . . 4
|
99 | 39, 98 | eqtr4d 2659 |
. . 3
|
100 | | iscrct 26685 |
. . 3
Circuits Trails |
101 | 14, 99, 100 | sylanbrc 698 |
. 2
Circuits |
102 | 12, 101 | pm2.61dane 2881 |
1
Circuits |