mullocpr - Intuitionistic Logic Explorer

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

Theorem mullocpr 7610

Description: Locatedness of multiplication on positive reals. Lemma 12.9 in [BauerTaylor], p. 56 (but where both

and

are positive, not just

). (Contributed by Jim Kingdon, 8-Dec-2019.)

**Assertion**
Ref	Expression
mullocpr	$/\$ $\/$

Distinct variable groups:

Proof of Theorem mullocpr Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prop 7514	. . . . . . . 8
2		prmuloc 7605	. . . . . . . 8 $/\$ $/\$ $/\$
3	1, 2	sylan 283	. . . . . . 7 $/\$ $/\$ $/\$
4		r2ex 2510	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5	3, 4	sylib 122	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
6	5	adantlr 477	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7	6	adantlr 477	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		simprr3 1049	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9		simprl 529	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		mulclnq 7415	. . . . . . . . 9 $/\$
11	9, 10	syl 14	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		appdivnq 7602	. . . . . . . 8 $/\$ $/\$
13	8, 11, 12	syl2anc 411	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		simprrr 540	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15	11	adantr 276	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		appdivnq 7602	. . . . . . . . 9 $/\$ $/\$
17	14, 15, 16	syl2anc 411	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18		simplll 533	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19	18	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		simprl 529	. . . . . . . . . 10 $/\$ $/\$
21	20	ad2antlr 489	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		simprrl 539	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
23		simprrr 540	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		simpllr 534	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	24	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	9	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27		3simpa 996	. . . . . . . . . . 11 $/\$ $/\$ $/\$
28	27	ad2antll 491	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	28	ad2antrr 488	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30		simplrl 535	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31		simprl 529	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	30, 31	jca 306	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33	19, 21, 22, 23, 25, 26, 29, 32	mullocprlem 7609	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
34	17, 33	rexlimddv 2612	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
35	13, 34	rexlimddv 2612	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
36	35	ex 115	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
37	36	exlimdvv 1909	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
38	7, 37	mpd 13	. . 3 $/\$ $/\$ $/\$ $/\$ $\/$
39	38	ex 115	. 2 $/\$ $/\$ $/\$ $\/$
40	39	ralrimivva 2572	1 $/\$ $\/$

Colors of variables: wff set class

Syntax hints:

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

wex 1503

wcel 2160

wral 2468

wrex 2469

cop 3617 class class class wbr 4025

cfv 5242 (class class class)co 5904

c1st 6171

c2nd 6172

cnq 7319

cmq 7322

cltq 7324

cnp 7330

cmp 7333

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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-coll 4140 ax-sep 4143 ax-nul 4151 ax-pow 4199 ax-pr 4234 ax-un 4458 ax-setind 4561 ax-iinf 4612

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-ral 2473 df-rex 2474 df-reu 2475 df-rab 2477 df-v 2758 df-sbc 2982 df-csb 3077 df-dif 3150 df-un 3152 df-in 3154 df-ss 3161 df-nul 3442 df-pw 3599 df-sn 3620 df-pr 3621 df-op 3623 df-uni 3832 df-int 3867 df-iun 3910 df-br 4026 df-opab 4087 df-mpt 4088 df-tr 4124 df-eprel 4314 df-id 4318 df-po 4321 df-iso 4322 df-iord 4391 df-on 4393 df-suc 4396 df-iom 4615 df-xp 4657 df-rel 4658 df-cnv 4659 df-co 4660 df-dm 4661 df-rn 4662 df-res 4663 df-ima 4664 df-iota 5203 df-fun 5244 df-fn 5245 df-f 5246 df-f1 5247 df-fo 5248 df-f1o 5249 df-fv 5250 df-ov 5907 df-oprab 5908 df-mpo 5909 df-1st 6173 df-2nd 6174 df-recs 6338 df-irdg 6403 df-1o 6449 df-2o 6450 df-oadd 6453 df-omul 6454 df-er 6567 df-ec 6569 df-qs 6573 df-ni 7343 df-pli 7344 df-mi 7345 df-lti 7346 df-plpq 7383 df-mpq 7384 df-enq 7386 df-nqqs 7387 df-plqqs 7388 df-mqqs 7389 df-1nqqs 7390 df-rq 7391 df-ltnqqs 7392 df-enq0 7463 df-nq0 7464 df-0nq0 7465 df-plq0 7466 df-mq0 7467 df-inp 7505 df-imp 7508

This theorem is referenced by: mulclpr 7611

W3C validator