qextltlem

Description: Lemma for qextlt and qextle . (Contributed by Mario Carneiro, 3-Oct-2014)

		Ref	Expression
	Assertion	qextltlem	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to \exists x \in ℚ (\neg (x < A \leftrightarrow x < B) \land \neg (x \leq A \leftrightarrow x \leq B)))$

Proof

Step	Hyp	Ref	Expression
1		qbtwnxr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A < B) \to \exists x \in ℚ (A < x \land x < B)$
2	1	3expia	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to \exists x \in ℚ (A < x \land x < B))$
3		simprl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to A < x$
4		simplll	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to A \in ℝ^{*}$
5		qre	$⊢ x \in ℚ \to x \in ℝ$
6	5	rexrd	$⊢ x \in ℚ \to x \in ℝ^{*}$
7	6	ad2antlr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to x \in ℝ^{*}$
8		xrltnle	$⊢ (A \in ℝ^{} \land x \in ℝ^{}) \to (A < x \leftrightarrow \neg x \leq A)$
9	4 7 8	syl2anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to (A < x \leftrightarrow \neg x \leq A)$
10	3 9	mpbid	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to \neg x \leq A$
11		xrltle	$⊢ (x \in ℝ^{} \land A \in ℝ^{}) \to (x < A \to x \leq A)$
12	7 4 11	syl2anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to (x < A \to x \leq A)$
13	10 12	mtod	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to \neg x < A$
14		simprr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to x < B$
15	13 14	2thd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to (\neg x < A \leftrightarrow x < B)$
16		nbbn	$⊢ (\neg x < A \leftrightarrow x < B) \leftrightarrow \neg (x < A \leftrightarrow x < B)$
17	15 16	sylib	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to \neg (x < A \leftrightarrow x < B)$
18		simpllr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to B \in ℝ^{*}$
19	7 18 14	xrltled	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to x \leq B$
20	10 19	2thd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to (\neg x \leq A \leftrightarrow x \leq B)$
21		nbbn	$⊢ (\neg x \leq A \leftrightarrow x \leq B) \leftrightarrow \neg (x \leq A \leftrightarrow x \leq B)$
22	20 21	sylib	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to \neg (x \leq A \leftrightarrow x \leq B)$
23	17 22	jca	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \land (A < x \land x < B)) \to (\neg (x < A \leftrightarrow x < B) \land \neg (x \leq A \leftrightarrow x \leq B))$
24	23	ex	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land x \in ℚ) \to ((A < x \land x < B) \to (\neg (x < A \leftrightarrow x < B) \land \neg (x \leq A \leftrightarrow x \leq B)))$
25	24	reximdva	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (\exists x \in ℚ (A < x \land x < B) \to \exists x \in ℚ (\neg (x < A \leftrightarrow x < B) \land \neg (x \leq A \leftrightarrow x \leq B)))$
26	2 25	syld	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A < B \to \exists x \in ℚ (\neg (x < A \leftrightarrow x < B) \land \neg (x \leq A \leftrightarrow x \leq B)))$

Metamath Proof Explorer

Theorem qextltlem

Proof