Metamath Proof Explorer


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 ( 𝜑𝐴 ∈ ℝ* )
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 ( 𝜑𝑁 ∈ ℕ0 )
11 10 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑁 ∈ ℕ0 )
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 ( 𝜑 → ( 𝐴𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝑥𝑁 ) ) ) )