Theorem pimrecltneg 47650

Description: The preimage of an unbounded below, open interval, with negative upper bound, for the reciprocal function. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypotheses

Ref	Expression
pimrecltneg.x	⊢ Ⅎ𝑥𝜑
pimrecltneg.b	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
pimrecltneg.n	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ 0)
pimrecltneg.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
pimrecltneg.l	⊢ (𝜑 → 𝐶 < 0)

Assertion

Ref	Expression
pimrecltneg	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)})

Proof of Theorem pimrecltneg

Step	Hyp	Ref	Expression
1		pimrecltneg.x	. . 3 ⊢ Ⅎ𝑥𝜑
2		rabidim1 3433	. . . . . . . 8 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶} → 𝑥 ∈ 𝐴)
3	2	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → 𝑥 ∈ 𝐴)
4		1red 11266	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℝ)
5		pimrecltneg.c	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		pimrecltneg.l	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 < 0)
7	5, 6	ltned 11403	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ≠ 0)
8	4, 5, 7	redivcld 12100	. . . . . . . . . 10 ⊢ (𝜑 → (1 / 𝐶) ∈ ℝ)
9	8	rexrd 11316	. . . . . . . . 9 ⊢ (𝜑 → (1 / 𝐶) ∈ ℝ*)
10	9	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → (1 / 𝐶) ∈ ℝ*)
11		0xr 11313	. . . . . . . . 9 ⊢ 0 ∈ ℝ*
12	11	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → 0 ∈ ℝ*)
13		pimrecltneg.b	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)
14	2, 13	sylan2 605	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → 𝐵 ∈ ℝ)
15		rabidim2 46032	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶} → (1 / 𝐵) < 𝐶)
16	15	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → (1 / 𝐵) < 𝐶)
17	4	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → 1 ∈ ℝ)
18		pimrecltneg.n	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ 0)
19	3, 18	syldan 603	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → 𝐵 ≠ 0)
20	14, 19	rereccld 12099	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → (1 / 𝐵) ∈ ℝ)
21	5	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → 𝐶 ∈ ℝ)
22		0red 11268	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → 0 ∈ ℝ)
23	6	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → 𝐶 < 0)
24	20, 21, 22, 16, 23	lttrd 11428	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → (1 / 𝐵) < 0)
25	14, 19	reclt0 46318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → (𝐵 < 0 ↔ (1 / 𝐵) < 0))
26	24, 25	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → 𝐵 < 0)
27	17, 14, 26, 21, 23	ltdiv23neg 46321	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → ((1 / 𝐵) < 𝐶 ↔ (1 / 𝐶) < 𝐵))
28	16, 27	mpbid 235	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → (1 / 𝐶) < 𝐵)
29	10, 12, 14, 28, 26	eliood 46426	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → 𝐵 ∈ ((1 / 𝐶)(,)0))
30	3, 29	jca 521	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((1 / 𝐶)(,)0)))
31		rabid 3432	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)} ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((1 / 𝐶)(,)0)))
32	30, 31	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)})
33	32	ex 418	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶} → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}))
34	31	simplbi 502	. . . . . . . 8 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)} → 𝑥 ∈ 𝐴)
35	34	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → 𝑥 ∈ 𝐴)
36	9	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → (1 / 𝐶) ∈ ℝ*)
37	11	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → 0 ∈ ℝ*)
38	31	simprbi 503	. . . . . . . . . 10 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)} → 𝐵 ∈ ((1 / 𝐶)(,)0))
39	38	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → 𝐵 ∈ ((1 / 𝐶)(,)0))
40	36, 37, 39	ioogtlbd 46478	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → (1 / 𝐶) < 𝐵)
41	4	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → 1 ∈ ℝ)
42	5	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → 𝐶 ∈ ℝ)
43	6	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → 𝐶 < 0)
44	35, 13	syldan 603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → 𝐵 ∈ ℝ)
45	36, 37, 39	iooltubd 46472	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → 𝐵 < 0)
46	41, 42, 43, 44, 45	ltdiv23neg 46321	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → ((1 / 𝐶) < 𝐵 ↔ (1 / 𝐵) < 𝐶))
47	40, 46	mpbid 235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → (1 / 𝐵) < 𝐶)
48	35, 47	jca 521	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → (𝑥 ∈ 𝐴 ∧ (1 / 𝐵) < 𝐶))
49		rabid 3432	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶} ↔ (𝑥 ∈ 𝐴 ∧ (1 / 𝐵) < 𝐶))
50	48, 49	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶})
51	50	ex 418	. . . 4 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)} → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}))
52	33, 51	impbid 215	. . 3 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶} ↔ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}))
53	1, 52	alrimi 2249	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶} ↔ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}))
54		nfrab1 3431	. . 3 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶}
55		nfrab1 3431	. . 3 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}
56	54, 55	cleqf 2950	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)} ↔ ∀𝑥(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶} ↔ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)}))
57	53, 56	sylibr 237	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (1 / 𝐵) < 𝐶} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ((1 / 𝐶)(,)0)})

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2145   ≠ wne 2955  {crab 3412   class class class wbr 5103  (class class class)co 7409  ℝcr 11156  0cc0 11157  1c1 11158  ℝ^*cxr 11299   < clt 11300   / cdiv 11928  (,)cioo 13431

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735  ax-cnex 11213  ax-resscn 11214  ax-1cn 11215  ax-icn 11216  ax-addcl 11217  ax-addrcl 11218  ax-mulcl 11219  ax-mulrcl 11220  ax-mulcom 11221  ax-addass 11222  ax-mulass 11223  ax-distr 11224  ax-i2m1 11225  ax-1ne0 11226  ax-1rid 11227  ax-rnegex 11228  ax-rrecex 11229  ax-cnre 11230  ax-pre-lttri 11231  ax-pre-lttrn 11232  ax-pre-ltadd 11233  ax-pre-mulgt0 11234

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5543  df-po 5556  df-so 5557  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-riota 7366  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7985  df-2nd 7986  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11302  df-mnf 11303  df-xr 11304  df-ltxr 11305  df-le 11306  df-sub 11500  df-neg 11501  df-div 11929  df-rp 13076  df-ioo 13435

This theorem is used by:  smfrec  47715