xposdif - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > xposdif		GIF version

Theorem xposdif 9818

Description: Extended real version of posdif 8353. (Contributed by Mario Carneiro, 24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.)

**Assertion**
Ref	Expression
xposdif	⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))

**Proof of Theorem xposdif**
Step	Hyp	Ref	Expression
1		elxr 9712	. . 3 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
2		elxr 9712	. . . . 5 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
3		posdif 8353	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
4		rexsub 9789	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 − 𝐴))
5	4	ancoms 266	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 − 𝐴))
6	5	breq2d 3994	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < (𝐵 − 𝐴)))
7	3, 6	bitr4d 190	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
8	7	ex 114	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
9		rexr 7944	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
10		pnfnlt 9723	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ^* → ¬ +∞ < 𝐵)
11	10	adantl 275	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ +∞ < 𝐵)
12	9, 11	sylan2 284	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ +∞ < 𝐵)
13		simpl 108	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐴 = +∞)
14	13	breq1d 3992	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
15	12, 14	mtbird 663	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ 𝐴 < 𝐵)
16		0xr 7945	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
17		nltmnf 9724	. . . . . . . . . 10 ⊢ (0 ∈ ℝ^* → ¬ 0 < -∞)
18	16, 17	ax-mp 5	. . . . . . . . 9 ⊢ ¬ 0 < -∞
19		xnegeq 9763	. . . . . . . . . . . . . 14 ⊢ (𝐴 = +∞ → -_𝑒𝐴 = -_𝑒+∞)
20	19	adantr 274	. . . . . . . . . . . . 13 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → -_𝑒𝐴 = -_𝑒+∞)
21		xnegpnf 9764	. . . . . . . . . . . . 13 ⊢ -_𝑒+∞ = -∞
22	20, 21	eqtrdi 2215	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → -_𝑒𝐴 = -∞)
23	22	oveq2d 5858	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
24		renepnf 7946	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ +∞)
25	24	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ +∞)
26		xaddmnf1 9784	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (𝐵 +_𝑒 -∞) = -∞)
27	9, 25, 26	syl2an2 584	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -∞) = -∞)
28	23, 27	eqtrd 2198	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
29	28	breq2d 3994	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
30	18, 29	mtbiri 665	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
31	15, 30	2falsed 692	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
32	31	ex 114	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
33		simpl 108	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐴 = -∞)
34		mnflt 9719	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → -∞ < 𝐵)
35	34	adantl 275	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → -∞ < 𝐵)
36	33, 35	eqbrtrd 4004	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐴 < 𝐵)
37		0ltpnf 9718	. . . . . . . . 9 ⊢ 0 < +∞
38		xnegeq 9763	. . . . . . . . . . . . 13 ⊢ (𝐴 = -∞ → -_𝑒𝐴 = -_𝑒-∞)
39		xnegmnf 9765	. . . . . . . . . . . . 13 ⊢ -_𝑒-∞ = +∞
40	38, 39	eqtrdi 2215	. . . . . . . . . . . 12 ⊢ (𝐴 = -∞ → -_𝑒𝐴 = +∞)
41	40	oveq2d 5858	. . . . . . . . . . 11 ⊢ (𝐴 = -∞ → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 +∞))
42	41	adantr 274	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 +∞))
43		renemnf 7947	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ -∞)
44	43	adantl 275	. . . . . . . . . . 11 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ -∞)
45		xaddpnf1 9782	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (𝐵 +_𝑒 +∞) = +∞)
46	9, 44, 45	syl2an2 584	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 +∞) = +∞)
47	42, 46	eqtrd 2198	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
48	37, 47	breqtrrid 4020	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
49	36, 48	2thd 174	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
50	49	ex 114	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
51	8, 32, 50	3jaoi 1293	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
52	2, 51	sylbi 120	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
53		ltpnf 9716	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
54	53	adantr 274	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < +∞)
55		simpr 109	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐵 = +∞)
56	54, 55	breqtrrd 4010	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
57	55	oveq1d 5857	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 -_𝑒𝐴))
58		rexneg 9766	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 = -𝐴)
59		renegcl 8159	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
60	58, 59	eqeltrd 2243	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ)
61	60	rexrd 7948	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ^*)
62	61	adantr 274	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -_𝑒𝐴 ∈ ℝ^*)
63	60	renemnfd 7950	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ≠ -∞)
64	63	adantr 274	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -_𝑒𝐴 ≠ -∞)
65		xaddpnf2 9783	. . . . . . . . . . 11 ⊢ ((-_𝑒𝐴 ∈ ℝ^* ∧ -_𝑒𝐴 ≠ -∞) → (+∞ +_𝑒 -_𝑒𝐴) = +∞)
66	62, 64, 65	syl2anc 409	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (+∞ +_𝑒 -_𝑒𝐴) = +∞)
67	57, 66	eqtrd 2198	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
68	37, 67	breqtrrid 4020	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
69	56, 68	2thd 174	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
70	69	ex 114	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
71		pnfxr 7951	. . . . . . . . . 10 ⊢ +∞ ∈ ℝ^*
72		xrltnr 9715	. . . . . . . . . 10 ⊢ (+∞ ∈ ℝ^* → ¬ +∞ < +∞)
73	71, 72	ax-mp 5	. . . . . . . . 9 ⊢ ¬ +∞ < +∞
74		breq12 3987	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ +∞ < +∞))
75	73, 74	mtbiri 665	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → ¬ 𝐴 < 𝐵)
76		0re 7899	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
77	76	ltnri 7991	. . . . . . . . 9 ⊢ ¬ 0 < 0
78		simpr 109	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → 𝐵 = +∞)
79	19, 21	eqtrdi 2215	. . . . . . . . . . . . 13 ⊢ (𝐴 = +∞ → -_𝑒𝐴 = -∞)
80	79	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → -_𝑒𝐴 = -∞)
81	78, 80	oveq12d 5860	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 -∞))
82		pnfaddmnf 9786	. . . . . . . . . . 11 ⊢ (+∞ +_𝑒 -∞) = 0
83	81, 82	eqtrdi 2215	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = 0)
84	83	breq2d 3994	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < 0))
85	77, 84	mtbiri 665	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
86	75, 85	2falsed 692	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
87	86	ex 114	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
88		mnfltpnf 9721	. . . . . . . . 9 ⊢ -∞ < +∞
89		breq12 3987	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ -∞ < +∞))
90	88, 89	mpbiri 167	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
91		oveq1 5849	. . . . . . . . . . 11 ⊢ (𝐵 = +∞ → (𝐵 +_𝑒 +∞) = (+∞ +_𝑒 +∞))
92	41, 91	sylan9eq 2219	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 +∞))
93		pnfnemnf 7953	. . . . . . . . . . 11 ⊢ +∞ ≠ -∞
94		xaddpnf1 9782	. . . . . . . . . . 11 ⊢ ((+∞ ∈ ℝ^* ∧ +∞ ≠ -∞) → (+∞ +_𝑒 +∞) = +∞)
95	71, 93, 94	mp2an 423	. . . . . . . . . 10 ⊢ (+∞ +_𝑒 +∞) = +∞
96	92, 95	eqtrdi 2215	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
97	37, 96	breqtrrid 4020	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
98	90, 97	2thd 174	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
99	98	ex 114	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
100	70, 87, 99	3jaoi 1293	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
101	2, 100	sylbi 120	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
102		rexr 7944	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
103	102	adantr 274	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐴 ∈ ℝ^*)
104		nltmnf 9724	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)
105	103, 104	syl 14	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
106		simpr 109	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐵 = -∞)
107	106	breq2d 3994	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
108	105, 107	mtbird 663	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
109	106	oveq1d 5857	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (-∞ +_𝑒 -_𝑒𝐴))
110		rexr 7944	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ^*)
111		renepnf 7946	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝐴 ∈ ℝ → -_𝑒𝐴 ≠ +∞)
112		xaddmnf2 9785	. . . . . . . . . . . . . 14 ⊢ ((-_𝑒𝐴 ∈ ℝ^* ∧ -_𝑒𝐴 ≠ +∞) → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
113	110, 111, 112	syl2anc 409	. . . . . . . . . . . . 13 ⊢ (-_𝑒𝐴 ∈ ℝ → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
114	60, 113	syl 14	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
115	114	adantr 274	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
116	109, 115	eqtrd 2198	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
117	116	breq2d 3994	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
118	18, 117	mtbiri 665	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
119	108, 118	2falsed 692	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
120	119	ex 114	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
121		eleq1 2229	. . . . . . . . . . . 12 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ^* ↔ +∞ ∈ ℝ^*))
122	71, 121	mpbiri 167	. . . . . . . . . . 11 ⊢ (𝐴 = +∞ → 𝐴 ∈ ℝ^*)
123	122	adantr 274	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐴 ∈ ℝ^*)
124	123, 104	syl 14	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
125		simpr 109	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐵 = -∞)
126	125	breq2d 3994	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
127	124, 126	mtbird 663	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
128	79	oveq2d 5858	. . . . . . . . . . . 12 ⊢ (𝐴 = +∞ → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
129	128	adantr 274	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
130		mnfxr 7955	. . . . . . . . . . . . 13 ⊢ -∞ ∈ ℝ^*
131		eleq1 2229	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → (𝐵 ∈ ℝ^* ↔ -∞ ∈ ℝ^*))
132	130, 131	mpbiri 167	. . . . . . . . . . . 12 ⊢ (𝐵 = -∞ → 𝐵 ∈ ℝ^*)
133		mnfnepnf 7954	. . . . . . . . . . . . . 14 ⊢ -∞ ≠ +∞
134		neeq1 2349	. . . . . . . . . . . . . 14 ⊢ (𝐵 = -∞ → (𝐵 ≠ +∞ ↔ -∞ ≠ +∞))
135	133, 134	mpbiri 167	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → 𝐵 ≠ +∞)
136	135	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐵 ≠ +∞)
137	132, 136, 26	syl2an2 584	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -∞) = -∞)
138	129, 137	eqtrd 2198	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
139	138	breq2d 3994	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
140	18, 139	mtbiri 665	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
141	127, 140	2falsed 692	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
142	141	ex 114	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
143		xrltnr 9715	. . . . . . . . . 10 ⊢ (-∞ ∈ ℝ^* → ¬ -∞ < -∞)
144	130, 143	ax-mp 5	. . . . . . . . 9 ⊢ ¬ -∞ < -∞
145		breq12 3987	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ -∞ < -∞))
146	144, 145	mtbiri 665	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
147		oveq1 5849	. . . . . . . . . . . 12 ⊢ (𝐵 = -∞ → (𝐵 +_𝑒 +∞) = (-∞ +_𝑒 +∞))
148	41, 147	sylan9eq 2219	. . . . . . . . . . 11 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (-∞ +_𝑒 +∞))
149		mnfaddpnf 9787	. . . . . . . . . . 11 ⊢ (-∞ +_𝑒 +∞) = 0
150	148, 149	eqtrdi 2215	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = 0)
151	150	breq2d 3994	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < 0))
152	77, 151	mtbiri 665	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
153	146, 152	2falsed 692	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
154	153	ex 114	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
155	120, 142, 154	3jaoi 1293	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
156	2, 155	sylbi 120	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
157	52, 101, 156	3jaod 1294	. . 3 ⊢ (𝐴 ∈ ℝ^* → ((𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
158	1, 157	syl5bi 151	. 2 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ ℝ^* → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
159	158	imp 123	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ w3o 967 = wceq 1343 ∈ wcel 2136 ≠ wne 2336 class class class wbr 3982 (class class class)co 5842 ℝcr 7752 0cc0 7753 +∞cpnf 7930 -∞cmnf 7931 ℝ^*cxr 7932 < clt 7933 − cmin 8069 -cneg 8070 -_𝑒cxne 9705 +_𝑒 cxad 9706

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-sep 4100 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-addcom 7853 ax-addass 7855 ax-distr 7857 ax-i2m1 7858 ax-0id 7861 ax-rnegex 7862 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltadd 7869

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rab 2453 df-v 2728 df-sbc 2952 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-if 3521 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-br 3983 df-opab 4044 df-id 4271 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-iota 5153 df-fun 5190 df-fv 5196 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-sub 8071 df-neg 8072 df-xneg 9708 df-xadd 9709

This theorem is referenced by: (None)

W3C validator