cdivcncfap - Intuitionistic Logic Explorer

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

Theorem cdivcncfap 14924

Description: Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.)

**Hypothesis**
Ref	Expression
cdivcncf.1	⊢ 𝐹 = (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (𝐴 / 𝑥))

**Assertion**
Ref	Expression
cdivcncfap	⊢ (𝐴 ∈ ℂ → 𝐹 ∈ ({𝑦 ∈ ℂ ∣ 𝑦 # 0}–cn→ℂ))

Distinct variable group: 𝑥,𝐴,𝑦 Allowed substitution hints: 𝐹(𝑥,𝑦)

Proof of Theorem cdivcncfap Dummy variables 𝑤 𝑧 𝑎 𝑏 𝑑 𝑒 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cdivcncf.1	. 2 ⊢ 𝐹 = (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (𝐴 / 𝑥))
2		simpl 109	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → 𝐴 ∈ ℂ)
3		breq1 4037	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 # 0 ↔ 𝑥 # 0))
4	3	elrab 2920	. . . . . . . 8 ⊢ (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↔ (𝑥 ∈ ℂ ∧ 𝑥 # 0))
5	4	biimpi 120	. . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} → (𝑥 ∈ ℂ ∧ 𝑥 # 0))
6	5	adantl 277	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → (𝑥 ∈ ℂ ∧ 𝑥 # 0))
7	6	simpld 112	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → 𝑥 ∈ ℂ)
8	6	simprd 114	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → 𝑥 # 0)
9	2, 7, 8	divrecapd 8837	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → (𝐴 / 𝑥) = (𝐴 · (1 / 𝑥)))
10	9	mpteq2dva 4124	. . 3 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (𝐴 / 𝑥)) = (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (𝐴 · (1 / 𝑥))))
11		recclap 8723	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ 𝑥 # 0) → (1 / 𝑥) ∈ ℂ)
12	4, 11	sylbi 121	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} → (1 / 𝑥) ∈ ℂ)
13	12	adantl 277	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → (1 / 𝑥) ∈ ℂ)
14		oveq2 5933	. . . . . . 7 ⊢ (𝑤 = 𝑥 → (1 / 𝑤) = (1 / 𝑥))
15	14	cbvmptv 4130	. . . . . 6 ⊢ (𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤)) = (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑥))
16	15	a1i 9	. . . . 5 ⊢ (𝐴 ∈ ℂ → (𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤)) = (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑥)))
17		eqidd 2197	. . . . 5 ⊢ (𝐴 ∈ ℂ → (𝑧 ∈ ℂ ↦ (𝐴 · 𝑧)) = (𝑧 ∈ ℂ ↦ (𝐴 · 𝑧)))
18		oveq2 5933	. . . . 5 ⊢ (𝑧 = (1 / 𝑥) → (𝐴 · 𝑧) = (𝐴 · (1 / 𝑥)))
19	13, 16, 17, 18	fmptco 5731	. . . 4 ⊢ (𝐴 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝐴 · 𝑧)) ∘ (𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))) = (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (𝐴 · (1 / 𝑥))))
20		breq1 4037	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑦 # 0 ↔ 𝑤 # 0))
21	20	elrab 2920	. . . . . . . . 9 ⊢ (𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↔ (𝑤 ∈ ℂ ∧ 𝑤 # 0))
22		recclap 8723	. . . . . . . . 9 ⊢ ((𝑤 ∈ ℂ ∧ 𝑤 # 0) → (1 / 𝑤) ∈ ℂ)
23	21, 22	sylbi 121	. . . . . . . 8 ⊢ (𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} → (1 / 𝑤) ∈ ℂ)
24	23	adantl 277	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → (1 / 𝑤) ∈ ℂ)
25	24	fmpttd 5720	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤)):{𝑦 ∈ ℂ ∣ 𝑦 # 0}⟶ℂ)
26		breq1 4037	. . . . . . . . 9 ⊢ (𝑦 = 𝑏 → (𝑦 # 0 ↔ 𝑏 # 0))
27	26	elrab 2920	. . . . . . . 8 ⊢ (𝑏 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↔ (𝑏 ∈ ℂ ∧ 𝑏 # 0))
28		eqid 2196	. . . . . . . . . . . 12 ⊢ (inf({1, ((abs‘𝑏) · 𝑒)}, ℝ, < ) · ((abs‘𝑏) / 2)) = (inf({1, ((abs‘𝑏) · 𝑒)}, ℝ, < ) · ((abs‘𝑏) / 2))
29	28	reccn2ap 11495	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) → ∃𝑑 ∈ ℝ⁺ ∀𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘((1 / 𝑎) − (1 / 𝑏))) < 𝑒))
30		eqidd 2197	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → (𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤)) = (𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤)))
31		oveq2 5933	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑎 → (1 / 𝑤) = (1 / 𝑎))
32	31	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) ∧ 𝑤 = 𝑎) → (1 / 𝑤) = (1 / 𝑎))
33		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0})
34		breq1 4037	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑎 → (𝑦 # 0 ↔ 𝑎 # 0))
35	34	elrab 2920	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↔ (𝑎 ∈ ℂ ∧ 𝑎 # 0))
36		recclap 8723	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ℂ ∧ 𝑎 # 0) → (1 / 𝑎) ∈ ℂ)
37	35, 36	sylbi 121	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} → (1 / 𝑎) ∈ ℂ)
38	37	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → (1 / 𝑎) ∈ ℂ)
39	30, 32, 33, 38	fvmptd 5645	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) = (1 / 𝑎))
40		oveq2 5933	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑏 → (1 / 𝑤) = (1 / 𝑏))
41	40	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) ∧ 𝑤 = 𝑏) → (1 / 𝑤) = (1 / 𝑏))
42		simpll1 1038	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → 𝑏 ∈ ℂ)
43		simpll2 1039	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → 𝑏 # 0)
44	26, 42, 43	elrabd 2922	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → 𝑏 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0})
45	42, 43	recclapd 8825	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → (1 / 𝑏) ∈ ℂ)
46	30, 41, 44, 45	fvmptd 5645	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏) = (1 / 𝑏))
47	39, 46	oveq12d 5943	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → (((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) − ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏)) = ((1 / 𝑎) − (1 / 𝑏)))
48	47	fveq2d 5565	. . . . . . . . . . . . . . 15 ⊢ ((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → (abs‘(((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) − ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏))) = (abs‘((1 / 𝑎) − (1 / 𝑏))))
49	48	breq1d 4044	. . . . . . . . . . . . . 14 ⊢ ((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → ((abs‘(((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) − ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏))) < 𝑒 ↔ (abs‘((1 / 𝑎) − (1 / 𝑏))) < 𝑒))
50	49	imbi2d 230	. . . . . . . . . . . . 13 ⊢ ((((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}) → (((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘(((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) − ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏))) < 𝑒) ↔ ((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘((1 / 𝑎) − (1 / 𝑏))) < 𝑒)))
51	50	ralbidva 2493	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) ∧ 𝑑 ∈ ℝ⁺) → (∀𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘(((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) − ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏))) < 𝑒) ↔ ∀𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘((1 / 𝑎) − (1 / 𝑏))) < 𝑒)))
52	51	rexbidva 2494	. . . . . . . . . . 11 ⊢ ((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) → (∃𝑑 ∈ ℝ⁺ ∀𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘(((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) − ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏))) < 𝑒) ↔ ∃𝑑 ∈ ℝ⁺ ∀𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘((1 / 𝑎) − (1 / 𝑏))) < 𝑒)))
53	29, 52	mpbird 167	. . . . . . . . . 10 ⊢ ((𝑏 ∈ ℂ ∧ 𝑏 # 0 ∧ 𝑒 ∈ ℝ⁺) → ∃𝑑 ∈ ℝ⁺ ∀𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘(((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) − ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏))) < 𝑒))
54	53	3expa 1205	. . . . . . . . 9 ⊢ (((𝑏 ∈ ℂ ∧ 𝑏 # 0) ∧ 𝑒 ∈ ℝ⁺) → ∃𝑑 ∈ ℝ⁺ ∀𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘(((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) − ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏))) < 𝑒))
55	54	ralrimiva 2570	. . . . . . . 8 ⊢ ((𝑏 ∈ ℂ ∧ 𝑏 # 0) → ∀𝑒 ∈ ℝ⁺ ∃𝑑 ∈ ℝ⁺ ∀𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘(((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) − ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏))) < 𝑒))
56	27, 55	sylbi 121	. . . . . . 7 ⊢ (𝑏 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} → ∀𝑒 ∈ ℝ⁺ ∃𝑑 ∈ ℝ⁺ ∀𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘(((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) − ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏))) < 𝑒))
57	56	rgen 2550	. . . . . 6 ⊢ ∀𝑏 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}∀𝑒 ∈ ℝ⁺ ∃𝑑 ∈ ℝ⁺ ∀𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘(((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) − ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏))) < 𝑒)
58		ssrab2 3269	. . . . . . 7 ⊢ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ⊆ ℂ
59		ssid 3204	. . . . . . 7 ⊢ ℂ ⊆ ℂ
60		elcncf2 14894	. . . . . . 7 ⊢ (({𝑦 ∈ ℂ ∣ 𝑦 # 0} ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤)) ∈ ({𝑦 ∈ ℂ ∣ 𝑦 # 0}–cn→ℂ) ↔ ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤)):{𝑦 ∈ ℂ ∣ 𝑦 # 0}⟶ℂ ∧ ∀𝑏 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}∀𝑒 ∈ ℝ⁺ ∃𝑑 ∈ ℝ⁺ ∀𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘(((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) − ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏))) < 𝑒))))
61	58, 59, 60	mp2an 426	. . . . . 6 ⊢ ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤)) ∈ ({𝑦 ∈ ℂ ∣ 𝑦 # 0}–cn→ℂ) ↔ ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤)):{𝑦 ∈ ℂ ∣ 𝑦 # 0}⟶ℂ ∧ ∀𝑏 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0}∀𝑒 ∈ ℝ⁺ ∃𝑑 ∈ ℝ⁺ ∀𝑎 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ((abs‘(𝑎 − 𝑏)) < 𝑑 → (abs‘(((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑎) − ((𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))‘𝑏))) < 𝑒)))
62	25, 57, 61	sylanblrc 416	. . . . 5 ⊢ (𝐴 ∈ ℂ → (𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤)) ∈ ({𝑦 ∈ ℂ ∣ 𝑦 # 0}–cn→ℂ))
63		eqid 2196	. . . . . 6 ⊢ (𝑧 ∈ ℂ ↦ (𝐴 · 𝑧)) = (𝑧 ∈ ℂ ↦ (𝐴 · 𝑧))
64	63	mulc1cncf 14909	. . . . 5 ⊢ (𝐴 ∈ ℂ → (𝑧 ∈ ℂ ↦ (𝐴 · 𝑧)) ∈ (ℂ–cn→ℂ))
65	62, 64	cncfco 14911	. . . 4 ⊢ (𝐴 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝐴 · 𝑧)) ∘ (𝑤 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (1 / 𝑤))) ∈ ({𝑦 ∈ ℂ ∣ 𝑦 # 0}–cn→ℂ))
66	19, 65	eqeltrrd 2274	. . 3 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (𝐴 · (1 / 𝑥))) ∈ ({𝑦 ∈ ℂ ∣ 𝑦 # 0}–cn→ℂ))
67	10, 66	eqeltrd 2273	. 2 ⊢ (𝐴 ∈ ℂ → (𝑥 ∈ {𝑦 ∈ ℂ ∣ 𝑦 # 0} ↦ (𝐴 / 𝑥)) ∈ ({𝑦 ∈ ℂ ∣ 𝑦 # 0}–cn→ℂ))
68	1, 67	eqeltrid 2283	1 ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ ({𝑦 ∈ ℂ ∣ 𝑦 # 0}–cn→ℂ))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 980 = wceq 1364 ∈ wcel 2167 ∀wral 2475 ∃wrex 2476 {crab 2479 ⊆ wss 3157 {cpr 3624 class class class wbr 4034 ↦ cmpt 4095 ∘ ccom 4668 ⟶wf 5255 ‘cfv 5259 (class class class)co 5925 infcinf 7058 ℂcc 7894 ℝcr 7895 0cc0 7896 1c1 7897 · cmul 7901 < clt 8078 − cmin 8214 # cap 8625 / cdiv 8716 2c2 9058 ℝ⁺crp 9745 abscabs 11179 –cn→ccncf 14890

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7987 ax-resscn 7988 ax-1cn 7989 ax-1re 7990 ax-icn 7991 ax-addcl 7992 ax-addrcl 7993 ax-mulcl 7994 ax-mulrcl 7995 ax-addcom 7996 ax-mulcom 7997 ax-addass 7998 ax-mulass 7999 ax-distr 8000 ax-i2m1 8001 ax-0lt1 8002 ax-1rid 8003 ax-0id 8004 ax-rnegex 8005 ax-precex 8006 ax-cnre 8007 ax-pre-ltirr 8008 ax-pre-ltwlin 8009 ax-pre-lttrn 8010 ax-pre-apti 8011 ax-pre-ltadd 8012 ax-pre-mulgt0 8013 ax-pre-mulext 8014 ax-arch 8015 ax-caucvg 8016

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-po 4332 df-iso 4333 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-isom 5268 df-riota 5880 df-ov 5928 df-oprab 5929 df-mpo 5930 df-1st 6207 df-2nd 6208 df-recs 6372 df-frec 6458 df-map 6718 df-sup 7059 df-inf 7060 df-pnf 8080 df-mnf 8081 df-xr 8082 df-ltxr 8083 df-le 8084 df-sub 8216 df-neg 8217 df-reap 8619 df-ap 8626 df-div 8717 df-inn 9008 df-2 9066 df-3 9067 df-4 9068 df-n0 9267 df-z 9344 df-uz 9619 df-rp 9746 df-seqfrec 10557 df-exp 10648 df-cj 11024 df-re 11025 df-im 11026 df-rsqrt 11180 df-abs 11181 df-cncf 14891

This theorem is referenced by: divcncfap 14934 dvrecap 15033

W3C validator