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	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
	xralrple4.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	xralrple4.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	xralrple4	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		xralrple4.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
2		xralrple4.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		xralrple4.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ⁺ ) → 𝐴 ∈ ℝ^* )
5	2	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ^* )
6	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ⁺ ) → 𝐵 ∈ ℝ^* )
7	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ⁺ ) → 𝐵 ∈ ℝ )
8		rpre	⊢ ( 𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ )
9	8	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → 𝑥 ∈ ℝ )
10	3	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → 𝑁 ∈ ℕ₀ )
12	9 11	reexpcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( 𝑥 ↑ 𝑁 ) ∈ ℝ )
13	12	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ⁺ ) → ( 𝑥 ↑ 𝑁 ) ∈ ℝ )
14	7 13	readdcld	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ⁺ ) → ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ∈ ℝ )
15	14	rexrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ⁺ ) → ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ∈ ℝ^* )
16		simplr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ⁺ ) → 𝐴 ≤ 𝐵 )
17		rpge0	⊢ ( 𝑥 ∈ ℝ⁺ → 0 ≤ 𝑥 )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → 0 ≤ 𝑥 )
19	9 11 18	expge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → 0 ≤ ( 𝑥 ↑ 𝑁 ) )
20	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → 𝐵 ∈ ℝ )
21	20 12	addge01d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ( 0 ≤ ( 𝑥 ↑ 𝑁 ) ↔ 𝐵 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ) )
22	19 21	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → 𝐵 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) )
23	22	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ⁺ ) → 𝐵 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) )
24	4 6 15 16 23	xrletrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ⁺ ) → 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) )
25	24	ralrimiva	⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) )
26	25	ex	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 → ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ) )
27		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → 𝑦 ∈ ℝ⁺ )
28	3	nnrpd	⊢ ( 𝜑 → 𝑁 ∈ ℝ⁺ )
29	28	rpreccld	⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℝ⁺ )
30	29	rpred	⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℝ )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( 1 / 𝑁 ) ∈ ℝ )
32	27 31	rpcxpcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) ∈ ℝ⁺ )
33	32	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ) ∧ 𝑦 ∈ ℝ⁺ ) → ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) ∈ ℝ⁺ )
34		simplr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ) ∧ 𝑦 ∈ ℝ⁺ ) → ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) )
35		oveq1	⊢ ( 𝑥 = ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) → ( 𝑥 ↑ 𝑁 ) = ( ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) )
36	35	oveq2d	⊢ ( 𝑥 = ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) → ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) = ( 𝐵 + ( ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) ) )
37	36	breq2d	⊢ ( 𝑥 = ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) → ( 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ↔ 𝐴 ≤ ( 𝐵 + ( ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) ) ) )
38	37	rspcva	⊢ ( ( ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) ∈ ℝ⁺ ∧ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ) → 𝐴 ≤ ( 𝐵 + ( ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) ) )
39	33 34 38	syl2anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ) ∧ 𝑦 ∈ ℝ⁺ ) → 𝐴 ≤ ( 𝐵 + ( ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) ) )
40	27	rpcnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → 𝑦 ∈ ℂ )
41	3	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → 𝑁 ∈ ℕ )
42		cxproot	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = 𝑦 )
43	40 41 42	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) = 𝑦 )
44	43	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ⁺ ) → ( 𝐵 + ( ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) ) = ( 𝐵 + 𝑦 ) )
45	44	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ) ∧ 𝑦 ∈ ℝ⁺ ) → ( 𝐵 + ( ( 𝑦 ↑_𝑐 ( 1 / 𝑁 ) ) ↑ 𝑁 ) ) = ( 𝐵 + 𝑦 ) )
46	39 45	breqtrd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ) ∧ 𝑦 ∈ ℝ⁺ ) → 𝐴 ≤ ( 𝐵 + 𝑦 ) )
47	46	ralrimiva	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ) → ∀ 𝑦 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + 𝑦 ) )
48		xralrple	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑦 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + 𝑦 ) ) )
49	1 2 48	syl2anc	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑦 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + 𝑦 ) ) )
50	49	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑦 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + 𝑦 ) ) )
51	47 50	mpbird	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ) → 𝐴 ≤ 𝐵 )
52	51	ex	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) → 𝐴 ≤ 𝐵 ) )
53	26 52	impbid	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ⁺ 𝐴 ≤ ( 𝐵 + ( 𝑥 ↑ 𝑁 ) ) ) )

Metamath Proof Explorer

Theorem xralrple4

Proof