Metamath Proof Explorer


Theorem hpgne2

Description: Points on the open half plane cannot lie on its border. (Contributed by Thierry Arnoux, 4-Mar-2020)

Ref Expression
Hypotheses ishpg.p P = Base G
ishpg.i I = Itv G
ishpg.l L = Line 𝒢 G
ishpg.o O = a b | a P D b P D t D t a I b
ishpg.g φ G 𝒢 Tarski
ishpg.d φ D ran L
hpgbr.a φ A P
hpgbr.b φ B P
hpgne1.1 φ A hp 𝒢 G D B
Assertion hpgne2 φ ¬ B D

Proof

Step Hyp Ref Expression
1 ishpg.p P = Base G
2 ishpg.i I = Itv G
3 ishpg.l L = Line 𝒢 G
4 ishpg.o O = a b | a P D b P D t D t a I b
5 ishpg.g φ G 𝒢 Tarski
6 ishpg.d φ D ran L
7 hpgbr.a φ A P
8 hpgbr.b φ B P
9 hpgne1.1 φ A hp 𝒢 G D B
10 eqid dist G = dist G
11 6 ad2antrr φ c P A O c B O c D ran L
12 5 ad2antrr φ c P A O c B O c G 𝒢 Tarski
13 8 ad2antrr φ c P A O c B O c B P
14 simplr φ c P A O c B O c c P
15 simprr φ c P A O c B O c B O c
16 1 10 2 4 3 11 12 13 14 15 oppne1 φ c P A O c B O c ¬ B D
17 1 2 3 4 5 6 7 8 hpgbr φ A hp 𝒢 G D B c P A O c B O c
18 9 17 mpbid φ c P A O c B O c
19 16 18 r19.29a φ ¬ B D