ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nqnq0pi Structured version   GIF version

Theorem nqnq0pi 6421
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 N B 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.
StepHypRef Expression
1 opelxp 4317 . . 3 (⟨A, B (N × N) ↔ (A N B N))
2 vex 2554 . . . . . . 7 y V
32elima2 4617 . . . . . 6 (y ( ~Q0 “ (N × N)) ↔ x(x (N × N) x ~Q0 y))
4 elxp 4305 . . . . . . . . . 10 (x (N × N) ↔ zw(x = ⟨z, w (z N w N)))
54anbi1i 431 . . . . . . . . 9 ((x (N × N) x ~Q0 y) ↔ (zw(x = ⟨z, w (z N w N)) x ~Q0 y))
6 19.41vv 1780 . . . . . . . . 9 (zw((x = ⟨z, w (z N w N)) x ~Q0 y) ↔ (zw(x = ⟨z, w (z N w N)) x ~Q0 y))
75, 6bitr4i 176 . . . . . . . 8 ((x (N × N) x ~Q0 y) ↔ zw((x = ⟨z, w (z N w N)) x ~Q0 y))
8 simplr 482 . . . . . . . . . . 11 (((x = ⟨z, w (z N w N)) x ~Q0 y) → (z N w N))
9 breq1 3758 . . . . . . . . . . . . 13 (x = ⟨z, w⟩ → (x ~Q0 y ↔ ⟨z, w⟩ ~Q0 y))
109adantr 261 . . . . . . . . . . . 12 ((x = ⟨z, w (z N w N)) → (x ~Q0 y ↔ ⟨z, w⟩ ~Q0 y))
1110biimpa 280 . . . . . . . . . . 11 (((x = ⟨z, w (z N w N)) x ~Q0 y) → ⟨z, w⟩ ~Q0 y)
12 id 19 . . . . . . . . . . . 12 (((z N w N) z, w⟩ ~Q0 y) → ((z N w N) z, w⟩ ~Q0 y))
13 enq0er 6418 . . . . . . . . . . . . . . 15 ~Q0 Er (𝜔 × N)
1413a1i 9 . . . . . . . . . . . . . 14 (((z N w N) z, w⟩ ~Q0 y) → ~Q0 Er (𝜔 × N))
15 simpr 103 . . . . . . . . . . . . . 14 (((z N w N) z, w⟩ ~Q0 y) → ⟨z, w⟩ ~Q0 y)
1614, 15ercl2 6055 . . . . . . . . . . . . 13 (((z N w N) z, w⟩ ~Q0 y) → y (𝜔 × N))
17 elxp 4305 . . . . . . . . . . . . 13 (y (𝜔 × N) ↔ uv(y = ⟨u, v (u 𝜔 v N)))
1816, 17sylib 127 . . . . . . . . . . . 12 (((z N w N) z, w⟩ ~Q0 y) → uv(y = ⟨u, v (u 𝜔 v N)))
19 19.42vv 1785 . . . . . . . . . . . 12 (uv(((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) ↔ (((z N w N) z, w⟩ ~Q0 y) uv(y = ⟨u, v (u 𝜔 v N))))
2012, 18, 19sylanbrc 394 . . . . . . . . . . 11 (((z N w N) z, w⟩ ~Q0 y) → uv(((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))))
218, 11, 20syl2anc 391 . . . . . . . . . 10 (((x = ⟨z, w (z N w N)) x ~Q0 y) → uv(((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))))
22 simprrl 491 . . . . . . . . . . . . 13 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → u 𝜔)
23 elni 6292 . . . . . . . . . . . . . . . . . . . . . . . . 25 (z N ↔ (z 𝜔 z ≠ ∅))
2423simprbi 260 . . . . . . . . . . . . . . . . . . . . . . . 24 (z Nz ≠ ∅)
2524neneqd 2221 . . . . . . . . . . . . . . . . . . . . . . 23 (z N → ¬ z = ∅)
2625ad2antrr 457 . . . . . . . . . . . . . . . . . . . . . 22 (((z N w N) (u 𝜔 v N)) → ¬ z = ∅)
27 elni 6292 . . . . . . . . . . . . . . . . . . . . . . . . 25 (v N ↔ (v 𝜔 v ≠ ∅))
2827simprbi 260 . . . . . . . . . . . . . . . . . . . . . . . 24 (v Nv ≠ ∅)
2928neneqd 2221 . . . . . . . . . . . . . . . . . . . . . . 23 (v N → ¬ v = ∅)
3029ad2antll 460 . . . . . . . . . . . . . . . . . . . . . 22 (((z N w N) (u 𝜔 v N)) → ¬ v = ∅)
3126, 30jca 290 . . . . . . . . . . . . . . . . . . . . 21 (((z N w N) (u 𝜔 v N)) → (¬ z = ∅ ¬ v = ∅))
32 pm4.56 805 . . . . . . . . . . . . . . . . . . . . 21 ((¬ z = ∅ ¬ v = ∅) ↔ ¬ (z = ∅ v = ∅))
3331, 32sylib 127 . . . . . . . . . . . . . . . . . . . 20 (((z N w N) (u 𝜔 v N)) → ¬ (z = ∅ v = ∅))
34 pinn 6293 . . . . . . . . . . . . . . . . . . . . . 22 (z Nz 𝜔)
3534ad2antrr 457 . . . . . . . . . . . . . . . . . . . . 21 (((z N w N) (u 𝜔 v N)) → z 𝜔)
36 pinn 6293 . . . . . . . . . . . . . . . . . . . . . 22 (v Nv 𝜔)
3736ad2antll 460 . . . . . . . . . . . . . . . . . . . . 21 (((z N w N) (u 𝜔 v N)) → v 𝜔)
38 nnm00 6038 . . . . . . . . . . . . . . . . . . . . 21 ((z 𝜔 v 𝜔) → ((z ·𝑜 v) = ∅ ↔ (z = ∅ v = ∅)))
3935, 37, 38syl2anc 391 . . . . . . . . . . . . . . . . . . . 20 (((z N w N) (u 𝜔 v N)) → ((z ·𝑜 v) = ∅ ↔ (z = ∅ v = ∅)))
4033, 39mtbird 597 . . . . . . . . . . . . . . . . . . 19 (((z N w N) (u 𝜔 v N)) → ¬ (z ·𝑜 v) = ∅)
4140ad2ant2rl 480 . . . . . . . . . . . . . . . . . 18 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → ¬ (z ·𝑜 v) = ∅)
42 breq2 3759 . . . . . . . . . . . . . . . . . . . . . 22 (y = ⟨u, v⟩ → (⟨z, w⟩ ~Q0 y ↔ ⟨z, w⟩ ~Q0u, v⟩))
4342biimpac 282 . . . . . . . . . . . . . . . . . . . . 21 ((⟨z, w⟩ ~Q0 y y = ⟨u, v⟩) → ⟨z, w⟩ ~Q0u, v⟩)
4443ad2ant2lr 479 . . . . . . . . . . . . . . . . . . . 20 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → ⟨z, w⟩ ~Q0u, v⟩)
45 enq0breq 6419 . . . . . . . . . . . . . . . . . . . . . 22 (((z 𝜔 w N) (u 𝜔 v N)) → (⟨z, w⟩ ~Q0u, v⟩ ↔ (z ·𝑜 v) = (w ·𝑜 u)))
4634, 45sylanl1 382 . . . . . . . . . . . . . . . . . . . . 21 (((z N w N) (u 𝜔 v N)) → (⟨z, w⟩ ~Q0u, v⟩ ↔ (z ·𝑜 v) = (w ·𝑜 u)))
4746ad2ant2rl 480 . . . . . . . . . . . . . . . . . . . 20 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → (⟨z, w⟩ ~Q0u, v⟩ ↔ (z ·𝑜 v) = (w ·𝑜 u)))
4844, 47mpbid 135 . . . . . . . . . . . . . . . . . . 19 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → (z ·𝑜 v) = (w ·𝑜 u))
4948eqeq1d 2045 . . . . . . . . . . . . . . . . . 18 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → ((z ·𝑜 v) = ∅ ↔ (w ·𝑜 u) = ∅))
5041, 49mtbid 596 . . . . . . . . . . . . . . . . 17 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → ¬ (w ·𝑜 u) = ∅)
51 pinn 6293 . . . . . . . . . . . . . . . . . . . 20 (w Nw 𝜔)
52 nnm00 6038 . . . . . . . . . . . . . . . . . . . 20 ((w 𝜔 u 𝜔) → ((w ·𝑜 u) = ∅ ↔ (w = ∅ u = ∅)))
5351, 52sylan 267 . . . . . . . . . . . . . . . . . . 19 ((w N u 𝜔) → ((w ·𝑜 u) = ∅ ↔ (w = ∅ u = ∅)))
5453ad2ant2lr 479 . . . . . . . . . . . . . . . . . 18 (((z N w N) (u 𝜔 v N)) → ((w ·𝑜 u) = ∅ ↔ (w = ∅ u = ∅)))
5554ad2ant2rl 480 . . . . . . . . . . . . . . . . 17 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → ((w ·𝑜 u) = ∅ ↔ (w = ∅ u = ∅)))
5650, 55mtbid 596 . . . . . . . . . . . . . . . 16 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → ¬ (w = ∅ u = ∅))
57 pm4.56 805 . . . . . . . . . . . . . . . 16 ((¬ w = ∅ ¬ u = ∅) ↔ ¬ (w = ∅ u = ∅))
5856, 57sylibr 137 . . . . . . . . . . . . . . 15 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → (¬ w = ∅ ¬ u = ∅))
5958simprd 107 . . . . . . . . . . . . . 14 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → ¬ u = ∅)
6059neneqad 2278 . . . . . . . . . . . . 13 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → u ≠ ∅)
61 elni 6292 . . . . . . . . . . . . 13 (u N ↔ (u 𝜔 u ≠ ∅))
6222, 60, 61sylanbrc 394 . . . . . . . . . . . 12 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → u N)
63 simprrr 492 . . . . . . . . . . . 12 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → v N)
64 eleq1 2097 . . . . . . . . . . . . . 14 (y = ⟨u, v⟩ → (y (N × N) ↔ ⟨u, v (N × N)))
65 opelxp 4317 . . . . . . . . . . . . . 14 (⟨u, v (N × N) ↔ (u N v N))
6664, 65syl6bb 185 . . . . . . . . . . . . 13 (y = ⟨u, v⟩ → (y (N × N) ↔ (u N v N)))
6766ad2antrl 459 . . . . . . . . . . . 12 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → (y (N × N) ↔ (u N v N)))
6862, 63, 67mpbir2and 850 . . . . . . . . . . 11 ((((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → y (N × N))
6968exlimivv 1773 . . . . . . . . . 10 (uv(((z N w N) z, w⟩ ~Q0 y) (y = ⟨u, v (u 𝜔 v N))) → y (N × N))
7021, 69syl 14 . . . . . . . . 9 (((x = ⟨z, w (z N w N)) x ~Q0 y) → y (N × N))
7170exlimivv 1773 . . . . . . . 8 (zw((x = ⟨z, w (z N w N)) x ~Q0 y) → y (N × N))
727, 71sylbi 114 . . . . . . 7 ((x (N × N) x ~Q0 y) → y (N × N))
7372exlimiv 1486 . . . . . 6 (x(x (N × N) x ~Q0 y) → y (N × N))
743, 73sylbi 114 . . . . 5 (y ( ~Q0 “ (N × N)) → y (N × N))
7574ssriv 2943 . . . 4 ( ~Q0 “ (N × N)) ⊆ (N × N)
76 ecinxp 6117 . . . 4 ((( ~Q0 “ (N × N)) ⊆ (N × N) A, B (N × N)) → [⟨A, B⟩] ~Q0 = [⟨A, B⟩]( ~Q0 ∩ ((N × N) × (N × N))))
7775, 76mpan 400 . . 3 (⟨A, B (N × N) → [⟨A, B⟩] ~Q0 = [⟨A, B⟩]( ~Q0 ∩ ((N × N) × (N × N))))
781, 77sylbir 125 . 2 ((A N B N) → [⟨A, B⟩] ~Q0 = [⟨A, B⟩]( ~Q0 ∩ ((N × N) × (N × N))))
79 enq0enq 6414 . . 3 ~Q = ( ~Q0 ∩ ((N × N) × (N × N)))
80 eceq2 6079 . . 3 ( ~Q = ( ~Q0 ∩ ((N × N) × (N × N))) → [⟨A, B⟩] ~Q = [⟨A, B⟩]( ~Q0 ∩ ((N × N) × (N × N))))
8179, 80ax-mp 7 . 2 [⟨A, B⟩] ~Q = [⟨A, B⟩]( ~Q0 ∩ ((N × N) × (N × N)))
8278, 81syl6eqr 2087 1 ((A N B N) → [⟨A, B⟩] ~Q0 = [⟨A, B⟩] ~Q )
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97  wb 98   wo 628   = wceq 1242  wex 1378   wcel 1390  wne 2201  cin 2910  wss 2911  c0 3218  cop 3370   class class class wbr 3755  𝜔com 4256   × cxp 4286  cima 4291  (class class class)co 5455   ·𝑜 comu 5938   Er wer 6039  [cec 6040  Ncnpi 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 6407
This theorem is referenced by:  nqnq0  6424  nqpnq0nq  6436  nqnq0a  6437  nqnq0m  6438  prarloclemlo  6477  prarloclemcalc  6485
  Copyright terms: Public domain W3C validator