xralrple

Description: Show that A is less than B by showing that there is no positive bound on the difference. (Contributed by Mario Carneiro, 12-Jun-2014)

		Ref	Expression
	Assertion	xralrple	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A \leq B \leftrightarrow \forall x \in ℝ^{+} A \leq B + x)$

Proof

Step	Hyp	Ref	Expression
1		rpge0	$⊢ x \in ℝ^{+} \to 0 \leq x$
2	1	adantl	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land x \in ℝ^{+}) \to 0 \leq x$
3		simplr	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land x \in ℝ^{+}) \to B \in ℝ$
4		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
5	4	adantl	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land x \in ℝ^{+}) \to x \in ℝ$
6	3 5	addge01d	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land x \in ℝ^{+}) \to (0 \leq x \leftrightarrow B \leq B + x)$
7	2 6	mpbid	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land x \in ℝ^{+}) \to B \leq B + x$
8		simpll	$⊢ ((A \in ℝ^{} \land B \in ℝ) \land x \in ℝ^{+}) \to A \in ℝ^{}$
9	3	rexrd	$⊢ ((A \in ℝ^{} \land B \in ℝ) \land x \in ℝ^{+}) \to B \in ℝ^{}$
10	3 5	readdcld	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land x \in ℝ^{+}) \to B + x \in ℝ$
11	10	rexrd	$⊢ ((A \in ℝ^{} \land B \in ℝ) \land x \in ℝ^{+}) \to B + x \in ℝ^{}$
12		xrletr	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land B + x \in ℝ^{*}) \to ((A \leq B \land B \leq B + x) \to A \leq B + x)$
13	8 9 11 12	syl3anc	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land x \in ℝ^{+}) \to ((A \leq B \land B \leq B + x) \to A \leq B + x)$
14	7 13	mpan2d	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land x \in ℝ^{+}) \to (A \leq B \to A \leq B + x)$
15	14	ralrimdva	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A \leq B \to \forall x \in ℝ^{+} A \leq B + x)$
16		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
17	16	adantl	$⊢ (A \in ℝ^{} \land B \in ℝ) \to B \in ℝ^{}$
18		simpl	$⊢ (A \in ℝ^{} \land B \in ℝ) \to A \in ℝ^{}$
19		qbtwnxr	$⊢ (B \in ℝ^{} \land A \in ℝ^{} \land B < A) \to \exists y \in ℚ (B < y \land y < A)$
20	19	3expia	$⊢ (B \in ℝ^{} \land A \in ℝ^{}) \to (B < A \to \exists y \in ℚ (B < y \land y < A))$
21	17 18 20	syl2anc	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (B < A \to \exists y \in ℚ (B < y \land y < A))$
22		simprrl	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to B < y$
23		simplr	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to B \in ℝ$
24		qre	$⊢ y \in ℚ \to y \in ℝ$
25	24	ad2antrl	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to y \in ℝ$
26		difrp	$⊢ (B \in ℝ \land y \in ℝ) \to (B < y \leftrightarrow y - B \in ℝ^{+})$
27	23 25 26	syl2anc	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to (B < y \leftrightarrow y - B \in ℝ^{+})$
28	22 27	mpbid	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to y - B \in ℝ^{+}$
29		simprrr	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to y < A$
30	25	rexrd	$⊢ ((A \in ℝ^{} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to y \in ℝ^{}$
31		simpll	$⊢ ((A \in ℝ^{} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to A \in ℝ^{}$
32		xrltnle	$⊢ (y \in ℝ^{} \land A \in ℝ^{}) \to (y < A \leftrightarrow \neg A \leq y)$
33	30 31 32	syl2anc	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to (y < A \leftrightarrow \neg A \leq y)$
34	29 33	mpbid	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to \neg A \leq y$
35	23	recnd	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to B \in ℂ$
36	25	recnd	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to y \in ℂ$
37	35 36	pncan3d	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to B + y - B = y$
38	37	breq2d	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to (A \leq B + y - B \leftrightarrow A \leq y)$
39	34 38	mtbird	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to \neg A \leq B + y - B$
40		oveq2	$⊢ x = y - B \to B + x = B + y - B$
41	40	breq2d	$⊢ x = y - B \to (A \leq B + x \leftrightarrow A \leq B + y - B)$
42	41	notbid	$⊢ x = y - B \to (\neg A \leq B + x \leftrightarrow \neg A \leq B + y - B)$
43	42	rspcev	$⊢ (y - B \in ℝ^{+} \land \neg A \leq B + y - B) \to \exists x \in ℝ^{+} \neg A \leq B + x$
44	28 39 43	syl2anc	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to \exists x \in ℝ^{+} \neg A \leq B + x$
45		rexnal	$⊢ \exists x \in ℝ^{+} \neg A \leq B + x \leftrightarrow \neg \forall x \in ℝ^{+} A \leq B + x$
46	44 45	sylib	$⊢ ((A \in ℝ^{*} \land B \in ℝ) \land (y \in ℚ \land (B < y \land y < A))) \to \neg \forall x \in ℝ^{+} A \leq B + x$
47	46	rexlimdvaa	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (\exists y \in ℚ (B < y \land y < A) \to \neg \forall x \in ℝ^{+} A \leq B + x)$
48	21 47	syld	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (B < A \to \neg \forall x \in ℝ^{+} A \leq B + x)$
49	48	con2d	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (\forall x \in ℝ^{+} A \leq B + x \to \neg B < A)$
50		xrlenlt	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A \leq B \leftrightarrow \neg B < A)$
51	16 50	sylan2	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A \leq B \leftrightarrow \neg B < A)$
52	49 51	sylibrd	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (\forall x \in ℝ^{+} A \leq B + x \to A \leq B)$
53	15 52	impbid	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A \leq B \leftrightarrow \forall x \in ℝ^{+} A \leq B + x)$

Metamath Proof Explorer

Theorem xralrple

Proof