Step | Hyp | Ref
| Expression |
1 | | outpasch.a |
. . . . . 6
   |
2 | 1 | adantr 467 |
. . . . 5
 
    
  |
3 | | simpr 463 |
. . . . . . 7
           |
4 | 3 | eleq1d 2512 |
. . . . . 6
             
       |
5 | 3 | oveq2d 6304 |
. . . . . . 7
                   |
6 | 5 | eleq2d 2513 |
. . . . . 6
         
   
       |
7 | 4, 6 | anbi12d 716 |
. . . . 5
                                 |
8 | | outpasch.p |
. . . . . . . 8
     |
9 | | eqid 2450 |
. . . . . . . 8
         |
10 | | outpasch.i |
. . . . . . . 8
Itv   |
11 | | outpasch.g |
. . . . . . . 8

TarskiG |
12 | | outpasch.b |
. . . . . . . 8
   |
13 | 8, 9, 10, 11, 1, 12 | tgbtwntriv1 24528 |
. . . . . . 7
       |
14 | 13 | adantr 467 |
. . . . . 6
 
    
      |
15 | 11 | adantr 467 |
. . . . . . 7
 
    
TarskiG |
16 | | outpasch.r |
. . . . . . . 8
   |
17 | 16 | adantr 467 |
. . . . . . 7
 
    
  |
18 | | outpasch.q |
. . . . . . . 8
   |
19 | 18 | adantr 467 |
. . . . . . 7
 
    
  |
20 | | outpasch.c |
. . . . . . . 8
   |
21 | 20 | adantr 467 |
. . . . . . 7
 
    
  |
22 | | simpr 463 |
. . . . . . 7
 
    
      |
23 | | outpasch.1 |
. . . . . . . . 9
       |
24 | 8, 9, 10, 11, 1, 20, 16, 23 | tgbtwncom 24525 |
. . . . . . . 8
       |
25 | 24 | adantr 467 |
. . . . . . 7
 
    
      |
26 | 8, 9, 10, 15, 17, 19, 21, 2, 22, 25 | tgbtwnexch 24535 |
. . . . . 6
 
    
      |
27 | 14, 26 | jca 535 |
. . . . 5
 
    
            |
28 | 2, 7, 27 | rspcedvd 3154 |
. . . 4
 
    

            |
29 | 28 | adantlr 720 |
. . 3
   
     
     

           |
30 | 12 | ad2antrr 731 |
. . . 4
   
     
    
  |
31 | | eleq1 2516 |
. . . . . 6
     
       |
32 | | eqidd 2451 |
. . . . . . 7
   |
33 | | oveq2 6296 |
. . . . . . 7
           |
34 | 32, 33 | eleq12d 2522 |
. . . . . 6
 
   
       |
35 | 31, 34 | anbi12d 716 |
. . . . 5
                         |
36 | 35 | adantl 468 |
. . . 4
    
                                    |
37 | 8, 9, 10, 11, 1, 12 | tgbtwntriv2 24524 |
. . . . . 6
       |
38 | 37 | ad2antrr 731 |
. . . . 5
   
     
    
      |
39 | 11 | ad2antrr 731 |
. . . . . . . 8
   
     
    
TarskiG |
40 | 39 | adantr 467 |
. . . . . . 7
    
                TarskiG |
41 | 20 | ad3antrrr 735 |
. . . . . . 7
    
                  |
42 | 16 | ad3antrrr 735 |
. . . . . . 7
    
                  |
43 | 18 | ad3antrrr 735 |
. . . . . . 7
    
                  |
44 | 30 | adantr 467 |
. . . . . . 7
    
                  |
45 | | simpr 463 |
. . . . . . . 8
    
                      |
46 | 8, 9, 10, 40, 43, 42, 41, 45 | tgbtwncom 24525 |
. . . . . . 7
    
                      |
47 | | outpasch.2 |
. . . . . . . . 9
       |
48 | 8, 9, 10, 11, 12, 18, 20, 47 | tgbtwncom 24525 |
. . . . . . . 8
       |
49 | 48 | ad3antrrr 735 |
. . . . . . 7
    
                      |
50 | 8, 9, 10, 40, 41, 42, 43, 44, 46, 49 | tgbtwnexch3 24531 |
. . . . . 6
    
                      |
51 | 39 | adantr 467 |
. . . . . . 7
    
                TarskiG |
52 | 30 | adantr 467 |
. . . . . . 7
    
                  |
53 | 18 | ad3antrrr 735 |
. . . . . . 7
    
                  |
54 | 16 | ad3antrrr 735 |
. . . . . . 7
    
                  |
55 | 20 | ad3antrrr 735 |
. . . . . . . 8
    
                  |
56 | | simpr 463 |
. . . . . . . . . . 11
           
    
    
   |
