Step | Hyp | Ref
| Expression |
1 | | outpasch.a |
. . . . . 6
|
2 | 1 | adantr 481 |
. . . . 5
|
3 | | simpr 477 |
. . . . . . 7
|
4 | 3 | eleq1d 2686 |
. . . . . 6
|
5 | 3 | oveq2d 6666 |
. . . . . . 7
|
6 | 5 | eleq2d 2687 |
. . . . . 6
|
7 | 4, 6 | anbi12d 747 |
. . . . 5
|
8 | | outpasch.p |
. . . . . . . 8
|
9 | | eqid 2622 |
. . . . . . . 8
|
10 | | outpasch.i |
. . . . . . . 8
Itv |
11 | | outpasch.g |
. . . . . . . 8
TarskiG |
12 | | outpasch.b |
. . . . . . . 8
|
13 | 8, 9, 10, 11, 1, 12 | tgbtwntriv1 25386 |
. . . . . . 7
|
14 | 13 | adantr 481 |
. . . . . 6
|
15 | 11 | adantr 481 |
. . . . . . 7
TarskiG |
16 | | outpasch.r |
. . . . . . . 8
|
17 | 16 | adantr 481 |
. . . . . . 7
|
18 | | outpasch.q |
. . . . . . . 8
|
19 | 18 | adantr 481 |
. . . . . . 7
|
20 | | outpasch.c |
. . . . . . . 8
|
21 | 20 | adantr 481 |
. . . . . . 7
|
22 | | simpr 477 |
. . . . . . 7
|
23 | | outpasch.1 |
. . . . . . . . 9
|
24 | 8, 9, 10, 11, 1, 20, 16, 23 | tgbtwncom 25383 |
. . . . . . . 8
|
25 | 24 | adantr 481 |
. . . . . . 7
|
26 | 8, 9, 10, 15, 17, 19, 21, 2, 22, 25 | tgbtwnexch 25393 |
. . . . . 6
|
27 | 14, 26 | jca 554 |
. . . . 5
|
28 | 2, 7, 27 | rspcedvd 3317 |
. . . 4
|
29 | 28 | adantlr 751 |
. . 3
|
30 | 12 | ad2antrr 762 |
. . . 4
|
31 | | eleq1 2689 |
. . . . . 6
|
32 | | eqidd 2623 |
. . . . . . 7
|
33 | | oveq2 6658 |
. . . . . . 7
|
34 | 32, 33 | eleq12d 2695 |
. . . . . 6
|
35 | 31, 34 | anbi12d 747 |
. . . . 5
|
36 | 35 | adantl 482 |
. . . 4
|
37 | 8, 9, 10, 11, 1, 12 | tgbtwntriv2 25382 |
. . . . . 6
|
38 | 37 | ad2antrr 762 |
. . . . 5
|
39 | 11 | ad2antrr 762 |
. . . . . . . 8
TarskiG |
40 | 39 | adantr 481 |
. . . . . . 7
TarskiG |
41 | 20 | ad3antrrr 766 |
. . . . . . 7
|
42 | 16 | ad3antrrr 766 |
. . . . . . 7
|
43 | 18 | ad3antrrr 766 |
. . . . . . 7
|
44 | 30 | adantr 481 |
. . . . . . 7
|
45 | | simpr 477 |
. . . . . . . 8
|
46 | 8, 9, 10, 40, 43, 42, 41, 45 | tgbtwncom 25383 |
. . . . . . 7
|
47 | | outpasch.2 |
. . . . . . . . 9
|
48 | 8, 9, 10, 11, 12, 18, 20, 47 | tgbtwncom 25383 |
. . . . . . . 8
|
49 | 48 | ad3antrrr 766 |
. . . . . . 7
|
50 | 8, 9, 10, 40, 41, 42, 43, 44, 46, 49 | tgbtwnexch3 25389 |
. . . . . 6
|
51 | 39 | adantr 481 |
. . . . . . 7
TarskiG |
52 | 30 | adantr 481 |
. . . . . . 7
|
53 | 18 | ad3antrrr 766 |
. . . . . . 7
|
54 | 16 | ad3antrrr 766 |
. . . . . . 7
|
55 | 20 | ad3antrrr 766 |
. . . . . . . 8
|
56 | | simpr 477 |
. . . . . . . . . . 11
|
57 | 8, 9, 10, 11, 16, 20 | tgbtwntriv2 25382 |
. . . . . . . . . . . 12
|
58 | 57 | ad4antr 768 |
. . . . . . . . . . 11
|
59 | 56, 58 | eqeltrd 2701 |
. . . . . . . . . 10
|
60 | | simpllr 799 |
. . . . . . . . . 10
|
61 | 59, 60 | pm2.65da 600 |
. . . . . . . . 9
|
62 | 61 | neqned 2801 |
. . . . . . . 8
|
63 | 47 | ad3antrrr 766 |
. . . . . . . 8
|
64 | | simpr 477 |
. . . . . . . 8
|
65 | 8, 9, 10, 51, 52, 53, 55, 54, 62, 63, 64 | tgbtwnouttr 25392 |
. . . . . . 7
|
66 | 8, 9, 10, 51, 52, 53, 54, 65 | tgbtwncom 25383 |
. . . . . 6
|
67 | | outpasch.l |
. . . . . . . . . . 11
LineG |
68 | 8, 67, 10, 11, 18, 20, 16 | tgcolg 25449 |
. . . . . . . . . 10
|
69 | 68 | biimpa 501 |
. . . . . . . . 9
|
70 | | 3orcoma 1046 |
. . . . . . . . . 10
|
71 | | 3orass 1040 |
. . . . . . . . . 10
|
72 | 70, 71 | bitr3i 266 |
. . . . . . . . 9
|
73 | 69, 72 | sylib 208 |
. . . . . . . 8
|
74 | 73 | ord 392 |
. . . . . . 7
|
75 | 74 | imp 445 |
. . . . . 6
|
76 | 50, 66, 75 | mpjaodan 827 |
. . . . 5
|
77 | 38, 76 | jca 554 |
. . . 4
|
78 | 30, 36, 77 | rspcedvd 3317 |
. . 3
|
79 | 29, 78 | pm2.61dan 832 |
. 2
|
80 | 12 | ad2antrr 762 |
. . . 4
|
81 | 35 | adantl 482 |
. . . 4
|
82 | 37 | ad2antrr 762 |
. . . . 5
|
83 | 11 | ad2antrr 762 |
. . . . . . 7
TarskiG |
84 | 16 | ad2antrr 762 |
. . . . . . 7
|
85 | 18 | ad2antrr 762 |
. . . . . . 7
|
86 | 20 | ad2antrr 762 |
. . . . . . 7
|
87 | | simplr 792 |
. . . . . . 7
|
88 | | simpr 477 |
. . . . . . 7
|
89 | 11 | adantr 481 |
. . . . . . . . 9
TarskiG |
90 | 16 | adantr 481 |
. . . . . . . . 9
|
91 | 18 | adantr 481 |
. . . . . . . . 9
|
92 | 20 | adantr 481 |
. . . . . . . . . 10
|
93 | | simpr 477 |
. . . . . . . . . 10
|
94 | 8, 10, 67, 89, 90, 91, 92, 93 | ncolne1 25520 |
. . . . . . . . 9
|
95 | 8, 10, 67, 89, 90, 91, 94 | tglinerflx2 25529 |
. . . . . . . 8
|
96 | 95 | adantr 481 |
. . . . . . 7
|
97 | 8, 67, 10, 89, 91, 92, 90, 93 | ncolcom 25456 |
. . . . . . . . . . 11
|
98 | 8, 67, 10, 89, 92, 91, 90, 97 | ncolrot1 25457 |
. . . . . . . . . 10
|
99 | 8, 10, 67, 89, 92, 91, 90, 98 | ncolne1 25520 |
. . . . . . . . 9
|
100 | 99 | adantr 481 |
. . . . . . . 8
|
101 | 48 | ad2antrr 762 |
. . . . . . . 8
|
102 | 8, 10, 67, 83, 86, 85, 80, 100, 101 | btwnlng3 25516 |
. . . . . . 7
|
103 | 8, 10, 67, 83, 86, 85, 100 | tglinerflx2 25529 |
. . . . . . 7
|
104 | 8, 10, 67, 83, 84, 85, 86, 85, 87, 88, 96, 102, 103 | tglineinteq 25540 |
. . . . . 6
|
105 | 8, 9, 10, 11, 16, 12 | tgbtwntriv2 25382 |
. . . . . . 7
|
106 | 105 | ad2antrr 762 |
. . . . . 6
|
107 | 104, 106 | eqeltrrd 2702 |
. . . . 5
|
108 | 82, 107 | jca 554 |
. . . 4
|
109 | 80, 81, 108 | rspcedvd 3317 |
. . 3
|
110 | | eleq1 2689 |
. . . . . . . . . 10
|
111 | 110 | cbvrexv 3172 |
. . . . . . . . 9
|
112 | 111 | anbi2i 730 |
. . . . . . . 8
|
113 | 112 | opabbii 4717 |
. . . . . . 7
|
114 | 89 | adantr 481 |
. . . . . . . 8
TarskiG |
115 | 90 | adantr 481 |
. . . . . . . 8
|
116 | 91 | adantr 481 |
. . . . . . . 8
|
117 | 94 | adantr 481 |
. . . . . . . 8
|
118 | 8, 10, 67, 114, 115, 116, 117 | tgelrnln 25525 |
. . . . . . 7
|
119 | | eqid 2622 |
. . . . . . 7
hlG hlG |
120 | 20 | ad2antrr 762 |
. . . . . . 7
|
121 | 1 | ad2antrr 762 |
. . . . . . 7
|
122 | 12 | adantr 481 |
. . . . . . . 8
|
123 | 122 | adantr 481 |
. . . . . . 7
|
124 | 95 | adantr 481 |
. . . . . . . 8
|
125 | 8, 67, 10, 89, 91, 92, 90, 93 | ncolrot2 25458 |
. . . . . . . . . 10
|
126 | | pm2.45 412 |
. . . . . . . . . 10
|
127 | 125, 126 | syl 17 |
. . . . . . . . 9
|
128 | 127 | adantr 481 |
. . . . . . . 8
|
129 | | simpr 477 |
. . . . . . . 8
|
130 | 48 | ad2antrr 762 |
. . . . . . . 8
|
131 | 8, 9, 10, 113, 120, 123, 124, 128, 129, 130 | islnoppd 25632 |
. . . . . . 7
|
132 | 8, 10, 67, 89, 90, 91, 94 | tglinerflx1 25528 |
. . . . . . . 8
|
133 | 132 | adantr 481 |
. . . . . . 7
|
134 | 23 | ad2antrr 762 |
. . . . . . . 8
|
135 | 24 | ad2antrr 762 |
. . . . . . . . . 10
|
136 | 8, 10, 67, 89, 92, 90, 91, 125 | ncolne1 25520 |
. . . . . . . . . . 11
|
137 | 136 | adantr 481 |
. . . . . . . . . 10
|
138 | 8, 9, 10, 114, 115, 120, 121, 135, 137 | tgbtwnne 25385 |
. . . . . . . . 9
|
139 | 138 | necomd 2849 |
. . . . . . . 8
|
140 | 8, 10, 119, 121, 115, 120, 114, 121, 134, 139, 137 | btwnhl2 25508 |
. . . . . . 7
hlG |
141 | 8, 9, 10, 113, 67, 118, 114, 119, 120, 121, 123, 131, 133, 140 | opphl 25646 |
. . . . . 6
|
142 | 8, 9, 10, 113, 121, 123 | islnopp 25631 |
. . . . . 6
|
143 | 141, 142 | mpbid 222 |
. . . . 5
|
144 | 143 | simprd 479 |
. . . 4
|
145 | 114 | ad2antrr 762 |
. . . . . . . . 9
TarskiG |
146 | 118 | ad2antrr 762 |
. . . . . . . . 9
|
147 | | simplr 792 |
. . . . . . . . 9
|
148 | 8, 67, 10, 145, 146, 147 | tglnpt 25444 |
. . . . . . . 8
|
149 | | simpr 477 |
. . . . . . . 8
|
150 | 145 | ad2antrr 762 |
. . . . . . . . . . 11
TarskiG |
151 | 90 | ad3antrrr 766 |
. . . . . . . . . . . 12
|
152 | 151 | ad2antrr 762 |
. . . . . . . . . . 11
|
153 | 91 | ad5antr 770 |
. . . . . . . . . . 11
|
154 | 120 | ad2antrr 762 |
. . . . . . . . . . . 12
|
155 | 154 | ad2antrr 762 |
. . . . . . . . . . 11
|
156 | 93 | ad5antr 770 |
. . . . . . . . . . 11
|
157 | | simplr 792 |
. . . . . . . . . . . 12
|
158 | 117 | ad4antr 768 |
. . . . . . . . . . . 12
|
159 | 148 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
160 | 94 | necomd 2849 |
. . . . . . . . . . . . . . 15
|
161 | 160 | ad5antr 770 |
. . . . . . . . . . . . . 14
|
162 | 147 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
163 | 8, 10, 67, 150, 153, 152, 159, 161, 162 | lncom 25517 |
. . . . . . . . . . . . 13
|
164 | | simprl 794 |
. . . . . . . . . . . . 13
|
165 | 8, 10, 67, 150, 159, 153, 152, 157, 163, 164 | coltr3 25543 |
. . . . . . . . . . . 12
|
166 | 8, 10, 67, 150, 152, 153, 157, 158, 165 | lncom 25517 |
. . . . . . . . . . 11
|
167 | 95 | ad5antr 770 |
. . . . . . . . . . 11
|
168 | 99 | ad5antr 770 |
. . . . . . . . . . . 12
|
169 | 123 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
170 | 169 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
171 | 99 | necomd 2849 |
. . . . . . . . . . . . . . 15
|
172 | 47 | adantr 481 |
. . . . . . . . . . . . . . 15
|
173 | 8, 10, 67, 89, 91, 92, 122, 171, 172 | btwnlng2 25515 |
. . . . . . . . . . . . . 14
|
174 | 173 | ad5antr 770 |
. . . . . . . . . . . . 13
|
175 | | simprr 796 |
. . . . . . . . . . . . . 14
|
176 | 8, 9, 10, 150, 155, 157, 170, 175 | tgbtwncom 25383 |
. . . . . . . . . . . . 13
|
177 | 8, 10, 67, 150, 170, 153, 155, 157, 174, 176 | coltr3 25543 |
. . . . . . . . . . . 12
|
178 | 8, 10, 67, 150, 155, 153, 157, 168, 177 | lncom 25517 |
. . . . . . . . . . 11
|
179 | 8, 10, 67, 89, 92, 91, 99 | tglinerflx2 25529 |
. . . . . . . . . . . 12
|
180 | 179 | ad5antr 770 |
. . . . . . . . . . 11
|
181 | 8, 10, 67, 150, 152, 153, 155, 153, 156, 166, 167, 178, 180 | tglineinteq 25540 |
. . . . . . . . . 10
|
182 | 8, 9, 10, 150, 159, 157, 152, 164 | tgbtwncom 25383 |
. . . . . . . . . 10
|
183 | 181, 182 | eqeltrrd 2702 |
. . . . . . . . 9
|
184 | 121 | ad2antrr 762 |
. . . . . . . . . 10
|
185 | 8, 9, 10, 145, 184, 148, 169, 149 | tgbtwncom 25383 |
. . . . . . . . . 10
|
186 | 24 | ad4antr 768 |
. . . . . . . . . 10
|
187 | 8, 9, 10, 145, 169, 151, 184, 148, 154, 185, 186 | axtgpasch 25366 |
. . . . . . . . 9
|
188 | 183, 187 | r19.29a 3078 |
. . . . . . . 8
|
189 | 148, 149,
188 | jca32 558 |
. . . . . . 7
|
190 | 189 | anasss 679 |
. . . . . 6
|
191 | 190 | ex 450 |
. . . . 5
|
192 | 191 | reximdv2 3014 |
. . . 4
|
193 | 144, 192 | mpd 15 |
. . 3
|
194 | 109, 193 | pm2.61dan 832 |
. 2
|
195 | 79, 194 | pm2.61dan 832 |
1
|