Proof of Theorem hlpasch
Step | Hyp | Ref
| Expression |
1 | | hlpasch.p |
. . . 4
     |
2 | | hlpasch.i |
. . . 4
Itv   |
3 | | eqid 2451 |
. . . 4
LineG  LineG   |
4 | | hlpasch.g |
. . . . 5

TarskiG |
5 | 4 | adantr 467 |
. . . 4
 
    
TarskiG |
6 | | hlpasch.5 |
. . . . 5
   |
7 | 6 | adantr 467 |
. . . 4
 
    
  |
8 | | hlpasch.4 |
. . . . 5
   |
9 | 8 | adantr 467 |
. . . 4
 
    
  |
10 | | hlpasch.3 |
. . . . 5
   |
11 | 10 | adantr 467 |
. . . 4
 
    
  |
12 | | hlpasch.2 |
. . . . 5
   |
13 | 12 | adantr 467 |
. . . 4
 
    
  |
14 | | hlpasch.1 |
. . . . 5
   |
15 | 14 | adantr 467 |
. . . 4
 
    
  |
16 | | eqid 2451 |
. . . . 5
         |
17 | | simpr 463 |
. . . . 5
 
    
      |
18 | 1, 16, 2, 5, 13, 11, 7, 17 | tgbtwncom 24532 |
. . . 4
 
    
      |
19 | | hlpasch.8 |
. . . . 5
       |
20 | 19 | adantr 467 |
. . . 4
 
    
      |
21 | 1, 2, 3, 5, 7, 9, 11, 13, 15, 18, 20 | outpasch 24797 |
. . 3
 
    

            |
22 | | hlpasch.k |
. . . . . . 7
hlG   |
23 | | simplr 762 |
. . . . . . 7
   
    
              |
24 | 13 | ad2antrr 732 |
. . . . . . 7
   
    
              |
25 | 15 | ad2antrr 732 |
. . . . . . 7
   
    
              |
26 | 5 | ad2antrr 732 |
. . . . . . 7
   
    
            TarskiG |
27 | | simprr 766 |
. . . . . . . 8
   
    
                  |
28 | 1, 16, 2, 26, 24, 25, 23, 27 | tgbtwncom 24532 |
. . . . . . 7
   
    
                  |
29 | 26 | adantr 467 |
. . . . . . . . . . 11
          
          

TarskiG |
30 | 24 | adantr 467 |
. . . . . . . . . . 11
          
          
   |
31 | 25 | adantr 467 |
. . . . . . . . . . 11
          
          
   |
32 | 27 | adantr 467 |
. . . . . . . . . . . 12
          
          
       |
33 | | simpr 463 |
. . . . . . . . . . . . 13
          
          
   |
34 | 33 | oveq2d 6306 |
. . . . . . . . . . . 12
          
          
           |
35 | 32, 34 | eleqtrd 2531 |
. . . . . . . . . . 11
          
          
       |
36 | 1, 16, 2, 29, 30, 31, 35 | axtgbtwnid 24514 |
. . . . . . . . . 10
          
          
   |
37 | 36 | eqcomd 2457 |
. . . . . . . . 9
          
          
   |
38 | | hlpasch.6 |
. . . . . . . . . . . 12
   |
39 | 38 | ad3antrrr 736 |
. . . . . . . . . . 11
   
    
              |
40 | 39 | adantr 467 |
. . . . . . . . . 10
          
          
   |
41 | 40 | neneqd 2629 |
. . . . . . . . 9
          
          
   |
42 | 37, 41 | pm2.65da 580 |
. . . . . . . 8
   
    
           
  |
43 | 42 | neqned 2631 |
. . . . . . 7
   
    
              |
44 | 1, 2, 22, 23, 24, 25, 26, 25, 28, 43, 39 | btwnhl2 24658 |
. . . . . 6
   
    
                    |
45 | 7 | ad2antrr 732 |
. . . . . . 7
   
    
              |
46 | 9 | ad2antrr 732 |
. . . . . . 7
   
    
              |
47 | | simprl 764 |
. . . . . . 7
   
    
                  |
48 | 1, 16, 2, 26, 45, 23, 46, 47 | tgbtwncom 24532 |
. . . . . 6
   
    
                  |
