remullem - Intuitionistic Logic Explorer

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

Theorem remullem 9896

Description: Lemma for remul 9897, immul 9904, and cjmul 9910. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)

**Assertion**
Ref	Expression
remullem	$/\$ $/\$ $/\$

**Proof of Theorem remullem**
Step	Hyp	Ref	Expression
1		replim 9884	. . . . . 6
2		replim 9884	. . . . . 6
3	1, 2	oveqan12d 5562	. . . . 5 $/\$
4		recl 9878	. . . . . . . . 9
5	4	adantr 270	. . . . . . . 8 $/\$
6	5	recnd 7209	. . . . . . 7 $/\$
7		ax-icn 7133	. . . . . . . 8
8		imcl 9879	. . . . . . . . . 10
9	8	adantr 270	. . . . . . . . 9 $/\$
10	9	recnd 7209	. . . . . . . 8 $/\$
11		mulcl 7162	. . . . . . . 8 $/\$
12	7, 10, 11	sylancr 405	. . . . . . 7 $/\$
13	6, 12	addcld 7200	. . . . . 6 $/\$
14		recl 9878	. . . . . . . 8
15	14	adantl 271	. . . . . . 7 $/\$
16	15	recnd 7209	. . . . . 6 $/\$
17		imcl 9879	. . . . . . . . 9
18	17	adantl 271	. . . . . . . 8 $/\$
19	18	recnd 7209	. . . . . . 7 $/\$
20		mulcl 7162	. . . . . . 7 $/\$
21	7, 19, 20	sylancr 405	. . . . . 6 $/\$
22	13, 16, 21	adddid 7205	. . . . 5 $/\$
23	6, 12, 16	adddird 7206	. . . . . . 7 $/\$
24	6, 12, 21	adddird 7206	. . . . . . 7 $/\$
25	23, 24	oveq12d 5561	. . . . . 6 $/\$
26	5, 15	remulcld 7211	. . . . . . . 8 $/\$
27	26	recnd 7209	. . . . . . 7 $/\$
28	12, 21	mulcld 7201	. . . . . . 7 $/\$
29	12, 16	mulcld 7201	. . . . . . 7 $/\$
30	6, 21	mulcld 7201	. . . . . . 7 $/\$
31	27, 28, 29, 30	add42d 7345	. . . . . 6 $/\$
32	7	a1i 9	. . . . . . . . . . 11 $/\$
33	32, 10, 32, 19	mul4d 7330	. . . . . . . . . 10 $/\$
34		ixi 7750	. . . . . . . . . . . 12
35	34	oveq1i 5553	. . . . . . . . . . 11
36	9, 18	remulcld 7211	. . . . . . . . . . . . 13 $/\$
37	36	recnd 7209	. . . . . . . . . . . 12 $/\$
38	37	mulm1d 7581	. . . . . . . . . . 11 $/\$
39	35, 38	syl5eq 2126	. . . . . . . . . 10 $/\$
40	33, 39	eqtrd 2114	. . . . . . . . 9 $/\$
41	40	oveq2d 5559	. . . . . . . 8 $/\$
42	27, 37	negsubd 7492	. . . . . . . 8 $/\$
43	41, 42	eqtrd 2114	. . . . . . 7 $/\$
44	9, 15	remulcld 7211	. . . . . . . . . . 11 $/\$
45	44	recnd 7209	. . . . . . . . . 10 $/\$
46		mulcl 7162	. . . . . . . . . 10 $/\$
47	7, 45, 46	sylancr 405	. . . . . . . . 9 $/\$
48	5, 18	remulcld 7211	. . . . . . . . . . 11 $/\$
49	48	recnd 7209	. . . . . . . . . 10 $/\$
50		mulcl 7162	. . . . . . . . . 10 $/\$
51	7, 49, 50	sylancr 405	. . . . . . . . 9 $/\$
52	47, 51	addcomd 7326	. . . . . . . 8 $/\$
53	32, 10, 16	mulassd 7204	. . . . . . . . 9 $/\$
54	6, 32, 19	mul12d 7327	. . . . . . . . 9 $/\$
55	53, 54	oveq12d 5561	. . . . . . . 8 $/\$
56	32, 49, 45	adddid 7205	. . . . . . . 8 $/\$
57	52, 55, 56	3eqtr4d 2124	. . . . . . 7 $/\$
58	43, 57	oveq12d 5561	. . . . . 6 $/\$
59	25, 31, 58	3eqtr2d 2120	. . . . 5 $/\$
60	3, 22, 59	3eqtrd 2118	. . . 4 $/\$
61	60	fveq2d 5213	. . 3 $/\$
62	26, 36	resubcld 7552	. . . 4 $/\$
63	48, 44	readdcld 7210	. . . 4 $/\$
64		crre 9882	. . . 4 $/\$
65	62, 63, 64	syl2anc 403	. . 3 $/\$
66	61, 65	eqtrd 2114	. 2 $/\$
67	60	fveq2d 5213	. . 3 $/\$
68		crim 9883	. . . 4 $/\$
69	62, 63, 68	syl2anc 403	. . 3 $/\$
70	67, 69	eqtrd 2114	. 2 $/\$
71		mulcl 7162	. . . 4 $/\$
72		remim 9885	. . . 4
73	71, 72	syl 14	. . 3 $/\$
74		remim 9885	. . . . 5
75		remim 9885	. . . . 5
76	74, 75	oveqan12d 5562	. . . 4 $/\$
77	16, 21	subcld 7486	. . . . 5 $/\$
78	6, 12, 77	subdird 7586	. . . 4 $/\$
79	27, 30, 29, 28	subadd4d 7534	. . . . 5 $/\$
80	6, 16, 21	subdid 7585	. . . . . 6 $/\$
81	12, 16, 21	subdid 7585	. . . . . 6 $/\$
82	80, 81	oveq12d 5561	. . . . 5 $/\$
83	65, 61, 43	3eqtr4d 2124	. . . . . 6 $/\$
84	70	oveq2d 5559	. . . . . . 7 $/\$
85	54, 53	oveq12d 5561	. . . . . . 7 $/\$
86	56, 84, 85	3eqtr4d 2124	. . . . . 6 $/\$
87	83, 86	oveq12d 5561	. . . . 5 $/\$
88	79, 82, 87	3eqtr4d 2124	. . . 4 $/\$
89	76, 78, 88	3eqtrd 2118	. . 3 $/\$
90	73, 89	eqtr4d 2117	. 2 $/\$
91	66, 70, 90	3jca 1119	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 102 $/\$ w3a 920

