Theorem nqnq0pi 6420

Description: A non-negative fraction is a positive fraction if its numerator and denominator are positive integers. (Contributed by Jim Kingdon, 10-Nov-2019.)

Assertion

Ref	Expression
nqnq0pi	|- ((A e. N. /\ B e. N.) -> [ <.A , B >.] ~Q0 = [ <.A , B >.] ~Q )

Proof of Theorem nqnq0pi

Dummy variables v u w x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opelxp 4317	. . 3 |- ( <.A , B >. e. ( N. X. N.) <-> (A e. N. /\ B e. N.))
2		vex 2554	. . . . . . 7 |- y e. _V
3	2	elima2 4617	. . . . . 6 |- (y e. ( ~Q0 "( N. X. N.)) <-> E.x(x e. ( N. X. N.) /\ x ~Q0 y))
4		elxp 4305	. . . . . . . . . 10 |- (x e. ( N. X. N.) <-> E.zE.w(x = <.z , w >. /\ (z e. N. /\ w e. N.)))
5	4	anbi1i 431	. . . . . . . . 9 |- ((x e. ( N. X. N.) /\ x ~Q0 y) <-> (E.zE.w(x = <.z , w >. /\ (z e. N. /\ w e. N.)) /\ x ~Q0 y))
6		19.41vv 1780	. . . . . . . . 9 |- (E.zE.w((x = <.z , w >. /\ (z e. N. /\ w e. N.)) /\ x ~Q0 y) <-> (E.zE.w(x = <.z , w >. /\ (z e. N. /\ w e. N.)) /\ x ~Q0 y))
7	5, 6	bitr4i 176	. . . . . . . 8 |- ((x e. ( N. X. N.) /\ x ~Q0 y) <-> E.zE.w((x = <.z , w >. /\ (z e. N. /\ w e. N.)) /\ x ~Q0 y))
8		simplr 482	. . . . . . . . . . 11 |- (((x = <.z , w >. /\ (z e. N. /\ w e. N.)) /\ x ~Q0 y) -> (z e. N. /\ w e. N.))
9		breq1 3758	. . . . . . . . . . . . 13 |- (x = <.z , w >. -> (x ~Q0 y <-> <.z , w >. ~Q0 y))
10	9	adantr 261	. . . . . . . . . . . 12 |- ((x = <.z , w >. /\ (z e. N. /\ w e. N.)) -> (x ~Q0 y <-> <.z , w >. ~Q0 y))
11	10	biimpa 280	. . . . . . . . . . 11 |- (((x = <.z , w >. /\ (z e. N. /\ w e. N.)) /\ x ~Q0 y) -> <.z , w >. ~Q0 y)
12		id 19	. . . . . . . . . . . 12 |- (((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) -> ((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y))
13		enq0er 6417	. . . . . . . . . . . . . . 15 |- ~Q0 Er ( om X. N.)
14	13	a1i 9	. . . . . . . . . . . . . 14 |- (((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) -> ~Q0 Er ( om X. N.))
15		simpr 103	. . . . . . . . . . . . . 14 |- (((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) -> <.z , w >. ~Q0 y)
16	14, 15	ercl2 6055	. . . . . . . . . . . . 13 |- (((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) -> y e. ( om X. N.))
17		elxp 4305	. . . . . . . . . . . . 13 |- (y e. ( om X. N.) <-> E.uE.v(y = <.u , v >. /\ (u e. om /\ v e. N.)))
18	16, 17	sylib 127	. . . . . . . . . . . 12 |- (((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) -> E.uE.v(y = <.u , v >. /\ (u e. om /\ v e. N.)))
19		19.42vv 1785	. . . . . . . . . . . 12 |- (E.uE.v(((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) <-> (((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ E.uE.v(y = <.u , v >. /\ (u e. om /\ v e. N.))))
20	12, 18, 19	sylanbrc 394	. . . . . . . . . . 11 |- (((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) -> E.uE.v(((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))))
21	8, 11, 20	syl2anc 391	. . . . . . . . . 10 |- (((x = <.z , w >. /\ (z e. N. /\ w e. N.)) /\ x ~Q0 y) -> E.uE.v(((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))))
22		simprrl 491	. . . . . . . . . . . . 13 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> u e. om)
23		elni 6292	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z e. N. <-> (z e. om /\ z =/= (/)))
24	23	simprbi 260	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z e. N. -> z =/= (/))
25	24	neneqd 2221	. . . . . . . . . . . . . . . . . . . . . . 23 |- (z e. N. -> -. z = (/))
26	25	ad2antrr 457	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z e. N. /\ w e. N.) /\ (u e. om /\ v e. N.)) -> -. z = (/))
27		elni 6292	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v e. N. <-> (v e. om /\ v =/= (/)))
28	27	simprbi 260	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v e. N. -> v =/= (/))
29	28	neneqd 2221	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v e. N. -> -. v = (/))
30	29	ad2antll 460	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z e. N. /\ w e. N.) /\ (u e. om /\ v e. N.)) -> -. v = (/))
31	26, 30	jca 290	. . . . . . . . . . . . . . . . . . . . 21 |- (((z e. N. /\ w e. N.) /\ (u e. om /\ v e. N.)) -> (-. z = (/) /\ -. v = (/)))
32		pm4.56 805	. . . . . . . . . . . . . . . . . . . . 21 |- ((-. z = (/) /\ -. v = (/)) <-> -. (z = (/) \/ v = (/)))
33	31, 32	sylib 127	. . . . . . . . . . . . . . . . . . . 20 |- (((z e. N. /\ w e. N.) /\ (u e. om /\ v e. N.)) -> -. (z = (/) \/ v = (/)))
34		pinn 6293	. . . . . . . . . . . . . . . . . . . . . 22 |- (z e. N. -> z e. om)
35	34	ad2antrr 457	. . . . . . . . . . . . . . . . . . . . 21 |- (((z e. N. /\ w e. N.) /\ (u e. om /\ v e. N.)) -> z e. om)
36		pinn 6293	. . . . . . . . . . . . . . . . . . . . . 22 |- (v e. N. -> v e. om)
37	36	ad2antll 460	. . . . . . . . . . . . . . . . . . . . 21 |- (((z e. N. /\ w e. N.) /\ (u e. om /\ v e. N.)) -> v e. om)
38		nnm00 6038	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. om /\ v e. om) -> ((z .o v) = (/) <-> (z = (/) \/ v = (/))))
39	35, 37, 38	syl2anc 391	. . . . . . . . . . . . . . . . . . . 20 |- (((z e. N. /\ w e. N.) /\ (u e. om /\ v e. N.)) -> ((z .o v) = (/) <-> (z = (/) \/ v = (/))))
40	33, 39	mtbird 597	. . . . . . . . . . . . . . . . . . 19 |- (((z e. N. /\ w e. N.) /\ (u e. om /\ v e. N.)) -> -. (z .o v) = (/))
41	40	ad2ant2rl 480	. . . . . . . . . . . . . . . . . 18 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> -. (z .o v) = (/))
42		breq2 3759	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = <.u , v >. -> ( <.z , w >. ~Q0 y <-> <.z , w >. ~Q0 <.u , v >.))
43	42	biimpac 282	. . . . . . . . . . . . . . . . . . . . 21 |- (( <.z , w >. ~Q0 y /\ y = <.u , v >.) -> <.z , w >. ~Q0 <.u , v >.)
44	43	ad2ant2lr 479	. . . . . . . . . . . . . . . . . . . 20 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> <.z , w >. ~Q0 <.u , v >.)
45		enq0breq 6418	. . . . . . . . . . . . . . . . . . . . . 22 |- (((z e. om /\ w e. N.) /\ (u e. om /\ v e. N.)) -> ( <.z , w >. ~Q0 <.u , v >. <-> (z .o v) = (w .o u)))
46	34, 45	sylanl1 382	. . . . . . . . . . . . . . . . . . . . 21 |- (((z e. N. /\ w e. N.) /\ (u e. om /\ v e. N.)) -> ( <.z , w >. ~Q0 <.u , v >. <-> (z .o v) = (w .o u)))
47	46	ad2ant2rl 480	. . . . . . . . . . . . . . . . . . . 20 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> ( <.z , w >. ~Q0 <.u , v >. <-> (z .o v) = (w .o u)))
48	44, 47	mpbid 135	. . . . . . . . . . . . . . . . . . 19 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> (z .o v) = (w .o u))
49	48	eqeq1d 2045	. . . . . . . . . . . . . . . . . 18 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> ((z .o v) = (/) <-> (w .o u) = (/)))
50	41, 49	mtbid 596	. . . . . . . . . . . . . . . . 17 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> -. (w .o u) = (/))
51		pinn 6293	. . . . . . . . . . . . . . . . . . . 20 |- (w e. N. -> w e. om)
52		nnm00 6038	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. om /\ u e. om) -> ((w .o u) = (/) <-> (w = (/) \/ u = (/))))
53	51, 52	sylan 267	. . . . . . . . . . . . . . . . . . 19 |- ((w e. N. /\ u e. om) -> ((w .o u) = (/) <-> (w = (/) \/ u = (/))))
54	53	ad2ant2lr 479	. . . . . . . . . . . . . . . . . 18 |- (((z e. N. /\ w e. N.) /\ (u e. om /\ v e. N.)) -> ((w .o u) = (/) <-> (w = (/) \/ u = (/))))
55	54	ad2ant2rl 480	. . . . . . . . . . . . . . . . 17 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> ((w .o u) = (/) <-> (w = (/) \/ u = (/))))
56	50, 55	mtbid 596	. . . . . . . . . . . . . . . 16 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> -. (w = (/) \/ u = (/)))
57		pm4.56 805	. . . . . . . . . . . . . . . 16 |- ((-. w = (/) /\ -. u = (/)) <-> -. (w = (/) \/ u = (/)))
58	56, 57	sylibr 137	. . . . . . . . . . . . . . 15 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> (-. w = (/) /\ -. u = (/)))
59	58	simprd 107	. . . . . . . . . . . . . 14 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> -. u = (/))
60	59	neneqad 2278	. . . . . . . . . . . . 13 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> u =/= (/))
61		elni 6292	. . . . . . . . . . . . 13 |- (u e. N. <-> (u e. om /\ u =/= (/)))
62	22, 60, 61	sylanbrc 394	. . . . . . . . . . . 12 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> u e. N.)
63		simprrr 492	. . . . . . . . . . . 12 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> v e. N.)
64		eleq1 2097	. . . . . . . . . . . . . 14 |- (y = <.u , v >. -> (y e. ( N. X. N.) <-> <.u , v >. e. ( N. X. N.)))
65		opelxp 4317	. . . . . . . . . . . . . 14 |- ( <.u , v >. e. ( N. X. N.) <-> (u e. N. /\ v e. N.))
66	64, 65	syl6bb 185	. . . . . . . . . . . . 13 |- (y = <.u , v >. -> (y e. ( N. X. N.) <-> (u e. N. /\ v e. N.)))
67	66	ad2antrl 459	. . . . . . . . . . . 12 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> (y e. ( N. X. N.) <-> (u e. N. /\ v e. N.)))
68	62, 63, 67	mpbir2and 850	. . . . . . . . . . 11 |- ((((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> y e. ( N. X. N.))
69	68	exlimivv 1773	. . . . . . . . . 10 |- (E.uE.v(((z e. N. /\ w e. N.) /\ <.z , w >. ~Q0 y) /\ (y = <.u , v >. /\ (u e. om /\ v e. N.))) -> y e. ( N. X. N.))
70	21, 69	syl 14	. . . . . . . . 9 |- (((x = <.z , w >. /\ (z e. N. /\ w e. N.)) /\ x ~Q0 y) -> y e. ( N. X. N.))
71	70	exlimivv 1773	. . . . . . . 8 |- (E.zE.w((x = <.z , w >. /\ (z e. N. /\ w e. N.)) /\ x ~Q0 y) -> y e. ( N. X. N.))
72	7, 71	sylbi 114	. . . . . . 7 |- ((x e. ( N. X. N.) /\ x ~Q0 y) -> y e. ( N. X. N.))
73	72	exlimiv 1486	. . . . . 6 |- (E.x(x e. ( N. X. N.) /\ x ~Q0 y) -> y e. ( N. X. N.))
74	3, 73	sylbi 114	. . . . 5 |- (y e. ( ~Q0 "( N. X. N.)) -> y e. ( N. X. N.))
75	74	ssriv 2943	. . . 4 |- ( ~Q0 "( N. X. N.)) C_ ( N. X. N.)
76		ecinxp 6117	. . . 4 |- ((( ~Q0 "( N. X. N.)) C_ ( N. X. N.) /\ <.A , B >. e. ( N. X. N.)) -> [ <.A , B >.] ~Q0 = [ <.A , B >.]( ~Q0 i^i (( N. X. N.) X. ( N. X. N.))))
77	75, 76	mpan 400	. . 3 |- ( <.A , B >. e. ( N. X. N.) -> [ <.A , B >.] ~Q0 = [ <.A , B >.]( ~Q0 i^i (( N. X. N.) X. ( N. X. N.))))
78	1, 77	sylbir 125	. 2 |- ((A e. N. /\ B e. N.) -> [ <.A , B >.] ~Q0 = [ <.A , B >.]( ~Q0 i^i (( N. X. N.) X. ( N. X. N.))))
79		enq0enq 6413	. . 3 |- ~Q = ( ~Q0 i^i (( N. X. N.) X. ( N. X. N.)))
80		eceq2 6079	. . 3 |- ( ~Q = ( ~Q0 i^i (( N. X. N.) X. ( N. X. N.))) -> [ <.A , B >.] ~Q = [ <.A , B >.]( ~Q0 i^i (( N. X. N.) X. ( N. X. N.))))
81	79, 80	ax-mp 7	. 2 |- [ <.A , B >.] ~Q = [ <.A , B >.]( ~Q0 i^i (( N. X. N.) X. ( N. X. N.)))
82	78, 81	syl6eqr 2087	1 |- ((A e. N. /\ B e. N.) -> [ <.A , B >.] ~Q0 = [ <.A , B >.] ~Q )

Syntax hints:  -. wn 3   -> wi 4   /\ wa 97   <-> wb 98   \/ wo 628   = wceq 1242  E.wex 1378   e. wcel 1390   =/= wne 2201   i^i cin 2910   C_ wss 2911   (/)c0 3218   <.cop 3370   class class class wbr 3755   omcom 4256   X. cxp 4286   "cima 4291  (class class class)co 5455   .o comu 5938   Er wer 6039  [cec 6040   N.cnpi 6256   ~Q ceq 6263   ~_Q0 ceq0 6270

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254

This theorem depends on definitions:  df-bi 110  df-dc 742  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-id 4021  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-oadd 5944  df-omul 5945  df-er 6042  df-ec 6044  df-ni 6288  df-mi 6290  df-enq 6331  df-enq0 6406

This theorem is referenced by:  nqnq0  6423  nqpnq0nq  6435  nqnq0a  6436  nqnq0m  6437  prarloclemlo  6476  prarloclemcalc  6484