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

Theorem mulpipqqs 6357
Description: Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.)
Assertion
Ref Expression
mulpipqqs (((A N B N) (𝐶 N 𝐷 N)) → ([⟨A, B⟩] ~Q ·Q [⟨𝐶, 𝐷⟩] ~Q ) = [⟨(A ·N 𝐶), (B ·N 𝐷)⟩] ~Q )

Proof of Theorem mulpipqqs
Dummy variables x y z w v u 𝑡 𝑠 f g 𝑎 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mulclpi 6312 . . . 4 ((A N 𝐶 N) → (A ·N 𝐶) N)
2 mulclpi 6312 . . . 4 ((B N 𝐷 N) → (B ·N 𝐷) N)
3 opelxpi 4319 . . . 4 (((A ·N 𝐶) N (B ·N 𝐷) N) → ⟨(A ·N 𝐶), (B ·N 𝐷)⟩ (N × N))
41, 2, 3syl2an 273 . . 3 (((A N 𝐶 N) (B N 𝐷 N)) → ⟨(A ·N 𝐶), (B ·N 𝐷)⟩ (N × N))
54an4s 522 . 2 (((A N B N) (𝐶 N 𝐷 N)) → ⟨(A ·N 𝐶), (B ·N 𝐷)⟩ (N × N))
6 mulclpi 6312 . . . 4 ((𝑎 N g N) → (𝑎 ·N g) N)
7 mulclpi 6312 . . . 4 ((𝑏 N N) → (𝑏 ·N ) N)
8 opelxpi 4319 . . . 4 (((𝑎 ·N g) N (𝑏 ·N ) N) → ⟨(𝑎 ·N g), (𝑏 ·N )⟩ (N × N))
96, 7, 8syl2an 273 . . 3 (((𝑎 N g N) (𝑏 N N)) → ⟨(𝑎 ·N g), (𝑏 ·N )⟩ (N × N))
109an4s 522 . 2 (((𝑎 N 𝑏 N) (g N N)) → ⟨(𝑎 ·N g), (𝑏 ·N )⟩ (N × N))
11 mulclpi 6312 . . . 4 ((𝑐 N 𝑡 N) → (𝑐 ·N 𝑡) N)
12 mulclpi 6312 . . . 4 ((𝑑 N 𝑠 N) → (𝑑 ·N 𝑠) N)
13 opelxpi 4319 . . . 4 (((𝑐 ·N 𝑡) N (𝑑 ·N 𝑠) N) → ⟨(𝑐 ·N 𝑡), (𝑑 ·N 𝑠)⟩ (N × N))
1411, 12, 13syl2an 273 . . 3 (((𝑐 N 𝑡 N) (𝑑 N 𝑠 N)) → ⟨(𝑐 ·N 𝑡), (𝑑 ·N 𝑠)⟩ (N × N))
1514an4s 522 . 2 (((𝑐 N 𝑑 N) (𝑡 N 𝑠 N)) → ⟨(𝑐 ·N 𝑡), (𝑑 ·N 𝑠)⟩ (N × N))
16 enqex 6344 . 2 ~Q V
17 enqer 6342 . 2 ~Q Er (N × N)
18 df-enq 6331 . 2 ~Q = {⟨x, y⟩ ∣ ((x (N × N) y (N × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·N u) = (w ·N v)))}
19 simpll 481 . . . 4 (((z = 𝑎 w = 𝑏) (v = 𝑐 u = 𝑑)) → z = 𝑎)
20 simprr 484 . . . 4 (((z = 𝑎 w = 𝑏) (v = 𝑐 u = 𝑑)) → u = 𝑑)
2119, 20oveq12d 5473 . . 3 (((z = 𝑎 w = 𝑏) (v = 𝑐 u = 𝑑)) → (z ·N u) = (𝑎 ·N 𝑑))
22 simplr 482 . . . 4 (((z = 𝑎 w = 𝑏) (v = 𝑐 u = 𝑑)) → w = 𝑏)
23 simprl 483 . . . 4 (((z = 𝑎 w = 𝑏) (v = 𝑐 u = 𝑑)) → v = 𝑐)
2422, 23oveq12d 5473 . . 3 (((z = 𝑎 w = 𝑏) (v = 𝑐 u = 𝑑)) → (w ·N v) = (𝑏 ·N 𝑐))
2521, 24eqeq12d 2051 . 2 (((z = 𝑎 w = 𝑏) (v = 𝑐 u = 𝑑)) → ((z ·N u) = (w ·N v) ↔ (𝑎 ·N 𝑑) = (𝑏 ·N 𝑐)))
26 simpll 481 . . . 4 (((z = g w = ) (v = 𝑡 u = 𝑠)) → z = g)
27 simprr 484 . . . 4 (((z = g w = ) (v = 𝑡 u = 𝑠)) → u = 𝑠)
2826, 27oveq12d 5473 . . 3 (((z = g w = ) (v = 𝑡 u = 𝑠)) → (z ·N u) = (g ·N 𝑠))
29 simplr 482 . . . 4 (((z = g w = ) (v = 𝑡 u = 𝑠)) → w = )
30 simprl 483 . . . 4 (((z = g w = ) (v = 𝑡 u = 𝑠)) → v = 𝑡)
3129, 30oveq12d 5473 . . 3 (((z = g w = ) (v = 𝑡 u = 𝑠)) → (w ·N v) = ( ·N 𝑡))
3228, 31eqeq12d 2051 . 2 (((z = g w = ) (v = 𝑡 u = 𝑠)) → ((z ·N u) = (w ·N v) ↔ (g ·N 𝑠) = ( ·N 𝑡)))
33 dfmpq2 6339 . 2 ·pQ = {⟨⟨x, y⟩, z⟩ ∣ ((x (N × N) y (N × N)) wvuf((x = ⟨w, v y = ⟨u, f⟩) z = ⟨(w ·N u), (v ·N f)⟩))}
34 simpll 481 . . . 4 (((w = 𝑎 v = 𝑏) (u = g f = )) → w = 𝑎)
35 simprl 483 . . . 4 (((w = 𝑎 v = 𝑏) (u = g f = )) → u = g)
3634, 35oveq12d 5473 . . 3 (((w = 𝑎 v = 𝑏) (u = g f = )) → (w ·N u) = (𝑎 ·N g))
37 simplr 482 . . . 4 (((w = 𝑎 v = 𝑏) (u = g f = )) → v = 𝑏)
38 simprr 484 . . . 4 (((w = 𝑎 v = 𝑏) (u = g f = )) → f = )
3937, 38oveq12d 5473 . . 3 (((w = 𝑎 v = 𝑏) (u = g f = )) → (v ·N f) = (𝑏 ·N ))
4036, 39opeq12d 3548 . 2 (((w = 𝑎 v = 𝑏) (u = g f = )) → ⟨(w ·N u), (v ·N f)⟩ = ⟨(𝑎 ·N g), (𝑏 ·N )⟩)
41 simpll 481 . . . 4 (((w = 𝑐 v = 𝑑) (u = 𝑡 f = 𝑠)) → w = 𝑐)
42 simprl 483 . . . 4 (((w = 𝑐 v = 𝑑) (u = 𝑡 f = 𝑠)) → u = 𝑡)
4341, 42oveq12d 5473 . . 3 (((w = 𝑐 v = 𝑑) (u = 𝑡 f = 𝑠)) → (w ·N u) = (𝑐 ·N 𝑡))
44 simplr 482 . . . 4 (((w = 𝑐 v = 𝑑) (u = 𝑡 f = 𝑠)) → v = 𝑑)
45 simprr 484 . . . 4 (((w = 𝑐 v = 𝑑) (u = 𝑡 f = 𝑠)) → f = 𝑠)
4644, 45oveq12d 5473 . . 3 (((w = 𝑐 v = 𝑑) (u = 𝑡 f = 𝑠)) → (v ·N f) = (𝑑 ·N 𝑠))
4743, 46opeq12d 3548 . 2 (((w = 𝑐 v = 𝑑) (u = 𝑡 f = 𝑠)) → ⟨(w ·N u), (v ·N f)⟩ = ⟨(𝑐 ·N 𝑡), (𝑑 ·N 𝑠)⟩)
48 simpll 481 . . . 4 (((w = A v = B) (u = 𝐶 f = 𝐷)) → w = A)
49 simprl 483 . . . 4 (((w = A v = B) (u = 𝐶 f = 𝐷)) → u = 𝐶)
5048, 49oveq12d 5473 . . 3 (((w = A v = B) (u = 𝐶 f = 𝐷)) → (w ·N u) = (A ·N 𝐶))
51 simplr 482 . . . 4 (((w = A v = B) (u = 𝐶 f = 𝐷)) → v = B)
52 simprr 484 . . . 4 (((w = A v = B) (u = 𝐶 f = 𝐷)) → f = 𝐷)
5351, 52oveq12d 5473 . . 3 (((w = A v = B) (u = 𝐶 f = 𝐷)) → (v ·N f) = (B ·N 𝐷))
5450, 53opeq12d 3548 . 2 (((w = A v = B) (u = 𝐶 f = 𝐷)) → ⟨(w ·N u), (v ·N f)⟩ = ⟨(A ·N 𝐶), (B ·N 𝐷)⟩)
55 df-mqqs 6334 . 2 ·Q = {⟨⟨x, y⟩, z⟩ ∣ ((x Q y Q) 𝑎𝑏𝑐𝑑((x = [⟨𝑎, 𝑏⟩] ~Q y = [⟨𝑐, 𝑑⟩] ~Q ) z = [(⟨𝑎, 𝑏⟩ ·pQ𝑐, 𝑑⟩)] ~Q ))}
56 df-nqqs 6332 . 2 Q = ((N × N) / ~Q )
57 mulcmpblnq 6352 . 2 ((((𝑎 N 𝑏 N) (𝑐 N 𝑑 N)) ((g N N) (𝑡 N 𝑠 N))) → (((𝑎 ·N 𝑑) = (𝑏 ·N 𝑐) (g ·N 𝑠) = ( ·N 𝑡)) → ⟨(𝑎 ·N g), (𝑏 ·N )⟩ ~Q ⟨(𝑐 ·N 𝑡), (𝑑 ·N 𝑠)⟩))
585, 10, 15, 16, 17, 18, 25, 32, 33, 40, 47, 54, 55, 56, 57oviec 6148 1 (((A N B N) (𝐶 N 𝐷 N)) → ([⟨A, B⟩] ~Q ·Q [⟨𝐶, 𝐷⟩] ~Q ) = [⟨(A ·N 𝐶), (B ·N 𝐷)⟩] ~Q )
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   = wceq 1242   wcel 1390  cop 3370   × cxp 4286  (class class class)co 5455  [cec 6040  Ncnpi 6256   ·N cmi 6258   ·pQ cmpq 6261   ~Q ceq 6263  Qcnq 6264   ·Q cmq 6267
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-qs 6048  df-ni 6288  df-mi 6290  df-mpq 6329  df-enq 6331  df-nqqs 6332  df-mqqs 6334
This theorem is referenced by:  mulclnq  6360  mulcomnqg  6367  mulassnqg  6368  distrnqg  6371  mulidnq  6373  recexnq  6374  ltmnqg  6385  nqnq0m  6437
  Copyright terms: Public domain W3C validator