divcn - Metamath Proof Explorer

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

Theorem divcn 23478

Description: Complex number division is a continuous function, when the second argument is nonzero. (Contributed by Mario Carneiro, 12-Aug-2014.)

**Hypotheses**
Ref	Expression
addcn.j	⊢ 𝐽 = (TopOpen‘ℂ_fld)
divcn.k	⊢ 𝐾 = (𝐽 ↾_t (ℂ ∖ {0}))

**Assertion**
Ref	Expression
divcn	⊢ / ∈ ((𝐽 ×_t 𝐾) Cn 𝐽)

Proof of Theorem divcn Dummy variables 𝑢 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-div 11300	. . 3 ⊢ / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥))
2		eldifsn 4721	. . . . 5 ⊢ (𝑦 ∈ (ℂ ∖ {0}) ↔ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
3		divval 11302	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (𝑥 / 𝑦) = (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥))
4		divrec 11316	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (𝑥 / 𝑦) = (𝑥 · (1 / 𝑦)))
5	3, 4	eqtr3d 2860	. . . . . 6 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥) = (𝑥 · (1 / 𝑦)))
6	5	3expb 1116	. . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥) = (𝑥 · (1 / 𝑦)))
7	2, 6	sylan2b 595	. . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0})) → (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥) = (𝑥 · (1 / 𝑦)))
8	7	mpoeq3ia 7234	. . 3 ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥)) = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑥 · (1 / 𝑦)))
9	1, 8	eqtri 2846	. 2 ⊢ / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑥 · (1 / 𝑦)))
10		addcn.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
11	10	cnfldtopon 23393	. . . . 5 ⊢ 𝐽 ∈ (TopOn‘ℂ)
12	11	a1i 11	. . . 4 ⊢ (⊤ → 𝐽 ∈ (TopOn‘ℂ))
13		divcn.k	. . . . 5 ⊢ 𝐾 = (𝐽 ↾_t (ℂ ∖ {0}))
14		difss 4110	. . . . . 6 ⊢ (ℂ ∖ {0}) ⊆ ℂ
15		resttopon 21771	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘ℂ) ∧ (ℂ ∖ {0}) ⊆ ℂ) → (𝐽 ↾_t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0})))
16	12, 14, 15	sylancl 588	. . . . 5 ⊢ (⊤ → (𝐽 ↾_t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖ {0})))
17	13, 16	eqeltrid 2919	. . . 4 ⊢ (⊤ → 𝐾 ∈ (TopOn‘(ℂ ∖ {0})))
18	12, 17	cnmpt1st 22278	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ 𝑥) ∈ ((𝐽 ×_t 𝐾) Cn 𝐽))
19	12, 17	cnmpt2nd 22279	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ 𝑦) ∈ ((𝐽 ×_t 𝐾) Cn 𝐾))
20		eqid 2823	. . . . . . . 8 ⊢ (𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))
21		eldifsn 4721	. . . . . . . . 9 ⊢ (𝑧 ∈ (ℂ ∖ {0}) ↔ (𝑧 ∈ ℂ ∧ 𝑧 ≠ 0))
22		reccl 11307	. . . . . . . . 9 ⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ≠ 0) → (1 / 𝑧) ∈ ℂ)
23	21, 22	sylbi 219	. . . . . . . 8 ⊢ (𝑧 ∈ (ℂ ∖ {0}) → (1 / 𝑧) ∈ ℂ)
24	20, 23	fmpti 6878	. . . . . . 7 ⊢ (𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧)):(ℂ ∖ {0})⟶ℂ
25		eqid 2823	. . . . . . . . . 10 ⊢ (if(1 ≤ ((abs‘𝑥) · 𝑦), 1, ((abs‘𝑥) · 𝑦)) · ((abs‘𝑥) / 2)) = (if(1 ≤ ((abs‘𝑥) · 𝑦), 1, ((abs‘𝑥) · 𝑦)) · ((abs‘𝑥) / 2))
26	25	reccn2 14955	. . . . . . . . 9 ⊢ ((𝑥 ∈ (ℂ ∖ {0}) ∧ 𝑦 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑤 ∈ (ℂ ∖ {0})((abs‘(𝑤 − 𝑥)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑥))) < 𝑦))
27		ovres 7316	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (ℂ ∖ {0}) ∧ 𝑤 ∈ (ℂ ∖ {0})) → (𝑥((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) = (𝑥(abs ∘ − )𝑤))
28		eldifi 4105	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (ℂ ∖ {0}) → 𝑥 ∈ ℂ)
29		eldifi 4105	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (ℂ ∖ {0}) → 𝑤 ∈ ℂ)
30		eqid 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (abs ∘ − ) = (abs ∘ − )
31	30	cnmetdval 23381	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑥(abs ∘ − )𝑤) = (abs‘(𝑥 − 𝑤)))
32		abssub 14688	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (abs‘(𝑥 − 𝑤)) = (abs‘(𝑤 − 𝑥)))
33	31, 32	eqtrd 2858	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑥(abs ∘ − )𝑤) = (abs‘(𝑤 − 𝑥)))
34	28, 29, 33	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (ℂ ∖ {0}) ∧ 𝑤 ∈ (ℂ ∖ {0})) → (𝑥(abs ∘ − )𝑤) = (abs‘(𝑤 − 𝑥)))
35	27, 34	eqtrd 2858	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (ℂ ∖ {0}) ∧ 𝑤 ∈ (ℂ ∖ {0})) → (𝑥((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) = (abs‘(𝑤 − 𝑥)))
36	35	breq1d 5078	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (ℂ ∖ {0}) ∧ 𝑤 ∈ (ℂ ∖ {0})) → ((𝑥((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 ↔ (abs‘(𝑤 − 𝑥)) < 𝑢))
37		oveq2 7166	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑥 → (1 / 𝑧) = (1 / 𝑥))
38		ovex 7191	. . . . . . . . . . . . . . . . 17 ⊢ (1 / 𝑥) ∈ V
39	37, 20, 38	fvmpt 6770	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (ℂ ∖ {0}) → ((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥) = (1 / 𝑥))
40		oveq2 7166	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑤 → (1 / 𝑧) = (1 / 𝑤))
41		ovex 7191	. . . . . . . . . . . . . . . . 17 ⊢ (1 / 𝑤) ∈ V
42	40, 20, 41	fvmpt 6770	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (ℂ ∖ {0}) → ((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑤) = (1 / 𝑤))
43	39, 42	oveqan12d 7177	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (ℂ ∖ {0}) ∧ 𝑤 ∈ (ℂ ∖ {0})) → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑤)) = ((1 / 𝑥)(abs ∘ − )(1 / 𝑤)))
44		eldifsn 4721	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (ℂ ∖ {0}) ↔ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
45		reccl 11307	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ ℂ)
46	44, 45	sylbi 219	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (ℂ ∖ {0}) → (1 / 𝑥) ∈ ℂ)
47		eldifsn 4721	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ (ℂ ∖ {0}) ↔ (𝑤 ∈ ℂ ∧ 𝑤 ≠ 0))
48		reccl 11307	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) → (1 / 𝑤) ∈ ℂ)
49	47, 48	sylbi 219	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ (ℂ ∖ {0}) → (1 / 𝑤) ∈ ℂ)
50	30	cnmetdval 23381	. . . . . . . . . . . . . . . . 17 ⊢ (((1 / 𝑥) ∈ ℂ ∧ (1 / 𝑤) ∈ ℂ) → ((1 / 𝑥)(abs ∘ − )(1 / 𝑤)) = (abs‘((1 / 𝑥) − (1 / 𝑤))))
51		abssub 14688	. . . . . . . . . . . . . . . . 17 ⊢ (((1 / 𝑥) ∈ ℂ ∧ (1 / 𝑤) ∈ ℂ) → (abs‘((1 / 𝑥) − (1 / 𝑤))) = (abs‘((1 / 𝑤) − (1 / 𝑥))))
52	50, 51	eqtrd 2858	. . . . . . . . . . . . . . . 16 ⊢ (((1 / 𝑥) ∈ ℂ ∧ (1 / 𝑤) ∈ ℂ) → ((1 / 𝑥)(abs ∘ − )(1 / 𝑤)) = (abs‘((1 / 𝑤) − (1 / 𝑥))))
53	46, 49, 52	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (ℂ ∖ {0}) ∧ 𝑤 ∈ (ℂ ∖ {0})) → ((1 / 𝑥)(abs ∘ − )(1 / 𝑤)) = (abs‘((1 / 𝑤) − (1 / 𝑥))))
54	43, 53	eqtrd 2858	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ (ℂ ∖ {0}) ∧ 𝑤 ∈ (ℂ ∖ {0})) → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑤)) = (abs‘((1 / 𝑤) − (1 / 𝑥))))
55	54	breq1d 5078	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (ℂ ∖ {0}) ∧ 𝑤 ∈ (ℂ ∖ {0})) → ((((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑤)) < 𝑦 ↔ (abs‘((1 / 𝑤) − (1 / 𝑥))) < 𝑦))
56	36, 55	imbi12d 347	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (ℂ ∖ {0}) ∧ 𝑤 ∈ (ℂ ∖ {0})) → (((𝑥((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑤)) < 𝑦) ↔ ((abs‘(𝑤 − 𝑥)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑥))) < 𝑦)))
57	56	ralbidva 3198	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℂ ∖ {0}) → (∀𝑤 ∈ (ℂ ∖ {0})((𝑥((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑤)) < 𝑦) ↔ ∀𝑤 ∈ (ℂ ∖ {0})((abs‘(𝑤 − 𝑥)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑥))) < 𝑦)))
58	57	rexbidv 3299	. . . . . . . . . 10 ⊢ (𝑥 ∈ (ℂ ∖ {0}) → (∃𝑢 ∈ ℝ⁺ ∀𝑤 ∈ (ℂ ∖ {0})((𝑥((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑤)) < 𝑦) ↔ ∃𝑢 ∈ ℝ⁺ ∀𝑤 ∈ (ℂ ∖ {0})((abs‘(𝑤 − 𝑥)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑥))) < 𝑦)))
59	58	adantr 483	. . . . . . . . 9 ⊢ ((𝑥 ∈ (ℂ ∖ {0}) ∧ 𝑦 ∈ ℝ⁺) → (∃𝑢 ∈ ℝ⁺ ∀𝑤 ∈ (ℂ ∖ {0})((𝑥((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑤)) < 𝑦) ↔ ∃𝑢 ∈ ℝ⁺ ∀𝑤 ∈ (ℂ ∖ {0})((abs‘(𝑤 − 𝑥)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑥))) < 𝑦)))
60	26, 59	mpbird 259	. . . . . . . 8 ⊢ ((𝑥 ∈ (ℂ ∖ {0}) ∧ 𝑦 ∈ ℝ⁺) → ∃𝑢 ∈ ℝ⁺ ∀𝑤 ∈ (ℂ ∖ {0})((𝑥((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑤)) < 𝑦))
61	60	rgen2 3205	. . . . . . 7 ⊢ ∀𝑥 ∈ (ℂ ∖ {0})∀𝑦 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑤 ∈ (ℂ ∖ {0})((𝑥((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑤)) < 𝑦)
62		cnxmet 23383	. . . . . . . . 9 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
63		xmetres2 22973	. . . . . . . . 9 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖ {0}) ⊆ ℂ) → ((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0}))) ∈ (∞Met‘(ℂ ∖ {0})))
64	62, 14, 63	mp2an 690	. . . . . . . 8 ⊢ ((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0}))) ∈ (∞Met‘(ℂ ∖ {0}))
65		eqid 2823	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0}))) = ((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))
66	10	cnfldtopn 23392	. . . . . . . . . . . 12 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
67		eqid 2823	. . . . . . . . . . . 12 ⊢ (MetOpen‘((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))) = (MetOpen‘((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0}))))
68	65, 66, 67	metrest 23136	. . . . . . . . . . 11 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖ {0}) ⊆ ℂ) → (𝐽 ↾_t (ℂ ∖ {0})) = (MetOpen‘((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))))
69	62, 14, 68	mp2an 690	. . . . . . . . . 10 ⊢ (𝐽 ↾_t (ℂ ∖ {0})) = (MetOpen‘((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0}))))
70	13, 69	eqtri 2846	. . . . . . . . 9 ⊢ 𝐾 = (MetOpen‘((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0}))))
71	70, 66	metcn 23155	. . . . . . . 8 ⊢ ((((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0}))) ∈ (∞Met‘(ℂ ∖ {0})) ∧ (abs ∘ − ) ∈ (∞Met‘ℂ)) → ((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧)) ∈ (𝐾 Cn 𝐽) ↔ ((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧)):(ℂ ∖ {0})⟶ℂ ∧ ∀𝑥 ∈ (ℂ ∖ {0})∀𝑦 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑤 ∈ (ℂ ∖ {0})((𝑥((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑤)) < 𝑦))))
72	64, 62, 71	mp2an 690	. . . . . . 7 ⊢ ((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧)) ∈ (𝐾 Cn 𝐽) ↔ ((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧)):(ℂ ∖ {0})⟶ℂ ∧ ∀𝑥 ∈ (ℂ ∖ {0})∀𝑦 ∈ ℝ⁺ ∃𝑢 ∈ ℝ⁺ ∀𝑤 ∈ (ℂ ∖ {0})((𝑥((abs ∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑤)) < 𝑦)))
73	24, 61, 72	mpbir2an 709	. . . . . 6 ⊢ (𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧)) ∈ (𝐾 Cn 𝐽)
74	73	a1i 11	. . . . 5 ⊢ (⊤ → (𝑧 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑧)) ∈ (𝐾 Cn 𝐽))
75		oveq2 7166	. . . . 5 ⊢ (𝑧 = 𝑦 → (1 / 𝑧) = (1 / 𝑦))
76	12, 17, 19, 17, 74, 75	cnmpt21 22281	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑦)) ∈ ((𝐽 ×_t 𝐾) Cn 𝐽))
77	10	mulcn 23477	. . . . 5 ⊢ · ∈ ((𝐽 ×_t 𝐽) Cn 𝐽)
78	77	a1i 11	. . . 4 ⊢ (⊤ → · ∈ ((𝐽 ×_t 𝐽) Cn 𝐽))
79	12, 17, 18, 76, 78	cnmpt22f 22285	. . 3 ⊢ (⊤ → (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑥 · (1 / 𝑦))) ∈ ((𝐽 ×_t 𝐾) Cn 𝐽))
80	79	mptru 1544	. 2 ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑥 · (1 / 𝑦))) ∈ ((𝐽 ×_t 𝐾) Cn 𝐽)
81	9, 80	eqeltri 2911	1 ⊢ / ∈ ((𝐽 ×_t 𝐾) Cn 𝐽)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ⊤wtru 1538 ∈ wcel 2114 ≠ wne 3018 ∀wral 3140 ∃wrex 3141 ∖ cdif 3935 ⊆ wss 3938 ifcif 4469 {csn 4569 class class class wbr 5068 ↦ cmpt 5148 × cxp 5555 ↾ cres 5559 ∘ ccom 5561 ⟶wf 6353 ‘cfv 6357 ℩crio 7115 (class class class)co 7158 ∈ cmpo 7160 ℂcc 10537 0cc0 10539 1c1 10540 · cmul 10544 < clt 10677 ≤ cle 10678 − cmin 10872 / cdiv 11299 2c2 11695 ℝ⁺crp 12392 abscabs 14595 ↾_t crest 16696 TopOpenctopn 16697 ∞Metcxmet 20532 MetOpencmopn 20537 ℂ_fldccnfld 20547 TopOnctopon 21520 Cn ccn 21834 ×_t ctx 22170

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616 ax-pre-sup 10617 ax-mulf 10619

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-iin 4924 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-se 5517 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-isom 6366 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-of 7411 df-om 7583 df-1st 7691 df-2nd 7692 df-supp 7833 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-2o 8105 df-oadd 8108 df-er 8291 df-map 8410 df-ixp 8464 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-fsupp 8836 df-fi 8877 df-sup 8908 df-inf 8909 df-oi 8976 df-card 9370 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-div 11300 df-nn 11641 df-2 11703 df-3 11704 df-4 11705 df-5 11706 df-6 11707 df-7 11708 df-8 11709 df-9 11710 df-n0 11901 df-z 11985 df-dec 12102 df-uz 12247 df-q 12352 df-rp 12393 df-xneg 12510 df-xadd 12511 df-xmul 12512 df-icc 12748 df-fz 12896 df-fzo 13037 df-seq 13373 df-exp 13433 df-hash 13694 df-cj 14460 df-re 14461 df-im 14462 df-sqrt 14596 df-abs 14597 df-struct 16487 df-ndx 16488 df-slot 16489 df-base 16491 df-sets 16492 df-ress 16493 df-plusg 16580 df-mulr 16581 df-starv 16582 df-sca 16583 df-vsca 16584 df-ip 16585 df-tset 16586 df-ple 16587 df-ds 16589 df-unif 16590 df-hom 16591 df-cco 16592 df-rest 16698 df-topn 16699 df-0g 16717 df-gsum 16718 df-topgen 16719 df-pt 16720 df-prds 16723 df-xrs 16777 df-qtop 16782 df-imas 16783 df-xps 16785 df-mre 16859 df-mrc 16860 df-acs 16862 df-mgm 17854 df-sgrp 17903 df-mnd 17914 df-submnd 17959 df-mulg 18227 df-cntz 18449 df-cmn 18910 df-psmet 20539 df-xmet 20540 df-met 20541 df-bl 20542 df-mopn 20543 df-cnfld 20548 df-top 21504 df-topon 21521 df-topsp 21543 df-bases 21556 df-cn 21837 df-cnp 21838 df-tx 22172 df-hmeo 22365 df-xms 22932 df-ms 22933 df-tms 22934

This theorem is referenced by: cdivcncf 23527 evth 23565 dvcnvlem 24575 lhop1lem 24612

W3C validator