49 | 44, 48 | jca 535 |
. . . . 5
   
    
                  
       |
50 | 49 | ex 436 |
. . . 4
                   
               |
51 | 50 | reximdva 2862 |
. . 3
 
    
 
    
            
        |
52 | 21, 51 | mpd 15 |
. 2
 
    

              |
53 | 6 | ad2antrr 732 |
. . . . . 6
          LineG    
  |
54 | 53 | adantr 467 |
. . . . 5
   
    
  LineG    
   |
55 | | simpr 463 |
. . . . . . 7
            LineG         |
56 | 55 | breq2d 4414 |
. . . . . 6
            LineG             
         |
57 | 55 | eleq1d 2513 |
. . . . . 6
            LineG           
       |
58 | 56, 57 | anbi12d 717 |
. . . . 5
            LineG                                   |
59 | 14 | ad2antrr 732 |
. . . . . . . 8
          LineG    
  |
60 | 59 | adantr 467 |
. . . . . . 7
   
    
  LineG    
   |
61 | 12 | ad2antrr 732 |
. . . . . . . 8
          LineG    
  |
62 | 61 | adantr 467 |
. . . . . . 7
   
    
  LineG    
   |
63 | 4 | ad2antrr 732 |
. . . . . . . 8
          LineG    
TarskiG |
64 | 63 | adantr 467 |
. . . . . . 7
   
    
  LineG    

TarskiG |
65 | | hlpasch.7 |
. . . . . . . . . 10
         |
66 | 1, 2, 22, 10, 6, 12, 4, 65 | hlcomd 24649 |
. . . . . . . . 9
         |
67 | 66 | ad3antrrr 736 |
. . . . . . . 8
   
    
  LineG    
         |
68 | 10 | adantr 467 |
. . . . . . . . . 10
 
    
  |
69 | 68 | ad2antrr 732 |
. . . . . . . . 9
   
    
  LineG    
   |
70 | 19 | adantr 467 |
. . . . . . . . . . 11
 
    
      |
71 | 70 | ad2antrr 732 |
. . . . . . . . . 10
   
    
  LineG    
       |
72 | | simpr 463 |
. . . . . . . . . . 11
   
    
  LineG    
   |
73 | 72 | oveq1d 6305 |
. . . . . . . . . 10
   
    
  LineG    
           |
74 | 71, 73 | eleqtrd 2531 |
. . . . . . . . 9
   
    
  LineG    
       |
75 | 1, 2, 22, 10, 6, 12, 4 | ishlg 24647 |
. . . . . . . . . . . 12
        
              |
76 | 65, 75 | mpbid 214 |
. . . . . . . . . . 11
 
             |
77 | 76 | simp1d 1020 |
. . . . . . . . . 10
   |
78 | 77 | ad3antrrr 736 |
. . . . . . . . 9
   
    
  LineG    
   |
79 | 38 | ad2antrr 732 |
. . . . . . . . . 10
          LineG    
  |
80 | 79 | adantr 467 |
. . . . . . . . 9
   
    
  LineG    
   |
81 | 1, 2, 22, 54, 69, 62, 64, 60, 74, 78, 80 | hlbtwn 24656 |
. . . . . . . 8
   
    
  LineG    
                 |
82 | 67, 81 | mpbid 214 |
. . . . . . 7
   
    
  LineG    
         |
83 | 1, 2, 22, 54, 60, 62, 64, 82 | hlcomd 24649 |
. . . . . 6
   
    
  LineG    
         |
84 | 8 | ad2antrr 732 |
. . . . . . . 8
          LineG    
  |
85 | 84 | adantr 467 |
. . . . . . 7
   
    
  LineG    
   |
86 | 1, 16, 2, 64, 85, 54 | tgbtwntriv2 24531 |
. . . . . 6
   
    
  LineG    
       |
87 | 83, 86 | jca 535 |
. . . . 5
   
    
  LineG    
               |
88 | 54, 58, 87 | rspcedvd 3155 |
. . . 4
   
    
  LineG    
        
       |
89 | 84 | ad2antrr 732 |
. . . . . 6
            LineG     
         |
90 | | simpr 463 |
. . . . . . . . 9
   
    
  LineG    
   |