57 | 8, 9, 10, 11, 16, 20 | tgbtwntriv2 24524 |
. . . . . . . . . . . 12
       |
58 | 57 | ad4antr 737 |
. . . . . . . . . . 11
           
    
    
       |
59 | 56, 58 | eqeltrd 2528 |
. . . . . . . . . 10
           
    
    
       |
60 | | simpllr 768 |
. . . . . . . . . 10
           
    
    
       |
61 | 59, 60 | pm2.65da 579 |
. . . . . . . . 9
    
               
  |
62 | 61 | neqned 2630 |
. . . . . . . 8
    
                  |
63 | 47 | ad3antrrr 735 |
. . . . . . . 8
    
                      |
64 | | simpr 463 |
. . . . . . . 8
    
                      |
65 | 8, 9, 10, 51, 52, 53, 55, 54, 62, 63, 64 | tgbtwnouttr 24534 |
. . . . . . 7
    
                      |
66 | 8, 9, 10, 51, 52, 53, 54, 65 | tgbtwncom 24525 |
. . . . . 6
    
                      |
67 | | outpasch.l |
. . . . . . . . . . 11
LineG   |
68 | 8, 67, 10, 11, 18, 20, 16 | tgcolg 24592 |
. . . . . . . . . 10
       
                 |
69 | 68 | biimpa 487 |
. . . . . . . . 9
 
                       |
70 | | 3orcoma 992 |
. . . . . . . . . 10
                               |
71 | | 3orass 987 |
. . . . . . . . . 10
                                 |
72 | 70, 71 | bitr3i 255 |
. . . . . . . . 9
                                 |
73 | 69, 72 | sylib 200 |
. . . . . . . 8
 
                         |
74 | 73 | ord 379 |
. . . . . . 7
 
           
             |
75 | 74 | imp 431 |
. . . . . 6
   
     
    
            |
76 | 50, 66, 75 | mpjaodan 794 |
. . . . 5
   
     
    
      |
77 | 38, 76 | jca 535 |
. . . 4
   
     
    
            |
78 | 30, 36, 77 | rspcedvd 3154 |
. . 3
   
     
    

            |
79 | 29, 78 | pm2.61dan 799 |
. 2
 
       

           |
80 | 12 | ad2antrr 731 |
. . . 4
   
             |
81 | 35 | adantl 468 |
. . . 4
                                         |
82 | 37 | ad2antrr 731 |
. . . . 5
   
                 |
83 | 11 | ad2antrr 731 |
. . . . . . 7
   
           TarskiG |
84 | 16 | ad2antrr 731 |
. . . . . . 7
   
             |
85 | 18 | ad2antrr 731 |
. . . . . . 7
   
             |
86 | 20 | ad2antrr 731 |
. . . . . . 7
   
             |
87 | | simplr 761 |
. . . . . . 7
   
           
       |
88 | | simpr 463 |
. . . . . . 7
   
                 |
89 | 11 | adantr 467 |
. . . . . . . . 9
 

     
TarskiG |
90 | 16 | adantr 467 |
. . . . . . . . 9
 

     
  |
91 | 18 | adantr 467 |
. . . . . . . . 9
 

     
  |
92 | 20 | adantr 467 |
. . . . . . . . . 10
 

     
  |
93 | | simpr 463 |
. . . . . . . . . 10
 

              |
94 | 8, 10, 67, 89, 90, 91, 92, 93 | ncolne1 24663 |
. . . . . . . . 9
 

        |
95 | 8, 10, 67, 89, 90, 91, 94 | tglinerflx2 24672 |
. . . . . . . 8
 

     
      |
96 | 95 | adantr 467 |
. . . . . . 7
   
                 |
97 | 8, 67, 10, 89, 91, 92, 90, 93 | ncolcom 24599 |
. . . . . . . . . . 11
 

              |
98 | 8, 67, 10, 89, 92, 91, 90, 97 | ncolrot1 24600 |
. . . . . . . . . 10
 

              |
99 | 8, 10, 67, 89, 92, 91, 90, 98 | ncolne1 24663 |
. . . . . . . . 9
 

        |
100 | 99 | adantr 467 |
. . . . . . . 8
   
             |
101 | 48 | ad2antrr 731 |
. . . . . . . 8
   
                 |
102 | 8, 10, 67, 83, 86, 85, 80, 100, 101 | btwnlng3 24659 |
. . . . . . 7
   
                 |
103 | 8, 10, 67, 83, 86, 85, 100 | tglinerflx2 24672 |
. . . . . . 7
   
                 |
104 | 8, 10, 67, 83, 84, 85, 86, 85, 87, 88, 96, 102, 103 | tglineinteq 24683 |
. . . . . 6
   
             |
