Metamath Proof Explorer

Theorem tgextancd

Description: The target-side non-collinearity of the exterior angle. Line C D is line C B -- C lies between B and D , and C =/= D -- so A is off it exactly because the triangle is non-degenerate. This is acopyeu 's acopy.2 frame hypothesis in tgextancgra , and it is what excludes isinag 's x = C branch in tgextahp . (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses tgextancd.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgextancd.m ⊢ − = ( dist ‘ 𝐺 )
tgextancd.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgextancd.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tgextancd.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgextancd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgextancd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgextancd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgextancd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgextancd.ext ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
tgextancd.ncol ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
tgextancd.ne ⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
Assertion tgextancd ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 tgextancd.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgextancd.m ⊢ − = ( dist ‘ 𝐺 )
3 tgextancd.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgextancd.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 tgextancd.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 tgextancd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 tgextancd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 tgextancd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 tgextancd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 tgextancd.ext ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
11 tgextancd.ncol ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
12 tgextancd.ne ⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
13 1 4 3 5 7 8 6 11 ncolcom ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∨ 𝐶 = 𝐵 ) )
14 ioran ⊢ ( ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∨ 𝐶 = 𝐵 ) ↔ ( ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∧ ¬ 𝐶 = 𝐵 ) )
15 13 14 sylib ⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∧ ¬ 𝐶 = 𝐵 ) )
16 15 simpld ⊢ ( 𝜑 → ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) )
17 15 simprd ⊢ ( 𝜑 → ¬ 𝐶 = 𝐵 )
18 17 neqned ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
19 12 necomd ⊢ ( 𝜑 → 𝐷 ≠ 𝐶 )
20 1 2 3 5 7 8 9 10 tgbtwncom ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) )
21 1 4 3 5 8 7 9 20 btwncolg2 ⊢ ( 𝜑 → ( 𝐷 ∈ ( 𝐶 𝐿 𝐵 ) ∨ 𝐶 = 𝐵 ) )
22 21 17 olcnd ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 𝐿 𝐵 ) )
23 1 3 4 5 8 7 18 9 19 22 tglineelsb2 ⊢ ( 𝜑 → ( 𝐶 𝐿 𝐵 ) = ( 𝐶 𝐿 𝐷 ) )
24 23 eleq2d ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ↔ 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ) )
25 16 24 mtbid ⊢ ( 𝜑 → ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) )
26 12 neneqd ⊢ ( 𝜑 → ¬ 𝐶 = 𝐷 )
27 25 26 jca ⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∧ ¬ 𝐶 = 𝐷 ) )
28 ioran ⊢ ( ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) ↔ ( ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∧ ¬ 𝐶 = 𝐷 ) )
29 27 28 sylibr ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )