Proof of Theorem cgracol
Step | Hyp | Ref
| Expression |
1 | | cgracol.p |
. . . . . . . . . 10
|
2 | | cgracol.i |
. . . . . . . . . 10
Itv |
3 | | cgracol.m |
. . . . . . . . . 10
|
4 | | cgracol.g |
. . . . . . . . . . 11
TarskiG |
5 | 4 | adantr 481 |
. . . . . . . . . 10
TarskiG |
6 | | cgracol.a |
. . . . . . . . . . 11
|
7 | 6 | adantr 481 |
. . . . . . . . . 10
|
8 | | cgracol.b |
. . . . . . . . . . 11
|
9 | 8 | adantr 481 |
. . . . . . . . . 10
|
10 | | cgracol.c |
. . . . . . . . . . 11
|
11 | 10 | adantr 481 |
. . . . . . . . . 10
|
12 | | cgracol.d |
. . . . . . . . . . 11
|
13 | 12 | adantr 481 |
. . . . . . . . . 10
|
14 | | cgracol.e |
. . . . . . . . . . 11
|
15 | 14 | adantr 481 |
. . . . . . . . . 10
|
16 | | cgracol.f |
. . . . . . . . . . 11
|
17 | 16 | adantr 481 |
. . . . . . . . . 10
|
18 | | cgracol.1 |
. . . . . . . . . . 11
cgrA |
19 | 18 | adantr 481 |
. . . . . . . . . 10
cgrA |
20 | | eqid 2622 |
. . . . . . . . . 10
hlG hlG |
21 | 1, 2, 20, 4, 6, 8,
10, 12, 14, 16, 18 | cgrane2 25705 |
. . . . . . . . . . . . . . . 16
|
22 | 21 | necomd 2849 |
. . . . . . . . . . . . . . 15
|
23 | 22 | adantr 481 |
. . . . . . . . . . . . . 14
|
24 | 1, 2, 20, 4, 6, 8,
10, 12, 14, 16, 18 | cgrane1 25704 |
. . . . . . . . . . . . . . 15
|
25 | 24 | adantr 481 |
. . . . . . . . . . . . . 14
|
26 | 4 | adantr 481 |
. . . . . . . . . . . . . . . 16
TarskiG |
27 | 6 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
28 | 10 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
29 | 8 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
30 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
31 | 1, 3, 2, 26, 27, 28, 29, 30 | tgbtwncom 25383 |
. . . . . . . . . . . . . . 15
|
32 | 31 | orcd 407 |
. . . . . . . . . . . . . 14
|
33 | 23, 25, 32 | 3jca 1242 |
. . . . . . . . . . . . 13
|
34 | 22 | adantr 481 |
. . . . . . . . . . . . . 14
|
35 | 24 | adantr 481 |
. . . . . . . . . . . . . 14
|
36 | 4 | adantr 481 |
. . . . . . . . . . . . . . . 16
TarskiG |
37 | 10 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
38 | 6 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
39 | 8 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
40 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
41 | 1, 3, 2, 36, 37, 38, 39, 40 | tgbtwncom 25383 |
. . . . . . . . . . . . . . 15
|
42 | 41 | olcd 408 |
. . . . . . . . . . . . . 14
|
43 | 34, 35, 42 | 3jca 1242 |
. . . . . . . . . . . . 13
|
44 | 33, 43 | jaodan 826 |
. . . . . . . . . . . 12
|
45 | 1, 2, 20, 10, 6, 8, 4 | ishlg 25497 |
. . . . . . . . . . . . 13
hlG
|
46 | 45 | adantr 481 |
. . . . . . . . . . . 12
hlG
|
47 | 44, 46 | mpbird 247 |
. . . . . . . . . . 11
hlG |
48 | 1, 2, 20, 11, 7, 9, 5, 47 | hlcomd 25499 |
. . . . . . . . . 10
hlG |
49 | 1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 19, 20, 48 | cgrahl 25718 |
. . . . . . . . 9
hlG |
50 | 1, 2, 20, 13, 17, 15, 5 | ishlg 25497 |
. . . . . . . . 9
hlG
|
51 | 49, 50 | mpbid 222 |
. . . . . . . 8
|
52 | 51 | simp3d 1075 |
. . . . . . 7
|
53 | 4 | adantr 481 |
. . . . . . . . . 10
TarskiG |
54 | 14 | adantr 481 |
. . . . . . . . . 10
|
55 | 12 | adantr 481 |
. . . . . . . . . 10
|
56 | 16 | adantr 481 |
. . . . . . . . . 10
|
57 | | simpr 477 |
. . . . . . . . . 10
|
58 | 1, 3, 2, 53, 54, 55, 56, 57 | tgbtwncom 25383 |
. . . . . . . . 9
|
59 | 58 | olcd 408 |
. . . . . . . 8
|
60 | 4 | adantr 481 |
. . . . . . . . . 10
TarskiG |
61 | 14 | adantr 481 |
. . . . . . . . . 10
|
62 | 16 | adantr 481 |
. . . . . . . . . 10
|
63 | 12 | adantr 481 |
. . . . . . . . . 10
|
64 | | simpr 477 |
. . . . . . . . . 10
|
65 | 1, 3, 2, 60, 61, 62, 63, 64 | tgbtwncom 25383 |
. . . . . . . . 9
|
66 | 65 | orcd 407 |
. . . . . . . 8
|
67 | 59, 66 | jaodan 826 |
. . . . . . 7
|
68 | 52, 67 | syldan 487 |
. . . . . 6
|
69 | 68 | orcd 407 |
. . . . 5
|
70 | | df-3or 1038 |
. . . . 5
|
71 | 69, 70 | sylibr 224 |
. . . 4
|
72 | | cgracol.l |
. . . . . 6
LineG |
73 | 1, 2, 4, 20, 6, 8,
10, 12, 14, 16, 18 | cgracom 25714 |
. . . . . . 7
cgrA |
74 | 1, 2, 20, 4, 12, 14, 16, 6, 8, 10, 73 | cgrane1 25704 |
. . . . . 6
|
75 | 1, 72, 2, 4, 12, 14, 74, 16 | tgellng 25448 |
. . . . 5
|
76 | 75 | adantr 481 |
. . . 4
|
77 | 71, 76 | mpbird 247 |
. . 3
|
78 | 77 | orcd 407 |
. 2
|
79 | 4 | adantr 481 |
. . 3
TarskiG |
80 | 12 | adantr 481 |
. . 3
|
81 | 14 | adantr 481 |
. . 3
|
82 | 16 | adantr 481 |
. . 3
|
83 | 6 | adantr 481 |
. . . 4
|
84 | 8 | adantr 481 |
. . . 4
|
85 | 10 | adantr 481 |
. . . 4
|
86 | 18 | adantr 481 |
. . . 4
cgrA |
87 | | simpr 477 |
. . . 4
|
88 | 1, 2, 3, 79, 83, 84, 85, 80, 81, 82, 86, 87 | cgrabtwn 25717 |
. . 3
|
89 | 1, 72, 2, 79, 80, 81, 82, 88 | btwncolg3 25452 |
. 2
|
90 | 24 | neneqd 2799 |
. . . . 5
|
91 | | cgracol.2 |
. . . . . . 7
|
92 | 91 | orcomd 403 |
. . . . . 6
|
93 | 92 | ord 392 |
. . . . 5
|
94 | 90, 93 | mpd 15 |
. . . 4
|
95 | 1, 72, 2, 4, 6, 8, 24, 10 | tgellng 25448 |
. . . 4
|
96 | 94, 95 | mpbid 222 |
. . 3
|
97 | | df-3or 1038 |
. . 3
|
98 | 96, 97 | sylib 208 |
. 2
|
99 | 78, 89, 98 | mpjaodan 827 |
1
|