105 | 8, 9, 10, 11, 16, 12 | tgbtwntriv2 24524 |
. . . . . . 7
       |
106 | 105 | ad2antrr 731 |
. . . . . 6
   
                 |
107 | 104, 106 | eqeltrrd 2529 |
. . . . 5
   
                 |
108 | 82, 107 | jca 535 |
. . . 4
   
           
           |
109 | 80, 81, 108 | rspcedvd 3154 |
. . 3
   
           
            |
110 | | eleq1 2516 |
. . . . . . . . . 10
     
       |
111 | 110 | cbvrexv 3019 |
. . . . . . . . 9
          
            |
112 | 111 | anbi2i 699 |
. . . . . . . 8
                                                       |
113 | 112 | opabbii 4466 |
. . . . . . 7
                                                               |
114 | 89 | adantr 467 |
. . . . . . . 8
   
           TarskiG |
115 | 90 | adantr 467 |
. . . . . . . 8
   
             |
116 | 91 | adantr 467 |
. . . . . . . 8
   
             |
117 | 94 | adantr 467 |
. . . . . . . 8
   
             |
118 | 8, 10, 67, 114, 115, 116, 117 | tgelrnln 24668 |
. . . . . . 7
   
                 |
119 | | eqid 2450 |
. . . . . . 7
hlG  hlG   |
120 | 20 | ad2antrr 731 |
. . . . . . 7
   
             |
121 | 1 | ad2antrr 731 |
. . . . . . 7
   
             |
122 | 12 | adantr 467 |
. . . . . . . 8
 

     
  |
123 | 122 | adantr 467 |
. . . . . . 7
   
             |
124 | 95 | adantr 467 |
. . . . . . . 8
   
                 |
125 | 8, 67, 10, 89, 91, 92, 90, 93 | ncolrot2 24601 |
. . . . . . . . . 10
 

              |
126 | | pm2.45 399 |
. . . . . . . . . 10
      
      |
127 | 125, 126 | syl 17 |
. . . . . . . . 9
 

     
      |
128 | 127 | adantr 467 |
. . . . . . . 8
   
          
      |
129 | | simpr 463 |
. . . . . . . 8
   
          
      |
130 | 48 | ad2antrr 731 |
. . . . . . . 8
   
                 |
131 | 8, 9, 10, 113, 120, 123, 124, 128, 129, 130 | islnoppd 24775 |
. . . . . . 7
   
               
       
                      |
132 | 8, 10, 67, 89, 90, 91, 94 | tglinerflx1 24671 |
. . . . . . . 8
 

     
      |
133 | 132 | adantr 467 |
. . . . . . 7
   
                 |
134 | 23 | ad2antrr 731 |
. . . . . . . 8
   
                 |
135 | 24 | ad2antrr 731 |
. . . . . . . . . 10
   
                 |
136 | 8, 10, 67, 89, 92, 90, 91, 125 | ncolne1 24663 |
. . . . . . . . . . 11
 

        |
137 | 136 | adantr 467 |
. . . . . . . . . 10
   
             |
138 | 8, 9, 10, 114, 115, 120, 121, 135, 137 | tgbtwnne 24527 |
. . . . . . . . 9
   
             |
139 | 138 | necomd 2678 |
. . . . . . . 8
   
             |
140 | 8, 10, 119, 121, 115, 120, 114, 121, 134, 139, 137 | btwnhl2 24651 |
. . . . . . 7
   
             hlG        |
141 | 8, 9, 10, 113, 67, 118, 114, 119, 120, 121, 123, 131, 133, 140 | opphl 24789 |
. . . . . 6
   
               
       
                      |
142 | 8, 9, 10, 113, 121, 123 | islnopp 24774 |
. . . . . 6
   
                
       
                         
                   |
143 | 141, 142 | mpbid 214 |
. . . . 5
   
                      
            |
144 | 143 | simprd 465 |
. . . 4
   
                       |
145 | 114 | ad2antrr 731 |
. . . . . . . . 9
           
               TarskiG |
146 | 118 | ad2antrr 731 |
. . . . . . . . 9
           
                     |
147 | | simplr 761 |
. . . . . . . . 9
           
                     |
148 | 8, 67, 10, 145, 146, 147 | tglnpt 24587 |
. . . . . . . 8
           
                 |
149 | | simpr 463 |
. . . . . . . 8
           
                     |
150 | 145 | ad2antrr 731 |
. . . . . . . . . . 11
       
                          
      TarskiG |
151 | 90 | ad3antrrr 735 |
. . . . . . . . . . . 12
           
                 |
152 | 151 | ad2antrr 731 |
. . . . . . . . . . 11
       
                          
        |
153 | 91 | ad5antr 739 |
. . . . . . . . . . 11
       
                          
        |
154 | 120 | ad2antrr 731 |
. . . . . . . . . . . 12
           
                 |
155 | 154 | ad2antrr 731 |
. . . . . . . . . . 11
       
                          
        |
156 | 93 | ad5antr 739 |
. . . . . . . . . . 11
       
                          
     
        |
157 | | simplr 761 |
. . . . . . . . . . . 12
       
                          
        |
158 | 117 | ad4antr 737 |
. . . . . . . . . . . 12
       
                          
        |
159 | 148 | ad2antrr 731 |
. . . . . . . . . . . . 13
       
                          
        |
160 | 94 | necomd 2678 |
. . . . . . . . . . . . . . 15
 

        |
161 | 160 | ad5antr 739 |
. . . . . . . . . . . . . 14
       
                          
        |
162 | 147 | ad2antrr 731 |
. . . . . . . . . . . . . 14
       
                          
            |
163 | 8, 10, 67, 150, 153, 152, 159, 161, 162 | lncom 24660 |
. . . . . . . . . . . . 13
       
                          
            |
164 | | simprl 763 |
. . . . . . . . . . . . 13
       
                          
            |
165 | 8, 10, 67, 150, 159, 153, 152, 157, 163, 164 | coltr3 24686 |
. . . . . . . . . . . 12
       
                          
            |
166 | 8, 10, 67, 150, 152, 153, 157, 158, 165 | lncom 24660 |
. . . . . . . . . . 11
       
                          
            |
167 | 95 | ad5antr 739 |
. . . . . . . . . . 11
       
                          
            |
168 | 99 | ad5antr 739 |
. . . . . . . . . . . 12
       
                          
        |
169 | 123 | ad2antrr 731 |
. . . . . . . . . . . . . 14
           
                 |
170 | 169 | ad2antrr 731 |
. . . . . . . . . . . . 13
       
                          
        |
171 | 99 | necomd 2678 |
. . . . . . . . . . . . . . 15
 

        |
172 | 47 | adantr 467 |
. . . . . . . . . . . . . . 15
 

     
      |
173 | 8, 10, 67, 89, 91, 92, 122, 171, 172 | btwnlng2 24658 |
. . . . . . . . . . . . . 14
 

     
      |
174 | 173 | ad5antr 739 |
. . . . . . . . . . . . 13
       
                          
            |
175 | | simprr 765 |
. . . . . . . . . . . . . 14
       
                          
            |
176 | 8, 9, 10, 150, 155, 157, 170, 175 | tgbtwncom 24525 |
. . . . . . . . . . . . 13
       
                          
            |
177 | 8, 10, 67, 150, 170, 153, 155, 157, 174, 176 | coltr3 24686 |
. . . . . . . . . . . 12
       
                          
            |
178 | 8, 10, 67, 150, 155, 153, 157, 168, 177 | lncom 24660 |
. . . . . . . . . . 11
       
                          
            |
179 | 8, 10, 67, 89, 92, 91, 99 | tglinerflx2 24672 |
. . . . . . . . . . . 12
 

     
      |
180 | 179 | ad5antr 739 |
. . . . . . . . . . 11
       
                          
            |
181 | 8, 10, 67, 150, 152, 153, 155, 153, 156, 166, 167, 178, 180 | tglineinteq 24683 |
. . . . . . . . . 10
       
                          
        |
182 | 8, 9, 10, 150, 159, 157, 152, 164 | tgbtwncom 24525 |
. . . . . . . . . 10
       
                          
            |
183 | 181, 182 | eqeltrrd 2529 |
. . . . . . . . 9
       
                          
            |
184 | 121 | ad2antrr 731 |
. . . . . . . . . 10
           
                 |
185 | 8, 9, 10, 145, 184, 148, 169, 149 | tgbtwncom 24525 |
. . . . . . . . . 10
           
                     |
186 | 24 | ad4antr 737 |
. . . . . . . . . 10
           
                     |
187 | 8, 9, 10, 145, 169, 151, 184, 148, 154, 185, 186 | axtgpasch 24508 |
. . . . . . . . 9
           
               
            |
188 | 183, 187 | r19.29a 2931 |
. . . . . . . 8
           
                     |
189 | 148, 149,
188 | jca32 538 |
. . . . . . 7
           
                
            |
190 | 189 | anasss 652 |
. . . . . 6
          
     
   
                    |
191 | 190 | ex 436 |
. . . . 5
   
                     

    
         |
192 | 191 | reximdv2 2857 |
. . . 4
   
            
         
             |
193 | 144, 192 | mpd 15 |
. . 3
   
           
            |
194 | 109, 193 | pm2.61dan 799 |
. 2
 

      

           |
195 | 79, 194 | pm2.61dan 799 |
1
  
           |