91 | 90 | breq2d 4414 |
. . . . . . . 8
   
    
  LineG    
                 |
92 | 90 | eleq1d 2513 |
. . . . . . . 8
   
    
  LineG    
             |
93 | 91, 92 | anbi12d 717 |
. . . . . . 7
   
    
  LineG    
             
               |
94 | 93 | ad4ant14 1235 |
. . . . . 6
     
       LineG            
             
               |
95 | | simpr 463 |
. . . . . . 7
            LineG     
               |
96 | 1, 16, 2, 63, 84, 53 | tgbtwntriv1 24535 |
. . . . . . . 8
          LineG    
      |
97 | 96 | ad2antrr 732 |
. . . . . . 7
            LineG     
             |
98 | 95, 97 | jca 535 |
. . . . . 6
            LineG     
             
       |
99 | 89, 94, 98 | rspcedvd 3155 |
. . . . 5
            LineG     
       
              |
100 | 53 | ad2antrr 732 |
. . . . . 6
            LineG     
    
  |
101 | | simpr 463 |
. . . . . . . 8
     
       LineG              |
102 | 101 | breq2d 4414 |
. . . . . . 7
     
       LineG                  
         |
103 | 101 | eleq1d 2513 |
. . . . . . 7
     
       LineG                
       |
104 | 102, 103 | anbi12d 717 |
. . . . . 6
     
       LineG                                        |
105 | 79 | ad2antrr 732 |
. . . . . . . . 9
            LineG     
    
  |
106 | 1, 2, 22, 10, 6, 12, 4, 65 | hlne2 24651 |
. . . . . . . . . 10
   |
107 | 106 | ad4antr 738 |
. . . . . . . . 9
            LineG     
    
  |
108 | 63 | ad2antrr 732 |
. . . . . . . . . 10
            LineG     
    
TarskiG |
109 | 61 | ad2antrr 732 |
. . . . . . . . . 10
            LineG     
    
  |
110 | 59 | ad2antrr 732 |
. . . . . . . . . 10
            LineG     
    
  |
111 | 68 | ad2antrr 732 |
. . . . . . . . . . 11
   
    
  LineG     
  |
112 | 111 | adantr 467 |
. . . . . . . . . 10
            LineG     
    
  |
113 | 84 | ad2antrr 732 |
. . . . . . . . . . 11
            LineG     
    
  |
114 | | simpr 463 |
. . . . . . . . . . 11
            LineG     
    
      |
115 | 70 | ad2antrr 732 |
. . . . . . . . . . . 12
   
    
  LineG     
      |
116 | 115 | adantr 467 |
. . . . . . . . . . 11
            LineG     
    
      |
117 | 1, 16, 2, 108, 113, 109, 110, 112, 114, 116 | tgbtwnexch3 24538 |
. . . . . . . . . 10
            LineG     
    
      |
118 | | simp-4r 777 |
. . . . . . . . . 10
            LineG     
    
      |
119 | 1, 2, 108, 109, 110, 100, 112, 117, 118 | tgbtwnconn3 24622 |
. . . . . . . . 9
            LineG     
    
            |
120 | 105, 107,
119 | 3jca 1188 |
. . . . . . . 8
            LineG     
    

             |
121 | 1, 2, 22, 14, 6, 12, 4 | ishlg 24647 |
. . . . . . . . 9
        
              |
122 | 121 | ad4antr 738 |
. . . . . . . 8
            LineG     
    
      

              |
123 | 120, 122 | mpbird 236 |
. . . . . . 7
            LineG     
    
        |
124 | 1, 16, 2, 108, 113, 100 | tgbtwntriv2 24531 |
. . . . . . 7
            LineG     
    
      |
125 | 123, 124 | jca 535 |
. . . . . 6
            LineG     
    
              |
126 | 100, 104,
125 | rspcedvd 3155 |
. . . . 5
            LineG     
    

              |
127 | 8 | ad3antrrr 736 |
. . . . . 6
   
    
  LineG     
  |
128 | 12 | ad3antrrr 736 |
. . . . . 6
   
    
  LineG     
  |
129 | 14 | ad3antrrr 736 |
. . . . . 6
   
    
  LineG     
  |
