rlimcnp2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rlimcnp2		Structured version Visualization version GIF version

Theorem rlimcnp2 26478

Description: Relate a limit of a real-valued sequence at infinity to the continuity of the function 𝑆(𝑦) = 𝑅(1 / 𝑦) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.)

**Hypotheses**
Ref	Expression
rlimcnp2.a	⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞))
rlimcnp2.0	⊢ (𝜑 → 0 ∈ 𝐴)
rlimcnp2.b	⊢ (𝜑 → 𝐵 ⊆ ℝ)
rlimcnp2.c	⊢ (𝜑 → 𝐶 ∈ ℂ)
rlimcnp2.r	⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ)
rlimcnp2.d	⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴))
rlimcnp2.s	⊢ (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅)
rlimcnp2.j	⊢ 𝐽 = (TopOpen‘ℂ_fld)
rlimcnp2.k	⊢ 𝐾 = (𝐽 ↾_t 𝐴)

**Assertion**
Ref	Expression
rlimcnp2	⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝_𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)))

Distinct variable groups: 𝑥,𝑦,𝐴 𝑥,𝐵,𝑦 𝑥,𝐶,𝑦 𝜑,𝑥,𝑦 𝑦,𝑅 𝑥,𝑆 Allowed substitution hints: 𝑅(𝑥) 𝑆(𝑦) 𝐽(𝑥,𝑦) 𝐾(𝑥,𝑦)

