halfnqq - Intuitionistic Logic Explorer

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

Theorem halfnqq 6662

Description: One-half of any positive fraction is a fraction. (Contributed by Jim Kingdon, 23-Sep-2019.)

**Assertion**
Ref	Expression
halfnqq

**Proof of Theorem halfnqq**
Step	Hyp	Ref	Expression
1		1nq 6618	. . . . . . . . 9
2		addclnq 6627	. . . . . . . . 9 $/\$
3	1, 1, 2	mp2an 417	. . . . . . . 8
4		recclnq 6644	. . . . . . . . 9
5	3, 4	ax-mp 7	. . . . . . . 8
6		distrnqg 6639	. . . . . . . 8 $/\$ $/\$
7	3, 5, 5, 6	mp3an 1269	. . . . . . 7
8		recidnq 6645	. . . . . . . . 9
9	3, 8	ax-mp 7	. . . . . . . 8
10	9, 9	oveq12i 5555	. . . . . . 7
11	7, 10	eqtri 2102	. . . . . 6
12	11	oveq1i 5553	. . . . 5
13	9	oveq2i 5554	. . . . . 6
14		addclnq 6627	. . . . . . . . 9 $/\$
15	5, 5, 14	mp2an 417	. . . . . . . 8
16		mulassnqg 6636	. . . . . . . 8 $/\$ $/\$
17	15, 3, 5, 16	mp3an 1269	. . . . . . 7
18		mulcomnqg 6635	. . . . . . . . 9 $/\$
19	15, 3, 18	mp2an 417	. . . . . . . 8
20	19	oveq1i 5553	. . . . . . 7
21	17, 20	eqtr3i 2104	. . . . . 6
22	4, 4, 14	syl2anc 403	. . . . . . 7
23		mulidnq 6641	. . . . . . 7
24	3, 22, 23	mp2b 8	. . . . . 6
25	13, 21, 24	3eqtr3i 2110	. . . . 5
26	12, 25, 9	3eqtr3i 2110	. . . 4
27	26	oveq2i 5554	. . 3
28		distrnqg 6639	. . . 4 $/\$ $/\$
29	5, 5, 28	mp3an23 1261	. . 3
30		mulidnq 6641	. . 3
31	27, 29, 30	3eqtr3a 2138	. 2
32		mulclnq 6628	. . . 4 $/\$
33	5, 32	mpan2 416	. . 3
34		id 19	. . . . . 6
35	34, 34	oveq12d 5561	. . . . 5
36	35	eqeq1d 2090	. . . 4
37	36	adantl 271	. . 3 $/\$
38	33, 37	rspcedv 2706	. 2
39	31, 38	mpd 13	1

Colors of variables: wff set class

Syntax hints:

wi 4

wb 103

wceq 1285

wcel 1434

wrex 2350

cfv 4932 (class class class)co 5543

cnq 6532

c1q 6533

cplq 6534

cmq 6535

crq 6536

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-coll 3901 ax-sep 3904 ax-nul 3912 ax-pow 3956 ax-pr 3972 ax-un 4196 ax-setind 4288 ax-iinf 4337

This theorem depends on definitions: df-bi 115 df-dc 777 df-3or 921 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-ral 2354 df-rex 2355 df-reu 2356 df-rab 2358 df-v 2604 df-sbc 2817 df-csb 2910 df-dif 2976 df-un 2978 df-in 2980 df-ss 2987 df-nul 3259 df-pw 3392 df-sn 3412 df-pr 3413 df-op 3415 df-uni 3610 df-int 3645 df-iun 3688 df-br 3794 df-opab 3848 df-mpt 3849 df-tr 3884 df-id 4056 df-iord 4129 df-on 4131 df-suc 4134 df-iom 4340 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-f1 4937 df-fo 4938 df-f1o 4939 df-fv 4940 df-ov 5546 df-oprab 5547 df-mpt2 5548 df-1st 5798 df-2nd 5799 df-recs 5954 df-irdg 6019 df-1o 6065 df-oadd 6069 df-omul 6070 df-er 6172 df-ec 6174 df-qs 6178 df-ni 6556 df-pli 6557 df-mi 6558 df-plpq 6596 df-mpq 6597 df-enq 6599 df-nqqs 6600 df-plqqs 6601 df-mqqs 6602 df-1nqqs 6603 df-rq 6604

This theorem is referenced by: halfnq 6663 nsmallnqq 6664 subhalfnqq 6666 addlocpr 6788 addcanprleml 6866 addcanprlemu 6867 cauappcvgprlemm 6897 cauappcvgprlem1 6911 caucvgprlemm 6920