remullem - Intuitionistic Logic Explorer

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

Theorem remullem 10200

Description: Lemma for remul 10201, immul 10208, and cjmul 10214. (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 10188	. . . . . 6
2		replim 10188	. . . . . 6
3	1, 2	oveqan12d 5632	. . . . 5 $/\$
4		recl 10182	. . . . . . . . 9
5	4	adantr 270	. . . . . . . 8 $/\$
6	5	recnd 7460	. . . . . . 7 $/\$
7		ax-icn 7384	. . . . . . . 8
8		imcl 10183	. . . . . . . . . 10
9	8	adantr 270	. . . . . . . . 9 $/\$
10	9	recnd 7460	. . . . . . . 8 $/\$
11		mulcl 7413	. . . . . . . 8 $/\$
12	7, 10, 11	sylancr 405	. . . . . . 7 $/\$
13	6, 12	addcld 7451	. . . . . 6 $/\$
14		recl 10182	. . . . . . . 8
15	14	adantl 271	. . . . . . 7 $/\$
16	15	recnd 7460	. . . . . 6 $/\$
17		imcl 10183	. . . . . . . . 9
18	17	adantl 271	. . . . . . . 8 $/\$
19	18	recnd 7460	. . . . . . 7 $/\$
20		mulcl 7413	. . . . . . 7 $/\$
21	7, 19, 20	sylancr 405	. . . . . 6 $/\$
22	13, 16, 21	adddid 7456	. . . . 5 $/\$
23	6, 12, 16	adddird 7457	. . . . . . 7 $/\$
24	6, 12, 21	adddird 7457	. . . . . . 7 $/\$
25	23, 24	oveq12d 5631	. . . . . 6 $/\$
26	5, 15	remulcld 7462	. . . . . . . 8 $/\$
27	26	recnd 7460	. . . . . . 7 $/\$
28	12, 21	mulcld 7452	. . . . . . 7 $/\$
29	12, 16	mulcld 7452	. . . . . . 7 $/\$
30	6, 21	mulcld 7452	. . . . . . 7 $/\$
31	27, 28, 29, 30	add42d 7596	. . . . . 6 $/\$
32	7	a1i 9	. . . . . . . . . . 11 $/\$
33	32, 10, 32, 19	mul4d 7581	. . . . . . . . . 10 $/\$
34		ixi 8001	. . . . . . . . . . . 12
35	34	oveq1i 5623	. . . . . . . . . . 11
36	9, 18	remulcld 7462	. . . . . . . . . . . . 13 $/\$
37	36	recnd 7460	. . . . . . . . . . . 12 $/\$
38	37	mulm1d 7832	. . . . . . . . . . 11 $/\$
39	35, 38	syl5eq 2129	. . . . . . . . . 10 $/\$
40	33, 39	eqtrd 2117	. . . . . . . . 9 $/\$
41	40	oveq2d 5629	. . . . . . . 8 $/\$
42	27, 37	negsubd 7743	. . . . . . . 8 $/\$
43	41, 42	eqtrd 2117	. . . . . . 7 $/\$
44	9, 15	remulcld 7462	. . . . . . . . . . 11 $/\$
45	44	recnd 7460	. . . . . . . . . 10 $/\$
46		mulcl 7413	. . . . . . . . . 10 $/\$
47	7, 45, 46	sylancr 405	. . . . . . . . 9 $/\$
48	5, 18	remulcld 7462	. . . . . . . . . . 11 $/\$
49	48	recnd 7460	. . . . . . . . . 10 $/\$
50		mulcl 7413	. . . . . . . . . 10 $/\$
51	7, 49, 50	sylancr 405	. . . . . . . . 9 $/\$
52	47, 51	addcomd 7577	. . . . . . . 8 $/\$
53	32, 10, 16	mulassd 7455	. . . . . . . . 9 $/\$
54	6, 32, 19	mul12d 7578	. . . . . . . . 9 $/\$
55	53, 54	oveq12d 5631	. . . . . . . 8 $/\$
56	32, 49, 45	adddid 7456	. . . . . . . 8 $/\$
57	52, 55, 56	3eqtr4d 2127	. . . . . . 7 $/\$
58	43, 57	oveq12d 5631	. . . . . 6 $/\$
59	25, 31, 58	3eqtr2d 2123	. . . . 5 $/\$
60	3, 22, 59	3eqtrd 2121	. . . 4 $/\$
61	60	fveq2d 5272	. . 3 $/\$
62	26, 36	resubcld 7803	. . . 4 $/\$
63	48, 44	readdcld 7461	. . . 4 $/\$
64		crre 10186	. . . 4 $/\$
65	62, 63, 64	syl2anc 403	. . 3 $/\$
66	61, 65	eqtrd 2117	. 2 $/\$
67	60	fveq2d 5272	. . 3 $/\$
68		crim 10187	. . . 4 $/\$
69	62, 63, 68	syl2anc 403	. . 3 $/\$
70	67, 69	eqtrd 2117	. 2 $/\$
71		mulcl 7413	. . . 4 $/\$
72		remim 10189	. . . 4
73	71, 72	syl 14	. . 3 $/\$
74		remim 10189	. . . . 5
75		remim 10189	. . . . 5
76	74, 75	oveqan12d 5632	. . . 4 $/\$
77	16, 21	subcld 7737	. . . . 5 $/\$
78	6, 12, 77	subdird 7837	. . . 4 $/\$
79	27, 30, 29, 28	subadd4d 7785	. . . . 5 $/\$
80	6, 16, 21	subdid 7836	. . . . . 6 $/\$
81	12, 16, 21	subdid 7836	. . . . . 6 $/\$
82	80, 81	oveq12d 5631	. . . . 5 $/\$
83	65, 61, 43	3eqtr4d 2127	. . . . . 6 $/\$
84	70	oveq2d 5629	. . . . . . 7 $/\$
85	54, 53	oveq12d 5631	. . . . . . 7 $/\$
86	56, 84, 85	3eqtr4d 2127	. . . . . 6 $/\$
87	83, 86	oveq12d 5631	. . . . 5 $/\$
88	79, 82, 87	3eqtr4d 2127	. . . 4 $/\$
89	76, 78, 88	3eqtrd 2121	. . 3 $/\$
90	73, 89	eqtr4d 2120	. 2 $/\$
91	66, 70, 90	3jca 1121	1 $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

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

wceq 1287

wcel 1436

cfv 4981 (class class class)co 5613

cc 7292

cr 7293

c1 7295

ci 7296

caddc 7297

cmul 7299

cmin 7597

cneg 7598

ccj 10168

cre 10169

cim 10170

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 1379 ax-7 1380 ax-gen 1381 ax-ie1 1425 ax-ie2 1426 ax-8 1438 ax-10 1439 ax-11 1440 ax-i12 1441 ax-bndl 1442 ax-4 1443 ax-13 1447 ax-14 1448 ax-17 1462 ax-i9 1466 ax-ial 1470 ax-i5r 1471 ax-ext 2067 ax-sep 3932 ax-pow 3984 ax-pr 4010 ax-un 4234 ax-setind 4326 ax-cnex 7380 ax-resscn 7381 ax-1cn 7382 ax-1re 7383 ax-icn 7384 ax-addcl 7385 ax-addrcl 7386 ax-mulcl 7387 ax-mulrcl 7388 ax-addcom 7389 ax-mulcom 7390 ax-addass 7391 ax-mulass 7392 ax-distr 7393 ax-i2m1 7394 ax-0lt1 7395 ax-1rid 7396 ax-0id 7397 ax-rnegex 7398 ax-precex 7399 ax-cnre 7400 ax-pre-ltirr 7401 ax-pre-ltwlin 7402 ax-pre-lttrn 7403 ax-pre-apti 7404 ax-pre-ltadd 7405 ax-pre-mulgt0 7406 ax-pre-mulext 7407

This theorem depends on definitions: df-bi 115 df-3an 924 df-tru 1290 df-fal 1293 df-nf 1393 df-sb 1690 df-eu 1948 df-mo 1949 df-clab 2072 df-cleq 2078 df-clel 2081 df-nfc 2214 df-ne 2252 df-nel 2347 df-ral 2360 df-rex 2361 df-reu 2362 df-rmo 2363 df-rab 2364 df-v 2617 df-sbc 2830 df-dif 2990 df-un 2992 df-in 2994 df-ss 3001 df-pw 3417 df-sn 3437 df-pr 3438 df-op 3440 df-uni 3637 df-br 3821 df-opab 3875 df-mpt 3876 df-id 4094 df-po 4097 df-iso 4098 df-xp 4417 df-rel 4418 df-cnv 4419 df-co 4420 df-dm 4421 df-rn 4422 df-res 4423 df-ima 4424 df-iota 4946 df-fun 4983 df-fn 4984 df-f 4985 df-fv 4989 df-riota 5569 df-ov 5616 df-oprab 5617 df-mpt2 5618 df-pnf 7468 df-mnf 7469 df-xr 7470 df-ltxr 7471 df-le 7472 df-sub 7599 df-neg 7600 df-reap 7993 df-ap 8000 df-div 8079 df-2 8416 df-cj 10171 df-re 10172 df-im 10173

This theorem is referenced by: remul 10201 immul 10208 cjmul 10214

W3C validator