segcon2

Description: Generalization of axsegcon . This time, we generate an endpoint for a segment on the ray Q A congruent to B C and starting at Q , as opposed to axsegcon , where the segment starts at A (Contributed by Scott Fenton, 14-Oct-2013) Remove unneeded inequality. (Revised by Scott Fenton, 15-Oct-2013)

		Ref	Expression
	Assertion	segcon2	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to \exists x \in 𝔼 (N) ((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩)$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ A = Q \to (A Btwn ⟨Q, x⟩ \leftrightarrow Q Btwn ⟨Q, x⟩)$
2	1	orbi1d	$⊢ A = Q \to ((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \leftrightarrow (Q Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩))$
3	2	anbi1d	$⊢ A = Q \to (((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩) \leftrightarrow ((Q Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩))$
4	3	rexbidv	$⊢ A = Q \to (\exists x \in 𝔼 (N) ((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩) \leftrightarrow \exists x \in 𝔼 (N) ((Q Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩))$
5		simp1	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to N \in ℕ$
6		simp2	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (Q \in 𝔼 (N) \land A \in 𝔼 (N))$
7	6	ancomd	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (A \in 𝔼 (N) \land Q \in 𝔼 (N))$
8		axsegcon	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land Q \in 𝔼 (N)) \land (A \in 𝔼 (N) \land Q \in 𝔼 (N))) \to \exists a \in 𝔼 (N) (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩)$
9	5 7 7 8	syl3anc	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to \exists a \in 𝔼 (N) (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩)$
10	9	adantr	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land A \neq Q) \to \exists a \in 𝔼 (N) (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩)$
11		simpl1	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land a \in 𝔼 (N)) \to N \in ℕ$
12		simpr	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land a \in 𝔼 (N)) \to a \in 𝔼 (N)$
13		simpl2l	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land a \in 𝔼 (N)) \to Q \in 𝔼 (N)$
14		simpl3	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land a \in 𝔼 (N)) \to (B \in 𝔼 (N) \land C \in 𝔼 (N))$
15		axsegcon	$⊢ (N \in ℕ \land (a \in 𝔼 (N) \land Q \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to \exists x \in 𝔼 (N) (Q Btwn ⟨a, x⟩ \land ⟨Q, x⟩ Cgr ⟨B, C⟩)$
16	11 12 13 14 15	syl121anc	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land a \in 𝔼 (N)) \to \exists x \in 𝔼 (N) (Q Btwn ⟨a, x⟩ \land ⟨Q, x⟩ Cgr ⟨B, C⟩)$
17	16	adantr	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land a \in 𝔼 (N)) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩))) \to \exists x \in 𝔼 (N) (Q Btwn ⟨a, x⟩ \land ⟨Q, x⟩ Cgr ⟨B, C⟩)$
18		anass	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land a \in 𝔼 (N)) \land x \in 𝔼 (N)) \leftrightarrow ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N)))$
19		df-3an	$⊢ (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \land Q Btwn ⟨a, x⟩) \leftrightarrow ((A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩)) \land Q Btwn ⟨a, x⟩)$
20		simpr1	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \land Q Btwn ⟨a, x⟩)) \to A \neq Q$
21		simpr2r	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \land Q Btwn ⟨a, x⟩)) \to ⟨Q, a⟩ Cgr ⟨A, Q⟩$
22		simpl1	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \to N \in ℕ$
23		simpl2l	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \to Q \in 𝔼 (N)$
24		simprl	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \to a \in 𝔼 (N)$
25		simpl2r	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \to A \in 𝔼 (N)$
26		cgrdegen	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land a \in 𝔼 (N)) \land (A \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (⟨Q, a⟩ Cgr ⟨A, Q⟩ \to (Q = a \leftrightarrow A = Q))$
27	22 23 24 25 23 26	syl122anc	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \to (⟨Q, a⟩ Cgr ⟨A, Q⟩ \to (Q = a \leftrightarrow A = Q))$
28	27	adantr	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \land Q Btwn ⟨a, x⟩)) \to (⟨Q, a⟩ Cgr ⟨A, Q⟩ \to (Q = a \leftrightarrow A = Q))$
29	21 28	mpd	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \land Q Btwn ⟨a, x⟩)) \to (Q = a \leftrightarrow A = Q)$
30	29	necon3bid	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \land Q Btwn ⟨a, x⟩)) \to (Q \neq a \leftrightarrow A \neq Q)$
31	20 30	mpbird	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \land Q Btwn ⟨a, x⟩)) \to Q \neq a$
32	31	necomd	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \land Q Btwn ⟨a, x⟩)) \to a \neq Q$
33		simpr2l	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \land Q Btwn ⟨a, x⟩)) \to Q Btwn ⟨A, a⟩$
34	22 23 25 24 33	btwncomand	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \land Q Btwn ⟨a, x⟩)) \to Q Btwn ⟨a, A⟩$
35		simpr3	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \land Q Btwn ⟨a, x⟩)) \to Q Btwn ⟨a, x⟩$
36		simprr	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \to x \in 𝔼 (N)$
37		btwnconn2	$⊢ (N \in ℕ \land (a \in 𝔼 (N) \land Q \in 𝔼 (N)) \land (A \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((a \neq Q \land Q Btwn ⟨a, A⟩ \land Q Btwn ⟨a, x⟩) \to (A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩))$
38	22 24 23 25 36 37	syl122anc	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \to ((a \neq Q \land Q Btwn ⟨a, A⟩ \land Q Btwn ⟨a, x⟩) \to (A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩))$
39	38	adantr	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \land Q Btwn ⟨a, x⟩)) \to ((a \neq Q \land Q Btwn ⟨a, A⟩ \land Q Btwn ⟨a, x⟩) \to (A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩))$
40	32 34 35 39	mp3and	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \land Q Btwn ⟨a, x⟩)) \to (A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩)$
41	19 40	sylan2br	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land ((A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩)) \land Q Btwn ⟨a, x⟩)) \to (A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩)$
42	41	expr	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩))) \to (Q Btwn ⟨a, x⟩ \to (A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩))$
43	42	anim1d	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (a \in 𝔼 (N) \land x \in 𝔼 (N))) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩))) \to ((Q Btwn ⟨a, x⟩ \land ⟨Q, x⟩ Cgr ⟨B, C⟩) \to ((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩))$
44	18 43	sylanb	$⊢ ((((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land a \in 𝔼 (N)) \land x \in 𝔼 (N)) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩))) \to ((Q Btwn ⟨a, x⟩ \land ⟨Q, x⟩ Cgr ⟨B, C⟩) \to ((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩))$
45	44	an32s	$⊢ ((((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land a \in 𝔼 (N)) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩))) \land x \in 𝔼 (N)) \to ((Q Btwn ⟨a, x⟩ \land ⟨Q, x⟩ Cgr ⟨B, C⟩) \to ((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩))$
46	45	reximdva	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land a \in 𝔼 (N)) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩))) \to (\exists x \in 𝔼 (N) (Q Btwn ⟨a, x⟩ \land ⟨Q, x⟩ Cgr ⟨B, C⟩) \to \exists x \in 𝔼 (N) ((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩))$
47	17 46	mpd	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land a \in 𝔼 (N)) \land (A \neq Q \land (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩))) \to \exists x \in 𝔼 (N) ((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩)$
48	47	expr	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land a \in 𝔼 (N)) \land A \neq Q) \to ((Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \to \exists x \in 𝔼 (N) ((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩))$
49	48	an32s	$⊢ (((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land A \neq Q) \land a \in 𝔼 (N)) \to ((Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \to \exists x \in 𝔼 (N) ((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩))$
50	49	rexlimdva	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land A \neq Q) \to (\exists a \in 𝔼 (N) (Q Btwn ⟨A, a⟩ \land ⟨Q, a⟩ Cgr ⟨A, Q⟩) \to \exists x \in 𝔼 (N) ((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩))$
51	10 50	mpd	$⊢ ((N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land A \neq Q) \to \exists x \in 𝔼 (N) ((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩)$
52		simp2l	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to Q \in 𝔼 (N)$
53		simp3	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (B \in 𝔼 (N) \land C \in 𝔼 (N))$
54		axsegcon	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land Q \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to \exists x \in 𝔼 (N) (Q Btwn ⟨Q, x⟩ \land ⟨Q, x⟩ Cgr ⟨B, C⟩)$
55	5 52 52 53 54	syl121anc	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to \exists x \in 𝔼 (N) (Q Btwn ⟨Q, x⟩ \land ⟨Q, x⟩ Cgr ⟨B, C⟩)$
56		orc	$⊢ Q Btwn ⟨Q, x⟩ \to (Q Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩)$
57	56	anim1i	$⊢ (Q Btwn ⟨Q, x⟩ \land ⟨Q, x⟩ Cgr ⟨B, C⟩) \to ((Q Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩)$
58	57	reximi	$⊢ \exists x \in 𝔼 (N) (Q Btwn ⟨Q, x⟩ \land ⟨Q, x⟩ Cgr ⟨B, C⟩) \to \exists x \in 𝔼 (N) ((Q Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩)$
59	55 58	syl	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to \exists x \in 𝔼 (N) ((Q Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩)$
60	4 51 59	pm2.61ne	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land A \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to \exists x \in 𝔼 (N) ((A Btwn ⟨Q, x⟩ \lor x Btwn ⟨Q, A⟩) \land ⟨Q, x⟩ Cgr ⟨B, C⟩)$

Metamath Proof Explorer

Theorem segcon2

Proof