mpomulcn - Intuitionistic Logic Explorer

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

Theorem mpomulcn 14812

Description: Complex number multiplication is a continuous function. (Contributed by GG, 16-Mar-2025.)

**Hypothesis**
Ref	Expression
mpomulcn.j	ℂ_fld

**Assertion**
Ref	Expression
mpomulcn

Distinct variable group:

Allowed substitution hints:

(

)

Proof of Theorem mpomulcn Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpomulcn.j	. . 3 ℂ_fld
2	1	cnfldtopn 14785	. 2
3		mpomulf 8018	. 2
4		mulcn2 11479	. . 3 $/\$ $/\$ $/\$
5		simplr 528	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
6		simplll 533	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
7		simplr 528	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8	7	fvoveq1d 5945	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9	8	breq1d 4044	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		simpr 110	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11	10	fvoveq1d 5945	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12	11	breq1d 4044	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13	9, 12	anbi12d 473	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		simplr 528	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
15	14	eqcomd 2202	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
16		simpr 110	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
17	16	eqcomd 2202	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
18	15, 17	oveq12d 5941	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
19		simplr 528	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
20		simplll 533	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
21		tru 1368	. . . . . . . . . . . . . . . . . . . . . 22
22		oveq1 5930	. . . . . . . . . . . . . . . . . . . . . . . . . 26
23		oveq2 5931	. . . . . . . . . . . . . . . . . . . . . . . . . 26
24	22, 23	cbvmpov 6003	. . . . . . . . . . . . . . . . . . . . . . . . 25
25	24	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24
26		eqidd 2197	. . . . . . . . . . . . . . . . . . . . . . . 24
27		mulcl 8008	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
28	27	3adant1 1017	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
29	25, 26, 28	fvmpopr2d 6060	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
30	29	eqcomd 2202	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
31	21, 30	mp3an1 1335	. . . . . . . . . . . . . . . . . . . . 21 $/\$
32		df-ov 5926	. . . . . . . . . . . . . . . . . . . . 21
33	31, 32	eqtr4di 2247	. . . . . . . . . . . . . . . . . . . 20 $/\$
34	19, 20, 33	syl2an2r 595	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
35	18, 34	eqtr3d 2231	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
36	35	adantllr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37		df-ov 5926	. . . . . . . . . . . . . . . . . . 19
38		oveq1 5930	. . . . . . . . . . . . . . . . . . . . . 22
39		oveq2 5931	. . . . . . . . . . . . . . . . . . . . . 22
40	38, 39	cbvmpov 6003	. . . . . . . . . . . . . . . . . . . . 21
41	40	a1i 9	. . . . . . . . . . . . . . . . . . . 20
42		eqidd 2197	. . . . . . . . . . . . . . . . . . . 20
43		mulcl 8008	. . . . . . . . . . . . . . . . . . . . 21 $/\$
44	43	3adant1 1017	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
45	41, 42, 44	fvmpopr2d 6060	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
46	37, 45	eqtr2id 2242	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
47	46	ad3antlr 493	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	36, 47	oveq12d 5941	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	48	fveq2d 5563	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	49	breq1d 4044	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	13, 50	imbi12d 234	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	6, 51	rspcdv 2871	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	5, 52	rspcimdv 2869	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54	53	expimpd 363	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	54	ex 115	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
56	55	com13 80	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
57	56	ralrimdv 2576	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
58	57	ex 115	. . . . . 6 $/\$ $/\$ $/\$ $/\$
59	58	ralrimdv 2576	. . . . 5 $/\$ $/\$ $/\$ $/\$
60	59	reximdv 2598	. . . 4 $/\$ $/\$ $/\$ $/\$
61	60	reximdv 2598	. . 3 $/\$ $/\$ $/\$ $/\$
62	4, 61	mpd 13	. 2 $/\$ $/\$ $/\$
63	2, 3, 62	addcncntoplem 14807	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104 $/\$ w3a 980

wceq 1364

wtru 1365

wcel 2167

wral 2475

wrex 2476

cop 3626 class class class wbr 4034

cfv 5259 (class class class)co 5923

cmpo 5925

cc 7879

cmul 7886

clt 8063

cmin 8199

crp 9730

cabs 11164

ctopn 12921 ℂ_fldccnfld 14122

ccn 14431

ctx 14498

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 7972 ax-resscn 7973 ax-1cn 7974 ax-1re 7975 ax-icn 7976 ax-addcl 7977 ax-addrcl 7978 ax-mulcl 7979 ax-mulrcl 7980 ax-addcom 7981 ax-mulcom 7982 ax-addass 7983 ax-mulass 7984 ax-distr 7985 ax-i2m1 7986 ax-0lt1 7987 ax-1rid 7988 ax-0id 7989 ax-rnegex 7990 ax-precex 7991 ax-cnre 7992 ax-pre-ltirr 7993 ax-pre-ltwlin 7994 ax-pre-lttrn 7995 ax-pre-apti 7996 ax-pre-ltadd 7997 ax-pre-mulgt0 7998 ax-pre-mulext 7999 ax-arch 8000 ax-caucvg 8001

This theorem depends on definitions: df-bi 117 df-stab 832 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-tp 3631 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 5878 df-ov 5926 df-oprab 5927 df-mpo 5928 df-1st 6199 df-2nd 6200 df-recs 6364 df-frec 6450 df-map 6710 df-sup 7051 df-inf 7052 df-pnf 8065 df-mnf 8066 df-xr 8067 df-ltxr 8068 df-le 8069 df-sub 8201 df-neg 8202 df-reap 8604 df-ap 8611 df-div 8702 df-inn 8993 df-2 9051 df-3 9052 df-4 9053 df-5 9054 df-6 9055 df-7 9056 df-8 9057 df-9 9058 df-n0 9252 df-z 9329 df-dec 9460 df-uz 9604 df-q 9696 df-rp 9731 df-xneg 9849 df-xadd 9850 df-fz 10086 df-seqfrec 10542 df-exp 10633 df-cj 11009 df-re 11010 df-im 11011 df-rsqrt 11165 df-abs 11166 df-struct 12690 df-ndx 12691 df-slot 12692 df-base 12694 df-plusg 12778 df-mulr 12779 df-starv 12780 df-tset 12784 df-ple 12785 df-ds 12787 df-unif 12788 df-rest 12922 df-topn 12923 df-topgen 12941 df-psmet 14109 df-xmet 14110 df-met 14111 df-bl 14112 df-mopn 14113 df-fg 14115 df-metu 14116 df-cnfld 14123 df-top 14244 df-topon 14257 df-bases 14289 df-cn 14434 df-cnp 14435 df-tx 14499

This theorem is referenced by: expcn 14815 plycn 15008

W3C validator