Theorem pimrecltneg

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

	Ref	Expression
Hypotheses	pimrecltneg.x	⊢ Ⅎ 𝑥 𝜑
	pimrecltneg.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	pimrecltneg.n	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≠ 0 )
	pimrecltneg.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	pimrecltneg.l	⊢ ( 𝜑 → 𝐶 < 0 )
Assertion	pimrecltneg	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( 1 / 𝐵 ) < 𝐶 } = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( ( 1 / 𝐶 ) (,) 0 ) } )

Proof

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