halfnqq - Intuitionistic Logic Explorer

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

Theorem halfnqq 7620

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 7576	. . . . . . . . 9
2		addclnq 7585	. . . . . . . . 9 $/\$
3	1, 1, 2	mp2an 426	. . . . . . . 8
4		recclnq 7602	. . . . . . . . 9
5	3, 4	ax-mp 5	. . . . . . . 8
6		distrnqg 7597	. . . . . . . 8 $/\$ $/\$
7	3, 5, 5, 6	mp3an 1371	. . . . . . 7
8		recidnq 7603	. . . . . . . . 9
9	3, 8	ax-mp 5	. . . . . . . 8
10	9, 9	oveq12i 6025	. . . . . . 7
11	7, 10	eqtri 2250	. . . . . 6
12	11	oveq1i 6023	. . . . 5
13	9	oveq2i 6024	. . . . . 6
14		addclnq 7585	. . . . . . . . 9 $/\$
15	5, 5, 14	mp2an 426	. . . . . . . 8
16		mulassnqg 7594	. . . . . . . 8 $/\$ $/\$
17	15, 3, 5, 16	mp3an 1371	. . . . . . 7
18		mulcomnqg 7593	. . . . . . . . 9 $/\$
19	15, 3, 18	mp2an 426	. . . . . . . 8
20	19	oveq1i 6023	. . . . . . 7
21	17, 20	eqtr3i 2252	. . . . . 6
22	4, 4, 14	syl2anc 411	. . . . . . 7
23		mulidnq 7599	. . . . . . 7
24	3, 22, 23	mp2b 8	. . . . . 6
25	13, 21, 24	3eqtr3i 2258	. . . . 5
26	12, 25, 9	3eqtr3i 2258	. . . 4
27	26	oveq2i 6024	. . 3
28		distrnqg 7597	. . . 4 $/\$ $/\$
29	5, 5, 28	mp3an23 1363	. . 3
30		mulidnq 7599	. . 3
31	27, 29, 30	3eqtr3a 2286	. 2
32		mulclnq 7586	. . . 4 $/\$
33	5, 32	mpan2 425	. . 3
34		id 19	. . . . . 6
35	34, 34	oveq12d 6031	. . . . 5
36	35	eqeq1d 2238	. . . 4
37	36	adantl 277	. . 3 $/\$
38	33, 37	rspcedv 2912	. 2
39	31, 38	mpd 13	1

Colors of variables: wff set class

Syntax hints:

wi 4

wb 105

wceq 1395

wcel 2200

wrex 2509

cfv 5324 (class class class)co 6013

cnq 7490

c1q 7491

cplq 7492

cmq 7493

crq 7494

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4202 ax-sep 4205 ax-nul 4213 ax-pow 4262 ax-pr 4297 ax-un 4528 ax-setind 4633 ax-iinf 4684

This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-ral 2513 df-rex 2514 df-reu 2515 df-rab 2517 df-v 2802 df-sbc 3030 df-csb 3126 df-dif 3200 df-un 3202 df-in 3204 df-ss 3211 df-nul 3493 df-pw 3652 df-sn 3673 df-pr 3674 df-op 3676 df-uni 3892 df-int 3927 df-iun 3970 df-br 4087 df-opab 4149 df-mpt 4150 df-tr 4186 df-id 4388 df-iord 4461 df-on 4463 df-suc 4466 df-iom 4687 df-xp 4729 df-rel 4730 df-cnv 4731 df-co 4732 df-dm 4733 df-rn 4734 df-res 4735 df-ima 4736 df-iota 5284 df-fun 5326 df-fn 5327 df-f 5328 df-f1 5329 df-fo 5330 df-f1o 5331 df-fv 5332 df-ov 6016 df-oprab 6017 df-mpo 6018 df-1st 6298 df-2nd 6299 df-recs 6466 df-irdg 6531 df-1o 6577 df-oadd 6581 df-omul 6582 df-er 6697 df-ec 6699 df-qs 6703 df-ni 7514 df-pli 7515 df-mi 7516 df-plpq 7554 df-mpq 7555 df-enq 7557 df-nqqs 7558 df-plqqs 7559 df-mqqs 7560 df-1nqqs 7561 df-rq 7562

This theorem is referenced by: halfnq 7621 nsmallnqq 7622 subhalfnqq 7624 addlocpr 7746 addcanprleml 7824 addcanprlemu 7825 cauappcvgprlemm 7855 cauappcvgprlem1 7869 caucvgprlemm 7878