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	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ) ) → ( ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐷 ) → ( 𝐴 +_𝑒 𝐵 ) < ( 𝐶 +_𝑒 𝐷 ) ) )

Proof

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

Metamath Proof Explorer

Theorem xlt2add

Proof