halfnqq - Intuitionistic Logic Explorer

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

Theorem halfnqq 7558

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 7514	. . . . . . . . 9
2		addclnq 7523	. . . . . . . . 9 $/\$
3	1, 1, 2	mp2an 426	. . . . . . . 8
4		recclnq 7540	. . . . . . . . 9
5	3, 4	ax-mp 5	. . . . . . . 8
6		distrnqg 7535	. . . . . . . 8 $/\$ $/\$
7	3, 5, 5, 6	mp3an 1350	. . . . . . 7
8		recidnq 7541	. . . . . . . . 9
9	3, 8	ax-mp 5	. . . . . . . 8
10	9, 9	oveq12i 5979	. . . . . . 7
11	7, 10	eqtri 2228	. . . . . 6
12	11	oveq1i 5977	. . . . 5
13	9	oveq2i 5978	. . . . . 6
14		addclnq 7523	. . . . . . . . 9 $/\$
15	5, 5, 14	mp2an 426	. . . . . . . 8
16		mulassnqg 7532	. . . . . . . 8 $/\$ $/\$
17	15, 3, 5, 16	mp3an 1350	. . . . . . 7
18		mulcomnqg 7531	. . . . . . . . 9 $/\$
19	15, 3, 18	mp2an 426	. . . . . . . 8
20	19	oveq1i 5977	. . . . . . 7
21	17, 20	eqtr3i 2230	. . . . . 6
22	4, 4, 14	syl2anc 411	. . . . . . 7
23		mulidnq 7537	. . . . . . 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 5978	. . 3
28		distrnqg 7535	. . . 4 $/\$ $/\$
29	5, 5, 28	mp3an23 1342	. . 3
30		mulidnq 7537	. . 3
31	27, 29, 30	3eqtr3a 2264	. 2
32		mulclnq 7524	. . . 4 $/\$
33	5, 32	mpan2 425	. . 3
34		id 19	. . . . . 6
35	34, 34	oveq12d 5985	. . . . 5
36	35	eqeq1d 2216	. . . 4
37	36	adantl 277	. . 3 $/\$
38	33, 37	rspcedv 2888	. 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 5290 (class class class)co 5967

cnq 7428

c1q 7429

cplq 7430

cmq 7431

crq 7432

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 4175 ax-sep 4178 ax-nul 4186 ax-pow 4234 ax-pr 4269 ax-un 4498 ax-setind 4603 ax-iinf 4654

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 2778 df-sbc 3006 df-csb 3102 df-dif 3176 df-un 3178 df-in 3180 df-ss 3187 df-nul 3469 df-pw 3628 df-sn 3649 df-pr 3650 df-op 3652 df-uni 3865 df-int 3900 df-iun 3943 df-br 4060 df-opab 4122 df-mpt 4123 df-tr 4159 df-id 4358 df-iord 4431 df-on 4433 df-suc 4436 df-iom 4657 df-xp 4699 df-rel 4700 df-cnv 4701 df-co 4702 df-dm 4703 df-rn 4704 df-res 4705 df-ima 4706 df-iota 5251 df-fun 5292 df-fn 5293 df-f 5294 df-f1 5295 df-fo 5296 df-f1o 5297 df-fv 5298 df-ov 5970 df-oprab 5971 df-mpo 5972 df-1st 6249 df-2nd 6250 df-recs 6414 df-irdg 6479 df-1o 6525 df-oadd 6529 df-omul 6530 df-er 6643 df-ec 6645 df-qs 6649 df-ni 7452 df-pli 7453 df-mi 7454 df-plpq 7492 df-mpq 7493 df-enq 7495 df-nqqs 7496 df-plqqs 7497 df-mqqs 7498 df-1nqqs 7499 df-rq 7500

This theorem is referenced by: halfnq 7559 nsmallnqq 7560 subhalfnqq 7562 addlocpr 7684 addcanprleml 7762 addcanprlemu 7763 cauappcvgprlemm 7793 cauappcvgprlem1 7807 caucvgprlemm 7816