xralrple2

Description: Show that A is less than B by showing that there is no positive bound on the difference. A variant on xralrple . (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	xralrple2.x	$⊢ Ⅎ x φ$
	xralrple2.a	$⊢ φ \to A \in ℝ^{*}$
	xralrple2.b	$⊢ φ \to B \in [0, +∞)$
Assertion	xralrple2	$⊢ φ \to (A \leq B \leftrightarrow \forall x \in ℝ^{+} A \leq (1 + x) B)$

Proof

Step	Hyp	Ref	Expression
1		xralrple2.x	$⊢ Ⅎ x φ$
2		xralrple2.a	$⊢ φ \to A \in ℝ^{*}$
3		xralrple2.b	$⊢ φ \to B \in [0, +∞)$
4		nfv	$⊢ Ⅎ x A \leq B$
5	1 4	nfan	$⊢ Ⅎ x (φ \land A \leq B)$
6	2	ad2antrr	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to A \in ℝ^{*}$
7		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
8	3	ad2antrr	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to B \in [0, +∞)$
9	7 8	sselid	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to B \in ℝ^{*}$
10		1red	$⊢ (φ \land x \in ℝ^{+}) \to 1 \in ℝ$
11		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
12	11	adantl	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ$
13	10 12	readdcld	$⊢ (φ \land x \in ℝ^{+}) \to 1 + x \in ℝ$
14		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
15	14 3	sselid	$⊢ φ \to B \in ℝ$
16	15	adantr	$⊢ (φ \land x \in ℝ^{+}) \to B \in ℝ$
17	13 16	remulcld	$⊢ (φ \land x \in ℝ^{+}) \to (1 + x) B \in ℝ$
18	17	rexrd	$⊢ (φ \land x \in ℝ^{+}) \to (1 + x) B \in ℝ^{*}$
19	18	adantlr	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to (1 + x) B \in ℝ^{*}$
20		simplr	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to A \leq B$
21	15	ad2antrr	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to B \in ℝ$
22		1red	$⊢ x \in ℝ^{+} \to 1 \in ℝ$
23	22 11	readdcld	$⊢ x \in ℝ^{+} \to 1 + x \in ℝ$
24	23	adantl	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to 1 + x \in ℝ$
25		0xr	$⊢ 0 \in ℝ^{*}$
26	25	a1i	$⊢ B \in [0, +∞) \to 0 \in ℝ^{*}$
27		pnfxr	$⊢ +∞ \in ℝ^{*}$
28	27	a1i	$⊢ B \in [0, +∞) \to +∞ \in ℝ^{*}$
29		id	$⊢ B \in [0, +∞) \to B \in [0, +∞)$
30		icogelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land B \in [0, +∞)) \to 0 \leq B$
31	26 28 29 30	syl3anc	$⊢ B \in [0, +∞) \to 0 \leq B$
32	3 31	syl	$⊢ φ \to 0 \leq B$
33	32	ad2antrr	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to 0 \leq B$
34		id	$⊢ x \in ℝ^{+} \to x \in ℝ^{+}$
35	22 34	ltaddrpd	$⊢ x \in ℝ^{+} \to 1 < 1 + x$
36	22 23 35	ltled	$⊢ x \in ℝ^{+} \to 1 \leq 1 + x$
37	36	adantl	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to 1 \leq 1 + x$
38	21 24 33 37	lemulge12d	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to B \leq (1 + x) B$
39	6 9 19 20 38	xrletrd	$⊢ ((φ \land A \leq B) \land x \in ℝ^{+}) \to A \leq (1 + x) B$
40	39	ex	$⊢ (φ \land A \leq B) \to (x \in ℝ^{+} \to A \leq (1 + x) B)$
41	5 40	ralrimi	$⊢ (φ \land A \leq B) \to \forall x \in ℝ^{+} A \leq (1 + x) B$
42	41	ex	$⊢ φ \to (A \leq B \to \forall x \in ℝ^{+} A \leq (1 + x) B)$
43	2	ad3antrrr	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \land B = 0) \to A \in ℝ^{*}$
44		id	$⊢ B = 0 \to B = 0$
45		0red	$⊢ B = 0 \to 0 \in ℝ$
46	44 45	eqeltrd	$⊢ B = 0 \to B \in ℝ$
47	46	adantl	$⊢ (y \in ℝ^{+} \land B = 0) \to B \in ℝ$
48		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
49	48	adantr	$⊢ (y \in ℝ^{+} \land B = 0) \to y \in ℝ$
50	47 49	readdcld	$⊢ (y \in ℝ^{+} \land B = 0) \to B + y \in ℝ$
51	50	rexrd	$⊢ (y \in ℝ^{+} \land B = 0) \to B + y \in ℝ^{*}$
52	51	adantll	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \land B = 0) \to B + y \in ℝ^{*}$
53	25	a1i	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \land B = 0) \to 0 \in ℝ^{*}$
54		1rp	$⊢ 1 \in ℝ^{+}$
55	54	a1i	$⊢ \forall x \in ℝ^{+} A \leq (1 + x) B \to 1 \in ℝ^{+}$
56		id	$⊢ \forall x \in ℝ^{+} A \leq (1 + x) B \to \forall x \in ℝ^{+} A \leq (1 + x) B$
57		oveq2	$⊢ x = 1 \to 1 + x = 1 + 1$
58	57	oveq1d	$⊢ x = 1 \to (1 + x) B = (1 + 1) B$
59	58	breq2d	$⊢ x = 1 \to (A \leq (1 + x) B \leftrightarrow A \leq (1 + 1) B)$
60	59	rspcva	$⊢ (1 \in ℝ^{+} \land \forall x \in ℝ^{+} A \leq (1 + x) B) \to A \leq (1 + 1) B$
61	55 56 60	syl2anc	$⊢ \forall x \in ℝ^{+} A \leq (1 + x) B \to A \leq (1 + 1) B$
62		1p1e2	$⊢ 1 + 1 = 2$
63	62	a1i	$⊢ \forall x \in ℝ^{+} A \leq (1 + x) B \to 1 + 1 = 2$
64	63	oveq1d	$⊢ \forall x \in ℝ^{+} A \leq (1 + x) B \to (1 + 1) B = 2 B$
65	61 64	breqtrd	$⊢ \forall x \in ℝ^{+} A \leq (1 + x) B \to A \leq 2 B$
66	65	adantr	$⊢ (\forall x \in ℝ^{+} A \leq (1 + x) B \land B = 0) \to A \leq 2 B$
67		simpr	$⊢ (\forall x \in ℝ^{+} A \leq (1 + x) B \land B = 0) \to B = 0$
68		simpl	$⊢ (A \leq 2 B \land B = 0) \to A \leq 2 B$
69		oveq2	$⊢ B = 0 \to 2 B = 2 \cdot 0$
70		2cnd	$⊢ B = 0 \to 2 \in ℂ$
71	70	mul01d	$⊢ B = 0 \to 2 \cdot 0 = 0$
72	69 71	eqtrd	$⊢ B = 0 \to 2 B = 0$
73	72	adantl	$⊢ (A \leq 2 B \land B = 0) \to 2 B = 0$
74	68 73	breqtrd	$⊢ (A \leq 2 B \land B = 0) \to A \leq 0$
75	66 67 74	syl2anc	$⊢ (\forall x \in ℝ^{+} A \leq (1 + x) B \land B = 0) \to A \leq 0$
76	75	ad4ant24	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \land B = 0) \to A \leq 0$
77		rpgt0	$⊢ y \in ℝ^{+} \to 0 < y$
78	77	adantr	$⊢ (y \in ℝ^{+} \land B = 0) \to 0 < y$
79		oveq1	$⊢ B = 0 \to B + y = 0 + y$
80	79	adantl	$⊢ (y \in ℝ^{+} \land B = 0) \to B + y = 0 + y$
81	48	recnd	$⊢ y \in ℝ^{+} \to y \in ℂ$
82	81	adantr	$⊢ (y \in ℝ^{+} \land B = 0) \to y \in ℂ$
83	82	addlidd	$⊢ (y \in ℝ^{+} \land B = 0) \to 0 + y = y$
84	80 83	eqtr2d	$⊢ (y \in ℝ^{+} \land B = 0) \to y = B + y$
85	78 84	breqtrd	$⊢ (y \in ℝ^{+} \land B = 0) \to 0 < B + y$
86	85	adantll	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \land B = 0) \to 0 < B + y$
87	43 53 52 76 86	xrlelttrd	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \land B = 0) \to A < B + y$
88	43 52 87	xrltled	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \land B = 0) \to A \leq B + y$
89		simpl	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \land \neg B = 0) \to ((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+})$
90	15	adantr	$⊢ (φ \land \neg B = 0) \to B \in ℝ$
91		0red	$⊢ (φ \land \neg B = 0) \to 0 \in ℝ$
92	32	adantr	$⊢ (φ \land \neg B = 0) \to 0 \leq B$
93	44	necon3bi	$⊢ \neg B = 0 \to B \neq 0$
94	93	adantl	$⊢ (φ \land \neg B = 0) \to B \neq 0$
95	91 90 92 94	leneltd	$⊢ (φ \land \neg B = 0) \to 0 < B$
96	90 95	elrpd	$⊢ (φ \land \neg B = 0) \to B \in ℝ^{+}$
97	96	ad4ant14	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \land \neg B = 0) \to B \in ℝ^{+}$
98		simplr	$⊢ ((\forall x \in ℝ^{+} A \leq (1 + x) B \land y \in ℝ^{+}) \land B \in ℝ^{+}) \to y \in ℝ^{+}$
99		simpr	$⊢ ((\forall x \in ℝ^{+} A \leq (1 + x) B \land y \in ℝ^{+}) \land B \in ℝ^{+}) \to B \in ℝ^{+}$
100	98 99	rpdivcld	$⊢ ((\forall x \in ℝ^{+} A \leq (1 + x) B \land y \in ℝ^{+}) \land B \in ℝ^{+}) \to \frac{y}{B} \in ℝ^{+}$
101		simpll	$⊢ ((\forall x \in ℝ^{+} A \leq (1 + x) B \land y \in ℝ^{+}) \land B \in ℝ^{+}) \to \forall x \in ℝ^{+} A \leq (1 + x) B$
102		oveq2	$⊢ x = \frac{y}{B} \to 1 + x = 1 + (\frac{y}{B})$
103	102	oveq1d	$⊢ x = \frac{y}{B} \to (1 + x) B = (1 + (\frac{y}{B})) B$
104	103	breq2d	$⊢ x = \frac{y}{B} \to (A \leq (1 + x) B \leftrightarrow A \leq (1 + (\frac{y}{B})) B)$
105	104	rspcva	$⊢ (\frac{y}{B} \in ℝ^{+} \land \forall x \in ℝ^{+} A \leq (1 + x) B) \to A \leq (1 + (\frac{y}{B})) B$
106	100 101 105	syl2anc	$⊢ ((\forall x \in ℝ^{+} A \leq (1 + x) B \land y \in ℝ^{+}) \land B \in ℝ^{+}) \to A \leq (1 + (\frac{y}{B})) B$
107	106	adantlll	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \land B \in ℝ^{+}) \to A \leq (1 + (\frac{y}{B})) B$
108		1cnd	$⊢ (y \in ℝ^{+} \land B \in ℝ^{+}) \to 1 \in ℂ$
109	81	adantr	$⊢ (y \in ℝ^{+} \land B \in ℝ^{+}) \to y \in ℂ$
110		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
111	110	adantl	$⊢ (y \in ℝ^{+} \land B \in ℝ^{+}) \to B \in ℂ$
112		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
113	112	adantl	$⊢ (y \in ℝ^{+} \land B \in ℝ^{+}) \to B \neq 0$
114	109 111 113	divcld	$⊢ (y \in ℝ^{+} \land B \in ℝ^{+}) \to \frac{y}{B} \in ℂ$
115	108 114 111	adddird	$⊢ (y \in ℝ^{+} \land B \in ℝ^{+}) \to (1 + (\frac{y}{B})) B = 1 B + (\frac{y}{B}) B$
116	111	mullidd	$⊢ (y \in ℝ^{+} \land B \in ℝ^{+}) \to 1 B = B$
117	109 111 113	divcan1d	$⊢ (y \in ℝ^{+} \land B \in ℝ^{+}) \to (\frac{y}{B}) B = y$
118	116 117	oveq12d	$⊢ (y \in ℝ^{+} \land B \in ℝ^{+}) \to 1 B + (\frac{y}{B}) B = B + y$
119		eqidd	$⊢ (y \in ℝ^{+} \land B \in ℝ^{+}) \to B + y = B + y$
120	115 118 119	3eqtrd	$⊢ (y \in ℝ^{+} \land B \in ℝ^{+}) \to (1 + (\frac{y}{B})) B = B + y$
121	120	adantll	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \land B \in ℝ^{+}) \to (1 + (\frac{y}{B})) B = B + y$
122	107 121	breqtrd	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \land B \in ℝ^{+}) \to A \leq B + y$
123	89 97 122	syl2anc	$⊢ (((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \land \neg B = 0) \to A \leq B + y$
124	88 123	pm2.61dan	$⊢ ((φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \land y \in ℝ^{+}) \to A \leq B + y$
125	124	ralrimiva	$⊢ (φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \to \forall y \in ℝ^{+} A \leq B + y$
126		xralrple	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A \leq B \leftrightarrow \forall y \in ℝ^{+} A \leq B + y)$
127	2 15 126	syl2anc	$⊢ φ \to (A \leq B \leftrightarrow \forall y \in ℝ^{+} A \leq B + y)$
128	127	adantr	$⊢ (φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \to (A \leq B \leftrightarrow \forall y \in ℝ^{+} A \leq B + y)$
129	125 128	mpbird	$⊢ (φ \land \forall x \in ℝ^{+} A \leq (1 + x) B) \to A \leq B$
130	129	ex	$⊢ φ \to (\forall x \in ℝ^{+} A \leq (1 + x) B \to A \leq B)$
131	42 130	impbid	$⊢ φ \to (A \leq B \leftrightarrow \forall x \in ℝ^{+} A \leq (1 + x) B)$

Metamath Proof Explorer

Theorem xralrple2

Proof