Metamath Proof Explorer

Theorem btwnsegle

Description: If B falls between A and C , then A B is no longer than A C . (Contributed by Scott Fenton, 16-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	btwnsegle	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (B Btwn ⟨A, C⟩ \to ⟨A, B⟩ {Seg}_{\leq} ⟨A, C⟩)$

Proof

Step	Hyp	Ref	Expression
1		simplr2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \land B Btwn ⟨A, C⟩) \to B \in 𝔼 (N)$
2		simpr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \land B Btwn ⟨A, C⟩) \to B Btwn ⟨A, C⟩$
3		simpl	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \to N \in ℕ$
4		simpr1	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \to A \in 𝔼 (N)$
5		simpr2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \to B \in 𝔼 (N)$
6	3 4 5	cgrrflxd	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \to ⟨A, B⟩ Cgr ⟨A, B⟩$
7	6	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \land B Btwn ⟨A, C⟩) \to ⟨A, B⟩ Cgr ⟨A, B⟩$
8		breq1	$⊢ x = B \to (x Btwn ⟨A, C⟩ \leftrightarrow B Btwn ⟨A, C⟩)$
9		opeq2	$⊢ x = B \to ⟨A, x⟩ = ⟨A, B⟩$
10	9	breq2d	$⊢ x = B \to (⟨A, B⟩ Cgr ⟨A, x⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨A, B⟩)$
11	8 10	anbi12d	$⊢ x = B \to ((x Btwn ⟨A, C⟩ \land ⟨A, B⟩ Cgr ⟨A, x⟩) \leftrightarrow (B Btwn ⟨A, C⟩ \land ⟨A, B⟩ Cgr ⟨A, B⟩))$
12	11	rspcev	$⊢ (B \in 𝔼 (N) \land (B Btwn ⟨A, C⟩ \land ⟨A, B⟩ Cgr ⟨A, B⟩)) \to \exists x \in 𝔼 (N) (x Btwn ⟨A, C⟩ \land ⟨A, B⟩ Cgr ⟨A, x⟩)$
13	1 2 7 12	syl12anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \land B Btwn ⟨A, C⟩) \to \exists x \in 𝔼 (N) (x Btwn ⟨A, C⟩ \land ⟨A, B⟩ Cgr ⟨A, x⟩)$
14		simpr3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \to C \in 𝔼 (N)$
15		brsegle	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (A \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨A, C⟩ \leftrightarrow \exists x \in 𝔼 (N) (x Btwn ⟨A, C⟩ \land ⟨A, B⟩ Cgr ⟨A, x⟩))$
16	3 4 5 4 14 15	syl122anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨A, C⟩ \leftrightarrow \exists x \in 𝔼 (N) (x Btwn ⟨A, C⟩ \land ⟨A, B⟩ Cgr ⟨A, x⟩))$
17	16	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \land B Btwn ⟨A, C⟩) \to (⟨A, B⟩ {Seg}_{\leq} ⟨A, C⟩ \leftrightarrow \exists x \in 𝔼 (N) (x Btwn ⟨A, C⟩ \land ⟨A, B⟩ Cgr ⟨A, x⟩))$
18	13 17	mpbird	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \land B Btwn ⟨A, C⟩) \to ⟨A, B⟩ {Seg}_{\leq} ⟨A, C⟩$
19	18	ex	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (B Btwn ⟨A, C⟩ \to ⟨A, B⟩ {Seg}_{\leq} ⟨A, C⟩)$