divcnOLD

Description: Obsolete version of divcn as of 6-Apr-2025. (Contributed by Mario Carneiro, 12-Aug-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	addcn.j	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
	divcnOLD.k	⊢ 𝐾 = ( 𝐽 ↾_t ( ℂ ∖ { 0 } ) )
Assertion	divcnOLD	⊢ / ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		addcn.j	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
2		divcnOLD.k	⊢ 𝐾 = ( 𝐽 ↾_t ( ℂ ∖ { 0 } ) )
3		df-div	⊢ / = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
4		eldifsn	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
5		divval	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 𝑥 / 𝑦 ) = ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
6		divrec	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 𝑥 / 𝑦 ) = ( 𝑥 · ( 1 / 𝑦 ) ) )
7	5 6	eqtr3d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) = ( 𝑥 · ( 1 / 𝑦 ) ) )
8	7	3expb	⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) = ( 𝑥 · ( 1 / 𝑦 ) ) )
9	4 8	sylan2b	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) = ( 𝑥 · ( 1 / 𝑦 ) ) )
10	9	mpoeq3ia	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · ( 1 / 𝑦 ) ) )
11	3 10	eqtri	⊢ / = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · ( 1 / 𝑦 ) ) )
12	1	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
13	12	a1i	⊢ ( ⊤ → 𝐽 ∈ ( TopOn ‘ ℂ ) )
14		difss	⊢ ( ℂ ∖ { 0 } ) ⊆ ℂ
15		resttopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ) → ( 𝐽 ↾_t ( ℂ ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) ) )
16	13 14 15	sylancl	⊢ ( ⊤ → ( 𝐽 ↾_t ( ℂ ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) ) )
17	2 16	eqeltrid	⊢ ( ⊤ → 𝐾 ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) ) )
18	13 17	cnmpt1st	⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ 𝑥 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐽 ) )
19	13 17	cnmpt2nd	⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ 𝑦 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐾 ) )
20		eqid	⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) = ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) )
21		eldifsn	⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 0 ) )
22		reccl	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 0 ) → ( 1 / 𝑧 ) ∈ ℂ )
23	21 22	sylbi	⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑧 ) ∈ ℂ )
24	20 23	fmpti	⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ
25		eqid	⊢ ( if ( 1 ≤ ( ( abs ‘ 𝑥 ) · 𝑦 ) , 1 , ( ( abs ‘ 𝑥 ) · 𝑦 ) ) · ( ( abs ‘ 𝑥 ) / 2 ) ) = ( if ( 1 ≤ ( ( abs ‘ 𝑥 ) · 𝑦 ) , 1 , ( ( abs ‘ 𝑥 ) · 𝑦 ) ) · ( ( abs ‘ 𝑥 ) / 2 ) )
26	25	reccn2	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑢 → ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) < 𝑦 ) )
27		ovres	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) = ( 𝑥 ( abs ∘ − ) 𝑤 ) )
28		eldifi	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → 𝑥 ∈ ℂ )
29		eldifi	⊢ ( 𝑤 ∈ ( ℂ ∖ { 0 } ) → 𝑤 ∈ ℂ )
30		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
31	30	cnmetdval	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 𝑤 ) = ( abs ‘ ( 𝑥 − 𝑤 ) ) )
32		abssub	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( abs ‘ ( 𝑥 − 𝑤 ) ) = ( abs ‘ ( 𝑤 − 𝑥 ) ) )
33	31 32	eqtrd	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 𝑤 ) = ( abs ‘ ( 𝑤 − 𝑥 ) ) )
34	28 29 33	syl2an	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( abs ∘ − ) 𝑤 ) = ( abs ‘ ( 𝑤 − 𝑥 ) ) )
35	27 34	eqtrd	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) = ( abs ‘ ( 𝑤 − 𝑥 ) ) )
36	35	breq1d	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 ↔ ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑢 ) )
37		oveq2	⊢ ( 𝑧 = 𝑥 → ( 1 / 𝑧 ) = ( 1 / 𝑥 ) )
38		ovex	⊢ ( 1 / 𝑥 ) ∈ V
39	37 20 38	fvmpt	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) = ( 1 / 𝑥 ) )
40		oveq2	⊢ ( 𝑧 = 𝑤 → ( 1 / 𝑧 ) = ( 1 / 𝑤 ) )
41		ovex	⊢ ( 1 / 𝑤 ) ∈ V
42	40 20 41	fvmpt	⊢ ( 𝑤 ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) = ( 1 / 𝑤 ) )
43	39 42	oveqan12d	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) = ( ( 1 / 𝑥 ) ( abs ∘ − ) ( 1 / 𝑤 ) ) )
44		eldifsn	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
45		reccl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ ℂ )
46	44 45	sylbi	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑥 ) ∈ ℂ )
47		eldifsn	⊢ ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) )
48		reccl	⊢ ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) → ( 1 / 𝑤 ) ∈ ℂ )
49	47 48	sylbi	⊢ ( 𝑤 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑤 ) ∈ ℂ )
50	30	cnmetdval	⊢ ( ( ( 1 / 𝑥 ) ∈ ℂ ∧ ( 1 / 𝑤 ) ∈ ℂ ) → ( ( 1 / 𝑥 ) ( abs ∘ − ) ( 1 / 𝑤 ) ) = ( abs ‘ ( ( 1 / 𝑥 ) − ( 1 / 𝑤 ) ) ) )
51		abssub	⊢ ( ( ( 1 / 𝑥 ) ∈ ℂ ∧ ( 1 / 𝑤 ) ∈ ℂ ) → ( abs ‘ ( ( 1 / 𝑥 ) − ( 1 / 𝑤 ) ) ) = ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) )
52	50 51	eqtrd	⊢ ( ( ( 1 / 𝑥 ) ∈ ℂ ∧ ( 1 / 𝑤 ) ∈ ℂ ) → ( ( 1 / 𝑥 ) ( abs ∘ − ) ( 1 / 𝑤 ) ) = ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) )
53	46 49 52	syl2an	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 1 / 𝑥 ) ( abs ∘ − ) ( 1 / 𝑤 ) ) = ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) )
54	43 53	eqtrd	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) = ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) )
55	54	breq1d	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ↔ ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) < 𝑦 ) )
56	36 55	imbi12d	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑢 → ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) < 𝑦 ) ) )
57	56	ralbidva	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → ( ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑢 → ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) < 𝑦 ) ) )
58	57	rexbidv	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → ( ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ) ↔ ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑢 → ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) < 𝑦 ) ) )
59	58	adantr	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ℝ⁺ ) → ( ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ) ↔ ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑢 → ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) < 𝑦 ) ) )
60	26 59	mpbird	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ℝ⁺ ) → ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ) )
61	60	rgen2	⊢ ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 )
62		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
63		xmetres2	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) ∈ ( ∞Met ‘ ( ℂ ∖ { 0 } ) ) )
64	62 14 63	mp2an	⊢ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) ∈ ( ∞Met ‘ ( ℂ ∖ { 0 } ) )
65		eqid	⊢ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) = ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) )
66	1	cnfldtopn	⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
67		eqid	⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) )
68	65 66 67	metrest	⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ) → ( 𝐽 ↾_t ( ℂ ∖ { 0 } ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) ) )
69	62 14 68	mp2an	⊢ ( 𝐽 ↾_t ( ℂ ∖ { 0 } ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) )
70	2 69	eqtri	⊢ 𝐾 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) )
71	70 66	metcn	⊢ ( ( ( ( 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	⊢ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 ) ↔ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑢 ∈ ℝ⁺ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ) ) )
73	24 61 72	mpbir2an	⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 )
74	73	a1i	⊢ ( ⊤ → ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 ) )
75		oveq2	⊢ ( 𝑧 = 𝑦 → ( 1 / 𝑧 ) = ( 1 / 𝑦 ) )
76	13 17 19 17 74 75	cnmpt21	⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐽 ) )
77	1	mulcn	⊢ · ∈ ( ( 𝐽 ×_t 𝐽 ) Cn 𝐽 )
78	77	a1i	⊢ ( ⊤ → · ∈ ( ( 𝐽 ×_t 𝐽 ) Cn 𝐽 ) )
79	13 17 18 76 78	cnmpt22f	⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · ( 1 / 𝑦 ) ) ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐽 ) )
80	79	mptru	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · ( 1 / 𝑦 ) ) ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐽 )
81	11 80	eqeltri	⊢ / ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐽 )

Metamath Proof Explorer

Theorem divcnOLD

Proof