Theorem xralrple4

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	xralrple4.a	$$⊢\phi \to A\in {ℝ}^{*}$$
	xralrple4.b	$$⊢\phi \to B\in ℝ$$
	xralrple4.n	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	xralrple4	$$⊢\phi \to \left(A\le B\leftrightarrow \forall x\in {ℝ}^{+}A\le B+x^N\right)$$

Proof

Step	Hyp	Ref	Expression
1		xralrple4.a	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xralrple4.b	$$⊢\phi \to B\in ℝ$$
3		xralrple4.n	$$⊢\phi \to N\in \mathbb{N}$$
4	1	ad2antrr	$$⊢\left(\left(\phi \wedge A\le B\right)\wedge x\in {ℝ}^{+}\right)\to A\in {ℝ}^{*}$$
5	2	rexrd	$$⊢\phi \to B\in {ℝ}^{*}$$
6	5	ad2antrr	$$⊢\left(\left(\phi \wedge A\le B\right)\wedge x\in {ℝ}^{+}\right)\to B\in {ℝ}^{*}$$
7	2	ad2antrr	$$⊢\left(\left(\phi \wedge A\le B\right)\wedge x\in {ℝ}^{+}\right)\to B\in ℝ$$
8		rpre	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
9	8	adantl	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to x\in ℝ$$
10	3	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
11	10	adantr	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to N\in {\mathbb{N}}_0$$
12	9 11	reexpcld	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to x^N\in ℝ$$
13	12	adantlr	$$⊢\left(\left(\phi \wedge A\le B\right)\wedge x\in {ℝ}^{+}\right)\to x^N\in ℝ$$
14	7 13	readdcld	$$⊢\left(\left(\phi \wedge A\le B\right)\wedge x\in {ℝ}^{+}\right)\to B+x^N\in ℝ$$
15	14	rexrd	$$⊢\left(\left(\phi \wedge A\le B\right)\wedge x\in {ℝ}^{+}\right)\to B+x^N\in {ℝ}^{*}$$
16		simplr	$$⊢\left(\left(\phi \wedge A\le B\right)\wedge x\in {ℝ}^{+}\right)\to A\le B$$
17		rpge0	$$⊢x\in {ℝ}^{+}\to 0\le x$$
18	17	adantl	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to 0\le x$$
19	9 11 18	expge0d	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to 0\le x^N$$
20	2	adantr	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to B\in ℝ$$
21	20 12	addge01d	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to \left(0\le x^N\leftrightarrow B\le B+x^N\right)$$
22	19 21	mpbid	$$⊢\left(\phi \wedge x\in {ℝ}^{+}\right)\to B\le B+x^N$$
23	22	adantlr	$$⊢\left(\left(\phi \wedge A\le B\right)\wedge x\in {ℝ}^{+}\right)\to B\le B+x^N$$
24	4 6 15 16 23	xrletrd	$$⊢\left(\left(\phi \wedge A\le B\right)\wedge x\in {ℝ}^{+}\right)\to A\le B+x^N$$
25	24	ralrimiva	$$⊢\left(\phi \wedge A\le B\right)\to \forall x\in {ℝ}^{+}A\le B+x^N$$
26	25	ex	$$⊢\phi \to \left(A\le B\to \forall x\in {ℝ}^{+}A\le B+x^N\right)$$
27		simpr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to y\in {ℝ}^{+}$$
28	3	nnrpd	$$⊢\phi \to N\in {ℝ}^{+}$$
29	28	rpreccld	$$⊢\phi \to \frac{1}{N}\in {ℝ}^{+}$$
30	29	rpred	$$⊢\phi \to \frac{1}{N}\in ℝ$$
31	30	adantr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to \frac{1}{N}\in ℝ$$
32	27 31	rpcxpcld	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to y^{\frac{1}{N}}\in {ℝ}^{+}$$
33	32	adantlr	$$⊢\left(\left(\phi \wedge \forall x\in {ℝ}^{+}A\le B+x^N\right)\wedge y\in {ℝ}^{+}\right)\to y^{\frac{1}{N}}\in {ℝ}^{+}$$
34		simplr	$$⊢\left(\left(\phi \wedge \forall x\in {ℝ}^{+}A\le B+x^N\right)\wedge y\in {ℝ}^{+}\right)\to \forall x\in {ℝ}^{+}A\le B+x^N$$
35		oveq1	$$⊢x=y^{\frac{1}{N}}\to x^N={\left(y^{\frac{1}{N}}\right)}^N$$
36	35	oveq2d	$$⊢x=y^{\frac{1}{N}}\to B+x^N=B+{\left(y^{\frac{1}{N}}\right)}^N$$
37	36	breq2d	$$⊢x=y^{\frac{1}{N}}\to \left(A\le B+x^N\leftrightarrow A\le B+{\left(y^{\frac{1}{N}}\right)}^N\right)$$
38	37	rspcva	$$⊢\left(y^{\frac{1}{N}}\in {ℝ}^{+}\wedge \forall x\in {ℝ}^{+}A\le B+x^N\right)\to A\le B+{\left(y^{\frac{1}{N}}\right)}^N$$
39	33 34 38	syl2anc	$$⊢\left(\left(\phi \wedge \forall x\in {ℝ}^{+}A\le B+x^N\right)\wedge y\in {ℝ}^{+}\right)\to A\le B+{\left(y^{\frac{1}{N}}\right)}^N$$
40	27	rpcnd	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to y\in ℂ$$
41	3	adantr	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to N\in \mathbb{N}$$
42		cxproot	$$⊢\left(y\in ℂ\wedge N\in \mathbb{N}\right)\to {\left(y^{\frac{1}{N}}\right)}^N=y$$
43	40 41 42	syl2anc	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to {\left(y^{\frac{1}{N}}\right)}^N=y$$
44	43	oveq2d	$$⊢\left(\phi \wedge y\in {ℝ}^{+}\right)\to B+{\left(y^{\frac{1}{N}}\right)}^N=B+y$$
45	44	adantlr	$$⊢\left(\left(\phi \wedge \forall x\in {ℝ}^{+}A\le B+x^N\right)\wedge y\in {ℝ}^{+}\right)\to B+{\left(y^{\frac{1}{N}}\right)}^N=B+y$$
46	39 45	breqtrd	$$⊢\left(\left(\phi \wedge \forall x\in {ℝ}^{+}A\le B+x^N\right)\wedge y\in {ℝ}^{+}\right)\to A\le B+y$$
47	46	ralrimiva	$$⊢\left(\phi \wedge \forall x\in {ℝ}^{+}A\le B+x^N\right)\to \forall y\in {ℝ}^{+}A\le B+y$$
48		xralrple	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\right)\to \left(A\le B\leftrightarrow \forall y\in {ℝ}^{+}A\le B+y\right)$$
49	1 2 48	syl2anc	$$⊢\phi \to \left(A\le B\leftrightarrow \forall y\in {ℝ}^{+}A\le B+y\right)$$
50	49	adantr	$$⊢\left(\phi \wedge \forall x\in {ℝ}^{+}A\le B+x^N\right)\to \left(A\le B\leftrightarrow \forall y\in {ℝ}^{+}A\le B+y\right)$$
51	47 50	mpbird	$$⊢\left(\phi \wedge \forall x\in {ℝ}^{+}A\le B+x^N\right)\to A\le B$$
52	51	ex	$$⊢\phi \to \left(\forall x\in {ℝ}^{+}A\le B+x^N\to A\le B\right)$$
53	26 52	impbid	$$⊢\phi \to \left(A\le B\leftrightarrow \forall x\in {ℝ}^{+}A\le B+x^N\right)$$