Proof of Theorem rlimcnp2 Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss1 4228	. . . . . . . 8 ⊢ (𝐵 ∩ (1[,)+∞)) ⊆ 𝐵
2		resmpt 6037	. . . . . . . 8 ⊢ ((𝐵 ∩ (1[,)+∞)) ⊆ 𝐵 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆))
3	1, 2	mp1i 13	. . . . . . 7 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆))
4		0xr 11263	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ^*
5		0lt1 11738	. . . . . . . . . . 11 ⊢ 0 < 1
6		df-ioo 13330	. . . . . . . . . . . 12 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
7		df-ico 13332	. . . . . . . . . . . 12 ⊢ [,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
8		xrltletr 13138	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → ((0 < 1 ∧ 1 ≤ 𝑤) → 0 < 𝑤))
9	6, 7, 8	ixxss1 13344	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ 0 < 1) → (1[,)+∞) ⊆ (0(,)+∞))
10	4, 5, 9	mp2an 690	. . . . . . . . . 10 ⊢ (1[,)+∞) ⊆ (0(,)+∞)
11		ioorp 13404	. . . . . . . . . 10 ⊢ (0(,)+∞) = ℝ⁺
12	10, 11	sseqtri 4018	. . . . . . . . 9 ⊢ (1[,)+∞) ⊆ ℝ⁺
13		sslin 4234	. . . . . . . . 9 ⊢ ((1[,)+∞) ⊆ ℝ⁺ → (𝐵 ∩ (1[,)+∞)) ⊆ (𝐵 ∩ ℝ⁺))
14	12, 13	ax-mp 5	. . . . . . . 8 ⊢ (𝐵 ∩ (1[,)+∞)) ⊆ (𝐵 ∩ ℝ⁺)
15		resmpt 6037	. . . . . . . 8 ⊢ ((𝐵 ∩ (1[,)+∞)) ⊆ (𝐵 ∩ ℝ⁺) → ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆))
16	14, 15	mp1i 13	. . . . . . 7 ⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = (𝑦 ∈ (𝐵 ∩ (1[,)+∞)) ↦ 𝑆))
17	3, 16	eqtr4d 2775	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))) = ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞))))
18		resres 5994	. . . . . 6 ⊢ (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞)))
19		resres 5994	. . . . . 6 ⊢ (((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ↾ (𝐵 ∩ (1[,)+∞)))
20	17, 18, 19	3eqtr4g 2797	. . . . 5 ⊢ (𝜑 → (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = (((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)))
21		rlimcnp2.r	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ)
22	21	fmpttd 7116	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ 𝑆):𝐵⟶ℂ)
23	22	ffnd 6718	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ 𝑆) Fn 𝐵)
24		fnresdm 6669	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐵 ↦ 𝑆) Fn 𝐵 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ 𝐵 ↦ 𝑆))
25	23, 24	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ 𝐵 ↦ 𝑆))
26	25	reseq1d 5980	. . . . 5 ⊢ (𝜑 → (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞)))
27		elinel1 4195	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝐵 ∩ ℝ⁺) → 𝑦 ∈ 𝐵)
28	27, 21	sylan2 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) → 𝑆 ∈ ℂ)
29	28	fmpttd 7116	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆):(𝐵 ∩ ℝ⁺)⟶ℂ)
30		frel 6722	. . . . . . . 8 ⊢ ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆):(𝐵 ∩ ℝ⁺)⟶ℂ → Rel (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆))
31	29, 30	syl 17	. . . . . . 7 ⊢ (𝜑 → Rel (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆))
32		eqid 2732	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) = (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆)
33	32, 28	dmmptd 6695	. . . . . . . 8 ⊢ (𝜑 → dom (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) = (𝐵 ∩ ℝ⁺))
34		inss1 4228	. . . . . . . 8 ⊢ (𝐵 ∩ ℝ⁺) ⊆ 𝐵
35	33, 34	eqsstrdi 4036	. . . . . . 7 ⊢ (𝜑 → dom (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ⊆ 𝐵)
36		relssres 6022	. . . . . . 7 ⊢ ((Rel (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ∧ dom (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ⊆ 𝐵) → ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆))
37	31, 35, 36	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ↾ 𝐵) = (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆))
38	37	reseq1d 5980	. . . . 5 ⊢ (𝜑 → (((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ↾ 𝐵) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ↾ (1[,)+∞)))
39	20, 26, 38	3eqtr3d 2780	. . . 4 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞)) = ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ↾ (1[,)+∞)))
40	39	breq1d 5158	. . 3 ⊢ (𝜑 → (((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞)) ⇝_𝑟 𝐶 ↔ ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ↾ (1[,)+∞)) ⇝_𝑟 𝐶))
41		rlimcnp2.b	. . . 4 ⊢ (𝜑 → 𝐵 ⊆ ℝ)
42		1red 11217	. . . 4 ⊢ (𝜑 → 1 ∈ ℝ)
43	22, 41, 42	rlimresb 15511	. . 3 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝_𝑟 𝐶 ↔ ((𝑦 ∈ 𝐵 ↦ 𝑆) ↾ (1[,)+∞)) ⇝_𝑟 𝐶))
44	34, 41	sstrid 3993	. . . 4 ⊢ (𝜑 → (𝐵 ∩ ℝ⁺) ⊆ ℝ)
45	29, 44, 42	rlimresb 15511	. . 3 ⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ⇝_𝑟 𝐶 ↔ ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ↾ (1[,)+∞)) ⇝_𝑟 𝐶))
46	40, 43, 45	3bitr4d 310	. 2 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝_𝑟 𝐶 ↔ (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ⇝_𝑟 𝐶))
47		inss2 4229	. . . . . . . . . . 11 ⊢ (𝐵 ∩ ℝ⁺) ⊆ ℝ⁺
48	47	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 ∩ ℝ⁺) ⊆ ℝ⁺)
49	48	sselda 3982	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) → 𝑦 ∈ ℝ⁺)
50	49	rpreccld 13028	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) → (1 / 𝑦) ∈ ℝ⁺)
51	50	rpne0d 13023	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) → (1 / 𝑦) ≠ 0)
52	51	neneqd 2945	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) → ¬ (1 / 𝑦) = 0)
53	52	iffalsed 4539	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) → if((1 / 𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅) = ⦋(1 / 𝑦) / 𝑥⦌𝑅)
54		oveq2 7419	. . . . . . . . . 10 ⊢ (𝑥 = (1 / 𝑦) → (1 / 𝑥) = (1 / (1 / 𝑦)))
55		rpcnne0 12994	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ⁺ → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
56		recrec 11913	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (1 / (1 / 𝑦)) = 𝑦)
57	49, 55, 56	3syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) → (1 / (1 / 𝑦)) = 𝑦)
58	54, 57	sylan9eqr 2794	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) ∧ 𝑥 = (1 / 𝑦)) → (1 / 𝑥) = 𝑦)
59	58	eqcomd 2738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) ∧ 𝑥 = (1 / 𝑦)) → 𝑦 = (1 / 𝑥))
60		rlimcnp2.s	. . . . . . . 8 ⊢ (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅)
61	59, 60	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) ∧ 𝑥 = (1 / 𝑦)) → 𝑆 = 𝑅)
62	61	eqcomd 2738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) ∧ 𝑥 = (1 / 𝑦)) → 𝑅 = 𝑆)
63	50, 62	csbied 3931	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) → ⦋(1 / 𝑦) / 𝑥⦌𝑅 = 𝑆)
64	53, 63	eqtrd 2772	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) → if((1 / 𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅) = 𝑆)
65	64	mpteq2dva 5248	. . 3 ⊢ (𝜑 → (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ if((1 / 𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) = (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆))
66	65	breq1d 5158	. 2 ⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ if((1 / 𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) ⇝_𝑟 𝐶 ↔ (𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ 𝑆) ⇝_𝑟 𝐶))
67		rlimcnp2.a	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞))
68		rlimcnp2.0	. . . 4 ⊢ (𝜑 → 0 ∈ 𝐴)
69		rlimcnp2.c	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ ℂ)
70	69	ad2antrr 724	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑤 = 0) → 𝐶 ∈ ℂ)
71	67	sselda 3982	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ (0[,)+∞))
72		0re 11218	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
73		pnfxr 11270	. . . . . . . . . . . . 13 ⊢ +∞ ∈ ℝ^*
74		elico2 13390	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ +∞ ∈ ℝ^*) → (𝑤 ∈ (0[,)+∞) ↔ (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤 ∧ 𝑤 < +∞)))
75	72, 73, 74	mp2an 690	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ (0[,)+∞) ↔ (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤 ∧ 𝑤 < +∞))
76	71, 75	sylib 217	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ ℝ ∧ 0 ≤ 𝑤 ∧ 𝑤 < +∞))
77	76	simp1d 1142	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ℝ)
78	77	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ ℝ)
79	76	simp2d 1143	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 0 ≤ 𝑤)
80		leloe 11302	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ 𝑤 ∈ ℝ) → (0 ≤ 𝑤 ↔ (0 < 𝑤 ∨ 0 = 𝑤)))
81	72, 77, 80	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (0 ≤ 𝑤 ↔ (0 < 𝑤 ∨ 0 = 𝑤)))
82	79, 81	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (0 < 𝑤 ∨ 0 = 𝑤))
83	82	ord 862	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (¬ 0 < 𝑤 → 0 = 𝑤))
84		eqcom 2739	. . . . . . . . . . . 12 ⊢ (0 = 𝑤 ↔ 𝑤 = 0)
85	83, 84	imbitrdi 250	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (¬ 0 < 𝑤 → 𝑤 = 0))
86	85	con1d 145	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (¬ 𝑤 = 0 → 0 < 𝑤))
87	86	imp 407	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 0 < 𝑤)
88	78, 87	elrpd 13015	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ ℝ⁺)
89		rpcnne0 12994	. . . . . . . . 9 ⊢ (𝑤 ∈ ℝ⁺ → (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0))
90		recrec 11913	. . . . . . . . 9 ⊢ ((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) → (1 / (1 / 𝑤)) = 𝑤)
91	89, 90	syl 17	. . . . . . . 8 ⊢ (𝑤 ∈ ℝ⁺ → (1 / (1 / 𝑤)) = 𝑤)
92	88, 91	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / (1 / 𝑤)) = 𝑤)
93	92	csbeq1d 3897	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ⦋(1 / (1 / 𝑤)) / 𝑥⦌𝑅 = ⦋𝑤 / 𝑥⦌𝑅)
94		oveq2 7419	. . . . . . . . 9 ⊢ (𝑦 = (1 / 𝑤) → (1 / 𝑦) = (1 / (1 / 𝑤)))
95	94	csbeq1d 3897	. . . . . . . 8 ⊢ (𝑦 = (1 / 𝑤) → ⦋(1 / 𝑦) / 𝑥⦌𝑅 = ⦋(1 / (1 / 𝑤)) / 𝑥⦌𝑅)
96	95	eleq1d 2818	. . . . . . 7 ⊢ (𝑦 = (1 / 𝑤) → (⦋(1 / 𝑦) / 𝑥⦌𝑅 ∈ ℂ ↔ ⦋(1 / (1 / 𝑤)) / 𝑥⦌𝑅 ∈ ℂ))
97	63, 28	eqeltrd 2833	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐵 ∩ ℝ⁺)) → ⦋(1 / 𝑦) / 𝑥⦌𝑅 ∈ ℂ)
98	97	ralrimiva 3146	. . . . . . . 8 ⊢ (𝜑 → ∀𝑦 ∈ (𝐵 ∩ ℝ⁺)⦋(1 / 𝑦) / 𝑥⦌𝑅 ∈ ℂ)
99	98	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ∀𝑦 ∈ (𝐵 ∩ ℝ⁺)⦋(1 / 𝑦) / 𝑥⦌𝑅 ∈ ℂ)
100		simplr 767	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝑤 ∈ 𝐴)
101		simpll 765	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → 𝜑)
102		eleq1 2821	. . . . . . . . . . . . 13 ⊢ (𝑦 = (1 / 𝑤) → (𝑦 ∈ 𝐵 ↔ (1 / 𝑤) ∈ 𝐵))
103	94	eleq1d 2818	. . . . . . . . . . . . 13 ⊢ (𝑦 = (1 / 𝑤) → ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑤)) ∈ 𝐴))
104	102, 103	bibi12d 345	. . . . . . . . . . . 12 ⊢ (𝑦 = (1 / 𝑤) → ((𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴) ↔ ((1 / 𝑤) ∈ 𝐵 ↔ (1 / (1 / 𝑤)) ∈ 𝐴)))
105		rlimcnp2.d	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ⁺) → (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴))
106	105	ralrimiva 3146	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑦 ∈ ℝ⁺ (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴))
107	106	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ∀𝑦 ∈ ℝ⁺ (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴))
108		rpreccl 13002	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ℝ⁺ → (1 / 𝑤) ∈ ℝ⁺)
109	108	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → (1 / 𝑤) ∈ ℝ⁺)
110	104, 107, 109	rspcdva 3613	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ((1 / 𝑤) ∈ 𝐵 ↔ (1 / (1 / 𝑤)) ∈ 𝐴))
111	91	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → (1 / (1 / 𝑤)) = 𝑤)
112	111	eleq1d 2818	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ((1 / (1 / 𝑤)) ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
113	110, 112	bitr2d 279	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → (𝑤 ∈ 𝐴 ↔ (1 / 𝑤) ∈ 𝐵))
114	101, 88, 113	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (𝑤 ∈ 𝐴 ↔ (1 / 𝑤) ∈ 𝐵))
115	100, 114	mpbid 231	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ 𝐵)
116	88	rpreccld 13028	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ ℝ⁺)
117	115, 116	elind 4194	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → (1 / 𝑤) ∈ (𝐵 ∩ ℝ⁺))
118	96, 99, 117	rspcdva 3613	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ⦋(1 / (1 / 𝑤)) / 𝑥⦌𝑅 ∈ ℂ)
119	93, 118	eqeltrrd 2834	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 = 0) → ⦋𝑤 / 𝑥⦌𝑅 ∈ ℂ)
120	70, 119	ifclda 4563	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) ∈ ℂ)
121	109	biantrud 532	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → ((1 / 𝑤) ∈ 𝐵 ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈ ℝ⁺)))
122	113, 121	bitrd 278	. . . . 5 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → (𝑤 ∈ 𝐴 ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈ ℝ⁺)))
123		elin 3964	. . . . 5 ⊢ ((1 / 𝑤) ∈ (𝐵 ∩ ℝ⁺) ↔ ((1 / 𝑤) ∈ 𝐵 ∧ (1 / 𝑤) ∈ ℝ⁺))
124	122, 123	bitr4di 288	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → (𝑤 ∈ 𝐴 ↔ (1 / 𝑤) ∈ (𝐵 ∩ ℝ⁺)))
125		iftrue 4534	. . . 4 ⊢ (𝑤 = 0 → if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) = 𝐶)
126		eqeq1 2736	. . . . 5 ⊢ (𝑤 = (1 / 𝑦) → (𝑤 = 0 ↔ (1 / 𝑦) = 0))
127		csbeq1 3896	. . . . 5 ⊢ (𝑤 = (1 / 𝑦) → ⦋𝑤 / 𝑥⦌𝑅 = ⦋(1 / 𝑦) / 𝑥⦌𝑅)
128	126, 127	ifbieq2d 4554	. . . 4 ⊢ (𝑤 = (1 / 𝑦) → if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅) = if((1 / 𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅))
129		rlimcnp2.j	. . . 4 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
130		rlimcnp2.k	. . . 4 ⊢ 𝐾 = (𝐽 ↾_t 𝐴)
131	67, 68, 48, 120, 124, 125, 128, 129, 130	rlimcnp 26477	. . 3 ⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ if((1 / 𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) ⇝_𝑟 𝐶 ↔ (𝑤 ∈ 𝐴 ↦ if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)))
132		nfcv 2903	. . . . 5 ⊢ Ⅎ𝑤if(𝑥 = 0, 𝐶, 𝑅)
133		nfv 1917	. . . . . 6 ⊢ Ⅎ𝑥 𝑤 = 0
134		nfcv 2903	. . . . . 6 ⊢ Ⅎ𝑥𝐶
135		nfcsb1v 3918	. . . . . 6 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝑅
136	133, 134, 135	nfif 4558	. . . . 5 ⊢ Ⅎ𝑥if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)
137		eqeq1 2736	. . . . . 6 ⊢ (𝑥 = 𝑤 → (𝑥 = 0 ↔ 𝑤 = 0))
138		csbeq1a 3907	. . . . . 6 ⊢ (𝑥 = 𝑤 → 𝑅 = ⦋𝑤 / 𝑥⦌𝑅)
139	137, 138	ifbieq2d 4554	. . . . 5 ⊢ (𝑥 = 𝑤 → if(𝑥 = 0, 𝐶, 𝑅) = if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅))
140	132, 136, 139	cbvmpt 5259	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) = (𝑤 ∈ 𝐴 ↦ if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅))
141	140	eleq1i 2824	. . 3 ⊢ ((𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0) ↔ (𝑤 ∈ 𝐴 ↦ if(𝑤 = 0, 𝐶, ⦋𝑤 / 𝑥⦌𝑅)) ∈ ((𝐾 CnP 𝐽)‘0))
142	131, 141	bitr4di 288	. 2 ⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∩ ℝ⁺) ↦ if((1 / 𝑦) = 0, 𝐶, ⦋(1 / 𝑦) / 𝑥⦌𝑅)) ⇝_𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)))
143	46, 66, 142	3bitr2d 306	1 ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝_𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2940 ∀wral 3061 ⦋csb 3893 ∩ cin 3947 ⊆ wss 3948 ifcif 4528 class class class wbr 5148 ↦ cmpt 5231 dom cdm 5676 ↾ cres 5678 Rel wrel 5681 Fn wfn 6538 ⟶wf 6539 ‘cfv 6543 (class class class)co 7411 ℂcc 11110 ℝcr 11111 0cc0 11112 1c1 11113 +∞cpnf 11247 ℝ^*cxr 11249 < clt 11250 ≤ cle 11251 / cdiv 11873 ℝ⁺crp 12976 (,)cioo 13326 [,)cico 13328 ⇝_𝑟 crli 15431 ↾_t crest 17368 TopOpenctopn 17369 ℂ_fldccnfld 20950 CnP ccnp 22736

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-er 8705 df-map 8824 df-pm 8825 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-sup 9439 df-inf 9440 df-pnf 11252 df-mnf 11253 df-xr 11254 df-ltxr 11255 df-le 11256 df-sub 11448 df-neg 11449 df-div 11874 df-nn 12215 df-2 12277 df-3 12278 df-4 12279 df-5 12280 df-6 12281 df-7 12282 df-8 12283 df-9 12284 df-n0 12475 df-z 12561 df-dec 12680 df-uz 12825 df-q 12935 df-rp 12977 df-xneg 13094 df-xadd 13095 df-xmul 13096 df-ioo 13330 df-ico 13332 df-fz 13487 df-seq 13969 df-exp 14030 df-cj 15048 df-re 15049 df-im 15050 df-sqrt 15184 df-abs 15185 df-rlim 15435 df-struct 17082 df-slot 17117 df-ndx 17129 df-base 17147 df-plusg 17212 df-mulr 17213 df-starv 17214 df-tset 17218 df-ple 17219 df-ds 17221 df-unif 17222 df-rest 17370 df-topn 17371 df-topgen 17391 df-psmet 20942 df-xmet 20943 df-met 20944 df-bl 20945 df-mopn 20946 df-cnfld 20951 df-top 22403 df-topon 22420 df-bases 22456 df-cnp 22739

This theorem is referenced by: rlimcnp3 26479

W3C validator