Proof of Theorem btwnconn1lem12
Step | Hyp | Ref
| Expression |
1 | | simp11 1091 |
. . . . 5
|
2 | | simp2l1 1160 |
. . . . 5
|
3 | | simp2l3 1162 |
. . . . 5
|
4 | | simp31 1097 |
. . . . 5
|
5 | | simp32 1098 |
. . . . 5
|
6 | | simp1l3 1156 |
. . . . . 6
Cgr
Cgr
Cgr Cgr |
7 | 6 | ad2antrl 764 |
. . . . 5
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
8 | | simpr1l 1118 |
. . . . . . 7
Cgr
Cgr
Cgr
|
9 | 8 | ad2antll 765 |
. . . . . 6
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
10 | | btwncolinear5 32180 |
. . . . . . . 8
|
11 | 1, 3, 4, 2, 10 | syl13anc 1328 |
. . . . . . 7
|
12 | 11 | adantr 481 |
. . . . . 6
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
13 | 9, 12 | mpd 15 |
. . . . 5
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
14 | | simp2l2 1161 |
. . . . . 6
|
15 | | simp2r1 1163 |
. . . . . . 7
|
16 | | simpr1r 1119 |
. . . . . . . 8
Cgr
Cgr
Cgr
Cgr |
17 | 16 | ad2antll 765 |
. . . . . . 7
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
18 | | simp2rr 1131 |
. . . . . . . 8
Cgr
Cgr
Cgr Cgr Cgr |
19 | 18 | ad2antrl 764 |
. . . . . . 7
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
20 | 1, 2, 4, 2, 15, 2,
14, 17, 19 | cgrtrand 32100 |
. . . . . 6
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
21 | | btwnconn1lem11 32204 |
. . . . . . 7
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
22 | 1, 14, 2, 5, 2, 21 | cgrcomlrand 32108 |
. . . . . 6
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
23 | 1, 2, 4, 2, 14, 2,
5, 20, 22 | cgrtrand 32100 |
. . . . 5
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
24 | | simp12 1092 |
. . . . . . . . . 10
|
25 | | simp13 1093 |
. . . . . . . . . 10
|
26 | | simp2r2 1164 |
. . . . . . . . . 10
|
27 | | simp1rr 1127 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr Cgr |
28 | 27 | ad2antrl 764 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
29 | | simp2ll 1128 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr Cgr |
30 | 29 | ad2antrl 764 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
31 | 1, 24, 25, 14, 3, 28, 30 | btwnexchand 32133 |
. . . . . . . . . 10
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
32 | | simp3ll 1132 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr Cgr
|
33 | 32 | ad2antrl 764 |
. . . . . . . . . 10
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
34 | 1, 24, 25, 3, 26, 31, 33 | btwnexch3and 32128 |
. . . . . . . . 9
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
35 | | opeq1 4402 |
. . . . . . . . . . . . . 14
|
36 | 35 | breq2d 4665 |
. . . . . . . . . . . . 13
|
37 | 36 | biimpac 503 |
. . . . . . . . . . . 12
|
38 | | axbtwnid 25819 |
. . . . . . . . . . . . 13
|
39 | 1, 3, 26, 38 | syl3anc 1326 |
. . . . . . . . . . . 12
|
40 | 37, 39 | syl5 34 |
. . . . . . . . . . 11
|
41 | 40 | expd 452 |
. . . . . . . . . 10
|
42 | 41 | adantr 481 |
. . . . . . . . 9
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
43 | 34, 42 | mpd 15 |
. . . . . . . 8
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
44 | | simp1 1061 |
. . . . . . . . . . 11
|
45 | | simp2l 1087 |
. . . . . . . . . . 11
|
46 | | simp2r 1088 |
. . . . . . . . . . 11
|
47 | 44, 45, 46 | 3jca 1242 |
. . . . . . . . . 10
|
48 | | simpl 473 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr Cgr |
49 | | simprl 794 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
50 | 48, 49 | jca 554 |
. . . . . . . . . 10
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr Cgr
|
51 | | btwnconn1lem7 32200 |
. . . . . . . . . 10
Cgr
Cgr
Cgr Cgr
|
52 | 47, 50, 51 | syl2an 494 |
. . . . . . . . 9
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
53 | | simp2rl 1130 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr Cgr |
54 | 53 | ad2antrl 764 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
55 | | simp3rl 1134 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr Cgr
|
56 | 55 | ad2antrl 764 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
57 | 1, 24, 2, 15, 26, 54, 56 | btwnexch3and 32128 |
. . . . . . . . . 10
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
58 | | btwncolinear2 32177 |
. . . . . . . . . . . 12
|
59 | 1, 2, 26, 15, 58 | syl13anc 1328 |
. . . . . . . . . . 11
|
60 | 59 | adantr 481 |
. . . . . . . . . 10
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
61 | 57, 60 | mpd 15 |
. . . . . . . . 9
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
62 | | simp33 1099 |
. . . . . . . . . 10
|
63 | | simpr2r 1121 |
. . . . . . . . . . . . . 14
Cgr
Cgr
Cgr
Cgr |
64 | 63 | ad2antll 765 |
. . . . . . . . . . . . 13
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
65 | | btwnconn1lem5 32198 |
. . . . . . . . . . . . . 14
Cgr
Cgr
Cgr Cgr
Cgr |
66 | 47, 50, 65 | syl2an 494 |
. . . . . . . . . . . . 13
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
67 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . 19
|
68 | 67 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
Cgr
Cgr |
69 | 68 | anbi1d 741 |
. . . . . . . . . . . . . . . . 17
Cgr Cgr
Cgr Cgr
|
70 | 69 | biimpac 503 |
. . . . . . . . . . . . . . . 16
Cgr Cgr
Cgr
Cgr |
71 | | simp2r3 1165 |
. . . . . . . . . . . . . . . . . 18
|
72 | | cgrid2 32110 |
. . . . . . . . . . . . . . . . . 18
Cgr
|
73 | 1, 2, 2, 71, 72 | syl13anc 1328 |
. . . . . . . . . . . . . . . . 17
Cgr
|
74 | | opeq1 4402 |
. . . . . . . . . . . . . . . . . . . 20
|
75 | | opeq1 4402 |
. . . . . . . . . . . . . . . . . . . 20
|
76 | 74, 75 | breq12d 4666 |
. . . . . . . . . . . . . . . . . . 19
Cgr
Cgr |
77 | 76 | biimpar 502 |
. . . . . . . . . . . . . . . . . 18
Cgr
Cgr |
78 | | cgrid2 32110 |
. . . . . . . . . . . . . . . . . . 19
Cgr |
79 | 1, 2, 2, 3, 78 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . 18
Cgr
|
80 | 77, 79 | syl5 34 |
. . . . . . . . . . . . . . . . 17
Cgr
|
81 | 73, 80 | syland 498 |
. . . . . . . . . . . . . . . 16
Cgr Cgr
|
82 | 70, 81 | syl5 34 |
. . . . . . . . . . . . . . 15
Cgr Cgr
|
83 | 82 | expd 452 |
. . . . . . . . . . . . . 14
Cgr Cgr
|
84 | 83 | adantr 481 |
. . . . . . . . . . . . 13
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
|
85 | 64, 66, 84 | mp2and 715 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
86 | 85 | necon3d 2815 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
87 | 7, 86 | mpd 15 |
. . . . . . . . . 10
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
88 | | simpr2l 1120 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr
|
89 | 88 | ad2antll 765 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
90 | | btwncolinear4 32179 |
. . . . . . . . . . . . 13
|
91 | 1, 15, 62, 2, 90 | syl13anc 1328 |
. . . . . . . . . . . 12
|
92 | 91 | adantr 481 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
93 | 89, 92 | mpd 15 |
. . . . . . . . . 10
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
94 | | simpr3r 1123 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr
Cgr |
95 | 94 | ad2antll 765 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
96 | 1, 62, 5, 62, 4, 95 | cgrcomand 32098 |
. . . . . . . . . 10
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
97 | 1, 62, 2, 15, 4, 5,
87, 93, 96, 23 | linecgrand 32189 |
. . . . . . . . 9
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
98 | 1, 2, 15, 26, 4, 5, 52, 61, 23, 97 | linecgrand 32189 |
. . . . . . . 8
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
99 | | opeq1 4402 |
. . . . . . . . . 10
|
100 | | opeq1 4402 |
. . . . . . . . . 10
|
101 | 99, 100 | breq12d 4666 |
. . . . . . . . 9
Cgr Cgr |
102 | 101 | biimprd 238 |
. . . . . . . 8
Cgr Cgr |
103 | 43, 98, 102 | syl6ci 71 |
. . . . . . 7
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
104 | 103 | com12 32 |
. . . . . 6
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
105 | | simprl 794 |
. . . . . . . . 9
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
106 | 34 | adantrl 752 |
. . . . . . . . . 10
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
107 | | btwncolinear1 32176 |
. . . . . . . . . . . 12
|
108 | 1, 25, 26, 3, 107 | syl13anc 1328 |
. . . . . . . . . . 11
|
109 | 108 | adantr 481 |
. . . . . . . . . 10
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
110 | 106, 109 | mpd 15 |
. . . . . . . . 9
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
111 | | simp1rl 1126 |
. . . . . . . . . . . . . 14
Cgr
Cgr
Cgr Cgr |
112 | 111 | ad2antrl 764 |
. . . . . . . . . . . . 13
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
113 | 1, 24, 25, 2, 15, 112, 54 | btwnexch3and 32128 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
114 | | btwncolinear6 32181 |
. . . . . . . . . . . . . 14
|
115 | 1, 25, 15, 2, 114 | syl13anc 1328 |
. . . . . . . . . . . . 13
|
116 | 115 | adantr 481 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
117 | 113, 116 | mpd 15 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
118 | 1, 2, 15, 25, 4, 5, 52, 117, 23, 97 | linecgrand 32189 |
. . . . . . . . . 10
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
119 | 118 | adantrl 752 |
. . . . . . . . 9
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
120 | 98 | adantrl 752 |
. . . . . . . . 9
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
121 | 1, 25, 26, 3, 4, 5,
105, 110, 119, 120 | linecgrand 32189 |
. . . . . . . 8
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
122 | 121 | an12s 843 |
. . . . . . 7
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
123 | 122 | ex 450 |
. . . . . 6
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
124 | 104, 123 | pm2.61ine 2877 |
. . . . 5
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
125 | 1, 2, 3, 4, 4, 5, 7, 13, 23, 124 | linecgrand 32189 |
. . . 4
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
126 | | cgrid2 32110 |
. . . . . 6
Cgr
|
127 | 1, 4, 4, 5, 126 | syl13anc 1328 |
. . . . 5
Cgr
|
128 | 127 | adantr 481 |
. . . 4
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
129 | 125, 128 | mpd 15 |
. . 3
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
130 | | btwnconn1lem10 32203 |
. . 3
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
131 | | opeq1 4402 |
. . . . . . 7
|
132 | 131 | breq2d 4665 |
. . . . . 6
Cgr
Cgr |
133 | 132 | biimpa 501 |
. . . . 5
Cgr
Cgr |
134 | | axcgrid 25796 |
. . . . . 6
Cgr
|
135 | 1, 15, 14, 5, 134 | syl13anc 1328 |
. . . . 5
Cgr
|
136 | 133, 135 | syl5 34 |
. . . 4
Cgr |
137 | 136 | adantr 481 |
. . 3
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
138 | 129, 130,
137 | mp2and 715 |
. 2
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|
139 | 138 | eqcomd 2628 |
1
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
|