mpomulcn

Description: Complex number multiplication is a continuous function. Version of mulcn using maps-to notation, which does not require ax-mulf . (Contributed by GG, 16-Mar-2025)

		Ref	Expression
	Hypothesis	mpomulcn.j	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
	Assertion	mpomulcn	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( 𝐽 ×_t 𝐽 ) Cn 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		mpomulcn.j	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
2		mpomulf	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) : ( ℂ × ℂ ) ⟶ ℂ
3		mulcn2	⊢ ( ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ∃ 𝑧 ∈ ℝ⁺ ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑑 ∈ ℂ ∀ 𝑒 ∈ ℂ ( ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ) )
4		simplr	⊢ ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) → 𝑢 ∈ ℂ )
5		simplll	⊢ ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) → 𝑣 ∈ ℂ )
6		simplr	⊢ ( ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → 𝑑 = 𝑢 )
7	6	fvoveq1d	⊢ ( ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( abs ‘ ( 𝑑 − 𝑏 ) ) = ( abs ‘ ( 𝑢 − 𝑏 ) ) )
8	7	breq1d	⊢ ( ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ) )
9		simpr	⊢ ( ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → 𝑒 = 𝑣 )
10	9	fvoveq1d	⊢ ( ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( abs ‘ ( 𝑒 − 𝑐 ) ) = ( abs ‘ ( 𝑣 − 𝑐 ) ) )
11	10	breq1d	⊢ ( ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ↔ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) )
12	8 11	anbi12d	⊢ ( ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ) ↔ ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) ) )
13		simplr	⊢ ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → 𝑑 = 𝑢 )
14	13	eqcomd	⊢ ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → 𝑢 = 𝑑 )
15		simpr	⊢ ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → 𝑒 = 𝑣 )
16	15	eqcomd	⊢ ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → 𝑣 = 𝑒 )
17	14 16	oveq12d	⊢ ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( 𝑢 · 𝑣 ) = ( 𝑑 · 𝑒 ) )
18		simplr	⊢ ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ 𝑑 = 𝑢 ) → 𝑢 ∈ ℂ )
19		simplll	⊢ ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → 𝑣 ∈ ℂ )
20		tru	⊢ ⊤
21		oveq1	⊢ ( 𝑥 = 𝑢 → ( 𝑥 · 𝑦 ) = ( 𝑢 · 𝑦 ) )
22		oveq2	⊢ ( 𝑦 = 𝑣 → ( 𝑢 · 𝑦 ) = ( 𝑢 · 𝑣 ) )
23	21 22	cbvmpov	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) = ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) )
24	23	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) = ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) )
25		eqidd	⊢ ( ⊤ → ⟨ 𝑢 , 𝑣 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ )
26		mulcl	⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑢 · 𝑣 ) ∈ ℂ )
27	26	3adant1	⊢ ( ( ⊤ ∧ 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑢 · 𝑣 ) ∈ ℂ )
28	24 25 27	fvmpopr2d	⊢ ( ( ⊤ ∧ 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ( 𝑢 · 𝑣 ) )
29	28	eqcomd	⊢ ( ( ⊤ ∧ 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑢 · 𝑣 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
30	20 29	mp3an1	⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑢 · 𝑣 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
31		df-ov	⊢ ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
32	30 31	eqtr4di	⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑢 · 𝑣 ) = ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) )
33	18 19 32	syl2an2r	⊢ ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( 𝑢 · 𝑣 ) = ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) )
34	17 33	eqtr3d	⊢ ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( 𝑑 · 𝑒 ) = ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) )
35	34	adantllr	⊢ ( ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( 𝑑 · 𝑒 ) = ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) )
36		df-ov	⊢ ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) = ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑏 , 𝑐 ⟩ )
37		oveq1	⊢ ( 𝑥 = 𝑏 → ( 𝑥 · 𝑦 ) = ( 𝑏 · 𝑦 ) )
38		oveq2	⊢ ( 𝑦 = 𝑐 → ( 𝑏 · 𝑦 ) = ( 𝑏 · 𝑐 ) )
39	37 38	cbvmpov	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) = ( 𝑏 ∈ ℂ , 𝑐 ∈ ℂ ↦ ( 𝑏 · 𝑐 ) )
40	39	a1i	⊢ ( 𝑎 ∈ ℝ⁺ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) = ( 𝑏 ∈ ℂ , 𝑐 ∈ ℂ ↦ ( 𝑏 · 𝑐 ) ) )
41		eqidd	⊢ ( 𝑎 ∈ ℝ⁺ → ⟨ 𝑏 , 𝑐 ⟩ = ⟨ 𝑏 , 𝑐 ⟩ )
42		mulcl	⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( 𝑏 · 𝑐 ) ∈ ℂ )
43	42	3adant1	⊢ ( ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( 𝑏 · 𝑐 ) ∈ ℂ )
44	40 41 43	fvmpopr2d	⊢ ( ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ‘ ⟨ 𝑏 , 𝑐 ⟩ ) = ( 𝑏 · 𝑐 ) )
45	36 44	eqtr2id	⊢ ( ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( 𝑏 · 𝑐 ) = ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) )
46	45	ad3antlr	⊢ ( ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( 𝑏 · 𝑐 ) = ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) )
47	35 46	oveq12d	⊢ ( ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) = ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) )
48	47	fveq2d	⊢ ( ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) = ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) )
49	48	breq1d	⊢ ( ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ↔ ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) < 𝑎 ) )
50	12 49	imbi12d	⊢ ( ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) ∧ 𝑒 = 𝑣 ) → ( ( ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ) ↔ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) < 𝑎 ) ) )
51	5 50	rspcdv	⊢ ( ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) ∧ 𝑑 = 𝑢 ) → ( ∀ 𝑒 ∈ ℂ ( ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ) → ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) < 𝑎 ) ) )
52	4 51	rspcimdv	⊢ ( ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) ∧ ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ) → ( ∀ 𝑑 ∈ ℂ ∀ 𝑒 ∈ ℂ ( ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ) → ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) < 𝑎 ) ) )
53	52	expimpd	⊢ ( ( 𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ ) → ( ( ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ∧ ∀ 𝑑 ∈ ℂ ∀ 𝑒 ∈ ℂ ( ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ) ) → ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) < 𝑎 ) ) )
54	53	ex	⊢ ( 𝑣 ∈ ℂ → ( 𝑢 ∈ ℂ → ( ( ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ∧ ∀ 𝑑 ∈ ℂ ∀ 𝑒 ∈ ℂ ( ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ) ) → ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) < 𝑎 ) ) ) )
55	54	com13	⊢ ( ( ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ∧ ∀ 𝑑 ∈ ℂ ∀ 𝑒 ∈ ℂ ( ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ) ) → ( 𝑢 ∈ ℂ → ( 𝑣 ∈ ℂ → ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) < 𝑎 ) ) ) )
56	55	ralrimdv	⊢ ( ( ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) ∧ ∀ 𝑑 ∈ ℂ ∀ 𝑒 ∈ ℂ ( ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ) ) → ( 𝑢 ∈ ℂ → ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) < 𝑎 ) ) )
57	56	ex	⊢ ( ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ∀ 𝑑 ∈ ℂ ∀ 𝑒 ∈ ℂ ( ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ) → ( 𝑢 ∈ ℂ → ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) < 𝑎 ) ) ) )
58	57	ralrimdv	⊢ ( ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ∀ 𝑑 ∈ ℂ ∀ 𝑒 ∈ ℂ ( ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ) → ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) < 𝑎 ) ) )
59	58	reximdv	⊢ ( ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑑 ∈ ℂ ∀ 𝑒 ∈ ℂ ( ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ) → ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) < 𝑎 ) ) )
60	59	reximdv	⊢ ( ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ( ∃ 𝑧 ∈ ℝ⁺ ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑑 ∈ ℂ ∀ 𝑒 ∈ ℂ ( ( ( abs ‘ ( 𝑑 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑒 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑑 · 𝑒 ) − ( 𝑏 · 𝑐 ) ) ) < 𝑎 ) → ∃ 𝑧 ∈ ℝ⁺ ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) < 𝑎 ) ) )
61	3 60	mpd	⊢ ( ( 𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ ) → ∃ 𝑧 ∈ ℝ⁺ ∃ 𝑤 ∈ ℝ⁺ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝑏 ) ) < 𝑧 ∧ ( abs ‘ ( 𝑣 − 𝑐 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑢 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) − ( 𝑏 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝑐 ) ) ) < 𝑎 ) )
62	1 2 61	addcnlem	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ∈ ( ( 𝐽 ×_t 𝐽 ) Cn 𝐽 )

Metamath Proof Explorer

Theorem mpomulcn

Proof