Theorem 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	⊢ Ⅎ 𝑥 𝜑
	xralrple2.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	xralrple2.b	⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,) +∞ ) )
Assertion	xralrple2	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( ( 1 + 𝑥 ) · 𝐵 ) ) )

Proof

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