Theorem xrlexaddrp

Description: If an extended real number A can be approximated from above, adding positive reals to B , then A is less than or equal to B . (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	xrlexaddrp.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	xrlexaddrp.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
	xrlexaddrp.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ≤ ( 𝐵 +𝑒 𝑥 ) )
Assertion	xrlexaddrp	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		xrlexaddrp.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		xrlexaddrp.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3		xrlexaddrp.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ≤ ( 𝐵 +𝑒 𝑥 ) )
4		pnfge	⊢ ( 𝐴 ∈ ℝ* → 𝐴 ≤ +∞ )
5	1 4	syl	⊢ ( 𝜑 → 𝐴 ≤ +∞ )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = +∞ ) → 𝐴 ≤ +∞ )
7		id	⊢ ( 𝐵 = +∞ → 𝐵 = +∞ )
8	7	eqcomd	⊢ ( 𝐵 = +∞ → +∞ = 𝐵 )
9	8	adantl	⊢ ( ( 𝜑 ∧ 𝐵 = +∞ ) → +∞ = 𝐵 )
10	6 9	breqtrd	⊢ ( ( 𝜑 ∧ 𝐵 = +∞ ) → 𝐴 ≤ 𝐵 )
11		simpl	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = +∞ ) → 𝜑 )
12		neqne	⊢ ( ¬ 𝐵 = +∞ → 𝐵 ≠ +∞ )
13	12	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = +∞ ) → 𝐵 ≠ +∞ )
14		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → 𝐴 = -∞ )
15		mnfle	⊢ ( 𝐵 ∈ ℝ* → -∞ ≤ 𝐵 )
16	2 15	syl	⊢ ( 𝜑 → -∞ ≤ 𝐵 )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → -∞ ≤ 𝐵 )
18	14 17	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝐴 = -∞ ) → 𝐴 ≤ 𝐵 )
19	18	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) ∧ 𝐴 = -∞ ) → 𝐴 ≤ 𝐵 )
20		simpl	⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → ( 𝜑 ∧ 𝐵 ≠ +∞ ) )
21		neqne	⊢ ( ¬ 𝐴 = -∞ → 𝐴 ≠ -∞ )
22	21	adantl	⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → 𝐴 ≠ -∞ )
23		simpll	⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) ∧ 𝐴 ≠ -∞ ) → 𝜑 )
24	2	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) → 𝐵 ∈ ℝ* )
25		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) → 𝐵 ≠ +∞ )
26	24 25	jca	⊢ ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) → ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) )
27		xrnepnf	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞ ) ↔ ( 𝐵 ∈ ℝ ∨ 𝐵 = -∞ ) )
28	26 27	sylib	⊢ ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = -∞ ) )
29	28	adantr	⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) ∧ ¬ 𝐵 ∈ ℝ ) → ( 𝐵 ∈ ℝ ∨ 𝐵 = -∞ ) )
30		simpr	⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) ∧ ¬ 𝐵 ∈ ℝ ) → ¬ 𝐵 ∈ ℝ )
31		pm2.53	⊢ ( ( 𝐵 ∈ ℝ ∨ 𝐵 = -∞ ) → ( ¬ 𝐵 ∈ ℝ → 𝐵 = -∞ ) )
32	29 30 31	sylc	⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) ∧ ¬ 𝐵 ∈ ℝ ) → 𝐵 = -∞ )
33	32	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐵 ∈ ℝ ) → 𝐵 = -∞ )
34		id	⊢ ( 𝜑 → 𝜑 )
35		1rp	⊢ 1 ∈ ℝ+
36	35	a1i	⊢ ( 𝜑 → 1 ∈ ℝ+ )
37		1re	⊢ 1 ∈ ℝ
38	37	elexi	⊢ 1 ∈ V
39		eleq1	⊢ ( 𝑥 = 1 → ( 𝑥 ∈ ℝ+ ↔ 1 ∈ ℝ+ ) )
40	39	anbi2d	⊢ ( 𝑥 = 1 → ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ↔ ( 𝜑 ∧ 1 ∈ ℝ+ ) ) )
41		oveq2	⊢ ( 𝑥 = 1 → ( 𝐵 +𝑒 𝑥 ) = ( 𝐵 +𝑒 1 ) )
42	41	breq2d	⊢ ( 𝑥 = 1 → ( 𝐴 ≤ ( 𝐵 +𝑒 𝑥 ) ↔ 𝐴 ≤ ( 𝐵 +𝑒 1 ) ) )
43	40 42	imbi12d	⊢ ( 𝑥 = 1 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ≤ ( 𝐵 +𝑒 𝑥 ) ) ↔ ( ( 𝜑 ∧ 1 ∈ ℝ+ ) → 𝐴 ≤ ( 𝐵 +𝑒 1 ) ) ) )
44	38 43 3	vtocl	⊢ ( ( 𝜑 ∧ 1 ∈ ℝ+ ) → 𝐴 ≤ ( 𝐵 +𝑒 1 ) )
45	34 36 44	syl2anc	⊢ ( 𝜑 → 𝐴 ≤ ( 𝐵 +𝑒 1 ) )
46	45	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ 𝐵 = -∞ ) → 𝐴 ≤ ( 𝐵 +𝑒 1 ) )
47		oveq1	⊢ ( 𝐵 = -∞ → ( 𝐵 +𝑒 1 ) = ( -∞ +𝑒 1 ) )
48		1xr	⊢ 1 ∈ ℝ*
49		ltpnf	⊢ ( 1 ∈ ℝ → 1 < +∞ )
50	37 49	ax-mp	⊢ 1 < +∞
51	37 50	ltneii	⊢ 1 ≠ +∞
52		xaddmnf2	⊢ ( ( 1 ∈ ℝ* ∧ 1 ≠ +∞ ) → ( -∞ +𝑒 1 ) = -∞ )
53	48 51 52	mp2an	⊢ ( -∞ +𝑒 1 ) = -∞
54	53	a1i	⊢ ( 𝐵 = -∞ → ( -∞ +𝑒 1 ) = -∞ )
55	47 54	eqtr2d	⊢ ( 𝐵 = -∞ → -∞ = ( 𝐵 +𝑒 1 ) )
56	55	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ 𝐵 = -∞ ) → -∞ = ( 𝐵 +𝑒 1 ) )
57	56	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ 𝐵 = -∞ ) → ( 𝐵 +𝑒 1 ) = -∞ )
58	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) → 𝐴 ∈ ℝ* )
59		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) → 𝐴 ≠ -∞ )
60		nemnftgtmnft	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ -∞ ) → -∞ < 𝐴 )
61	58 59 60	syl2anc	⊢ ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) → -∞ < 𝐴 )
62	61	adantr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ 𝐵 = -∞ ) → -∞ < 𝐴 )
63	57 62	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ 𝐵 = -∞ ) → ( 𝐵 +𝑒 1 ) < 𝐴 )
64	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ 𝐵 = -∞ ) → 𝐵 ∈ ℝ* )
65	48	a1i	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ 𝐵 = -∞ ) → 1 ∈ ℝ* )
66	64 65	xaddcld	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ 𝐵 = -∞ ) → ( 𝐵 +𝑒 1 ) ∈ ℝ* )
67	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ 𝐵 = -∞ ) → 𝐴 ∈ ℝ* )
68		xrltnle	⊢ ( ( ( 𝐵 +𝑒 1 ) ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( ( 𝐵 +𝑒 1 ) < 𝐴 ↔ ¬ 𝐴 ≤ ( 𝐵 +𝑒 1 ) ) )
69	66 67 68	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ 𝐵 = -∞ ) → ( ( 𝐵 +𝑒 1 ) < 𝐴 ↔ ¬ 𝐴 ≤ ( 𝐵 +𝑒 1 ) ) )
70	63 69	mpbid	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) ∧ 𝐵 = -∞ ) → ¬ 𝐴 ≤ ( 𝐵 +𝑒 1 ) )
71	46 70	pm2.65da	⊢ ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) → ¬ 𝐵 = -∞ )
72	71	neqned	⊢ ( ( 𝜑 ∧ 𝐴 ≠ -∞ ) → 𝐵 ≠ -∞ )
73	72	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐵 ∈ ℝ ) → 𝐵 ≠ -∞ )
74	73	neneqd	⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) ∧ 𝐴 ≠ -∞ ) ∧ ¬ 𝐵 ∈ ℝ ) → ¬ 𝐵 = -∞ )
75	33 74	condan	⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) ∧ 𝐴 ≠ -∞ ) → 𝐵 ∈ ℝ )
76	3	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ≤ ( 𝐵 +𝑒 𝑥 ) )
77		simpl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
78		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
79	78	adantl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
80		rexadd	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐵 +𝑒 𝑥 ) = ( 𝐵 + 𝑥 ) )
81	77 79 80	syl2anc	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 +𝑒 𝑥 ) = ( 𝐵 + 𝑥 ) )
82	81	adantll	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 +𝑒 𝑥 ) = ( 𝐵 + 𝑥 ) )
83	76 82	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝐴 ≤ ( 𝐵 + 𝑥 ) )
84	83	ralrimiva	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) )
85	1	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ* )
86		simpr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
87		xralrple	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
88	85 86 87	syl2anc	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ∀ 𝑥 ∈ ℝ+ 𝐴 ≤ ( 𝐵 + 𝑥 ) ) )
89	84 88	mpbird	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → 𝐴 ≤ 𝐵 )
90	23 75 89	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) ∧ 𝐴 ≠ -∞ ) → 𝐴 ≤ 𝐵 )
91	20 22 90	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) ∧ ¬ 𝐴 = -∞ ) → 𝐴 ≤ 𝐵 )
92	19 91	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝐵 ≠ +∞ ) → 𝐴 ≤ 𝐵 )
93	11 13 92	syl2anc	⊢ ( ( 𝜑 ∧ ¬ 𝐵 = +∞ ) → 𝐴 ≤ 𝐵 )
94	10 93	pm2.61dan	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )