halfnqq - Intuitionistic Logic Explorer

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

Theorem halfnqq 7525

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 7481	. . . . . . . . 9
2		addclnq 7490	. . . . . . . . 9 $/\$
3	1, 1, 2	mp2an 426	. . . . . . . 8
4		recclnq 7507	. . . . . . . . 9
5	3, 4	ax-mp 5	. . . . . . . 8
6		distrnqg 7502	. . . . . . . 8 $/\$ $/\$
7	3, 5, 5, 6	mp3an 1350	. . . . . . 7
8		recidnq 7508	. . . . . . . . 9
9	3, 8	ax-mp 5	. . . . . . . 8
10	9, 9	oveq12i 5958	. . . . . . 7
11	7, 10	eqtri 2226	. . . . . 6
12	11	oveq1i 5956	. . . . 5
13	9	oveq2i 5957	. . . . . 6
14		addclnq 7490	. . . . . . . . 9 $/\$
15	5, 5, 14	mp2an 426	. . . . . . . 8
16		mulassnqg 7499	. . . . . . . 8 $/\$ $/\$
17	15, 3, 5, 16	mp3an 1350	. . . . . . 7
18		mulcomnqg 7498	. . . . . . . . 9 $/\$
19	15, 3, 18	mp2an 426	. . . . . . . 8
20	19	oveq1i 5956	. . . . . . 7
21	17, 20	eqtr3i 2228	. . . . . 6
22	4, 4, 14	syl2anc 411	. . . . . . 7
23		mulidnq 7504	. . . . . . 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 5957	. . 3
28		distrnqg 7502	. . . 4 $/\$ $/\$
29	5, 5, 28	mp3an23 1342	. . 3
30		mulidnq 7504	. . 3
31	27, 29, 30	3eqtr3a 2262	. 2
32		mulclnq 7491	. . . 4 $/\$
33	5, 32	mpan2 425	. . 3
34		id 19	. . . . . 6
35	34, 34	oveq12d 5964	. . . . 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 5272 (class class class)co 5946

cnq 7395

c1q 7396

cplq 7397

cmq 7398

crq 7399

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 4160 ax-sep 4163 ax-nul 4171 ax-pow 4219 ax-pr 4254 ax-un 4481 ax-setind 4586 ax-iinf 4637

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 4046 df-opab 4107 df-mpt 4108 df-tr 4144 df-id 4341 df-iord 4414 df-on 4416 df-suc 4419 df-iom 4640 df-xp 4682 df-rel 4683 df-cnv 4684 df-co 4685 df-dm 4686 df-rn 4687 df-res 4688 df-ima 4689 df-iota 5233 df-fun 5274 df-fn 5275 df-f 5276 df-f1 5277 df-fo 5278 df-f1o 5279 df-fv 5280 df-ov 5949 df-oprab 5950 df-mpo 5951 df-1st 6228 df-2nd 6229 df-recs 6393 df-irdg 6458 df-1o 6504 df-oadd 6508 df-omul 6509 df-er 6622 df-ec 6624 df-qs 6628 df-ni 7419 df-pli 7420 df-mi 7421 df-plpq 7459 df-mpq 7460 df-enq 7462 df-nqqs 7463 df-plqqs 7464 df-mqqs 7465 df-1nqqs 7466 df-rq 7467

This theorem is referenced by: halfnq 7526 nsmallnqq 7527 subhalfnqq 7529 addlocpr 7651 addcanprleml 7729 addcanprlemu 7730 cauappcvgprlemm 7760 cauappcvgprlem1 7774 caucvgprlemm 7783