130 | 4 | ad3antrrr 736 |
. . . . . 6
   
    
  LineG     
TarskiG |
131 | | simpr 463 |
. . . . . . . 8
   
    
  LineG        |
132 | 131 | neneqd 2629 |
. . . . . . 7
   
    
  LineG     
  |
133 | 63 | adantr 467 |
. . . . . . . . . 10
   
    
  LineG     
TarskiG |
134 | 133 | adantr 467 |
. . . . . . . . . . . . . 14
            LineG     
 TarskiG |
135 | 127 | adantr 467 |
. . . . . . . . . . . . . 14
            LineG     
   |
136 | 129 | adantr 467 |
. . . . . . . . . . . . . 14
            LineG     
   |
137 | 115 | adantr 467 |
. . . . . . . . . . . . . . 15
            LineG     
       |
138 | | simpr 463 |
. . . . . . . . . . . . . . . 16
            LineG     
   |
139 | 138 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
            LineG     
           |
140 | 137, 139 | eleqtrrd 2532 |
. . . . . . . . . . . . . 14
            LineG     
       |
141 | 1, 16, 2, 134, 135, 136, 140 | axtgbtwnid 24514 |
. . . . . . . . . . . . 13
            LineG     
   |
142 | 141 | olcd 395 |
. . . . . . . . . . . 12
            LineG     
 
  LineG       |
143 | 133 | adantr 467 |
. . . . . . . . . . . . 13
            LineG     

TarskiG |
144 | 128 | adantr 467 |
. . . . . . . . . . . . 13
            LineG     

  |
145 | 111 | adantr 467 |
. . . . . . . . . . . . 13
            LineG     

  |
146 | 127 | adantr 467 |
. . . . . . . . . . . . 13
            LineG     

  |
147 | 129 | adantr 467 |
. . . . . . . . . . . . 13
            LineG     

  |
148 | | simpr 463 |
. . . . . . . . . . . . . . . 16
            LineG     

  |
149 | 148 | necomd 2679 |
. . . . . . . . . . . . . . 15
            LineG     

  |
150 | 149 | neneqd 2629 |
. . . . . . . . . . . . . 14
            LineG     

  |
151 | 53 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
   
    
  LineG     
  |
152 | 106 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . 20
   
    
  LineG        |
153 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . 20
   
    
  LineG     
  LineG      |
154 | 1, 2, 3, 133, 151, 128, 127, 152, 153 | lncom 24667 |
. . . . . . . . . . . . . . . . . . 19
   
    
  LineG     
  LineG      |
155 | 77 | necomd 2679 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
156 | 155 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . 21
   
    
  LineG        |
157 | 66 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . . . . . 22
   
    
  LineG              |
158 | 1, 2, 22, 151, 111, 128, 133, 3, 157 | hlln 24652 |
. . . . . . . . . . . . . . . . . . . . 21
   
    
  LineG     
  LineG      |
159 | 1, 2, 3, 133, 128, 111, 151, 156, 158 | lncom 24667 |
. . . . . . . . . . . . . . . . . . . 20
   
    
  LineG     
  LineG      |
160 | 159 | orcd 394 |
. . . . . . . . . . . . . . . . . . 19
   
    
  LineG         LineG       |
161 | 1, 2, 3, 133, 127, 151, 128, 111, 154, 160 | coltr 24692 |
. . . . . . . . . . . . . . . . . 18
   
    
  LineG         LineG       |
162 | 1, 3, 2, 133, 128, 111, 127, 161 | colrot1 24604 |
. . . . . . . . . . . . . . . . 17
   
    
  LineG         LineG       |
163 | 162 | orcomd 390 |
. . . . . . . . . . . . . . . 16
   
    
  LineG         LineG       |
164 | 163 | adantr 467 |
. . . . . . . . . . . . . . 15
            LineG     


  LineG       |
165 | 164 | ord 379 |
. . . . . . . . . . . . . 14
            LineG     


  LineG       |
166 | 150, 165 | mpd 15 |
. . . . . . . . . . . . 13
            LineG     

  LineG      |
167 | 1, 3, 2, 133, 127, 129, 111, 115 | btwncolg3 24602 |
. . . . . . . . . . . . . 14
   
    
  LineG         LineG       |
