seglelin

Description: Linearity law for segment comparison. Theorem 5.10 of Schwabhauser p. 42. (Contributed by Scott Fenton, 14-Oct-2013)

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

Proof

Step	Hyp	Ref	Expression
1		segcon2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to \exists x \in 𝔼 (N) ((B Btwn ⟨A, x⟩ \lor x Btwn ⟨A, B⟩) \land ⟨A, x⟩ Cgr ⟨C, D⟩)$
2		andir	$⊢ ((B Btwn ⟨A, x⟩ \lor x Btwn ⟨A, B⟩) \land ⟨A, x⟩ Cgr ⟨C, D⟩) \leftrightarrow ((B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \lor (x Btwn ⟨A, B⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩))$
3		simpl1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to N \in ℕ$
4		simpl2l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to A \in 𝔼 (N)$
5		simpr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to x \in 𝔼 (N)$
6		simpl3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to (C \in 𝔼 (N) \land D \in 𝔼 (N))$
7		cgrcom	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land x \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨A, x⟩ Cgr ⟨C, D⟩ \leftrightarrow ⟨C, D⟩ Cgr ⟨A, x⟩)$
8	3 4 5 6 7	syl121anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to (⟨A, x⟩ Cgr ⟨C, D⟩ \leftrightarrow ⟨C, D⟩ Cgr ⟨A, x⟩)$
9	8	anbi2d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to ((x Btwn ⟨A, B⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \leftrightarrow (x Btwn ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩))$
10	9	orbi2d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to (((B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \lor (x Btwn ⟨A, B⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩)) \leftrightarrow ((B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \lor (x Btwn ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩)))$
11	2 10	bitrid	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \land x \in 𝔼 (N)) \to (((B Btwn ⟨A, x⟩ \lor x Btwn ⟨A, B⟩) \land ⟨A, x⟩ Cgr ⟨C, D⟩) \leftrightarrow ((B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \lor (x Btwn ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩)))$
12	11	rexbidva	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (\exists x \in 𝔼 (N) ((B Btwn ⟨A, x⟩ \lor x Btwn ⟨A, B⟩) \land ⟨A, x⟩ Cgr ⟨C, D⟩) \leftrightarrow \exists x \in 𝔼 (N) ((B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \lor (x Btwn ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩)))$
13		brsegle2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \leftrightarrow \exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩))$
14		brsegle	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land D \in 𝔼 (N)) \land (A \in 𝔼 (N) \land B \in 𝔼 (N))) \to (⟨C, D⟩ {Seg}_{\leq} ⟨A, B⟩ \leftrightarrow \exists x \in 𝔼 (N) (x Btwn ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩))$
15	14	3com23	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨C, D⟩ {Seg}_{\leq} ⟨A, B⟩ \leftrightarrow \exists x \in 𝔼 (N) (x Btwn ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩))$
16	13 15	orbi12d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \lor ⟨C, D⟩ {Seg}_{\leq} ⟨A, B⟩) \leftrightarrow (\exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \lor \exists x \in 𝔼 (N) (x Btwn ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩)))$
17		r19.43	$⊢ \exists x \in 𝔼 (N) ((B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \lor (x Btwn ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩)) \leftrightarrow (\exists x \in 𝔼 (N) (B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \lor \exists x \in 𝔼 (N) (x Btwn ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩))$
18	16 17	bitr4di	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to ((⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \lor ⟨C, D⟩ {Seg}_{\leq} ⟨A, B⟩) \leftrightarrow \exists x \in 𝔼 (N) ((B Btwn ⟨A, x⟩ \land ⟨A, x⟩ Cgr ⟨C, D⟩) \lor (x Btwn ⟨A, B⟩ \land ⟨C, D⟩ Cgr ⟨A, x⟩)))$
19	12 18	bitr4d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (\exists x \in 𝔼 (N) ((B Btwn ⟨A, x⟩ \lor x Btwn ⟨A, B⟩) \land ⟨A, x⟩ Cgr ⟨C, D⟩) \leftrightarrow (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \lor ⟨C, D⟩ {Seg}_{\leq} ⟨A, B⟩))$
20	1 19	mpbid	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land D \in 𝔼 (N))) \to (⟨A, B⟩ {Seg}_{\leq} ⟨C, D⟩ \lor ⟨C, D⟩ {Seg}_{\leq} ⟨A, B⟩)$

Metamath Proof Explorer

Theorem seglelin

Proof