Theorem xlt2add 9972

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

Assertion

Ref	Expression
xlt2add	⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷)))

Proof of Theorem xlt2add

Step	Hyp	Ref	Expression
1		xaddcl 9952	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
2	1	3ad2ant1 1020	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
3	2	adantr 276	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐴 +𝑒 𝐵) ∈ ℝ*)
4		simp1l 1023	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐴 ∈ ℝ*)
5		simp2r 1026	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐷 ∈ ℝ*)
6		xaddcl 9952	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) → (𝐴 +𝑒 𝐷) ∈ ℝ*)
7	4, 5, 6	syl2anc 411	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (𝐴 +𝑒 𝐷) ∈ ℝ*)
8	7	adantr 276	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐴 +𝑒 𝐷) ∈ ℝ*)
9		xaddcl 9952	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) → (𝐶 +𝑒 𝐷) ∈ ℝ*)
10	9	3ad2ant2 1021	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (𝐶 +𝑒 𝐷) ∈ ℝ*)
11	10	adantr 276	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐶 +𝑒 𝐷) ∈ ℝ*)
12		simp3r 1028	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐵 < 𝐷)
13	12	adantr 276	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐵 < 𝐷)
14		simp1r 1024	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐵 ∈ ℝ*)
15	14	adantr 276	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐵 ∈ ℝ*)
16	5	adantr 276	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐷 ∈ ℝ*)
17		simprl 529	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐴 ∈ ℝ)
18		xltadd2 9969	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐴 ∈ ℝ) → (𝐵 < 𝐷 ↔ (𝐴 +𝑒 𝐵) < (𝐴 +𝑒 𝐷)))
19	15, 16, 17, 18	syl3anc 1249	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐵 < 𝐷 ↔ (𝐴 +𝑒 𝐵) < (𝐴 +𝑒 𝐷)))
20	13, 19	mpbid 147	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐴 +𝑒 𝐵) < (𝐴 +𝑒 𝐷))
21		simp3l 1027	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐴 < 𝐶)
22	21	adantr 276	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐴 < 𝐶)
23	4	adantr 276	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐴 ∈ ℝ*)
24		simp2l 1025	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐶 ∈ ℝ*)
25	24	adantr 276	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐶 ∈ ℝ*)
26		simprr 531	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → 𝐷 ∈ ℝ)
27		xltadd1 9968	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ) → (𝐴 < 𝐶 ↔ (𝐴 +𝑒 𝐷) < (𝐶 +𝑒 𝐷)))
28	23, 25, 26, 27	syl3anc 1249	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐴 < 𝐶 ↔ (𝐴 +𝑒 𝐷) < (𝐶 +𝑒 𝐷)))
29	22, 28	mpbid 147	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐴 +𝑒 𝐷) < (𝐶 +𝑒 𝐷))
30	3, 8, 11, 20, 29	xrlttrd 9901	. . . . 5 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ (𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))
31	30	anassrs 400	. . . 4 ⊢ (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐴 ∈ ℝ) ∧ 𝐷 ∈ ℝ) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))
32		pnfxr 8096	. . . . . . . . . . . 12 ⊢ +∞ ∈ ℝ*
33	32	a1i 9	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → +∞ ∈ ℝ*)
34		pnfge 9881	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ ℝ* → 𝐶 ≤ +∞)
35	24, 34	syl 14	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐶 ≤ +∞)
36	4, 24, 33, 21, 35	xrltletrd 9903	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐴 < +∞)
37		npnflt 9907	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ* → (𝐴 < +∞ ↔ 𝐴 ≠ +∞))
38	4, 37	syl 14	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (𝐴 < +∞ ↔ 𝐴 ≠ +∞))
39	36, 38	mpbid 147	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐴 ≠ +∞)
40		pnfge 9881	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ ℝ* → 𝐷 ≤ +∞)
41	5, 40	syl 14	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐷 ≤ +∞)
42	14, 5, 33, 12, 41	xrltletrd 9903	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐵 < +∞)
43		npnflt 9907	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ* → (𝐵 < +∞ ↔ 𝐵 ≠ +∞))
44	14, 43	syl 14	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (𝐵 < +∞ ↔ 𝐵 ≠ +∞))
45	42, 44	mpbid 147	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐵 ≠ +∞)
46		xaddnepnf 9950	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞) ∧ (𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞)) → (𝐴 +𝑒 𝐵) ≠ +∞)
47	4, 39, 14, 45, 46	syl22anc 1250	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (𝐴 +𝑒 𝐵) ≠ +∞)
48		npnflt 9907	. . . . . . . . 9 ⊢ ((𝐴 +𝑒 𝐵) ∈ ℝ* → ((𝐴 +𝑒 𝐵) < +∞ ↔ (𝐴 +𝑒 𝐵) ≠ +∞))
49	2, 48	syl 14	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → ((𝐴 +𝑒 𝐵) < +∞ ↔ (𝐴 +𝑒 𝐵) ≠ +∞))
50	47, 49	mpbird 167	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (𝐴 +𝑒 𝐵) < +∞)
51	50	adantr 276	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐷 = +∞) → (𝐴 +𝑒 𝐵) < +∞)
52		oveq2 5933	. . . . . . 7 ⊢ (𝐷 = +∞ → (𝐶 +𝑒 𝐷) = (𝐶 +𝑒 +∞))
53		mnfxr 8100	. . . . . . . . . . 11 ⊢ -∞ ∈ ℝ*
54	53	a1i 9	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → -∞ ∈ ℝ*)
55		mnfle 9884	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ* → -∞ ≤ 𝐴)
56	4, 55	syl 14	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → -∞ ≤ 𝐴)
57	54, 4, 24, 56, 21	xrlelttrd 9902	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → -∞ < 𝐶)
58		nmnfgt 9910	. . . . . . . . . 10 ⊢ (𝐶 ∈ ℝ* → (-∞ < 𝐶 ↔ 𝐶 ≠ -∞))
59	24, 58	syl 14	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (-∞ < 𝐶 ↔ 𝐶 ≠ -∞))
60	57, 59	mpbid 147	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐶 ≠ -∞)
61		xaddpnf1 9938	. . . . . . . 8 ⊢ ((𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞) → (𝐶 +𝑒 +∞) = +∞)
62	24, 60, 61	syl2anc 411	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (𝐶 +𝑒 +∞) = +∞)
63	52, 62	sylan9eqr 2251	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐷 = +∞) → (𝐶 +𝑒 𝐷) = +∞)
64	51, 63	breqtrrd 4062	. . . . 5 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐷 = +∞) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))
65	64	adantlr 477	. . . 4 ⊢ (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐴 ∈ ℝ) ∧ 𝐷 = +∞) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))
66		simpr 110	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐷 = -∞) → 𝐷 = -∞)
67		mnfle 9884	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ* → -∞ ≤ 𝐵)
68	14, 67	syl 14	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → -∞ ≤ 𝐵)
69	54, 14, 5, 68, 12	xrlelttrd 9902	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → -∞ < 𝐷)
70		nmnfgt 9910	. . . . . . . . 9 ⊢ (𝐷 ∈ ℝ* → (-∞ < 𝐷 ↔ 𝐷 ≠ -∞))
71	5, 70	syl 14	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (-∞ < 𝐷 ↔ 𝐷 ≠ -∞))
72	69, 71	mpbid 147	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → 𝐷 ≠ -∞)
73	72	adantr 276	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐷 = -∞) → 𝐷 ≠ -∞)
74	66, 73	pm2.21ddne 2450	. . . . 5 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐷 = -∞) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))
75	74	adantlr 477	. . . 4 ⊢ (((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐴 ∈ ℝ) ∧ 𝐷 = -∞) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))
76		elxr 9868	. . . . . 6 ⊢ (𝐷 ∈ ℝ* ↔ (𝐷 ∈ ℝ ∨ 𝐷 = +∞ ∨ 𝐷 = -∞))
77	5, 76	sylib 122	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (𝐷 ∈ ℝ ∨ 𝐷 = +∞ ∨ 𝐷 = -∞))
78	77	adantr 276	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐴 ∈ ℝ) → (𝐷 ∈ ℝ ∨ 𝐷 = +∞ ∨ 𝐷 = -∞))
79	31, 65, 75, 78	mpjao3dan 1318	. . 3 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐴 ∈ ℝ) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))
80		simpr 110	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐴 = +∞) → 𝐴 = +∞)
81	39	adantr 276	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐴 = +∞) → 𝐴 ≠ +∞)
82	80, 81	pm2.21ddne 2450	. . 3 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))
83		oveq1 5932	. . . . 5 ⊢ (𝐴 = -∞ → (𝐴 +𝑒 𝐵) = (-∞ +𝑒 𝐵))
84		xaddmnf2 9941	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝐵 ≠ +∞) → (-∞ +𝑒 𝐵) = -∞)
85	14, 45, 84	syl2anc 411	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (-∞ +𝑒 𝐵) = -∞)
86	83, 85	sylan9eqr 2251	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐴 = -∞) → (𝐴 +𝑒 𝐵) = -∞)
87		xaddnemnf 9949	. . . . . . 7 ⊢ (((𝐶 ∈ ℝ* ∧ 𝐶 ≠ -∞) ∧ (𝐷 ∈ ℝ* ∧ 𝐷 ≠ -∞)) → (𝐶 +𝑒 𝐷) ≠ -∞)
88	24, 60, 5, 72, 87	syl22anc 1250	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (𝐶 +𝑒 𝐷) ≠ -∞)
89		nmnfgt 9910	. . . . . . 7 ⊢ ((𝐶 +𝑒 𝐷) ∈ ℝ* → (-∞ < (𝐶 +𝑒 𝐷) ↔ (𝐶 +𝑒 𝐷) ≠ -∞))
90	10, 89	syl 14	. . . . . 6 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (-∞ < (𝐶 +𝑒 𝐷) ↔ (𝐶 +𝑒 𝐷) ≠ -∞))
91	88, 90	mpbird 167	. . . . 5 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → -∞ < (𝐶 +𝑒 𝐷))
92	91	adantr 276	. . . 4 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐴 = -∞) → -∞ < (𝐶 +𝑒 𝐷))
93	86, 92	eqbrtrd 4056	. . 3 ⊢ ((((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) ∧ 𝐴 = -∞) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))
94		elxr 9868	. . . 4 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
95	4, 94	sylib 122	. . 3 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
96	79, 82, 93, 95	mpjao3dan 1318	. 2 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*) ∧ (𝐴 < 𝐶 ∧ 𝐵 < 𝐷)) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷))
97	96	3expia 1207	1 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ*)) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐷) → (𝐴 +𝑒 𝐵) < (𝐶 +𝑒 𝐷)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ w3o 979   ∧ w3a 980   = wceq 1364   ∈ wcel 2167   ≠ wne 2367   class class class wbr 4034  (class class class)co 5925  ℝcr 7895  +∞cpnf 8075  -∞cmnf 8076  ℝ^*cxr 8077   < clt 8078   ≤ cle 8079   +_𝑒 cxad 9862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-pow 4208  ax-pr 4243  ax-un 4469  ax-setind 4574  ax-cnex 7987  ax-resscn 7988  ax-1cn 7989  ax-1re 7990  ax-icn 7991  ax-addcl 7992  ax-addrcl 7993  ax-mulcl 7994  ax-addcom 7996  ax-addass 7998  ax-i2m1 8001  ax-0id 8004  ax-rnegex 8005  ax-pre-ltirr 8008  ax-pre-ltwlin 8009  ax-pre-lttrn 8010  ax-pre-ltadd 8012

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-if 3563  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-iun 3919  df-br 4035  df-opab 4096  df-mpt 4097  df-id 4329  df-po 4332  df-iso 4333  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-rn 4675  df-res 4676  df-ima 4677  df-iota 5220  df-fun 5261  df-fn 5262  df-f 5263  df-fv 5267  df-ov 5928  df-oprab 5929  df-mpo 5930  df-1st 6207  df-2nd 6208  df-pnf 8080  df-mnf 8081  df-xr 8082  df-ltxr 8083  df-le 8084  df-xadd 9865

This theorem is referenced by:  bldisj  14721