xposdif - Intuitionistic Logic Explorer

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

Theorem xposdif 9839

Description: Extended real version of posdif 8374. (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 9733	. . 3 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
2		elxr 9733	. . . . 5 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
3		posdif 8374	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
4		rexsub 9810	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 − 𝐴))
5	4	ancoms 266	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 − 𝐴))
6	5	breq2d 4001	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < (𝐵 − 𝐴)))
7	3, 6	bitr4d 190	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
8	7	ex 114	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
9		rexr 7965	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
10		pnfnlt 9744	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ^* → ¬ +∞ < 𝐵)
11	10	adantl 275	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ +∞ < 𝐵)
12	9, 11	sylan2 284	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ +∞ < 𝐵)
13		simpl 108	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐴 = +∞)
14	13	breq1d 3999	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
15	12, 14	mtbird 668	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ 𝐴 < 𝐵)
16		0xr 7966	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
17		nltmnf 9745	. . . . . . . . . 10 ⊢ (0 ∈ ℝ^* → ¬ 0 < -∞)
18	16, 17	ax-mp 5	. . . . . . . . 9 ⊢ ¬ 0 < -∞
19		xnegeq 9784	. . . . . . . . . . . . . 14 ⊢ (𝐴 = +∞ → -_𝑒𝐴 = -_𝑒+∞)
20	19	adantr 274	. . . . . . . . . . . . 13 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → -_𝑒𝐴 = -_𝑒+∞)
21		xnegpnf 9785	. . . . . . . . . . . . 13 ⊢ -_𝑒+∞ = -∞
22	20, 21	eqtrdi 2219	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → -_𝑒𝐴 = -∞)
23	22	oveq2d 5869	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
24		renepnf 7967	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ +∞)
25	24	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ +∞)
26		xaddmnf1 9805	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (𝐵 +_𝑒 -∞) = -∞)
27	9, 25, 26	syl2an2 589	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -∞) = -∞)
28	23, 27	eqtrd 2203	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
29	28	breq2d 4001	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
30	18, 29	mtbiri 670	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
31	15, 30	2falsed 697	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
32	31	ex 114	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
33		simpl 108	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐴 = -∞)
34		mnflt 9740	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → -∞ < 𝐵)
35	34	adantl 275	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → -∞ < 𝐵)
36	33, 35	eqbrtrd 4011	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐴 < 𝐵)
37		0ltpnf 9739	. . . . . . . . 9 ⊢ 0 < +∞
38		xnegeq 9784	. . . . . . . . . . . . 13 ⊢ (𝐴 = -∞ → -_𝑒𝐴 = -_𝑒-∞)
39		xnegmnf 9786	. . . . . . . . . . . . 13 ⊢ -_𝑒-∞ = +∞
40	38, 39	eqtrdi 2219	. . . . . . . . . . . 12 ⊢ (𝐴 = -∞ → -_𝑒𝐴 = +∞)
41	40	oveq2d 5869	. . . . . . . . . . 11 ⊢ (𝐴 = -∞ → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 +∞))
42	41	adantr 274	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 +∞))
43		renemnf 7968	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ -∞)
44	43	adantl 275	. . . . . . . . . . 11 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ -∞)
45		xaddpnf1 9803	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (𝐵 +_𝑒 +∞) = +∞)
46	9, 44, 45	syl2an2 589	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 +∞) = +∞)
47	42, 46	eqtrd 2203	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
48	37, 47	breqtrrid 4027	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
49	36, 48	2thd 174	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
50	49	ex 114	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
51	8, 32, 50	3jaoi 1298	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
52	2, 51	sylbi 120	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
53		ltpnf 9737	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
54	53	adantr 274	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < +∞)
55		simpr 109	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐵 = +∞)
56	54, 55	breqtrrd 4017	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
57	55	oveq1d 5868	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 -_𝑒𝐴))
58		rexneg 9787	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 = -𝐴)
59		renegcl 8180	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
60	58, 59	eqeltrd 2247	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ)
61	60	rexrd 7969	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ^*)
62	61	adantr 274	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -_𝑒𝐴 ∈ ℝ^*)
63	60	renemnfd 7971	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ≠ -∞)
64	63	adantr 274	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -_𝑒𝐴 ≠ -∞)
65		xaddpnf2 9804	. . . . . . . . . . 11 ⊢ ((-_𝑒𝐴 ∈ ℝ^* ∧ -_𝑒𝐴 ≠ -∞) → (+∞ +_𝑒 -_𝑒𝐴) = +∞)
66	62, 64, 65	syl2anc 409	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (+∞ +_𝑒 -_𝑒𝐴) = +∞)
67	57, 66	eqtrd 2203	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
68	37, 67	breqtrrid 4027	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
69	56, 68	2thd 174	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
70	69	ex 114	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
71		pnfxr 7972	. . . . . . . . . 10 ⊢ +∞ ∈ ℝ^*
72		xrltnr 9736	. . . . . . . . . 10 ⊢ (+∞ ∈ ℝ^* → ¬ +∞ < +∞)
73	71, 72	ax-mp 5	. . . . . . . . 9 ⊢ ¬ +∞ < +∞
74		breq12 3994	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ +∞ < +∞))
75	73, 74	mtbiri 670	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → ¬ 𝐴 < 𝐵)
76		0re 7920	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
77	76	ltnri 8012	. . . . . . . . 9 ⊢ ¬ 0 < 0
78		simpr 109	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → 𝐵 = +∞)
79	19, 21	eqtrdi 2219	. . . . . . . . . . . . 13 ⊢ (𝐴 = +∞ → -_𝑒𝐴 = -∞)
80	79	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → -_𝑒𝐴 = -∞)
81	78, 80	oveq12d 5871	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 -∞))
82		pnfaddmnf 9807	. . . . . . . . . . 11 ⊢ (+∞ +_𝑒 -∞) = 0
83	81, 82	eqtrdi 2219	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = 0)
84	83	breq2d 4001	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < 0))
85	77, 84	mtbiri 670	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
86	75, 85	2falsed 697	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
87	86	ex 114	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
88		mnfltpnf 9742	. . . . . . . . 9 ⊢ -∞ < +∞
89		breq12 3994	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ -∞ < +∞))
90	88, 89	mpbiri 167	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
91		oveq1 5860	. . . . . . . . . . 11 ⊢ (𝐵 = +∞ → (𝐵 +_𝑒 +∞) = (+∞ +_𝑒 +∞))
92	41, 91	sylan9eq 2223	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 +∞))
93		pnfnemnf 7974	. . . . . . . . . . 11 ⊢ +∞ ≠ -∞
94		xaddpnf1 9803	. . . . . . . . . . 11 ⊢ ((+∞ ∈ ℝ^* ∧ +∞ ≠ -∞) → (+∞ +_𝑒 +∞) = +∞)
95	71, 93, 94	mp2an 424	. . . . . . . . . 10 ⊢ (+∞ +_𝑒 +∞) = +∞
96	92, 95	eqtrdi 2219	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
97	37, 96	breqtrrid 4027	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
98	90, 97	2thd 174	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
99	98	ex 114	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
100	70, 87, 99	3jaoi 1298	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
101	2, 100	sylbi 120	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
102		rexr 7965	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
103	102	adantr 274	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐴 ∈ ℝ^*)
104		nltmnf 9745	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)
105	103, 104	syl 14	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
106		simpr 109	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐵 = -∞)
107	106	breq2d 4001	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
108	105, 107	mtbird 668	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
109	106	oveq1d 5868	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (-∞ +_𝑒 -_𝑒𝐴))
110		rexr 7965	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ^*)
111		renepnf 7967	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝐴 ∈ ℝ → -_𝑒𝐴 ≠ +∞)
112		xaddmnf2 9806	. . . . . . . . . . . . . 14 ⊢ ((-_𝑒𝐴 ∈ ℝ^* ∧ -_𝑒𝐴 ≠ +∞) → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
113	110, 111, 112	syl2anc 409	. . . . . . . . . . . . 13 ⊢ (-_𝑒𝐴 ∈ ℝ → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
114	60, 113	syl 14	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
115	114	adantr 274	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
116	109, 115	eqtrd 2203	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
117	116	breq2d 4001	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
118	18, 117	mtbiri 670	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
119	108, 118	2falsed 697	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
120	119	ex 114	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
121		eleq1 2233	. . . . . . . . . . . 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 4001	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
127	124, 126	mtbird 668	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
128	79	oveq2d 5869	. . . . . . . . . . . 12 ⊢ (𝐴 = +∞ → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
129	128	adantr 274	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
130		mnfxr 7976	. . . . . . . . . . . . 13 ⊢ -∞ ∈ ℝ^*
131		eleq1 2233	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → (𝐵 ∈ ℝ^* ↔ -∞ ∈ ℝ^*))
132	130, 131	mpbiri 167	. . . . . . . . . . . 12 ⊢ (𝐵 = -∞ → 𝐵 ∈ ℝ^*)
133		mnfnepnf 7975	. . . . . . . . . . . . . 14 ⊢ -∞ ≠ +∞
134		neeq1 2353	. . . . . . . . . . . . . 14 ⊢ (𝐵 = -∞ → (𝐵 ≠ +∞ ↔ -∞ ≠ +∞))
135	133, 134	mpbiri 167	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → 𝐵 ≠ +∞)
136	135	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐵 ≠ +∞)
137	132, 136, 26	syl2an2 589	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -∞) = -∞)
138	129, 137	eqtrd 2203	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
139	138	breq2d 4001	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
140	18, 139	mtbiri 670	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
141	127, 140	2falsed 697	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
142	141	ex 114	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
143		xrltnr 9736	. . . . . . . . . 10 ⊢ (-∞ ∈ ℝ^* → ¬ -∞ < -∞)
144	130, 143	ax-mp 5	. . . . . . . . 9 ⊢ ¬ -∞ < -∞
145		breq12 3994	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ -∞ < -∞))
146	144, 145	mtbiri 670	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
147		oveq1 5860	. . . . . . . . . . . 12 ⊢ (𝐵 = -∞ → (𝐵 +_𝑒 +∞) = (-∞ +_𝑒 +∞))
148	41, 147	sylan9eq 2223	. . . . . . . . . . 11 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (-∞ +_𝑒 +∞))
149		mnfaddpnf 9808	. . . . . . . . . . 11 ⊢ (-∞ +_𝑒 +∞) = 0
150	148, 149	eqtrdi 2219	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = 0)
151	150	breq2d 4001	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < 0))
152	77, 151	mtbiri 670	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
153	146, 152	2falsed 697	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
154	153	ex 114	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
155	120, 142, 154	3jaoi 1298	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
156	2, 155	sylbi 120	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
157	52, 101, 156	3jaod 1299	. . 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 972 = wceq 1348 ∈ wcel 2141 ≠ wne 2340 class class class wbr 3989 (class class class)co 5853 ℝcr 7773 0cc0 7774 +∞cpnf 7951 -∞cmnf 7952 ℝ^*cxr 7953 < clt 7954 − cmin 8090 -cneg 8091 -_𝑒cxne 9726 +_𝑒 cxad 9727

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 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-sep 4107 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-addcom 7874 ax-addass 7876 ax-distr 7878 ax-i2m1 7879 ax-0id 7882 ax-rnegex 7883 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltadd 7890

This theorem depends on definitions: df-bi 116 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rab 2457 df-v 2732 df-sbc 2956 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-if 3527 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-br 3990 df-opab 4051 df-id 4278 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-iota 5160 df-fun 5200 df-fv 5206 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-sub 8092 df-neg 8093 df-xneg 9729 df-xadd 9730

This theorem is referenced by: (None)

W3C validator