168 | 167 | adantr 467 |
. . . . . . . . . . . . 13
            LineG     

   LineG       |
169 | 1, 2, 3, 143, 144, 145, 146, 147, 166, 168 | coltr 24692 |
. . . . . . . . . . . 12
            LineG     

   LineG       |
170 | 142, 169 | pm2.61dane 2711 |
. . . . . . . . . . 11
   
    
  LineG         LineG       |
171 | 1, 3, 2, 133, 127, 129, 128, 170 | colrot2 24605 |
. . . . . . . . . 10
   
    
  LineG         LineG       |
172 | 1, 3, 2, 133, 128, 127, 129, 171 | colcom 24603 |
. . . . . . . . 9
   
    
  LineG         LineG       |
173 | 172 | orcomd 390 |
. . . . . . . 8
   
    
  LineG         LineG       |
174 | 173 | ord 379 |
. . . . . . 7
   
    
  LineG      
  LineG       |
175 | 132, 174 | mpd 15 |
. . . . . 6
   
    
  LineG     
  LineG      |
176 | 1, 2, 22, 127, 128, 129, 130, 129, 3, 175 | lnhl 24660 |
. . . . 5
   
    
  LineG                    |
177 | 99, 126, 176 | mpjaodan 795 |
. . . 4
   
    
  LineG      
      
       |
178 | 88, 177 | pm2.61dane 2711 |
. . 3
          LineG    

              |
179 | 4 | adantr 467 |
. . . . . 6
 
    
TarskiG |
180 | 8 | adantr 467 |
. . . . . 6
 
    
  |
181 | 12 | adantr 467 |
. . . . . 6
 
    
  |
182 | 14 | adantr 467 |
. . . . . 6
 
    
  |
183 | 6 | adantr 467 |
. . . . . 6
 
    
  |
184 | | simpr 463 |
. . . . . 6
 
    
      |
185 | 1, 16, 2, 179, 180, 181, 68, 182, 183, 70, 184 | axtgpasch 24515 |
. . . . 5
 
    

            |
186 | 185 | adantr 467 |
. . . 4
       
  LineG     
            |
187 | | simplr 762 |
. . . . . . . 8
            LineG          
        |
188 | 182 | ad3antrrr 736 |
. . . . . . . 8
            LineG          
        |
189 | 181 | ad3antrrr 736 |
. . . . . . . 8
            LineG          
        |
190 | 179 | ad3antrrr 736 |
. . . . . . . 8
            LineG          
      TarskiG |
191 | | simprl 764 |
. . . . . . . . . 10
            LineG          
            |
192 | 1, 16, 2, 190, 188, 187, 189, 191 | tgbtwncom 24532 |
. . . . . . . . 9
            LineG          
            |
193 | 38 | necomd 2679 |
. . . . . . . . . 10
   |
194 | 193 | ad4antr 738 |
. . . . . . . . 9
            LineG          
        |
195 | 190 | adantr 467 |
. . . . . . . . . . . . 13
     
       LineG          
      
TarskiG |
196 | 6 | ad5antr 740 |
. . . . . . . . . . . . 13
     
       LineG          
      
  |
197 | 8 | ad5antr 740 |
. . . . . . . . . . . . 13
     
       LineG          
      
  |
198 | 189 | adantr 467 |
. . . . . . . . . . . . 13
     
       LineG          
      
  |
199 | | simp-4r 777 |
. . . . . . . . . . . . . . . 16
     
       LineG          
      
  LineG      |
200 | 106 | necomd 2679 |
. . . . . . . . . . . . . . . . . 18
   |
201 | 200 | ad5antr 740 |
. . . . . . . . . . . . . . . . 17
     
       LineG          
      
  |
202 | 201 | neneqd 2629 |
. . . . . . . . . . . . . . . 16
     
       LineG          
      
  |
203 | 199, 202 | jca 535 |
. . . . . . . . . . . . . . 15
     
       LineG          
      

  LineG   
   |
204 | | ioran 493 |
. . . . . . . . . . . . . . 15
    LineG        LineG       |
205 | 203, 204 | sylibr 216 |
. . . . . . . . . . . . . 14
     
       LineG          
      

  LineG       |
