xleadd1a

Description: Extended real version of leadd1 ; note that the converse implication is not true, unlike the real version (for example 0 < 1 but ( 1 +e +oo ) <_ ( 0 +e +oo ) ). (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xleadd1a	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to A +_{𝑒} C \leq B +_{𝑒} C$

Proof

Step	Hyp	Ref	Expression
1		simplrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \land B \in ℝ) \to A \in ℝ$
2		simpr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \land B \in ℝ) \to B \in ℝ$
3		simplrl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \land B \in ℝ) \to C \in ℝ$
4		simpllr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \land B \in ℝ) \to A \leq B$
5	1 2 3 4	leadd1dd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \land B \in ℝ) \to A + C \leq B + C$
6	1 3	rexaddd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \land B \in ℝ) \to A +_{𝑒} C = A + C$
7	2 3	rexaddd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \land B \in ℝ) \to B +_{𝑒} C = B + C$
8	5 6 7	3brtr4d	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \land B \in ℝ) \to A +_{𝑒} C \leq B +_{𝑒} C$
9		simpl1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to A \in ℝ^{}$
10		simpl3	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to C \in ℝ^{}$
11		xaddcl	$⊢ (A \in ℝ^{} \land C \in ℝ^{}) \to A +_{𝑒} C \in ℝ^{*}$
12	9 10 11	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to A +_{𝑒} C \in ℝ^{}$
13	12	ad2antrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \land B = +∞) \to A +_{𝑒} C \in ℝ^{}$
14		pnfge	$⊢ A +_{𝑒} C \in ℝ^{*} \to A +_{𝑒} C \leq +∞$
15	13 14	syl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \land B = +∞) \to A +_{𝑒} C \leq +∞$
16		oveq1	$⊢ B = +∞ \to B +_{𝑒} C = +∞ +_{𝑒} C$
17		rexr	$⊢ C \in ℝ \to C \in ℝ^{*}$
18		renemnf	$⊢ C \in ℝ \to C \neq −∞$
19		xaddpnf2	$⊢ (C \in ℝ^{*} \land C \neq −∞) \to +∞ +_{𝑒} C = +∞$
20	17 18 19	syl2anc	$⊢ C \in ℝ \to +∞ +_{𝑒} C = +∞$
21	20	ad2antrl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \to +∞ +_{𝑒} C = +∞$
22	16 21	sylan9eqr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \land B = +∞) \to B +_{𝑒} C = +∞$
23	15 22	breqtrrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \land B = +∞) \to A +_{𝑒} C \leq B +_{𝑒} C$
24	12	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \land B = −∞) \to A +_{𝑒} C \in ℝ^{}$
25	24	xrleidd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land B = −∞) \to A +_{𝑒} C \leq A +_{𝑒} C$
26		simplr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land B = −∞) \to A \leq B$
27		simpr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land B = −∞) \to B = −∞$
28	9	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \land B = −∞) \to A \in ℝ^{}$
29		mnfle	$⊢ A \in ℝ^{*} \to −∞ \leq A$
30	28 29	syl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land B = −∞) \to −∞ \leq A$
31	27 30	eqbrtrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land B = −∞) \to B \leq A$
32		simpl2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to B \in ℝ^{}$
33		xrletri3	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (A = B \leftrightarrow (A \leq B \land B \leq A))$
34	9 32 33	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to (A = B \leftrightarrow (A \leq B \land B \leq A))$
35	34	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land B = −∞) \to (A = B \leftrightarrow (A \leq B \land B \leq A))$
36	26 31 35	mpbir2and	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land B = −∞) \to A = B$
37	36	oveq1d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land B = −∞) \to A +_{𝑒} C = B +_{𝑒} C$
38	25 37	breqtrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land B = −∞) \to A +_{𝑒} C \leq B +_{𝑒} C$
39	38	adantlr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \land B = −∞) \to A +_{𝑒} C \leq B +_{𝑒} C$
40		elxr	$⊢ B \in ℝ^{*} \leftrightarrow (B \in ℝ \lor B = +∞ \lor B = −∞)$
41	32 40	sylib	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to (B \in ℝ \lor B = +∞ \lor B = −∞)$
42	41	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \to (B \in ℝ \lor B = +∞ \lor B = −∞)$
43	8 23 39 42	mpjao3dan	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land (C \in ℝ \land A \in ℝ)) \to A +_{𝑒} C \leq B +_{𝑒} C$
44	43	anassrs	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C \in ℝ) \land A \in ℝ) \to A +_{𝑒} C \leq B +_{𝑒} C$
45	12	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \land A = +∞) \to A +_{𝑒} C \in ℝ^{}$
46	45	xrleidd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land A = +∞) \to A +_{𝑒} C \leq A +_{𝑒} C$
47		simplr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land A = +∞) \to A \leq B$
48		pnfge	$⊢ B \in ℝ^{*} \to B \leq +∞$
49	32 48	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to B \leq +∞$
50	49	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land A = +∞) \to B \leq +∞$
51		simpr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land A = +∞) \to A = +∞$
52	50 51	breqtrrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land A = +∞) \to B \leq A$
53	34	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land A = +∞) \to (A = B \leftrightarrow (A \leq B \land B \leq A))$
54	47 52 53	mpbir2and	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land A = +∞) \to A = B$
55	54	oveq1d	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land A = +∞) \to A +_{𝑒} C = B +_{𝑒} C$
56	46 55	breqtrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land A = +∞) \to A +_{𝑒} C \leq B +_{𝑒} C$
57	56	adantlr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C \in ℝ) \land A = +∞) \to A +_{𝑒} C \leq B +_{𝑒} C$
58		oveq1	$⊢ A = −∞ \to A +_{𝑒} C = −∞ +_{𝑒} C$
59		renepnf	$⊢ C \in ℝ \to C \neq +∞$
60		xaddmnf2	$⊢ (C \in ℝ^{*} \land C \neq +∞) \to −∞ +_{𝑒} C = −∞$
61	17 59 60	syl2anc	$⊢ C \in ℝ \to −∞ +_{𝑒} C = −∞$
62	61	adantl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C \in ℝ) \to −∞ +_{𝑒} C = −∞$
63	58 62	sylan9eqr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C \in ℝ) \land A = −∞) \to A +_{𝑒} C = −∞$
64		xaddcl	$⊢ (B \in ℝ^{} \land C \in ℝ^{}) \to B +_{𝑒} C \in ℝ^{*}$
65	32 10 64	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \to B +_{𝑒} C \in ℝ^{}$
66	65	ad2antrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \land C \in ℝ) \land A = −∞) \to B +_{𝑒} C \in ℝ^{}$
67		mnfle	$⊢ B +_{𝑒} C \in ℝ^{*} \to −∞ \leq B +_{𝑒} C$
68	66 67	syl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C \in ℝ) \land A = −∞) \to −∞ \leq B +_{𝑒} C$
69	63 68	eqbrtrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C \in ℝ) \land A = −∞) \to A +_{𝑒} C \leq B +_{𝑒} C$
70		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
71	9 70	sylib	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to (A \in ℝ \lor A = +∞ \lor A = −∞)$
72	71	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C \in ℝ) \to (A \in ℝ \lor A = +∞ \lor A = −∞)$
73	44 57 69 72	mpjao3dan	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C \in ℝ) \to A +_{𝑒} C \leq B +_{𝑒} C$
74	38	adantlr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = +∞) \land B = −∞) \to A +_{𝑒} C \leq B +_{𝑒} C$
75	12	ad2antrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \land C = +∞) \land B \neq −∞) \to A +_{𝑒} C \in ℝ^{}$
76	75 14	syl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = +∞) \land B \neq −∞) \to A +_{𝑒} C \leq +∞$
77		simplr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = +∞) \land B \neq −∞) \to C = +∞$
78	77	oveq2d	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = +∞) \land B \neq −∞) \to B +_{𝑒} C = B +_{𝑒} +∞$
79	32	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \land C = +∞) \to B \in ℝ^{}$
80		xaddpnf1	$⊢ (B \in ℝ^{*} \land B \neq −∞) \to B +_{𝑒} +∞ = +∞$
81	79 80	sylan	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = +∞) \land B \neq −∞) \to B +_{𝑒} +∞ = +∞$
82	78 81	eqtrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = +∞) \land B \neq −∞) \to B +_{𝑒} C = +∞$
83	76 82	breqtrrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = +∞) \land B \neq −∞) \to A +_{𝑒} C \leq B +_{𝑒} C$
84	74 83	pm2.61dane	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = +∞) \to A +_{𝑒} C \leq B +_{𝑒} C$
85	56	adantlr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = −∞) \land A = +∞) \to A +_{𝑒} C \leq B +_{𝑒} C$
86		simplr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = −∞) \land A \neq +∞) \to C = −∞$
87	86	oveq2d	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = −∞) \land A \neq +∞) \to A +_{𝑒} C = A +_{𝑒} −∞$
88	9	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \land C = −∞) \to A \in ℝ^{}$
89		xaddmnf1	$⊢ (A \in ℝ^{*} \land A \neq +∞) \to A +_{𝑒} −∞ = −∞$
90	88 89	sylan	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = −∞) \land A \neq +∞) \to A +_{𝑒} −∞ = −∞$
91	87 90	eqtrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = −∞) \land A \neq +∞) \to A +_{𝑒} C = −∞$
92	65	ad2antrr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{}) \land A \leq B) \land C = −∞) \land A \neq +∞) \to B +_{𝑒} C \in ℝ^{}$
93	92 67	syl	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = −∞) \land A \neq +∞) \to −∞ \leq B +_{𝑒} C$
94	91 93	eqbrtrd	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = −∞) \land A \neq +∞) \to A +_{𝑒} C \leq B +_{𝑒} C$
95	85 94	pm2.61dane	$⊢ (((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \land C = −∞) \to A +_{𝑒} C \leq B +_{𝑒} C$
96		elxr	$⊢ C \in ℝ^{*} \leftrightarrow (C \in ℝ \lor C = +∞ \lor C = −∞)$
97	10 96	sylib	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to (C \in ℝ \lor C = +∞ \lor C = −∞)$
98	73 84 95 97	mpjao3dan	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land A \leq B) \to A +_{𝑒} C \leq B +_{𝑒} C$

Metamath Proof Explorer

Theorem xleadd1a

Proof