halfnqq - Intuitionistic Logic Explorer

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

Theorem halfnqq 7560

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 7516	. . . . . . . . 9
2		addclnq 7525	. . . . . . . . 9 $/\$
3	1, 1, 2	mp2an 426	. . . . . . . 8
4		recclnq 7542	. . . . . . . . 9
5	3, 4	ax-mp 5	. . . . . . . 8
6		distrnqg 7537	. . . . . . . 8 $/\$ $/\$
7	3, 5, 5, 6	mp3an 1350	. . . . . . 7
8		recidnq 7543	. . . . . . . . 9
9	3, 8	ax-mp 5	. . . . . . . 8
10	9, 9	oveq12i 5981	. . . . . . 7
11	7, 10	eqtri 2228	. . . . . 6
12	11	oveq1i 5979	. . . . 5
13	9	oveq2i 5980	. . . . . 6
14		addclnq 7525	. . . . . . . . 9 $/\$
15	5, 5, 14	mp2an 426	. . . . . . . 8
16		mulassnqg 7534	. . . . . . . 8 $/\$ $/\$
17	15, 3, 5, 16	mp3an 1350	. . . . . . 7
18		mulcomnqg 7533	. . . . . . . . 9 $/\$
19	15, 3, 18	mp2an 426	. . . . . . . 8
20	19	oveq1i 5979	. . . . . . 7
21	17, 20	eqtr3i 2230	. . . . . 6
22	4, 4, 14	syl2anc 411	. . . . . . 7
23		mulidnq 7539	. . . . . . 7
24	3, 22, 23	mp2b 8	. . . . . 6
25	13, 21, 24	3eqtr3i 2236	. . . . 5
26	12, 25, 9	3eqtr3i 2236	. . . 4
27	26	oveq2i 5980	. . 3
28		distrnqg 7537	. . . 4 $/\$ $/\$
29	5, 5, 28	mp3an23 1342	. . 3
30		mulidnq 7539	. . 3
31	27, 29, 30	3eqtr3a 2264	. 2
32		mulclnq 7526	. . . 4 $/\$
33	5, 32	mpan2 425	. . 3
34		id 19	. . . . . 6
35	34, 34	oveq12d 5987	. . . . 5
36	35	eqeq1d 2216	. . . 4
37	36	adantl 277	. . 3 $/\$
38	33, 37	rspcedv 2889	. 2
39	31, 38	mpd 13	1

Colors of variables: wff set class

Syntax hints:

wi 4

wb 105

wceq 1373

wcel 2178

wrex 2487

cfv 5291 (class class class)co 5969

cnq 7430

c1q 7431

cplq 7432

cmq 7433

crq 7434

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 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2180 ax-14 2181 ax-ext 2189 ax-coll 4176 ax-sep 4179 ax-nul 4187 ax-pow 4235 ax-pr 4270 ax-un 4499 ax-setind 4604 ax-iinf 4655

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 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ne 2379 df-ral 2491 df-rex 2492 df-reu 2493 df-rab 2495 df-v 2779 df-sbc 3007 df-csb 3103 df-dif 3177 df-un 3179 df-in 3181 df-ss 3188 df-nul 3470 df-pw 3629 df-sn 3650 df-pr 3651 df-op 3653 df-uni 3866 df-int 3901 df-iun 3944 df-br 4061 df-opab 4123 df-mpt 4124 df-tr 4160 df-id 4359 df-iord 4432 df-on 4434 df-suc 4437 df-iom 4658 df-xp 4700 df-rel 4701 df-cnv 4702 df-co 4703 df-dm 4704 df-rn 4705 df-res 4706 df-ima 4707 df-iota 5252 df-fun 5293 df-fn 5294 df-f 5295 df-f1 5296 df-fo 5297 df-f1o 5298 df-fv 5299 df-ov 5972 df-oprab 5973 df-mpo 5974 df-1st 6251 df-2nd 6252 df-recs 6416 df-irdg 6481 df-1o 6527 df-oadd 6531 df-omul 6532 df-er 6645 df-ec 6647 df-qs 6651 df-ni 7454 df-pli 7455 df-mi 7456 df-plpq 7494 df-mpq 7495 df-enq 7497 df-nqqs 7498 df-plqqs 7499 df-mqqs 7500 df-1nqqs 7501 df-rq 7502

This theorem is referenced by: halfnq 7561 nsmallnqq 7562 subhalfnqq 7564 addlocpr 7686 addcanprleml 7764 addcanprlemu 7765 cauappcvgprlemm 7795 cauappcvgprlem1 7809 caucvgprlemm 7818