206 | 1, 3, 2, 195, 198, 196, 197, 205 | ncolrot2 24608 |
. . . . . . . . . . . . 13
     
       LineG          
      

  LineG       |
207 | | simpr 463 |
. . . . . . . . . . . . . 14
     
       LineG          
      
  |
208 | 187 | adantr 467 |
. . . . . . . . . . . . . . 15
     
       LineG          
      
  |
209 | 1, 2, 3, 195, 196, 197, 198, 206 | ncolne1 24670 |
. . . . . . . . . . . . . . 15
     
       LineG          
      
  |
210 | | simplrr 771 |
. . . . . . . . . . . . . . 15
     
       LineG          
      
      |
211 | 1, 2, 3, 195, 196, 197, 208, 209, 210 | btwnlng1 24664 |
. . . . . . . . . . . . . 14
     
       LineG          
      
  LineG      |
212 | 207, 211 | eqeltrrd 2530 |
. . . . . . . . . . . . 13
     
       LineG          
      
  LineG      |
213 | 1, 3, 2, 195, 196, 197, 212 | tglngne 24595 |
. . . . . . . . . . . . . 14
     
       LineG          
      
  |
214 | 1, 2, 3, 195, 196, 197, 213 | tglinerflx1 24678 |
. . . . . . . . . . . . 13
     
       LineG          
      
  LineG      |
215 | 106 | ad5antr 740 |
. . . . . . . . . . . . . . 15
     
       LineG          
      
  |
216 | 215 | necomd 2679 |
. . . . . . . . . . . . . 14
     
       LineG          
      
  |
217 | 1, 2, 3, 195, 198, 196, 216 | tglinerflx1 24678 |
. . . . . . . . . . . . 13
     
       LineG          
      
  LineG      |
218 | 1, 2, 3, 195, 198, 196, 216 | tglinerflx2 24679 |
. . . . . . . . . . . . 13
     
       LineG          
      
  LineG      |
219 | 1, 2, 3, 195, 196, 197, 198, 196, 206, 212, 214, 217, 218 | tglineinteq 24690 |
. . . . . . . . . . . 12
     
       LineG          
      
  |
220 | 219 | eqcomd 2457 |
. . . . . . . . . . 11
     
       LineG          
      
  |
221 | 215 | neneqd 2629 |
. . . . . . . . . . 11
     
       LineG          
      
  |
222 | 220, 221 | pm2.65da 580 |
. . . . . . . . . 10
            LineG          
     
  |
223 | 222 | neqned 2631 |
. . . . . . . . 9
            LineG          
        |
224 | 1, 2, 22, 189, 188, 187, 190, 188, 192, 194, 223 | btwnhl1 24657 |
. . . . . . . 8
            LineG          
              |
225 | 1, 2, 22, 187, 188, 189, 190, 224 | hlcomd 24649 |
. . . . . . 7
            LineG          
              |
226 | 179 | ad3antrrr 736 |
. . . . . . . . 9
            LineG           TarskiG |
227 | 183 | ad3antrrr 736 |
. . . . . . . . 9
            LineG             |
228 | | simplr 762 |
. . . . . . . . 9
            LineG             |
229 | 180 | ad3antrrr 736 |
. . . . . . . . 9
            LineG             |
230 | | simpr 463 |
. . . . . . . . 9
            LineG                 |
231 | 1, 16, 2, 226, 227, 228, 229, 230 | tgbtwncom 24532 |
. . . . . . . 8
            LineG                 |
232 | 231 | adantrl 722 |
. . . . . . 7
            LineG          
            |
233 | 225, 232 | jca 535 |
. . . . . 6
            LineG          
                    |
234 | 233 | ex 436 |
. . . . 5
   
    
  LineG    
                  
        |
235 | 234 | reximdva 2862 |
. . . 4
       
  LineG                 
               |
236 | 186, 235 | mpd 15 |
. . 3
       
  LineG     
      
       |
237 | 178, 236 | pm2.61dan 800 |
. 2
 
    

              |
238 | 76 | simp3d 1022 |
. 2
             |
239 | 52, 237, 238 | mpjaodan 795 |
1
        
       |