wceq 1285

wcel 1434

cfv 4932 (class class class)co 5543

cc 7041

cr 7042

c1 7044

ci 7045

caddc 7046

cmul 7048

cmin 7346

cneg 7347

ccj 9864

cre 9865

cim 9866

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-sep 3904 ax-pow 3956 ax-pr 3972 ax-un 4196 ax-setind 4288 ax-cnex 7129 ax-resscn 7130 ax-1cn 7131 ax-1re 7132 ax-icn 7133 ax-addcl 7134 ax-addrcl 7135 ax-mulcl 7136 ax-mulrcl 7137 ax-addcom 7138 ax-mulcom 7139 ax-addass 7140 ax-mulass 7141 ax-distr 7142 ax-i2m1 7143 ax-0lt1 7144 ax-1rid 7145 ax-0id 7146 ax-rnegex 7147 ax-precex 7148 ax-cnre 7149 ax-pre-ltirr 7150 ax-pre-ltwlin 7151 ax-pre-lttrn 7152 ax-pre-apti 7153 ax-pre-ltadd 7154 ax-pre-mulgt0 7155 ax-pre-mulext 7156

This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1687 df-eu 1945 df-mo 1946 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ne 2247 df-nel 2341 df-ral 2354 df-rex 2355 df-reu 2356 df-rmo 2357 df-rab 2358 df-v 2604 df-sbc 2817 df-dif 2976 df-un 2978 df-in 2980 df-ss 2987 df-pw 3392 df-sn 3412 df-pr 3413 df-op 3415 df-uni 3610 df-br 3794 df-opab 3848 df-mpt 3849 df-id 4056 df-po 4059 df-iso 4060 df-xp 4377 df-rel 4378 df-cnv 4379 df-co 4380 df-dm 4381 df-rn 4382 df-res 4383 df-ima 4384 df-iota 4897 df-fun 4934 df-fn 4935 df-f 4936 df-fv 4940 df-riota 5499 df-ov 5546 df-oprab 5547 df-mpt2 5548 df-pnf 7217 df-mnf 7218 df-xr 7219 df-ltxr 7220 df-le 7221 df-sub 7348 df-neg 7349 df-reap 7742 df-ap 7749 df-div 7828 df-2 8165 df-cj 9867 df-re 9868 df-im 9869

This theorem is referenced by: remul 9897 immul 9904 cjmul 9910

W3C validator