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	$⊢ φ \to A \in ℝ^{*}$
	xrlexaddrp.2	$⊢ φ \to B \in ℝ^{*}$
	xrlexaddrp.3	$⊢ (φ \land x \in ℝ^{+}) \to A \leq B +_{𝑒} x$
Assertion	xrlexaddrp	$⊢ φ \to A \leq B$

Proof

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

Metamath Proof Explorer

Theorem xrlexaddrp

Proof