mulreim - Intuitionistic Logic Explorer

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

Theorem mulreim 8631

Description: Complex multiplication in terms of real and imaginary parts. (Contributed by Jim Kingdon, 23-Feb-2020.)

**Assertion**
Ref	Expression
mulreim	$/\$ $/\$ $/\$

**Proof of Theorem mulreim**
Step	Hyp	Ref	Expression
1		simpll 527	. . . 4 $/\$ $/\$ $/\$
2	1	recnd 8055	. . 3 $/\$ $/\$ $/\$
3		ax-icn 7974	. . . . 5
4	3	a1i 9	. . . 4 $/\$ $/\$ $/\$
5		simplr 528	. . . . 5 $/\$ $/\$ $/\$
6	5	recnd 8055	. . . 4 $/\$ $/\$ $/\$
7	4, 6	mulcld 8047	. . 3 $/\$ $/\$ $/\$
8		simprl 529	. . . 4 $/\$ $/\$ $/\$
9	8	recnd 8055	. . 3 $/\$ $/\$ $/\$
10		simprr 531	. . . . 5 $/\$ $/\$ $/\$
11	10	recnd 8055	. . . 4 $/\$ $/\$ $/\$
12	4, 11	mulcld 8047	. . 3 $/\$ $/\$ $/\$
13	2, 7, 9, 12	muladdd 8442	. 2 $/\$ $/\$ $/\$
14	4, 11, 4, 6	mul4d 8181	. . . . . 6 $/\$ $/\$ $/\$
15		ixi 8610	. . . . . . 7
16	15	oveq1i 5932	. . . . . 6
17	14, 16	eqtrdi 2245	. . . . 5 $/\$ $/\$ $/\$
18	11, 6	mulcld 8047	. . . . . 6 $/\$ $/\$ $/\$
19	18	mulm1d 8436	. . . . 5 $/\$ $/\$ $/\$
20	11, 6	mulcomd 8048	. . . . . 6 $/\$ $/\$ $/\$
21	20	negeqd 8221	. . . . 5 $/\$ $/\$ $/\$
22	17, 19, 21	3eqtrd 2233	. . . 4 $/\$ $/\$ $/\$
23	22	oveq2d 5938	. . 3 $/\$ $/\$ $/\$
24	11, 2	mulcld 8047	. . . . . 6 $/\$ $/\$ $/\$
25	4, 24	mulcld 8047	. . . . 5 $/\$ $/\$ $/\$
26	9, 6	mulcld 8047	. . . . . 6 $/\$ $/\$ $/\$
27	4, 26	mulcld 8047	. . . . 5 $/\$ $/\$ $/\$
28	25, 27	addcomd 8177	. . . 4 $/\$ $/\$ $/\$
29	2, 4, 11	mul12d 8178	. . . . . 6 $/\$ $/\$ $/\$
30	2, 11	mulcomd 8048	. . . . . . 7 $/\$ $/\$ $/\$
31	30	oveq2d 5938	. . . . . 6 $/\$ $/\$ $/\$
32	29, 31	eqtrd 2229	. . . . 5 $/\$ $/\$ $/\$
33	9, 4, 6	mul12d 8178	. . . . 5 $/\$ $/\$ $/\$
34	32, 33	oveq12d 5940	. . . 4 $/\$ $/\$ $/\$
35	4, 26, 24	adddid 8051	. . . 4 $/\$ $/\$ $/\$
36	28, 34, 35	3eqtr4d 2239	. . 3 $/\$ $/\$ $/\$
37	23, 36	oveq12d 5940	. 2 $/\$ $/\$ $/\$
38	13, 37	eqtrd 2229	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wceq 1364

wcel 2167 (class class class)co 5922

cc 7877

cr 7878

c1 7880

ci 7881

caddc 7882

cmul 7884

cneg 8198

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-14 2170 ax-ext 2178 ax-sep 4151 ax-pow 4207 ax-pr 4242 ax-setind 4573 ax-resscn 7971 ax-1cn 7972 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-addcom 7979 ax-mulcom 7980 ax-addass 7981 ax-mulass 7982 ax-distr 7983 ax-i2m1 7984 ax-1rid 7986 ax-0id 7987 ax-rnegex 7988 ax-cnre 7990

This theorem depends on definitions: df-bi 117 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-ral 2480 df-rex 2481 df-reu 2482 df-rab 2484 df-v 2765 df-sbc 2990 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-br 4034 df-opab 4095 df-id 4328 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-iota 5219 df-fun 5260 df-fv 5266 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-sub 8199 df-neg 8200

This theorem is referenced by: mulext1 8639