xposdif - Intuitionistic Logic Explorer

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

Theorem xposdif 9948

Description: Extended real version of posdif 8474. (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 9842	. . 3 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
2		elxr 9842	. . . . 5 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
3		posdif 8474	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
4		rexsub 9919	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 − 𝐴))
5	4	ancoms 268	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 − 𝐴))
6	5	breq2d 4041	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < (𝐵 − 𝐴)))
7	3, 6	bitr4d 191	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
8	7	ex 115	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
9		rexr 8065	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
10		pnfnlt 9853	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ^* → ¬ +∞ < 𝐵)
11	10	adantl 277	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ +∞ < 𝐵)
12	9, 11	sylan2 286	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ +∞ < 𝐵)
13		simpl 109	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐴 = +∞)
14	13	breq1d 4039	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
15	12, 14	mtbird 674	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ 𝐴 < 𝐵)
16		0xr 8066	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
17		nltmnf 9854	. . . . . . . . . 10 ⊢ (0 ∈ ℝ^* → ¬ 0 < -∞)
18	16, 17	ax-mp 5	. . . . . . . . 9 ⊢ ¬ 0 < -∞
19		xnegeq 9893	. . . . . . . . . . . . . 14 ⊢ (𝐴 = +∞ → -_𝑒𝐴 = -_𝑒+∞)
20	19	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → -_𝑒𝐴 = -_𝑒+∞)
21		xnegpnf 9894	. . . . . . . . . . . . 13 ⊢ -_𝑒+∞ = -∞
22	20, 21	eqtrdi 2242	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → -_𝑒𝐴 = -∞)
23	22	oveq2d 5934	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
24		renepnf 8067	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ +∞)
25	24	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ +∞)
26		xaddmnf1 9914	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (𝐵 +_𝑒 -∞) = -∞)
27	9, 25, 26	syl2an2 594	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -∞) = -∞)
28	23, 27	eqtrd 2226	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
29	28	breq2d 4041	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
30	18, 29	mtbiri 676	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
31	15, 30	2falsed 703	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
32	31	ex 115	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
33		simpl 109	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐴 = -∞)
34		mnflt 9849	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → -∞ < 𝐵)
35	34	adantl 277	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → -∞ < 𝐵)
36	33, 35	eqbrtrd 4051	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐴 < 𝐵)
37		0ltpnf 9848	. . . . . . . . 9 ⊢ 0 < +∞
38		xnegeq 9893	. . . . . . . . . . . . 13 ⊢ (𝐴 = -∞ → -_𝑒𝐴 = -_𝑒-∞)
39		xnegmnf 9895	. . . . . . . . . . . . 13 ⊢ -_𝑒-∞ = +∞
40	38, 39	eqtrdi 2242	. . . . . . . . . . . 12 ⊢ (𝐴 = -∞ → -_𝑒𝐴 = +∞)
41	40	oveq2d 5934	. . . . . . . . . . 11 ⊢ (𝐴 = -∞ → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 +∞))
42	41	adantr 276	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 +∞))
43		renemnf 8068	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ -∞)
44	43	adantl 277	. . . . . . . . . . 11 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ -∞)
45		xaddpnf1 9912	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (𝐵 +_𝑒 +∞) = +∞)
46	9, 44, 45	syl2an2 594	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 +∞) = +∞)
47	42, 46	eqtrd 2226	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
48	37, 47	breqtrrid 4067	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
49	36, 48	2thd 175	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
50	49	ex 115	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
51	8, 32, 50	3jaoi 1314	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
52	2, 51	sylbi 121	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
53		ltpnf 9846	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
54	53	adantr 276	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < +∞)
55		simpr 110	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐵 = +∞)
56	54, 55	breqtrrd 4057	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
57	55	oveq1d 5933	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 -_𝑒𝐴))
58		rexneg 9896	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 = -𝐴)
59		renegcl 8280	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
60	58, 59	eqeltrd 2270	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ)
61	60	rexrd 8069	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ^*)
62	61	adantr 276	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -_𝑒𝐴 ∈ ℝ^*)
63	60	renemnfd 8071	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ≠ -∞)
64	63	adantr 276	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -_𝑒𝐴 ≠ -∞)
65		xaddpnf2 9913	. . . . . . . . . . 11 ⊢ ((-_𝑒𝐴 ∈ ℝ^* ∧ -_𝑒𝐴 ≠ -∞) → (+∞ +_𝑒 -_𝑒𝐴) = +∞)
66	62, 64, 65	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (+∞ +_𝑒 -_𝑒𝐴) = +∞)
67	57, 66	eqtrd 2226	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
68	37, 67	breqtrrid 4067	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
69	56, 68	2thd 175	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
70	69	ex 115	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
71		pnfxr 8072	. . . . . . . . . 10 ⊢ +∞ ∈ ℝ^*
72		xrltnr 9845	. . . . . . . . . 10 ⊢ (+∞ ∈ ℝ^* → ¬ +∞ < +∞)
73	71, 72	ax-mp 5	. . . . . . . . 9 ⊢ ¬ +∞ < +∞
74		breq12 4034	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ +∞ < +∞))
75	73, 74	mtbiri 676	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → ¬ 𝐴 < 𝐵)
76		0re 8019	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
77	76	ltnri 8112	. . . . . . . . 9 ⊢ ¬ 0 < 0
78		simpr 110	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → 𝐵 = +∞)
79	19, 21	eqtrdi 2242	. . . . . . . . . . . . 13 ⊢ (𝐴 = +∞ → -_𝑒𝐴 = -∞)
80	79	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → -_𝑒𝐴 = -∞)
81	78, 80	oveq12d 5936	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 -∞))
82		pnfaddmnf 9916	. . . . . . . . . . 11 ⊢ (+∞ +_𝑒 -∞) = 0
83	81, 82	eqtrdi 2242	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = 0)
84	83	breq2d 4041	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < 0))
85	77, 84	mtbiri 676	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
86	75, 85	2falsed 703	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
87	86	ex 115	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
88		mnfltpnf 9851	. . . . . . . . 9 ⊢ -∞ < +∞
89		breq12 4034	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ -∞ < +∞))
90	88, 89	mpbiri 168	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
91		oveq1 5925	. . . . . . . . . . 11 ⊢ (𝐵 = +∞ → (𝐵 +_𝑒 +∞) = (+∞ +_𝑒 +∞))
92	41, 91	sylan9eq 2246	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 +∞))
93		pnfnemnf 8074	. . . . . . . . . . 11 ⊢ +∞ ≠ -∞
94		xaddpnf1 9912	. . . . . . . . . . 11 ⊢ ((+∞ ∈ ℝ^* ∧ +∞ ≠ -∞) → (+∞ +_𝑒 +∞) = +∞)
95	71, 93, 94	mp2an 426	. . . . . . . . . 10 ⊢ (+∞ +_𝑒 +∞) = +∞
96	92, 95	eqtrdi 2242	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
97	37, 96	breqtrrid 4067	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
98	90, 97	2thd 175	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
99	98	ex 115	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
100	70, 87, 99	3jaoi 1314	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
101	2, 100	sylbi 121	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
102		rexr 8065	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
103	102	adantr 276	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐴 ∈ ℝ^*)
104		nltmnf 9854	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)
105	103, 104	syl 14	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
106		simpr 110	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐵 = -∞)
107	106	breq2d 4041	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
108	105, 107	mtbird 674	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
109	106	oveq1d 5933	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (-∞ +_𝑒 -_𝑒𝐴))
110		rexr 8065	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ^*)
111		renepnf 8067	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝐴 ∈ ℝ → -_𝑒𝐴 ≠ +∞)
112		xaddmnf2 9915	. . . . . . . . . . . . . 14 ⊢ ((-_𝑒𝐴 ∈ ℝ^* ∧ -_𝑒𝐴 ≠ +∞) → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
113	110, 111, 112	syl2anc 411	. . . . . . . . . . . . 13 ⊢ (-_𝑒𝐴 ∈ ℝ → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
114	60, 113	syl 14	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
115	114	adantr 276	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
116	109, 115	eqtrd 2226	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
117	116	breq2d 4041	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
118	18, 117	mtbiri 676	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
119	108, 118	2falsed 703	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
120	119	ex 115	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
121		eleq1 2256	. . . . . . . . . . . 12 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ^* ↔ +∞ ∈ ℝ^*))
122	71, 121	mpbiri 168	. . . . . . . . . . 11 ⊢ (𝐴 = +∞ → 𝐴 ∈ ℝ^*)
123	122	adantr 276	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐴 ∈ ℝ^*)
124	123, 104	syl 14	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
125		simpr 110	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐵 = -∞)
126	125	breq2d 4041	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
127	124, 126	mtbird 674	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
128	79	oveq2d 5934	. . . . . . . . . . . 12 ⊢ (𝐴 = +∞ → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
129	128	adantr 276	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
130		mnfxr 8076	. . . . . . . . . . . . 13 ⊢ -∞ ∈ ℝ^*
131		eleq1 2256	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → (𝐵 ∈ ℝ^* ↔ -∞ ∈ ℝ^*))
132	130, 131	mpbiri 168	. . . . . . . . . . . 12 ⊢ (𝐵 = -∞ → 𝐵 ∈ ℝ^*)
133		mnfnepnf 8075	. . . . . . . . . . . . . 14 ⊢ -∞ ≠ +∞
134		neeq1 2377	. . . . . . . . . . . . . 14 ⊢ (𝐵 = -∞ → (𝐵 ≠ +∞ ↔ -∞ ≠ +∞))
135	133, 134	mpbiri 168	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → 𝐵 ≠ +∞)
136	135	adantl 277	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐵 ≠ +∞)
137	132, 136, 26	syl2an2 594	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -∞) = -∞)
138	129, 137	eqtrd 2226	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
139	138	breq2d 4041	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
140	18, 139	mtbiri 676	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
141	127, 140	2falsed 703	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
142	141	ex 115	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
143		xrltnr 9845	. . . . . . . . . 10 ⊢ (-∞ ∈ ℝ^* → ¬ -∞ < -∞)
144	130, 143	ax-mp 5	. . . . . . . . 9 ⊢ ¬ -∞ < -∞
145		breq12 4034	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ -∞ < -∞))
146	144, 145	mtbiri 676	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
147		oveq1 5925	. . . . . . . . . . . 12 ⊢ (𝐵 = -∞ → (𝐵 +_𝑒 +∞) = (-∞ +_𝑒 +∞))
148	41, 147	sylan9eq 2246	. . . . . . . . . . 11 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (-∞ +_𝑒 +∞))
149		mnfaddpnf 9917	. . . . . . . . . . 11 ⊢ (-∞ +_𝑒 +∞) = 0
150	148, 149	eqtrdi 2242	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = 0)
151	150	breq2d 4041	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < 0))
152	77, 151	mtbiri 676	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
153	146, 152	2falsed 703	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
154	153	ex 115	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
155	120, 142, 154	3jaoi 1314	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
156	2, 155	sylbi 121	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
157	52, 101, 156	3jaod 1315	. . 3 ⊢ (𝐴 ∈ ℝ^* → ((𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
158	1, 157	biimtrid 152	. 2 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ ℝ^* → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
159	158	imp 124	1 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ w3o 979 = wceq 1364 ∈ wcel 2164 ≠ wne 2364 class class class wbr 4029 (class class class)co 5918 ℝcr 7871 0cc0 7872 +∞cpnf 8051 -∞cmnf 8052 ℝ^*cxr 8053 < clt 8054 − cmin 8190 -cneg 8191 -_𝑒cxne 9835 +_𝑒 cxad 9836

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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-sep 4147 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-addcom 7972 ax-addass 7974 ax-distr 7976 ax-i2m1 7977 ax-0id 7980 ax-rnegex 7981 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltadd 7988

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 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rab 2481 df-v 2762 df-sbc 2986 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-br 4030 df-opab 4091 df-id 4324 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-iota 5215 df-fun 5256 df-fv 5262 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-sub 8192 df-neg 8193 df-xneg 9838 df-xadd 9839

This theorem is referenced by: (None)

W3C validator