halfnqq - Intuitionistic Logic Explorer

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

Theorem halfnqq 7523

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 7479	. . . . . . . . 9
2		addclnq 7488	. . . . . . . . 9 $/\$
3	1, 1, 2	mp2an 426	. . . . . . . 8
4		recclnq 7505	. . . . . . . . 9
5	3, 4	ax-mp 5	. . . . . . . 8
6		distrnqg 7500	. . . . . . . 8 $/\$ $/\$
7	3, 5, 5, 6	mp3an 1350	. . . . . . 7
8		recidnq 7506	. . . . . . . . 9
9	3, 8	ax-mp 5	. . . . . . . 8
10	9, 9	oveq12i 5956	. . . . . . 7
11	7, 10	eqtri 2226	. . . . . 6
12	11	oveq1i 5954	. . . . 5
13	9	oveq2i 5955	. . . . . 6
14		addclnq 7488	. . . . . . . . 9 $/\$
15	5, 5, 14	mp2an 426	. . . . . . . 8
16		mulassnqg 7497	. . . . . . . 8 $/\$ $/\$
17	15, 3, 5, 16	mp3an 1350	. . . . . . 7
18		mulcomnqg 7496	. . . . . . . . 9 $/\$
19	15, 3, 18	mp2an 426	. . . . . . . 8
20	19	oveq1i 5954	. . . . . . 7
21	17, 20	eqtr3i 2228	. . . . . 6
22	4, 4, 14	syl2anc 411	. . . . . . 7
23		mulidnq 7502	. . . . . . 7
24	3, 22, 23	mp2b 8	. . . . . 6
25	13, 21, 24	3eqtr3i 2234	. . . . 5
26	12, 25, 9	3eqtr3i 2234	. . . 4
27	26	oveq2i 5955	. . 3
28		distrnqg 7500	. . . 4 $/\$ $/\$
29	5, 5, 28	mp3an23 1342	. . 3
30		mulidnq 7502	. . 3
31	27, 29, 30	3eqtr3a 2262	. 2
32		mulclnq 7489	. . . 4 $/\$
33	5, 32	mpan2 425	. . 3
34		id 19	. . . . . 6
35	34, 34	oveq12d 5962	. . . . 5
36	35	eqeq1d 2214	. . . 4
37	36	adantl 277	. . 3 $/\$
38	33, 37	rspcedv 2881	. 2
39	31, 38	mpd 13	1

Colors of variables: wff set class

Syntax hints:

wi 4

wb 105

wceq 1373

wcel 2176

wrex 2485

cfv 5271 (class class class)co 5944

cnq 7393

c1q 7394

cplq 7395

cmq 7396

crq 7397

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 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-coll 4159 ax-sep 4162 ax-nul 4170 ax-pow 4218 ax-pr 4253 ax-un 4480 ax-setind 4585 ax-iinf 4636

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-ral 2489 df-rex 2490 df-reu 2491 df-rab 2493 df-v 2774 df-sbc 2999 df-csb 3094 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-int 3886 df-iun 3929 df-br 4045 df-opab 4106 df-mpt 4107 df-tr 4143 df-id 4340 df-iord 4413 df-on 4415 df-suc 4418 df-iom 4639 df-xp 4681 df-rel 4682 df-cnv 4683 df-co 4684 df-dm 4685 df-rn 4686 df-res 4687 df-ima 4688 df-iota 5232 df-fun 5273 df-fn 5274 df-f 5275 df-f1 5276 df-fo 5277 df-f1o 5278 df-fv 5279 df-ov 5947 df-oprab 5948 df-mpo 5949 df-1st 6226 df-2nd 6227 df-recs 6391 df-irdg 6456 df-1o 6502 df-oadd 6506 df-omul 6507 df-er 6620 df-ec 6622 df-qs 6626 df-ni 7417 df-pli 7418 df-mi 7419 df-plpq 7457 df-mpq 7458 df-enq 7460 df-nqqs 7461 df-plqqs 7462 df-mqqs 7463 df-1nqqs 7464 df-rq 7465

This theorem is referenced by: halfnq 7524 nsmallnqq 7525 subhalfnqq 7527 addlocpr 7649 addcanprleml 7727 addcanprlemu 7728 cauappcvgprlemm 7758 cauappcvgprlem1 7772 caucvgprlemm 7781