Theorem tgbtwnne

Description: Betweenness and inequality. (Contributed by Thierry Arnoux, 1-Dec-2019)

	Ref	Expression
Hypotheses	tkgeom.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tkgeom.d	⊢ − = ( dist ‘ 𝐺 )
	tkgeom.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tkgeom.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgbtwntriv2.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgbtwntriv2.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	tgbtwncomb.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	tgbtwnne.1	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
	tgbtwnne.2	⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
Assertion	tgbtwnne	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		tkgeom.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tkgeom.d	⊢ − = ( dist ‘ 𝐺 )
3		tkgeom.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tkgeom.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tgbtwntriv2.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		tgbtwntriv2.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		tgbtwncomb.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		tgbtwnne.1	⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
9		tgbtwnne.2	⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
10	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐺 ∈ TarskiG )
11	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 ∈ 𝑃 )
12	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐵 ∈ 𝑃 )
13	8	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
14		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 = 𝐶 )
15	14	oveq2d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐴 𝐼 𝐴 ) = ( 𝐴 𝐼 𝐶 ) )
16	13 15	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐵 ∈ ( 𝐴 𝐼 𝐴 ) )
17	1 2 3 10 11 12 16	axtgbtwnid	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 = 𝐵 )
18	17	eqcomd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐵 = 𝐴 )
19	9	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐵 ≠ 𝐴 )
20	19	neneqd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ¬ 𝐵 = 𝐴 )
21	18 20	pm2.65da	⊢ ( 𝜑 → ¬ 𝐴 = 𝐶 )
22	21	neqned	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )