Step | Hyp | Ref
| Expression |
1 | | lnopp2hpgb.c |
. . . . 5
|
2 | 1 | adantr 481 |
. . . 4
|
3 | | lnopp2hpgb.1 |
. . . . 5
|
4 | 3 | adantr 481 |
. . . 4
|
5 | | simpr 477 |
. . . 4
|
6 | | breq2 4657 |
. . . . . 6
|
7 | | breq2 4657 |
. . . . . 6
|
8 | 6, 7 | anbi12d 747 |
. . . . 5
|
9 | 8 | rspcev 3309 |
. . . 4
|
10 | 2, 4, 5, 9 | syl12anc 1324 |
. . 3
|
11 | | ishpg.p |
. . . . 5
|
12 | | ishpg.i |
. . . . 5
Itv |
13 | | ishpg.l |
. . . . 5
LineG |
14 | | ishpg.o |
. . . . 5
|
15 | | ishpg.g |
. . . . 5
TarskiG |
16 | | ishpg.d |
. . . . 5
|
17 | | hpgbr.a |
. . . . 5
|
18 | | hpgbr.b |
. . . . 5
|
19 | 11, 12, 13, 14, 15, 16, 17, 18 | hpgbr 25652 |
. . . 4
hpG
|
20 | 19 | adantr 481 |
. . 3
hpG
|
21 | 10, 20 | mpbird 247 |
. 2
hpG |
22 | | eqid 2622 |
. . . . . . . 8
|
23 | 16 | ad7antr 774 |
. . . . . . . . 9
hpG
|
24 | 23 | ad3antrrr 766 |
. . . . . . . 8
hpG
|
25 | 15 | ad7antr 774 |
. . . . . . . . 9
hpG
TarskiG |
26 | 25 | ad3antrrr 766 |
. . . . . . . 8
hpG
TarskiG |
27 | | eqid 2622 |
. . . . . . . 8
hlG hlG |
28 | 17 | ad3antrrr 766 |
. . . . . . . . . 10
hpG
|
29 | 28 | ad4antr 768 |
. . . . . . . . 9
hpG
|
30 | 29 | ad3antrrr 766 |
. . . . . . . 8
hpG
|
31 | 18 | ad3antrrr 766 |
. . . . . . . . . 10
hpG
|
32 | 31 | ad4antr 768 |
. . . . . . . . 9
hpG
|
33 | 32 | ad3antrrr 766 |
. . . . . . . 8
hpG
|
34 | 1 | ad10antr 780 |
. . . . . . . 8
hpG
|
35 | 3 | ad10antr 780 |
. . . . . . . 8
hpG
|
36 | | simpr 477 |
. . . . . . . 8
hpG
|
37 | | simplr 792 |
. . . . . . . . . . . . . . . 16
hpG
|
38 | 11, 13, 12, 25, 23, 37 | tglnpt 25444 |
. . . . . . . . . . . . . . 15
hpG
|
39 | 38 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
hpG
|
40 | | simp-5r 809 |
. . . . . . . . . . . . . . 15
hpG
|
41 | 11, 22, 12, 14, 13, 24, 26, 30, 34, 35 | oppne1 25633 |
. . . . . . . . . . . . . . 15
hpG
|
42 | | nelne2 2891 |
. . . . . . . . . . . . . . 15
|
43 | 40, 41, 42 | syl2anc 693 |
. . . . . . . . . . . . . 14
hpG
|
44 | 11, 12, 13, 26, 39, 30, 43 | tgelrnln 25525 |
. . . . . . . . . . . . 13
hpG
|
45 | 11, 12, 13, 26, 39, 30, 43 | tglinerflx2 25529 |
. . . . . . . . . . . . . . 15
hpG
|
46 | | nelne1 2890 |
. . . . . . . . . . . . . . 15
|
47 | 45, 41, 46 | syl2anc 693 |
. . . . . . . . . . . . . 14
hpG
|
48 | 47 | necomd 2849 |
. . . . . . . . . . . . 13
hpG
|
49 | | simpllr 799 |
. . . . . . . . . . . . . . 15
hpG
|
50 | | simplrr 801 |
. . . . . . . . . . . . . . 15
hpG
|
51 | 11, 12, 13, 26, 39, 30, 49, 43, 50 | btwnlng1 25514 |
. . . . . . . . . . . . . 14
hpG
|
52 | 36, 51 | elind 3798 |
. . . . . . . . . . . . 13
hpG
|
53 | 11, 12, 13, 26, 39, 30, 43 | tglinerflx1 25528 |
. . . . . . . . . . . . . 14
hpG
|
54 | 40, 53 | elind 3798 |
. . . . . . . . . . . . 13
hpG
|
55 | 11, 12, 13, 26, 24, 44, 48, 52, 54 | tglineineq 25538 |
. . . . . . . . . . . 12
hpG
|
56 | 55, 43 | eqnetrd 2861 |
. . . . . . . . . . 11
hpG
|
57 | 56 | necomd 2849 |
. . . . . . . . . 10
hpG
|
58 | | simp-4r 807 |
. . . . . . . . . . . . . . . 16
hpG
|
59 | 11, 13, 12, 25, 23, 58 | tglnpt 25444 |
. . . . . . . . . . . . . . 15
hpG
|
60 | 59 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
hpG
|
61 | | simp-7r 813 |
. . . . . . . . . . . . . . 15
hpG
|
62 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
hpG
|
63 | 62 | ad4antr 768 |
. . . . . . . . . . . . . . . . 17
hpG
|
64 | 63 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
hpG
|
65 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
hpG
|
66 | 65 | ad7antr 774 |
. . . . . . . . . . . . . . . 16
hpG
|
67 | 11, 22, 12, 14, 13, 24, 26, 33, 64, 66 | oppne1 25633 |
. . . . . . . . . . . . . . 15
hpG
|
68 | | nelne2 2891 |
. . . . . . . . . . . . . . 15
|
69 | 61, 67, 68 | syl2anc 693 |
. . . . . . . . . . . . . 14
hpG
|
70 | 11, 12, 13, 26, 60, 33, 69 | tgelrnln 25525 |
. . . . . . . . . . . . 13
hpG
|
71 | 11, 12, 13, 26, 60, 33, 69 | tglinerflx2 25529 |
. . . . . . . . . . . . . . 15
hpG
|
72 | | nelne1 2890 |
. . . . . . . . . . . . . . 15
|
73 | 71, 67, 72 | syl2anc 693 |
. . . . . . . . . . . . . 14
hpG
|
74 | 73 | necomd 2849 |
. . . . . . . . . . . . 13
hpG
|
75 | | simplrl 800 |
. . . . . . . . . . . . . . 15
hpG
|
76 | 11, 12, 13, 26, 60, 33, 49, 69, 75 | btwnlng1 25514 |
. . . . . . . . . . . . . 14
hpG
|
77 | 36, 76 | elind 3798 |
. . . . . . . . . . . . 13
hpG
|
78 | 11, 12, 13, 26, 60, 33, 69 | tglinerflx1 25528 |
. . . . . . . . . . . . . 14
hpG
|
79 | 61, 78 | elind 3798 |
. . . . . . . . . . . . 13
hpG
|
80 | 11, 12, 13, 26, 24, 70, 74, 77, 79 | tglineineq 25538 |
. . . . . . . . . . . 12
hpG
|
81 | 80, 69 | eqnetrd 2861 |
. . . . . . . . . . 11
hpG
|
82 | 81 | necomd 2849 |
. . . . . . . . . 10
hpG
|
83 | | simprl 794 |
. . . . . . . . . . . . . . 15
hpG
|
84 | 83 | ad7antr 774 |
. . . . . . . . . . . . . 14
hpG
|
85 | 11, 22, 12, 14, 13, 24, 26, 30, 64, 84 | oppne2 25634 |
. . . . . . . . . . . . 13
hpG
|
86 | | nelne2 2891 |
. . . . . . . . . . . . 13
|
87 | 36, 85, 86 | syl2anc 693 |
. . . . . . . . . . . 12
hpG
|
88 | 87 | necomd 2849 |
. . . . . . . . . . 11
hpG
|
89 | | simpllr 799 |
. . . . . . . . . . . . . 14
hpG
|
90 | 89 | ad3antrrr 766 |
. . . . . . . . . . . . 13
hpG
|
91 | 11, 22, 12, 26, 30, 60, 64, 90 | tgbtwncom 25383 |
. . . . . . . . . . . 12
hpG
|
92 | 80, 91 | eqeltrd 2701 |
. . . . . . . . . . 11
hpG
|
93 | | simpr 477 |
. . . . . . . . . . . . . 14
hpG
|
94 | 93 | ad3antrrr 766 |
. . . . . . . . . . . . 13
hpG
|
95 | 11, 22, 12, 26, 33, 39, 64, 94 | tgbtwncom 25383 |
. . . . . . . . . . . 12
hpG
|
96 | 55, 95 | eqeltrd 2701 |
. . . . . . . . . . 11
hpG
|
97 | 11, 12, 26, 64, 49, 30, 33, 88, 92, 96 | tgbtwnconn2 25471 |
. . . . . . . . . 10
hpG
|
98 | 57, 82, 97 | 3jca 1242 |
. . . . . . . . 9
hpG
|
99 | 11, 12, 27, 30, 33, 49, 26 | ishlg 25497 |
. . . . . . . . 9
hpG
hlG
|
100 | 98, 99 | mpbird 247 |
. . . . . . . 8
hpG
hlG |
101 | 11, 22, 12, 14, 13, 24, 26, 27, 30, 33, 34, 35, 36, 100 | opphl 25646 |
. . . . . . 7
hpG
|
102 | 23 | ad3antrrr 766 |
. . . . . . . 8
hpG
|
103 | 25 | ad3antrrr 766 |
. . . . . . . 8
hpG
TarskiG |
104 | | simpllr 799 |
. . . . . . . 8
hpG
|
105 | 32 | ad3antrrr 766 |
. . . . . . . 8
hpG
|
106 | 1 | ad10antr 780 |
. . . . . . . 8
hpG
|
107 | 29 | ad3antrrr 766 |
. . . . . . . . 9
hpG
|
108 | 3 | ad10antr 780 |
. . . . . . . . 9
hpG
|
109 | 37 | ad3antrrr 766 |
. . . . . . . . 9
hpG
|
110 | 38 | ad3antrrr 766 |
. . . . . . . . . 10
hpG
|
111 | | simplrr 801 |
. . . . . . . . . . 11
hpG
|
112 | | simpr 477 |
. . . . . . . . . . . . . 14
hpG
|
113 | | nelne2 2891 |
. . . . . . . . . . . . . 14
|
114 | 109, 112,
113 | syl2anc 693 |
. . . . . . . . . . . . 13
hpG
|
115 | 114 | necomd 2849 |
. . . . . . . . . . . 12
hpG
|
116 | 11, 22, 12, 103, 110, 104, 107, 111, 115 | tgbtwnne 25385 |
. . . . . . . . . . 11
hpG
|
117 | 11, 12, 27, 110, 107, 104, 103, 107, 111, 116, 115 | btwnhl1 25507 |
. . . . . . . . . 10
hpG
hlG |
118 | 11, 12, 27, 104, 107, 110, 103, 117 | hlcomd 25499 |
. . . . . . . . 9
hpG
hlG |
119 | 11, 22, 12, 14, 13, 102, 103, 27, 107, 104, 106, 108, 109, 118 | opphl 25646 |
. . . . . . . 8
hpG
|
120 | 58 | ad3antrrr 766 |
. . . . . . . 8
hpG
|
121 | 59 | ad3antrrr 766 |
. . . . . . . . 9
hpG
|
122 | | simplrl 800 |
. . . . . . . . 9
hpG
|
123 | | nelne2 2891 |
. . . . . . . . . . . 12
|
124 | 120, 112,
123 | syl2anc 693 |
. . . . . . . . . . 11
hpG
|
125 | 124 | necomd 2849 |
. . . . . . . . . 10
hpG
|
126 | 11, 22, 12, 103, 121, 104, 105, 122, 125 | tgbtwnne 25385 |
. . . . . . . . 9
hpG
|
127 | 11, 12, 27, 121, 105, 104, 103, 107, 122, 126, 125 | btwnhl1 25507 |
. . . . . . . 8
hpG
hlG |
128 | 11, 22, 12, 14, 13, 102, 103, 27, 104, 105, 106, 119, 120, 127 | opphl 25646 |
. . . . . . 7
hpG
|
129 | 101, 128 | pm2.61dan 832 |
. . . . . 6
hpG
|
130 | 11, 22, 12, 25, 29, 32, 63, 59, 38, 89, 93 | axtgpasch 25366 |
. . . . . 6
hpG
|
131 | 129, 130 | r19.29a 3078 |
. . . . 5
hpG
|
132 | 11, 22, 12, 14, 31, 62 | islnopp 25631 |
. . . . . . . . 9
hpG
|
133 | 65, 132 | mpbid 222 |
. . . . . . . 8
hpG
|
134 | 133 | simprd 479 |
. . . . . . 7
hpG
|
135 | | eleq1 2689 |
. . . . . . . 8
|
136 | 135 | cbvrexv 3172 |
. . . . . . 7
|
137 | 134, 136 | sylib 208 |
. . . . . 6
hpG
|
138 | 137 | ad2antrr 762 |
. . . . 5
hpG
|
139 | 131, 138 | r19.29a 3078 |
. . . 4
hpG
|
140 | 11, 22, 12, 14, 28, 62 | islnopp 25631 |
. . . . . . 7
hpG
|
141 | 83, 140 | mpbid 222 |
. . . . . 6
hpG
|
142 | 141 | simprd 479 |
. . . . 5
hpG
|
143 | | eleq1 2689 |
. . . . . 6
|
144 | 143 | cbvrexv 3172 |
. . . . 5
|
145 | 142, 144 | sylib 208 |
. . . 4
hpG
|
146 | 139, 145 | r19.29a 3078 |
. . 3
hpG
|
147 | 19 | biimpa 501 |
. . 3
hpG |
148 | 146, 147 | r19.29a 3078 |
. 2
hpG |
149 | 21, 148 | impbida 877 |
1
hpG |