xposdif - Intuitionistic Logic Explorer

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

Theorem xposdif 9665

Description: Extended real version of posdif 8217. (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 9563	. . 3 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
2		elxr 9563	. . . . 5 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
3		posdif 8217	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
4		rexsub 9636	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 − 𝐴))
5	4	ancoms 266	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 − 𝐴))
6	5	breq2d 3941	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < (𝐵 − 𝐴)))
7	3, 6	bitr4d 190	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
8	7	ex 114	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
9		rexr 7811	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
10		pnfnlt 9573	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ^* → ¬ +∞ < 𝐵)
11	10	adantl 275	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ +∞ < 𝐵)
12	9, 11	sylan2 284	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ +∞ < 𝐵)
13		simpl 108	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐴 = +∞)
14	13	breq1d 3939	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
15	12, 14	mtbird 662	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ 𝐴 < 𝐵)
16		0xr 7812	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
17		nltmnf 9574	. . . . . . . . . 10 ⊢ (0 ∈ ℝ^* → ¬ 0 < -∞)
18	16, 17	ax-mp 5	. . . . . . . . 9 ⊢ ¬ 0 < -∞
19		xnegeq 9610	. . . . . . . . . . . . . 14 ⊢ (𝐴 = +∞ → -_𝑒𝐴 = -_𝑒+∞)
20	19	adantr 274	. . . . . . . . . . . . 13 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → -_𝑒𝐴 = -_𝑒+∞)
21		xnegpnf 9611	. . . . . . . . . . . . 13 ⊢ -_𝑒+∞ = -∞
22	20, 21	syl6eq 2188	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → -_𝑒𝐴 = -∞)
23	22	oveq2d 5790	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
24		renepnf 7813	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ +∞)
25	24	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ +∞)
26		xaddmnf1 9631	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (𝐵 +_𝑒 -∞) = -∞)
27	9, 25, 26	syl2an2 583	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -∞) = -∞)
28	23, 27	eqtrd 2172	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
29	28	breq2d 3941	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
30	18, 29	mtbiri 664	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
31	15, 30	2falsed 691	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
32	31	ex 114	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
33		simpl 108	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐴 = -∞)
34		mnflt 9569	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → -∞ < 𝐵)
35	34	adantl 275	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → -∞ < 𝐵)
36	33, 35	eqbrtrd 3950	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐴 < 𝐵)
37		0ltpnf 9568	. . . . . . . . 9 ⊢ 0 < +∞
38		xnegeq 9610	. . . . . . . . . . . . 13 ⊢ (𝐴 = -∞ → -_𝑒𝐴 = -_𝑒-∞)
39		xnegmnf 9612	. . . . . . . . . . . . 13 ⊢ -_𝑒-∞ = +∞
40	38, 39	syl6eq 2188	. . . . . . . . . . . 12 ⊢ (𝐴 = -∞ → -_𝑒𝐴 = +∞)
41	40	oveq2d 5790	. . . . . . . . . . 11 ⊢ (𝐴 = -∞ → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 +∞))
42	41	adantr 274	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 +∞))
43		renemnf 7814	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ -∞)
44	43	adantl 275	. . . . . . . . . . 11 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ -∞)
45		xaddpnf1 9629	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (𝐵 +_𝑒 +∞) = +∞)
46	9, 44, 45	syl2an2 583	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 +∞) = +∞)
47	42, 46	eqtrd 2172	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
48	37, 47	breqtrrid 3966	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
49	36, 48	2thd 174	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
50	49	ex 114	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
51	8, 32, 50	3jaoi 1281	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
52	2, 51	sylbi 120	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
53		ltpnf 9567	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
54	53	adantr 274	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < +∞)
55		simpr 109	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐵 = +∞)
56	54, 55	breqtrrd 3956	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
57	55	oveq1d 5789	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 -_𝑒𝐴))
58		rexneg 9613	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 = -𝐴)
59		renegcl 8023	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
60	58, 59	eqeltrd 2216	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ)
61	60	rexrd 7815	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ^*)
62	61	adantr 274	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -_𝑒𝐴 ∈ ℝ^*)
63	60	renemnfd 7817	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ≠ -∞)
64	63	adantr 274	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -_𝑒𝐴 ≠ -∞)
65		xaddpnf2 9630	. . . . . . . . . . 11 ⊢ ((-_𝑒𝐴 ∈ ℝ^* ∧ -_𝑒𝐴 ≠ -∞) → (+∞ +_𝑒 -_𝑒𝐴) = +∞)
66	62, 64, 65	syl2anc 408	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (+∞ +_𝑒 -_𝑒𝐴) = +∞)
67	57, 66	eqtrd 2172	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
68	37, 67	breqtrrid 3966	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
69	56, 68	2thd 174	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
70	69	ex 114	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
71		pnfxr 7818	. . . . . . . . . 10 ⊢ +∞ ∈ ℝ^*
72		xrltnr 9566	. . . . . . . . . 10 ⊢ (+∞ ∈ ℝ^* → ¬ +∞ < +∞)
73	71, 72	ax-mp 5	. . . . . . . . 9 ⊢ ¬ +∞ < +∞
74		breq12 3934	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ +∞ < +∞))
75	73, 74	mtbiri 664	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → ¬ 𝐴 < 𝐵)
76		0re 7766	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
77	76	ltnri 7856	. . . . . . . . 9 ⊢ ¬ 0 < 0
78		simpr 109	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → 𝐵 = +∞)
79	19, 21	syl6eq 2188	. . . . . . . . . . . . 13 ⊢ (𝐴 = +∞ → -_𝑒𝐴 = -∞)
80	79	adantr 274	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → -_𝑒𝐴 = -∞)
81	78, 80	oveq12d 5792	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 -∞))
82		pnfaddmnf 9633	. . . . . . . . . . 11 ⊢ (+∞ +_𝑒 -∞) = 0
83	81, 82	syl6eq 2188	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = 0)
84	83	breq2d 3941	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < 0))
85	77, 84	mtbiri 664	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
86	75, 85	2falsed 691	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
87	86	ex 114	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
88		mnfltpnf 9571	. . . . . . . . 9 ⊢ -∞ < +∞
89		breq12 3934	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ -∞ < +∞))
90	88, 89	mpbiri 167	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
91		oveq1 5781	. . . . . . . . . . 11 ⊢ (𝐵 = +∞ → (𝐵 +_𝑒 +∞) = (+∞ +_𝑒 +∞))
92	41, 91	sylan9eq 2192	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 +∞))
93		pnfnemnf 7820	. . . . . . . . . . 11 ⊢ +∞ ≠ -∞
94		xaddpnf1 9629	. . . . . . . . . . 11 ⊢ ((+∞ ∈ ℝ^* ∧ +∞ ≠ -∞) → (+∞ +_𝑒 +∞) = +∞)
95	71, 93, 94	mp2an 422	. . . . . . . . . 10 ⊢ (+∞ +_𝑒 +∞) = +∞
96	92, 95	syl6eq 2188	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
97	37, 96	breqtrrid 3966	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
98	90, 97	2thd 174	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
99	98	ex 114	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
100	70, 87, 99	3jaoi 1281	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
101	2, 100	sylbi 120	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
102		rexr 7811	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
103	102	adantr 274	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐴 ∈ ℝ^*)
104		nltmnf 9574	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)
105	103, 104	syl 14	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
106		simpr 109	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐵 = -∞)
107	106	breq2d 3941	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
108	105, 107	mtbird 662	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
109	106	oveq1d 5789	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (-∞ +_𝑒 -_𝑒𝐴))
110		rexr 7811	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ^*)
111		renepnf 7813	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝐴 ∈ ℝ → -_𝑒𝐴 ≠ +∞)
112		xaddmnf2 9632	. . . . . . . . . . . . . 14 ⊢ ((-_𝑒𝐴 ∈ ℝ^* ∧ -_𝑒𝐴 ≠ +∞) → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
113	110, 111, 112	syl2anc 408	. . . . . . . . . . . . 13 ⊢ (-_𝑒𝐴 ∈ ℝ → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
114	60, 113	syl 14	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
115	114	adantr 274	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
116	109, 115	eqtrd 2172	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
117	116	breq2d 3941	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
118	18, 117	mtbiri 664	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
119	108, 118	2falsed 691	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
120	119	ex 114	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
121		eleq1 2202	. . . . . . . . . . . 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 3941	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
127	124, 126	mtbird 662	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
128	79	oveq2d 5790	. . . . . . . . . . . 12 ⊢ (𝐴 = +∞ → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
129	128	adantr 274	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
130		mnfxr 7822	. . . . . . . . . . . . 13 ⊢ -∞ ∈ ℝ^*
131		eleq1 2202	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → (𝐵 ∈ ℝ^* ↔ -∞ ∈ ℝ^*))
132	130, 131	mpbiri 167	. . . . . . . . . . . 12 ⊢ (𝐵 = -∞ → 𝐵 ∈ ℝ^*)
133		mnfnepnf 7821	. . . . . . . . . . . . . 14 ⊢ -∞ ≠ +∞
134		neeq1 2321	. . . . . . . . . . . . . 14 ⊢ (𝐵 = -∞ → (𝐵 ≠ +∞ ↔ -∞ ≠ +∞))
135	133, 134	mpbiri 167	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → 𝐵 ≠ +∞)
136	135	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐵 ≠ +∞)
137	132, 136, 26	syl2an2 583	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -∞) = -∞)
138	129, 137	eqtrd 2172	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
139	138	breq2d 3941	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
140	18, 139	mtbiri 664	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
141	127, 140	2falsed 691	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
142	141	ex 114	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
143		xrltnr 9566	. . . . . . . . . 10 ⊢ (-∞ ∈ ℝ^* → ¬ -∞ < -∞)
144	130, 143	ax-mp 5	. . . . . . . . 9 ⊢ ¬ -∞ < -∞
145		breq12 3934	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ -∞ < -∞))
146	144, 145	mtbiri 664	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
147		oveq1 5781	. . . . . . . . . . . 12 ⊢ (𝐵 = -∞ → (𝐵 +_𝑒 +∞) = (-∞ +_𝑒 +∞))
148	41, 147	sylan9eq 2192	. . . . . . . . . . 11 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (-∞ +_𝑒 +∞))
149		mnfaddpnf 9634	. . . . . . . . . . 11 ⊢ (-∞ +_𝑒 +∞) = 0
150	148, 149	syl6eq 2188	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = 0)
151	150	breq2d 3941	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < 0))
152	77, 151	mtbiri 664	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
153	146, 152	2falsed 691	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
154	153	ex 114	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
155	120, 142, 154	3jaoi 1281	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
156	2, 155	sylbi 120	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
157	52, 101, 156	3jaod 1282	. . 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 961 = wceq 1331 ∈ wcel 1480 ≠ wne 2308 class class class wbr 3929 (class class class)co 5774 ℝcr 7619 0cc0 7620 +∞cpnf 7797 -∞cmnf 7798 ℝ^*cxr 7799 < clt 7800 − cmin 7933 -cneg 7934 -_𝑒cxne 9556 +_𝑒 cxad 9557

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 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452 ax-cnex 7711 ax-resscn 7712 ax-1cn 7713 ax-1re 7714 ax-icn 7715 ax-addcl 7716 ax-addrcl 7717 ax-mulcl 7718 ax-addcom 7720 ax-addass 7722 ax-distr 7724 ax-i2m1 7725 ax-0id 7728 ax-rnegex 7729 ax-cnre 7731 ax-pre-ltirr 7732 ax-pre-ltadd 7736

This theorem depends on definitions: df-bi 116 df-dc 820 df-3or 963 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-nel 2404 df-ral 2421 df-rex 2422 df-reu 2423 df-rab 2425 df-v 2688 df-sbc 2910 df-dif 3073 df-un 3075 df-in 3077 df-ss 3084 df-if 3475 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-br 3930 df-opab 3990 df-id 4215 df-xp 4545 df-rel 4546 df-cnv 4547 df-co 4548 df-dm 4549 df-iota 5088 df-fun 5125 df-fv 5131 df-riota 5730 df-ov 5777 df-oprab 5778 df-mpo 5779 df-pnf 7802 df-mnf 7803 df-xr 7804 df-ltxr 7805 df-sub 7935 df-neg 7936 df-xneg 9559 df-xadd 9560

This theorem is referenced by: (None)

W3C validator