xlt2add

Description: Extended real version of lt2add . Note that ltleadd , which has weaker assumptions, is not true for the extended reals (since 0 + +oo < 1 + +oo fails). (Contributed by Mario Carneiro, 23-Aug-2015)

		Ref	Expression
	Assertion	xlt2add	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{})) \to ((A < C \land B < D) \to A +_{𝑒} B < C +_{𝑒} D)$

Proof

Step	Hyp	Ref	Expression
1		xaddcl	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A +_{𝑒} B \in ℝ^{*}$
2	1	3ad2ant1	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to A +_{𝑒} B \in ℝ^{*}$
3	2	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to A +_{𝑒} B \in ℝ^{*}$
4		simp1l	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to A \in ℝ^{*}$
5		simp2r	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to D \in ℝ^{*}$
6		xaddcl	$⊢ (A \in ℝ^{} \land D \in ℝ^{}) \to A +_{𝑒} D \in ℝ^{*}$
7	4 5 6	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to A +_{𝑒} D \in ℝ^{*}$
8	7	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to A +_{𝑒} D \in ℝ^{*}$
9		xaddcl	$⊢ (C \in ℝ^{} \land D \in ℝ^{}) \to C +_{𝑒} D \in ℝ^{*}$
10	9	3ad2ant2	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to C +_{𝑒} D \in ℝ^{*}$
11	10	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to C +_{𝑒} D \in ℝ^{*}$
12		simp3r	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to B < D$
13	12	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to B < D$
14		simp1r	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to B \in ℝ^{*}$
15	14	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to B \in ℝ^{*}$
16	5	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to D \in ℝ^{*}$
17		simprl	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to A \in ℝ$
18		xltadd2	$⊢ (B \in ℝ^{} \land D \in ℝ^{} \land A \in ℝ) \to (B < D \leftrightarrow A +_{𝑒} B < A +_{𝑒} D)$
19	15 16 17 18	syl3anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to (B < D \leftrightarrow A +_{𝑒} B < A +_{𝑒} D)$
20	13 19	mpbid	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to A +_{𝑒} B < A +_{𝑒} D$
21		simp3l	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to A < C$
22	21	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to A < C$
23	4	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to A \in ℝ^{*}$
24		simp2l	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to C \in ℝ^{*}$
25	24	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to C \in ℝ^{*}$
26		simprr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to D \in ℝ$
27		xltadd1	$⊢ (A \in ℝ^{} \land C \in ℝ^{} \land D \in ℝ) \to (A < C \leftrightarrow A +_{𝑒} D < C +_{𝑒} D)$
28	23 25 26 27	syl3anc	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to (A < C \leftrightarrow A +_{𝑒} D < C +_{𝑒} D)$
29	22 28	mpbid	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to A +_{𝑒} D < C +_{𝑒} D$
30	3 8 11 20 29	xrlttrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land (A \in ℝ \land D \in ℝ)) \to A +_{𝑒} B < C +_{𝑒} D$
31	30	anassrs	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land A \in ℝ) \land D \in ℝ) \to A +_{𝑒} B < C +_{𝑒} D$
32		pnfxr	$⊢ +∞ \in ℝ^{*}$
33	32	a1i	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to +∞ \in ℝ^{*}$
34		pnfge	$⊢ C \in ℝ^{*} \to C \leq +∞$
35	24 34	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to C \leq +∞$
36	4 24 33 21 35	xrltletrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to A < +∞$
37		nltpnft	$⊢ A \in ℝ^{*} \to (A = +∞ \leftrightarrow \neg A < +∞)$
38	37	necon2abid	$⊢ A \in ℝ^{*} \to (A < +∞ \leftrightarrow A \neq +∞)$
39	4 38	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to (A < +∞ \leftrightarrow A \neq +∞)$
40	36 39	mpbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to A \neq +∞$
41		pnfge	$⊢ D \in ℝ^{*} \to D \leq +∞$
42	5 41	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to D \leq +∞$
43	14 5 33 12 42	xrltletrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to B < +∞$
44		nltpnft	$⊢ B \in ℝ^{*} \to (B = +∞ \leftrightarrow \neg B < +∞)$
45	44	necon2abid	$⊢ B \in ℝ^{*} \to (B < +∞ \leftrightarrow B \neq +∞)$
46	14 45	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to (B < +∞ \leftrightarrow B \neq +∞)$
47	43 46	mpbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to B \neq +∞$
48		xaddnepnf	$⊢ ((A \in ℝ^{} \land A \neq +∞) \land (B \in ℝ^{} \land B \neq +∞)) \to A +_{𝑒} B \neq +∞$
49	4 40 14 47 48	syl22anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to A +_{𝑒} B \neq +∞$
50		nltpnft	$⊢ A +_{𝑒} B \in ℝ^{*} \to (A +_{𝑒} B = +∞ \leftrightarrow \neg A +_{𝑒} B < +∞)$
51	50	necon2abid	$⊢ A +_{𝑒} B \in ℝ^{*} \to (A +_{𝑒} B < +∞ \leftrightarrow A +_{𝑒} B \neq +∞)$
52	2 51	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to (A +_{𝑒} B < +∞ \leftrightarrow A +_{𝑒} B \neq +∞)$
53	49 52	mpbird	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to A +_{𝑒} B < +∞$
54	53	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land D = +∞) \to A +_{𝑒} B < +∞$
55		oveq2	$⊢ D = +∞ \to C +_{𝑒} D = C +_{𝑒} +∞$
56		mnfxr	$⊢ −∞ \in ℝ^{*}$
57	56	a1i	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to −∞ \in ℝ^{*}$
58		mnfle	$⊢ A \in ℝ^{*} \to −∞ \leq A$
59	4 58	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to −∞ \leq A$
60	57 4 24 59 21	xrlelttrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to −∞ < C$
61		ngtmnft	$⊢ C \in ℝ^{*} \to (C = −∞ \leftrightarrow \neg −∞ < C)$
62	61	necon2abid	$⊢ C \in ℝ^{*} \to (−∞ < C \leftrightarrow C \neq −∞)$
63	24 62	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to (−∞ < C \leftrightarrow C \neq −∞)$
64	60 63	mpbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to C \neq −∞$
65		xaddpnf1	$⊢ (C \in ℝ^{*} \land C \neq −∞) \to C +_{𝑒} +∞ = +∞$
66	24 64 65	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to C +_{𝑒} +∞ = +∞$
67	55 66	sylan9eqr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land D = +∞) \to C +_{𝑒} D = +∞$
68	54 67	breqtrrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land D = +∞) \to A +_{𝑒} B < C +_{𝑒} D$
69	68	adantlr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land A \in ℝ) \land D = +∞) \to A +_{𝑒} B < C +_{𝑒} D$
70		mnfle	$⊢ B \in ℝ^{*} \to −∞ \leq B$
71	14 70	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to −∞ \leq B$
72	57 14 5 71 12	xrlelttrd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to −∞ < D$
73		ngtmnft	$⊢ D \in ℝ^{*} \to (D = −∞ \leftrightarrow \neg −∞ < D)$
74	73	necon2abid	$⊢ D \in ℝ^{*} \to (−∞ < D \leftrightarrow D \neq −∞)$
75	5 74	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to (−∞ < D \leftrightarrow D \neq −∞)$
76	72 75	mpbid	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to D \neq −∞$
77	76	a1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to (\neg A +_{𝑒} B < C +_{𝑒} D \to D \neq −∞)$
78	77	necon4bd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to (D = −∞ \to A +_{𝑒} B < C +_{𝑒} D)$
79	78	imp	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land D = −∞) \to A +_{𝑒} B < C +_{𝑒} D$
80	79	adantlr	$⊢ ((((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land A \in ℝ) \land D = −∞) \to A +_{𝑒} B < C +_{𝑒} D$
81		elxr	$⊢ D \in ℝ^{*} \leftrightarrow (D \in ℝ \lor D = +∞ \lor D = −∞)$
82	5 81	sylib	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to (D \in ℝ \lor D = +∞ \lor D = −∞)$
83	82	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land A \in ℝ) \to (D \in ℝ \lor D = +∞ \lor D = −∞)$
84	31 69 80 83	mpjao3dan	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land A \in ℝ) \to A +_{𝑒} B < C +_{𝑒} D$
85	40	a1d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to (\neg A +_{𝑒} B < C +_{𝑒} D \to A \neq +∞)$
86	85	necon4bd	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to (A = +∞ \to A +_{𝑒} B < C +_{𝑒} D)$
87	86	imp	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land A = +∞) \to A +_{𝑒} B < C +_{𝑒} D$
88		oveq1	$⊢ A = −∞ \to A +_{𝑒} B = −∞ +_{𝑒} B$
89		xaddmnf2	$⊢ (B \in ℝ^{*} \land B \neq +∞) \to −∞ +_{𝑒} B = −∞$
90	14 47 89	syl2anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to −∞ +_{𝑒} B = −∞$
91	88 90	sylan9eqr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land A = −∞) \to A +_{𝑒} B = −∞$
92		xaddnemnf	$⊢ ((C \in ℝ^{} \land C \neq −∞) \land (D \in ℝ^{} \land D \neq −∞)) \to C +_{𝑒} D \neq −∞$
93	24 64 5 76 92	syl22anc	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to C +_{𝑒} D \neq −∞$
94		ngtmnft	$⊢ C +_{𝑒} D \in ℝ^{*} \to (C +_{𝑒} D = −∞ \leftrightarrow \neg −∞ < C +_{𝑒} D)$
95	94	necon2abid	$⊢ C +_{𝑒} D \in ℝ^{*} \to (−∞ < C +_{𝑒} D \leftrightarrow C +_{𝑒} D \neq −∞)$
96	10 95	syl	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to (−∞ < C +_{𝑒} D \leftrightarrow C +_{𝑒} D \neq −∞)$
97	93 96	mpbird	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to −∞ < C +_{𝑒} D$
98	97	adantr	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land A = −∞) \to −∞ < C +_{𝑒} D$
99	91 98	eqbrtrd	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \land A = −∞) \to A +_{𝑒} B < C +_{𝑒} D$
100		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
101	4 100	sylib	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to (A \in ℝ \lor A = +∞ \lor A = −∞)$
102	84 87 99 101	mpjao3dan	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{}) \land (A < C \land B < D)) \to A +_{𝑒} B < C +_{𝑒} D$
103	102	3expia	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (C \in ℝ^{} \land D \in ℝ^{})) \to ((A < C \land B < D) \to A +_{𝑒} B < C +_{𝑒} D)$

Metamath Proof Explorer

Theorem xlt2add

Proof