Theorem xralrple3

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	xralrple3.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	xralrple3.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	xralrple3.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	xralrple3.g	⊢ ( 𝜑 → 0 ≤ 𝐶 )
Assertion	xralrple3	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		xralrple3.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		xralrple3.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		xralrple3.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		xralrple3.g	⊢ ( 𝜑 → 0 ≤ 𝐶 )
5	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ∈ ℝ* )
6	2	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
7	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ∈ ℝ* )
8	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
9	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
10		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
11	10	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
12	9 11	remulcld	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐶 · 𝑥 ) ∈ ℝ )
13	8 12	readdcld	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 + ( 𝐶 · 𝑥 ) ) ∈ ℝ )
14	13	rexrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 + ( 𝐶 · 𝑥 ) ) ∈ ℝ* )
15		simplr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ≤ 𝐵 )
16	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
17	10	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
18	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ 𝐶 )
19		rpge0	⊢ ( 𝑥 ∈ ℝ+ → 0 ≤ 𝑥 )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ 𝑥 )
21	16 17 18 20	mulge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ ( 𝐶 · 𝑥 ) )
22	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
23	16 17	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝐶 · 𝑥 ) ∈ ℝ )
24	22 23	addge01d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 0 ≤ ( 𝐶 · 𝑥 ) ↔ 𝐵 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) )
25	21 24	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) )
26	25	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) )
27	5 7 14 15 26	xrletrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) )
28	27	ralrimiva	⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) )
29	28	ex	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 → ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) )
30		1rp	⊢ 1 ∈ ℝ+
31		oveq2	⊢ ( 𝑥 = 1 → ( 𝐶 · 𝑥 ) = ( 𝐶 · 1 ) )
32	31	oveq2d	⊢ ( 𝑥 = 1 → ( 𝐵 + ( 𝐶 · 𝑥 ) ) = ( 𝐵 + ( 𝐶 · 1 ) ) )
33	32	breq2d	⊢ ( 𝑥 = 1 → ( 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ↔ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 1 ) ) ) )
34	33	rspcva	⊢ ( ( 1 ∈ ℝ+ ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) → 𝐴 ≤ ( 𝐵 + ( 𝐶 · 1 ) ) )
35	30 34	mpan	⊢ ( ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) → 𝐴 ≤ ( 𝐵 + ( 𝐶 · 1 ) ) )
36	35	ad2antlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) ∧ 𝐶 = 0 ) → 𝐴 ≤ ( 𝐵 + ( 𝐶 · 1 ) ) )
37		oveq1	⊢ ( 𝐶 = 0 → ( 𝐶 · 1 ) = ( 0 · 1 ) )
38		0cn	⊢ 0 ∈ ℂ
39	38	mulid1i	⊢ ( 0 · 1 ) = 0
40	39	a1i	⊢ ( 𝐶 = 0 → ( 0 · 1 ) = 0 )
41	37 40	eqtrd	⊢ ( 𝐶 = 0 → ( 𝐶 · 1 ) = 0 )
42	41	oveq2d	⊢ ( 𝐶 = 0 → ( 𝐵 + ( 𝐶 · 1 ) ) = ( 𝐵 + 0 ) )
43	42	adantl	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ( 𝐵 + ( 𝐶 · 1 ) ) = ( 𝐵 + 0 ) )
44	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → 𝐵 ∈ ℂ )
46	45	addid1d	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ( 𝐵 + 0 ) = 𝐵 )
47	43 46	eqtrd	⊢ ( ( 𝜑 ∧ 𝐶 = 0 ) → ( 𝐵 + ( 𝐶 · 1 ) ) = 𝐵 )
48	47	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) ∧ 𝐶 = 0 ) → ( 𝐵 + ( 𝐶 · 1 ) ) = 𝐵 )
49	36 48	breqtrd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) ∧ 𝐶 = 0 ) → 𝐴 ≤ 𝐵 )
50		neqne	⊢ ( ¬ 𝐶 = 0 → 𝐶 ≠ 0 )
51	50	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐶 = 0 ) → 𝐶 ≠ 0 )
52	3	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 0 ) → 𝐶 ∈ ℝ )
53		0red	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 0 ) → 0 ∈ ℝ )
54	4	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 0 ) → 0 ≤ 𝐶 )
55		simpr	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 0 ) → 𝐶 ≠ 0 )
56	53 52 54 55	leneltd	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 0 ) → 0 < 𝐶 )
57	52 56	elrpd	⊢ ( ( 𝜑 ∧ 𝐶 ≠ 0 ) → 𝐶 ∈ ℝ+ )
58	51 57	syldan	⊢ ( ( 𝜑 ∧ ¬ 𝐶 = 0 ) → 𝐶 ∈ ℝ+ )
59	58	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) ∧ ¬ 𝐶 = 0 ) → 𝐶 ∈ ℝ+ )
60		simpr	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
61		simpl	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → 𝐶 ∈ ℝ+ )
62	60 61	rpdivcld	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 𝐶 ) ∈ ℝ+ )
63	62	adantll	⊢ ( ( ( ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ∧ 𝐶 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 / 𝐶 ) ∈ ℝ+ )
64		simpll	⊢ ( ( ( ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ∧ 𝐶 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) )
65		oveq2	⊢ ( 𝑥 = ( 𝑦 / 𝐶 ) → ( 𝐶 · 𝑥 ) = ( 𝐶 · ( 𝑦 / 𝐶 ) ) )
66	65	oveq2d	⊢ ( 𝑥 = ( 𝑦 / 𝐶 ) → ( 𝐵 + ( 𝐶 · 𝑥 ) ) = ( 𝐵 + ( 𝐶 · ( 𝑦 / 𝐶 ) ) ) )
67	66	breq2d	⊢ ( 𝑥 = ( 𝑦 / 𝐶 ) → ( 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ↔ 𝐴 ≤ ( 𝐵 + ( 𝐶 · ( 𝑦 / 𝐶 ) ) ) ) )
68	67	rspcva	⊢ ( ( ( 𝑦 / 𝐶 ) ∈ ℝ+ ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) → 𝐴 ≤ ( 𝐵 + ( 𝐶 · ( 𝑦 / 𝐶 ) ) ) )
69	63 64 68	syl2anc	⊢ ( ( ( ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ∧ 𝐶 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → 𝐴 ≤ ( 𝐵 + ( 𝐶 · ( 𝑦 / 𝐶 ) ) ) )
70	69	adantlll	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) ∧ 𝐶 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → 𝐴 ≤ ( 𝐵 + ( 𝐶 · ( 𝑦 / 𝐶 ) ) ) )
71	60	rpcnd	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℂ )
72	61	rpcnd	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → 𝐶 ∈ ℂ )
73	61	rpne0d	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → 𝐶 ≠ 0 )
74	71 72 73	divcan2d	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ) → ( 𝐶 · ( 𝑦 / 𝐶 ) ) = 𝑦 )
75	74	adantll	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) ∧ 𝐶 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐶 · ( 𝑦 / 𝐶 ) ) = 𝑦 )
76	75	oveq2d	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) ∧ 𝐶 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝐵 + ( 𝐶 · ( 𝑦 / 𝐶 ) ) ) = ( 𝐵 + 𝑦 ) )
77	70 76	breqtrd	⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) ∧ 𝐶 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ+ ) → 𝐴 ≤ ( 𝐵 + 𝑦 ) )
78	77	ralrimiva	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) ∧ 𝐶 ∈ ℝ+ ) → ∀ 𝑦 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑦 ) )
79		xralrple	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑦 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑦 ) ) )
80	1 2 79	syl2anc	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑦 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑦 ) ) )
81	80	ad2antrr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑦 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑦 ) ) )
82	78 81	mpbird	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) ∧ 𝐶 ∈ ℝ+ ) → 𝐴 ≤ 𝐵 )
83	59 82	syldan	⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) ∧ ¬ 𝐶 = 0 ) → 𝐴 ≤ 𝐵 )
84	49 83	pm2.61dan	⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) → 𝐴 ≤ 𝐵 )
85	84	ex	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) → 𝐴 ≤ 𝐵 ) )
86	29 85	impbid	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + ( 𝐶 · 𝑥 ) ) ) )