xralrple3

Description: Show that A is less than B by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	xralrple3.a	$⊢ φ \to A \in ℝ^{*}$
	xralrple3.b	$⊢ φ \to B \in ℝ$
	xralrple3.c	$⊢ φ \to C \in ℝ$
	xralrple3.g	$⊢ φ \to 0 \leq C$
Assertion	xralrple3	$⊢ φ \to (A \leq B \leftrightarrow \forall x \in ℝ^{+} A \leq B + C x)$

Proof

Step	Hyp	Ref	Expression
1		xralrple3.a	$⊢ φ \to A \in ℝ^{*}$
2		xralrple3.b	$⊢ φ \to B \in ℝ$
3		xralrple3.c	$⊢ φ \to C \in ℝ$
4		xralrple3.g	$⊢ φ \to 0 \leq C$
5	1	ad2antrr	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to A \in ℝ^{*}$
6	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
7	6	ad2antrr	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to B \in ℝ^{*}$
8	2	ad2antrr	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to B \in ℝ$
9	3	ad2antrr	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to C \in ℝ$
10		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
11	10	adantl	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to x \in ℝ$
12	9 11	remulcld	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to C x \in ℝ$
13	8 12	readdcld	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to B + C x \in ℝ$
14	13	rexrd	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to B + C x \in ℝ^{*}$
15		simplr	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to A \leq B$
16	3	adantr	$⊢ (φ \land x \in ℝ^{+}) \to C \in ℝ$
17	10	adantl	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ$
18	4	adantr	$⊢ (φ \land x \in ℝ^{+}) \to 0 \leq C$
19		rpge0	$⊢ x \in ℝ^{+} \to 0 \leq x$
20	19	adantl	$⊢ (φ \land x \in ℝ^{+}) \to 0 \leq x$
21	16 17 18 20	mulge0d	$⊢ (φ \land x \in ℝ^{+}) \to 0 \leq C x$
22	2	adantr	$⊢ (φ \land x \in ℝ^{+}) \to B \in ℝ$
23	16 17	remulcld	$⊢ (φ \land x \in ℝ^{+}) \to C x \in ℝ$
24	22 23	addge01d	$⊢ (φ \land x \in ℝ^{+}) \to (0 \leq C x \leftrightarrow B \leq B + C x)$
25	21 24	mpbid	$⊢ (φ \land x \in ℝ^{+}) \to B \leq B + C x$
26	25	adantlr	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to B \leq B + C x$
27	5 7 14 15 26	xrletrd	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to A \leq B + C x$
28	27	ralrimiva	$⊢ (φ \land A \leq B) \to \forall x \in ℝ^{+} A \leq B + C x$
29	28	ex	$⊢ φ \to (A \leq B \to \forall x \in ℝ^{+} A \leq B + C x)$
30		1rp	$⊢ 1 \in ℝ^{+}$
31		oveq2	$⊢ x = 1 \to C x = C \cdot 1$
32	31	oveq2d	$⊢ x = 1 \to B + C x = B + C \cdot 1$
33	32	breq2d	$⊢ x = 1 \to (A \leq B + C x \leftrightarrow A \leq B + C \cdot 1)$
34	33	rspcva	$⊢ (1 \in ℝ^{+} \land \forall x \in ℝ^{+} A \leq B + C x) \to A \leq B + C \cdot 1$
35	30 34	mpan	$⊢ \forall x \in ℝ^{+} A \leq B + C x \to A \leq B + C \cdot 1$
36	35	ad2antlr	$⊢ ((φ \land \forall x \in ℝ^{+} A \leq B + C x) \land C = 0) \to A \leq B + C \cdot 1$
37		oveq1	$⊢ C = 0 \to C \cdot 1 = 0 \cdot 1$
38		0cn	$⊢ 0 \in ℂ$
39	38	mulid1i	$⊢ 0 \cdot 1 = 0$
40	39	a1i	$⊢ C = 0 \to 0 \cdot 1 = 0$
41	37 40	eqtrd	$⊢ C = 0 \to C \cdot 1 = 0$
42	41	oveq2d	$⊢ C = 0 \to B + C \cdot 1 = B + 0$
43	42	adantl	$⊢ (φ \land C = 0) \to B + C \cdot 1 = B + 0$
44	2	recnd	$⊢ φ \to B \in ℂ$
45	44	adantr	$⊢ (φ \land C = 0) \to B \in ℂ$
46	45	addid1d	$⊢ (φ \land C = 0) \to B + 0 = B$
47	43 46	eqtrd	$⊢ (φ \land C = 0) \to B + C \cdot 1 = B$
48	47	adantlr	$⊢ ((φ \land \forall x \in ℝ^{+} A \leq B + C x) \land C = 0) \to B + C \cdot 1 = B$
49	36 48	breqtrd	$⊢ ((φ \land \forall x \in ℝ^{+} A \leq B + C x) \land C = 0) \to A \leq B$
50		neqne	$⊢ \neg C = 0 \to C \neq 0$
51	50	adantl	$⊢ (φ \land \neg C = 0) \to C \neq 0$
52	3	adantr	$⊢ (φ \land C \neq 0) \to C \in ℝ$
53		0red	$⊢ (φ \land C \neq 0) \to 0 \in ℝ$
54	4	adantr	$⊢ (φ \land C \neq 0) \to 0 \leq C$
55		simpr	$⊢ (φ \land C \neq 0) \to C \neq 0$
56	53 52 54 55	leneltd	$⊢ (φ \land C \neq 0) \to 0 < C$
57	52 56	elrpd	$⊢ (φ \land C \neq 0) \to C \in ℝ^{+}$
58	51 57	syldan	$⊢ (φ \land \neg C = 0) \to C \in ℝ^{+}$
59	58	adantlr	$⊢ ((φ \land \forall x \in ℝ^{+} A \leq B + C x) \land \neg C = 0) \to C \in ℝ^{+}$
60		simpr	$⊢ (C \in ℝ^{+} \land y \in ℝ^{+}) \to y \in ℝ^{+}$
61		simpl	$⊢ (C \in ℝ^{+} \land y \in ℝ^{+}) \to C \in ℝ^{+}$
62	60 61	rpdivcld	$⊢ (C \in ℝ^{+} \land y \in ℝ^{+}) \to \frac{y}{C} \in ℝ^{+}$
63	62	adantll	$⊢ ((\forall x \in ℝ^{+} A \leq B + C x \land C \in ℝ^{+}) \land y \in ℝ^{+}) \to \frac{y}{C} \in ℝ^{+}$
64		simpll	$⊢ ((\forall x \in ℝ^{+} A \leq B + C x \land C \in ℝ^{+}) \land y \in ℝ^{+}) \to \forall x \in ℝ^{+} A \leq B + C x$
65		oveq2	$⊢ x = \frac{y}{C} \to C x = C (\frac{y}{C})$
66	65	oveq2d	$⊢ x = \frac{y}{C} \to B + C x = B + C (\frac{y}{C})$
67	66	breq2d	$⊢ x = \frac{y}{C} \to (A \leq B + C x \leftrightarrow A \leq B + C (\frac{y}{C}))$
68	67	rspcva	$⊢ (\frac{y}{C} \in ℝ^{+} \land \forall x \in ℝ^{+} A \leq B + C x) \to A \leq B + C (\frac{y}{C})$
69	63 64 68	syl2anc	$⊢ ((\forall x \in ℝ^{+} A \leq B + C x \land C \in ℝ^{+}) \land y \in ℝ^{+}) \to A \leq B + C (\frac{y}{C})$
70	69	adantlll	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq B + C x) \land C \in ℝ^{+}) \land y \in ℝ^{+}) \to A \leq B + C (\frac{y}{C})$
71	60	rpcnd	$⊢ (C \in ℝ^{+} \land y \in ℝ^{+}) \to y \in ℂ$
72	61	rpcnd	$⊢ (C \in ℝ^{+} \land y \in ℝ^{+}) \to C \in ℂ$
73	61	rpne0d	$⊢ (C \in ℝ^{+} \land y \in ℝ^{+}) \to C \neq 0$
74	71 72 73	divcan2d	$⊢ (C \in ℝ^{+} \land y \in ℝ^{+}) \to C (\frac{y}{C}) = y$
75	74	adantll	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq B + C x) \land C \in ℝ^{+}) \land y \in ℝ^{+}) \to C (\frac{y}{C}) = y$
76	75	oveq2d	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq B + C x) \land C \in ℝ^{+}) \land y \in ℝ^{+}) \to B + C (\frac{y}{C}) = B + y$
77	70 76	breqtrd	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq B + C x) \land C \in ℝ^{+}) \land y \in ℝ^{+}) \to A \leq B + y$
78	77	ralrimiva	$⊢ ((φ \land \forall x \in ℝ^{+} A \leq B + C x) \land C \in ℝ^{+}) \to \forall y \in ℝ^{+} A \leq B + y$
79		xralrple	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A \leq B \leftrightarrow \forall y \in ℝ^{+} A \leq B + y)$
80	1 2 79	syl2anc	$⊢ φ \to (A \leq B \leftrightarrow \forall y \in ℝ^{+} A \leq B + y)$
81	80	ad2antrr	$⊢ ((φ \land \forall x \in ℝ^{+} A \leq B + C x) \land C \in ℝ^{+}) \to (A \leq B \leftrightarrow \forall y \in ℝ^{+} A \leq B + y)$
82	78 81	mpbird	$⊢ ((φ \land \forall x \in ℝ^{+} A \leq B + C x) \land C \in ℝ^{+}) \to A \leq B$
83	59 82	syldan	$⊢ ((φ \land \forall x \in ℝ^{+} A \leq B + C x) \land \neg C = 0) \to A \leq B$
84	49 83	pm2.61dan	$⊢ (φ \land \forall x \in ℝ^{+} A \leq B + C x) \to A \leq B$
85	84	ex	$⊢ φ \to (\forall x \in ℝ^{+} A \leq B + C x \to A \leq B)$
86	29 85	impbid	$⊢ φ \to (A \leq B \leftrightarrow \forall x \in ℝ^{+} A \leq B + C x)$

Metamath Proof Explorer

Theorem xralrple3

Proof