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

Theorem mulclnq 6871
Description: Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.)
Assertion
Ref Expression
mulclnq ((𝐴Q𝐵Q) → (𝐴 ·Q 𝐵) ∈ Q)

Proof of Theorem mulclnq
Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nqqs 6843 . . 3 Q = ((N × N) / ~Q )
2 oveq1 5613 . . . 4 ([⟨𝑥, 𝑦⟩] ~Q = 𝐴 → ([⟨𝑥, 𝑦⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q ) = (𝐴 ·Q [⟨𝑧, 𝑤⟩] ~Q ))
32eleq1d 2153 . . 3 ([⟨𝑥, 𝑦⟩] ~Q = 𝐴 → (([⟨𝑥, 𝑦⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q ) ∈ ((N × N) / ~Q ) ↔ (𝐴 ·Q [⟨𝑧, 𝑤⟩] ~Q ) ∈ ((N × N) / ~Q )))
4 oveq2 5614 . . . 4 ([⟨𝑧, 𝑤⟩] ~Q = 𝐵 → (𝐴 ·Q [⟨𝑧, 𝑤⟩] ~Q ) = (𝐴 ·Q 𝐵))
54eleq1d 2153 . . 3 ([⟨𝑧, 𝑤⟩] ~Q = 𝐵 → ((𝐴 ·Q [⟨𝑧, 𝑤⟩] ~Q ) ∈ ((N × N) / ~Q ) ↔ (𝐴 ·Q 𝐵) ∈ ((N × N) / ~Q )))
6 mulpipqqs 6868 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → ([⟨𝑥, 𝑦⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q ) = [⟨(𝑥 ·N 𝑧), (𝑦 ·N 𝑤)⟩] ~Q )
7 mulclpi 6823 . . . . . . 7 ((𝑥N𝑧N) → (𝑥 ·N 𝑧) ∈ N)
8 mulclpi 6823 . . . . . . 7 ((𝑦N𝑤N) → (𝑦 ·N 𝑤) ∈ N)
97, 8anim12i 331 . . . . . 6 (((𝑥N𝑧N) ∧ (𝑦N𝑤N)) → ((𝑥 ·N 𝑧) ∈ N ∧ (𝑦 ·N 𝑤) ∈ N))
109an4s 553 . . . . 5 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → ((𝑥 ·N 𝑧) ∈ N ∧ (𝑦 ·N 𝑤) ∈ N))
11 opelxpi 4440 . . . . 5 (((𝑥 ·N 𝑧) ∈ N ∧ (𝑦 ·N 𝑤) ∈ N) → ⟨(𝑥 ·N 𝑧), (𝑦 ·N 𝑤)⟩ ∈ (N × N))
12 enqex 6855 . . . . . 6 ~Q ∈ V
1312ecelqsi 6291 . . . . 5 (⟨(𝑥 ·N 𝑧), (𝑦 ·N 𝑤)⟩ ∈ (N × N) → [⟨(𝑥 ·N 𝑧), (𝑦 ·N 𝑤)⟩] ~Q ∈ ((N × N) / ~Q ))
1410, 11, 133syl 17 . . . 4 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → [⟨(𝑥 ·N 𝑧), (𝑦 ·N 𝑤)⟩] ~Q ∈ ((N × N) / ~Q ))
156, 14eqeltrd 2161 . . 3 (((𝑥N𝑦N) ∧ (𝑧N𝑤N)) → ([⟨𝑥, 𝑦⟩] ~Q ·Q [⟨𝑧, 𝑤⟩] ~Q ) ∈ ((N × N) / ~Q ))
161, 3, 5, 152ecoptocl 6325 . 2 ((𝐴Q𝐵Q) → (𝐴 ·Q 𝐵) ∈ ((N × N) / ~Q ))
1716, 1syl6eleqr 2178 1 ((𝐴Q𝐵Q) → (𝐴 ·Q 𝐵) ∈ Q)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1287  wcel 1436  cop 3433   × cxp 4407  (class class class)co 5606  [cec 6235   / cqs 6236  Ncnpi 6767   ·N cmi 6769   ~Q ceq 6774  Qcnq 6775   ·Q cmq 6778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3927  ax-sep 3930  ax-nul 3938  ax-pow 3982  ax-pr 4008  ax-un 4232  ax-setind 4324  ax-iinf 4374
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-pw 3416  df-sn 3436  df-pr 3437  df-op 3439  df-uni 3636  df-int 3671  df-iun 3714  df-br 3820  df-opab 3874  df-mpt 3875  df-tr 3910  df-id 4092  df-iord 4165  df-on 4167  df-suc 4170  df-iom 4377  df-xp 4415  df-rel 4416  df-cnv 4417  df-co 4418  df-dm 4419  df-rn 4420  df-res 4421  df-ima 4422  df-iota 4942  df-fun 4979  df-fn 4980  df-f 4981  df-f1 4982  df-fo 4983  df-f1o 4984  df-fv 4985  df-ov 5609  df-oprab 5610  df-mpt2 5611  df-1st 5861  df-2nd 5862  df-recs 6017  df-irdg 6082  df-oadd 6132  df-omul 6133  df-er 6237  df-ec 6239  df-qs 6243  df-ni 6799  df-mi 6801  df-mpq 6840  df-enq 6842  df-nqqs 6843  df-mqqs 6845
This theorem is referenced by:  halfnqq  6905  prarloclemarch  6913  prarloclemarch2  6914  ltrnqg  6915  prarloclemlt  6988  prarloclemlo  6989  prarloclemcalc  6997  addnqprllem  7022  addnqprulem  7023  addnqprl  7024  addnqpru  7025  mpvlu  7034  dmmp  7036  appdivnq  7058  prmuloclemcalc  7060  prmuloc  7061  mulnqprl  7063  mulnqpru  7064  mullocprlem  7065  mullocpr  7066  mulclpr  7067  mulnqprlemrl  7068  mulnqprlemru  7069  mulnqprlemfl  7070  mulnqprlemfu  7071  mulnqpr  7072  mulassprg  7076  distrlem1prl  7077  distrlem1pru  7078  distrlem4prl  7079  distrlem4pru  7080  distrlem5prl  7081  distrlem5pru  7082  1idprl  7085  1idpru  7086  recexprlem1ssl  7128  recexprlem1ssu  7129  recexprlemss1l  7130  recexprlemss1u  7131
  Copyright terms: Public domain W3C validator