xposdif - Intuitionistic Logic Explorer

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

Theorem xposdif 9506

Description: Extended real version of posdif 8084. (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 9404	. . 3 ⊢ (𝐵 ∈ ℝ^* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
2		elxr 9404	. . . . 5 ⊢ (𝐴 ∈ ℝ^* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
3		posdif 8084	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
4		rexsub 9477	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 − 𝐴))
5	4	ancoms 266	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 − 𝐴))
6	5	breq2d 3887	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < (𝐵 − 𝐴)))
7	3, 6	bitr4d 190	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
8	7	ex 114	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
9		rexr 7683	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℝ^*)
10		pnfnlt 9414	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ^* → ¬ +∞ < 𝐵)
11	10	adantl 273	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ^*) → ¬ +∞ < 𝐵)
12	9, 11	sylan2 282	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ +∞ < 𝐵)
13		simpl 108	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐴 = +∞)
14	13	breq1d 3885	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
15	12, 14	mtbird 639	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ 𝐴 < 𝐵)
16		0xr 7684	. . . . . . . . . 10 ⊢ 0 ∈ ℝ^*
17		nltmnf 9415	. . . . . . . . . 10 ⊢ (0 ∈ ℝ^* → ¬ 0 < -∞)
18	16, 17	ax-mp 7	. . . . . . . . 9 ⊢ ¬ 0 < -∞
19		xnegeq 9451	. . . . . . . . . . . . . 14 ⊢ (𝐴 = +∞ → -_𝑒𝐴 = -_𝑒+∞)
20	19	adantr 272	. . . . . . . . . . . . 13 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → -_𝑒𝐴 = -_𝑒+∞)
21		xnegpnf 9452	. . . . . . . . . . . . 13 ⊢ -_𝑒+∞ = -∞
22	20, 21	syl6eq 2148	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → -_𝑒𝐴 = -∞)
23	22	oveq2d 5722	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
24		renepnf 7685	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ +∞)
25	24	adantl 273	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ +∞)
26		xaddmnf1 9472	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ +∞) → (𝐵 +_𝑒 -∞) = -∞)
27	9, 25, 26	syl2an2 564	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -∞) = -∞)
28	23, 27	eqtrd 2132	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
29	28	breq2d 3887	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
30	18, 29	mtbiri 641	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
31	15, 30	2falsed 659	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
32	31	ex 114	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
33		simpl 108	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐴 = -∞)
34		mnflt 9410	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → -∞ < 𝐵)
35	34	adantl 273	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → -∞ < 𝐵)
36	33, 35	eqbrtrd 3895	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐴 < 𝐵)
37		0ltpnf 9409	. . . . . . . . 9 ⊢ 0 < +∞
38		xnegeq 9451	. . . . . . . . . . . . 13 ⊢ (𝐴 = -∞ → -_𝑒𝐴 = -_𝑒-∞)
39		xnegmnf 9453	. . . . . . . . . . . . 13 ⊢ -_𝑒-∞ = +∞
40	38, 39	syl6eq 2148	. . . . . . . . . . . 12 ⊢ (𝐴 = -∞ → -_𝑒𝐴 = +∞)
41	40	oveq2d 5722	. . . . . . . . . . 11 ⊢ (𝐴 = -∞ → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 +∞))
42	41	adantr 272	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 +∞))
43		renemnf 7686	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → 𝐵 ≠ -∞)
44	43	adantl 273	. . . . . . . . . . 11 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ -∞)
45		xaddpnf1 9470	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ^* ∧ 𝐵 ≠ -∞) → (𝐵 +_𝑒 +∞) = +∞)
46	9, 44, 45	syl2an2 564	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 +∞) = +∞)
47	42, 46	eqtrd 2132	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
48	37, 47	syl5breqr 3911	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
49	36, 48	2thd 174	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
50	49	ex 114	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
51	8, 32, 50	3jaoi 1249	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
52	2, 51	sylbi 120	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
53		ltpnf 9408	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ → 𝐴 < +∞)
54	53	adantr 272	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < +∞)
55		simpr 109	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐵 = +∞)
56	54, 55	breqtrrd 3901	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
57	55	oveq1d 5721	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 -_𝑒𝐴))
58		rexneg 9454	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 = -𝐴)
59		renegcl 7894	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
60	58, 59	eqeltrd 2176	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ)
61	60	rexrd 7687	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ^*)
62	61	adantr 272	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -_𝑒𝐴 ∈ ℝ^*)
63	60	renemnfd 7689	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → -_𝑒𝐴 ≠ -∞)
64	63	adantr 272	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -_𝑒𝐴 ≠ -∞)
65		xaddpnf2 9471	. . . . . . . . . . 11 ⊢ ((-_𝑒𝐴 ∈ ℝ^* ∧ -_𝑒𝐴 ≠ -∞) → (+∞ +_𝑒 -_𝑒𝐴) = +∞)
66	62, 64, 65	syl2anc 406	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (+∞ +_𝑒 -_𝑒𝐴) = +∞)
67	57, 66	eqtrd 2132	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
68	37, 67	syl5breqr 3911	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
69	56, 68	2thd 174	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
70	69	ex 114	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
71		pnfxr 7690	. . . . . . . . . 10 ⊢ +∞ ∈ ℝ^*
72		xrltnr 9407	. . . . . . . . . 10 ⊢ (+∞ ∈ ℝ^* → ¬ +∞ < +∞)
73	71, 72	ax-mp 7	. . . . . . . . 9 ⊢ ¬ +∞ < +∞
74		breq12 3880	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ +∞ < +∞))
75	73, 74	mtbiri 641	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → ¬ 𝐴 < 𝐵)
76		0re 7638	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
77	76	ltnri 7727	. . . . . . . . 9 ⊢ ¬ 0 < 0
78		simpr 109	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → 𝐵 = +∞)
79	19, 21	syl6eq 2148	. . . . . . . . . . . . 13 ⊢ (𝐴 = +∞ → -_𝑒𝐴 = -∞)
80	79	adantr 272	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → -_𝑒𝐴 = -∞)
81	78, 80	oveq12d 5724	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 -∞))
82		pnfaddmnf 9474	. . . . . . . . . . 11 ⊢ (+∞ +_𝑒 -∞) = 0
83	81, 82	syl6eq 2148	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = 0)
84	83	breq2d 3887	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < 0))
85	77, 84	mtbiri 641	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
86	75, 85	2falsed 659	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
87	86	ex 114	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
88		mnfltpnf 9412	. . . . . . . . 9 ⊢ -∞ < +∞
89		breq12 3880	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ -∞ < +∞))
90	88, 89	mpbiri 167	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
91		oveq1 5713	. . . . . . . . . . 11 ⊢ (𝐵 = +∞ → (𝐵 +_𝑒 +∞) = (+∞ +_𝑒 +∞))
92	41, 91	sylan9eq 2152	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (+∞ +_𝑒 +∞))
93		pnfnemnf 7692	. . . . . . . . . . 11 ⊢ +∞ ≠ -∞
94		xaddpnf1 9470	. . . . . . . . . . 11 ⊢ ((+∞ ∈ ℝ^* ∧ +∞ ≠ -∞) → (+∞ +_𝑒 +∞) = +∞)
95	71, 93, 94	mp2an 420	. . . . . . . . . 10 ⊢ (+∞ +_𝑒 +∞) = +∞
96	92, 95	syl6eq 2148	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐵 +_𝑒 -_𝑒𝐴) = +∞)
97	37, 96	syl5breqr 3911	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → 0 < (𝐵 +_𝑒 -_𝑒𝐴))
98	90, 97	2thd 174	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
99	98	ex 114	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
100	70, 87, 99	3jaoi 1249	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
101	2, 100	sylbi 120	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
102		rexr 7683	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℝ^*)
103	102	adantr 272	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐴 ∈ ℝ^*)
104		nltmnf 9415	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℝ^* → ¬ 𝐴 < -∞)
105	103, 104	syl 14	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
106		simpr 109	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐵 = -∞)
107	106	breq2d 3887	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
108	105, 107	mtbird 639	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
109	106	oveq1d 5721	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (-∞ +_𝑒 -_𝑒𝐴))
110		rexr 7683	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝐴 ∈ ℝ → -_𝑒𝐴 ∈ ℝ^*)
111		renepnf 7685	. . . . . . . . . . . . . 14 ⊢ (-_𝑒𝐴 ∈ ℝ → -_𝑒𝐴 ≠ +∞)
112		xaddmnf2 9473	. . . . . . . . . . . . . 14 ⊢ ((-_𝑒𝐴 ∈ ℝ^* ∧ -_𝑒𝐴 ≠ +∞) → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
113	110, 111, 112	syl2anc 406	. . . . . . . . . . . . 13 ⊢ (-_𝑒𝐴 ∈ ℝ → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
114	60, 113	syl 14	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℝ → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
115	114	adantr 272	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (-∞ +_𝑒 -_𝑒𝐴) = -∞)
116	109, 115	eqtrd 2132	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
117	116	breq2d 3887	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
118	18, 117	mtbiri 641	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
119	108, 118	2falsed 659	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
120	119	ex 114	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
121		eleq1 2162	. . . . . . . . . . . 12 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ^* ↔ +∞ ∈ ℝ^*))
122	71, 121	mpbiri 167	. . . . . . . . . . 11 ⊢ (𝐴 = +∞ → 𝐴 ∈ ℝ^*)
123	122	adantr 272	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐴 ∈ ℝ^*)
124	123, 104	syl 14	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
125		simpr 109	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐵 = -∞)
126	125	breq2d 3887	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 𝐴 < -∞))
127	124, 126	mtbird 639	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
128	79	oveq2d 5722	. . . . . . . . . . . 12 ⊢ (𝐴 = +∞ → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
129	128	adantr 272	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (𝐵 +_𝑒 -∞))
130		mnfxr 7694	. . . . . . . . . . . . 13 ⊢ -∞ ∈ ℝ^*
131		eleq1 2162	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → (𝐵 ∈ ℝ^* ↔ -∞ ∈ ℝ^*))
132	130, 131	mpbiri 167	. . . . . . . . . . . 12 ⊢ (𝐵 = -∞ → 𝐵 ∈ ℝ^*)
133		mnfnepnf 7693	. . . . . . . . . . . . . 14 ⊢ -∞ ≠ +∞
134		neeq1 2280	. . . . . . . . . . . . . 14 ⊢ (𝐵 = -∞ → (𝐵 ≠ +∞ ↔ -∞ ≠ +∞))
135	133, 134	mpbiri 167	. . . . . . . . . . . . 13 ⊢ (𝐵 = -∞ → 𝐵 ≠ +∞)
136	135	adantl 273	. . . . . . . . . . . 12 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐵 ≠ +∞)
137	132, 136, 26	syl2an2 564	. . . . . . . . . . 11 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -∞) = -∞)
138	129, 137	eqtrd 2132	. . . . . . . . . 10 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = -∞)
139	138	breq2d 3887	. . . . . . . . 9 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < -∞))
140	18, 139	mtbiri 641	. . . . . . . 8 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
141	127, 140	2falsed 659	. . . . . . 7 ⊢ ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
142	141	ex 114	. . . . . 6 ⊢ (𝐴 = +∞ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
143		xrltnr 9407	. . . . . . . . . 10 ⊢ (-∞ ∈ ℝ^* → ¬ -∞ < -∞)
144	130, 143	ax-mp 7	. . . . . . . . 9 ⊢ ¬ -∞ < -∞
145		breq12 3880	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ -∞ < -∞))
146	144, 145	mtbiri 641	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
147		oveq1 5713	. . . . . . . . . . . 12 ⊢ (𝐵 = -∞ → (𝐵 +_𝑒 +∞) = (-∞ +_𝑒 +∞))
148	41, 147	sylan9eq 2152	. . . . . . . . . . 11 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = (-∞ +_𝑒 +∞))
149		mnfaddpnf 9475	. . . . . . . . . . 11 ⊢ (-∞ +_𝑒 +∞) = 0
150	148, 149	syl6eq 2148	. . . . . . . . . 10 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐵 +_𝑒 -_𝑒𝐴) = 0)
151	150	breq2d 3887	. . . . . . . . 9 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (0 < (𝐵 +_𝑒 -_𝑒𝐴) ↔ 0 < 0))
152	77, 151	mtbiri 641	. . . . . . . 8 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +_𝑒 -_𝑒𝐴))
153	146, 152	2falsed 659	. . . . . . 7 ⊢ ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴)))
154	153	ex 114	. . . . . 6 ⊢ (𝐴 = -∞ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
155	120, 142, 154	3jaoi 1249	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
156	2, 155	sylbi 120	. . . 4 ⊢ (𝐴 ∈ ℝ^* → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +_𝑒 -_𝑒𝐴))))
157	52, 101, 156	3jaod 1250	. . 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 929 = wceq 1299 ∈ wcel 1448 ≠ wne 2267 class class class wbr 3875 (class class class)co 5706 ℝcr 7499 0cc0 7500 +∞cpnf 7669 -∞cmnf 7670 ℝ^*cxr 7671 < clt 7672 − cmin 7804 -cneg 7805 -_𝑒cxne 9397 +_𝑒 cxad 9398

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-13 1459 ax-14 1460 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-sep 3986 ax-pow 4038 ax-pr 4069 ax-un 4293 ax-setind 4390 ax-cnex 7586 ax-resscn 7587 ax-1cn 7588 ax-1re 7589 ax-icn 7590 ax-addcl 7591 ax-addrcl 7592 ax-mulcl 7593 ax-addcom 7595 ax-addass 7597 ax-distr 7599 ax-i2m1 7600 ax-0id 7603 ax-rnegex 7604 ax-cnre 7606 ax-pre-ltirr 7607 ax-pre-ltadd 7611

This theorem depends on definitions: df-bi 116 df-dc 787 df-3or 931 df-3an 932 df-tru 1302 df-fal 1305 df-nf 1405 df-sb 1704 df-eu 1963 df-mo 1964 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ne 2268 df-nel 2363 df-ral 2380 df-rex 2381 df-reu 2382 df-rab 2384 df-v 2643 df-sbc 2863 df-dif 3023 df-un 3025 df-in 3027 df-ss 3034 df-if 3422 df-pw 3459 df-sn 3480 df-pr 3481 df-op 3483 df-uni 3684 df-br 3876 df-opab 3930 df-id 4153 df-xp 4483 df-rel 4484 df-cnv 4485 df-co 4486 df-dm 4487 df-iota 5024 df-fun 5061 df-fv 5067 df-riota 5662 df-ov 5709 df-oprab 5710 df-mpo 5711 df-pnf 7674 df-mnf 7675 df-xr 7676 df-ltxr 7677 df-sub 7806 df-neg 7807 df-xneg 9400 df-xadd 9401

This theorem is referenced by: (None)

W3C validator