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	$⊢ φ \to A \in ℝ^{*}$
	xralrple4.b	$⊢ φ \to B \in ℝ$
	xralrple4.n	$⊢ φ \to N \in ℕ$
Assertion	xralrple4	$⊢ φ \to (A \leq B \leftrightarrow \forall x \in ℝ^{+} A \leq B + x^{N})$

Proof

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

Metamath Proof Explorer

Theorem xralrple4

Proof