trisegint

Description: A line segment between two sides of a triange intersects a segment crossing from the remaining side to the opposite vertex. Theorem 3.17 of Schwabhauser p. 33. (Contributed by Scott Fenton, 24-Sep-2013)

		Ref	Expression
	Assertion	trisegint	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \to ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩) \to \exists q \in 𝔼 (N) (q Btwn ⟨P, C⟩ \land q Btwn ⟨B, E⟩))$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to N \in ℕ$
2		simpl23	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to C \in 𝔼 (N)$
3		simpl21	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to A \in 𝔼 (N)$
4		simpl31	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to D \in 𝔼 (N)$
5	2 3 4	3jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to (C \in 𝔼 (N) \land A \in 𝔼 (N) \land D \in 𝔼 (N))$
6		simpl32	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to E \in 𝔼 (N)$
7		simpl33	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to P \in 𝔼 (N)$
8	6 7	jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to (E \in 𝔼 (N) \land P \in 𝔼 (N))$
9	1 5 8	3jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to (N \in ℕ \land (C \in 𝔼 (N) \land A \in 𝔼 (N) \land D \in 𝔼 (N)) \land (E \in 𝔼 (N) \land P \in 𝔼 (N)))$
10		simpr2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to E Btwn ⟨D, C⟩$
11		btwncom	$⊢ (N \in ℕ \land (E \in 𝔼 (N) \land D \in 𝔼 (N) \land C \in 𝔼 (N))) \to (E Btwn ⟨D, C⟩ \leftrightarrow E Btwn ⟨C, D⟩)$
12	1 6 4 2 11	syl13anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to (E Btwn ⟨D, C⟩ \leftrightarrow E Btwn ⟨C, D⟩)$
13	10 12	mpbid	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to E Btwn ⟨C, D⟩$
14		simpr3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to P Btwn ⟨A, D⟩$
15	13 14	jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to (E Btwn ⟨C, D⟩ \land P Btwn ⟨A, D⟩)$
16		axpasch	$⊢ (N \in ℕ \land (C \in 𝔼 (N) \land A \in 𝔼 (N) \land D \in 𝔼 (N)) \land (E \in 𝔼 (N) \land P \in 𝔼 (N))) \to ((E Btwn ⟨C, D⟩ \land P Btwn ⟨A, D⟩) \to \exists r \in 𝔼 (N) (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩))$
17	9 15 16	sylc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to \exists r \in 𝔼 (N) (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)$
18		simp1l1	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to N \in ℕ$
19	6	3ad2ant1	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to E \in 𝔼 (N)$
20	2	3ad2ant1	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to C \in 𝔼 (N)$
21	3	3ad2ant1	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to A \in 𝔼 (N)$
22	19 20 21	3jca	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to (E \in 𝔼 (N) \land C \in 𝔼 (N) \land A \in 𝔼 (N))$
23		simp2	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to r \in 𝔼 (N)$
24		simpl22	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to B \in 𝔼 (N)$
25	24	3ad2ant1	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to B \in 𝔼 (N)$
26	23 25	jca	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to (r \in 𝔼 (N) \land B \in 𝔼 (N))$
27	18 22 26	3jca	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to (N \in ℕ \land (E \in 𝔼 (N) \land C \in 𝔼 (N) \land A \in 𝔼 (N)) \land (r \in 𝔼 (N) \land B \in 𝔼 (N)))$
28		simp3l	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to r Btwn ⟨E, A⟩$
29		simp1r1	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to B Btwn ⟨A, C⟩$
30		btwncom	$⊢ (N \in ℕ \land (B \in 𝔼 (N) \land A \in 𝔼 (N) \land C \in 𝔼 (N))) \to (B Btwn ⟨A, C⟩ \leftrightarrow B Btwn ⟨C, A⟩)$
31	18 25 21 20 30	syl13anc	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to (B Btwn ⟨A, C⟩ \leftrightarrow B Btwn ⟨C, A⟩)$
32	29 31	mpbid	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to B Btwn ⟨C, A⟩$
33	28 32	jca	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to (r Btwn ⟨E, A⟩ \land B Btwn ⟨C, A⟩)$
34		axpasch	$⊢ (N \in ℕ \land (E \in 𝔼 (N) \land C \in 𝔼 (N) \land A \in 𝔼 (N)) \land (r \in 𝔼 (N) \land B \in 𝔼 (N))) \to ((r Btwn ⟨E, A⟩ \land B Btwn ⟨C, A⟩) \to \exists q \in 𝔼 (N) (q Btwn ⟨r, C⟩ \land q Btwn ⟨B, E⟩))$
35	27 33 34	sylc	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to \exists q \in 𝔼 (N) (q Btwn ⟨r, C⟩ \land q Btwn ⟨B, E⟩)$
36		simpll1	$⊢ (((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \land q Btwn ⟨r, C⟩) \to ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩))$
37	36 1	syl	$⊢ (((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \land q Btwn ⟨r, C⟩) \to N \in ℕ$
38	36 7	syl	$⊢ (((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \land q Btwn ⟨r, C⟩) \to P \in 𝔼 (N)$
39		simpll2	$⊢ (((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \land q Btwn ⟨r, C⟩) \to r \in 𝔼 (N)$
40	38 39	jca	$⊢ (((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \land q Btwn ⟨r, C⟩) \to (P \in 𝔼 (N) \land r \in 𝔼 (N))$
41		simplr	$⊢ (((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \land q Btwn ⟨r, C⟩) \to q \in 𝔼 (N)$
42	36 2	syl	$⊢ (((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \land q Btwn ⟨r, C⟩) \to C \in 𝔼 (N)$
43	41 42	jca	$⊢ (((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \land q Btwn ⟨r, C⟩) \to (q \in 𝔼 (N) \land C \in 𝔼 (N))$
44	37 40 43	3jca	$⊢ (((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \land q Btwn ⟨r, C⟩) \to (N \in ℕ \land (P \in 𝔼 (N) \land r \in 𝔼 (N)) \land (q \in 𝔼 (N) \land C \in 𝔼 (N)))$
45		simpl3r	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \to r Btwn ⟨P, C⟩$
46	45	anim1i	$⊢ (((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \land q Btwn ⟨r, C⟩) \to (r Btwn ⟨P, C⟩ \land q Btwn ⟨r, C⟩)$
47		btwnexch2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land r \in 𝔼 (N)) \land (q \in 𝔼 (N) \land C \in 𝔼 (N))) \to ((r Btwn ⟨P, C⟩ \land q Btwn ⟨r, C⟩) \to q Btwn ⟨P, C⟩)$
48	44 46 47	sylc	$⊢ (((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \land q Btwn ⟨r, C⟩) \to q Btwn ⟨P, C⟩$
49	48	ex	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \to (q Btwn ⟨r, C⟩ \to q Btwn ⟨P, C⟩)$
50	49	anim1d	$⊢ ((((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \land q \in 𝔼 (N)) \to ((q Btwn ⟨r, C⟩ \land q Btwn ⟨B, E⟩) \to (q Btwn ⟨P, C⟩ \land q Btwn ⟨B, E⟩))$
51	50	reximdva	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to (\exists q \in 𝔼 (N) (q Btwn ⟨r, C⟩ \land q Btwn ⟨B, E⟩) \to \exists q \in 𝔼 (N) (q Btwn ⟨P, C⟩ \land q Btwn ⟨B, E⟩))$
52	35 51	mpd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \land r \in 𝔼 (N) \land (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩)) \to \exists q \in 𝔼 (N) (q Btwn ⟨P, C⟩ \land q Btwn ⟨B, E⟩)$
53	52	rexlimdv3a	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to (\exists r \in 𝔼 (N) (r Btwn ⟨E, A⟩ \land r Btwn ⟨P, C⟩) \to \exists q \in 𝔼 (N) (q Btwn ⟨P, C⟩ \land q Btwn ⟨B, E⟩))$
54	17 53	mpd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \land (B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩)) \to \exists q \in 𝔼 (N) (q Btwn ⟨P, C⟩ \land q Btwn ⟨B, E⟩)$
55	54	ex	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land P \in 𝔼 (N))) \to ((B Btwn ⟨A, C⟩ \land E Btwn ⟨D, C⟩ \land P Btwn ⟨A, D⟩) \to \exists q \in 𝔼 (N) (q Btwn ⟨P, C⟩ \land q Btwn ⟨B, E⟩))$

Metamath Proof Explorer

Theorem trisegint

Proof