MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  recmulnq Structured version   Visualization version   GIF version

Theorem recmulnq 9474
Description: Relationship between reciprocal and multiplication on positive fractions. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
Assertion
Ref Expression
recmulnq (𝐴Q → ((*Q𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))

Proof of Theorem recmulnq
Dummy variables 𝑥 𝑦 𝑠 𝑟 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 5937 . . . 4 (*Q𝐴) ∈ V
21a1i 11 . . 3 (𝐴Q → (*Q𝐴) ∈ V)
3 eleq1 2571 . . 3 ((*Q𝐴) = 𝐵 → ((*Q𝐴) ∈ V ↔ 𝐵 ∈ V))
42, 3syl5ibcom 230 . 2 (𝐴Q → ((*Q𝐴) = 𝐵𝐵 ∈ V))
5 id 22 . . . . . . 7 ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) = 1Q)
6 1nq 9438 . . . . . . 7 1QQ
75, 6syl6eqel 2591 . . . . . 6 ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) ∈ Q)
8 mulnqf 9459 . . . . . . . 8 ·Q :(Q × Q)⟶Q
98fdmi 5791 . . . . . . 7 dom ·Q = (Q × Q)
10 0nnq 9434 . . . . . . 7 ¬ ∅ ∈ Q
119, 10ndmovrcl 6530 . . . . . 6 ((𝐴 ·Q 𝐵) ∈ Q → (𝐴Q𝐵Q))
127, 11syl 17 . . . . 5 ((𝐴 ·Q 𝐵) = 1Q → (𝐴Q𝐵Q))
1312simprd 472 . . . 4 ((𝐴 ·Q 𝐵) = 1Q𝐵Q)
14 elex 3075 . . . 4 (𝐵Q𝐵 ∈ V)
1513, 14syl 17 . . 3 ((𝐴 ·Q 𝐵) = 1Q𝐵 ∈ V)
1615a1i 11 . 2 (𝐴Q → ((𝐴 ·Q 𝐵) = 1Q𝐵 ∈ V))
17 oveq1 6370 . . . . 5 (𝑥 = 𝐴 → (𝑥 ·Q 𝑦) = (𝐴 ·Q 𝑦))
1817eqeq1d 2507 . . . 4 (𝑥 = 𝐴 → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝑦) = 1Q))
19 oveq2 6371 . . . . 5 (𝑦 = 𝐵 → (𝐴 ·Q 𝑦) = (𝐴 ·Q 𝐵))
2019eqeq1d 2507 . . . 4 (𝑦 = 𝐵 → ((𝐴 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝐵) = 1Q))
21 nqerid 9443 . . . . . . . . . 10 (𝑥Q → ([Q]‘𝑥) = 𝑥)
22 relxp 4989 . . . . . . . . . . . 12 Rel (N × N)
23 elpqn 9435 . . . . . . . . . . . 12 (𝑥Q𝑥 ∈ (N × N))
24 1st2nd 6916 . . . . . . . . . . . 12 ((Rel (N × N) ∧ 𝑥 ∈ (N × N)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
2522, 23, 24sylancr 685 . . . . . . . . . . 11 (𝑥Q𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
2625fveq2d 5931 . . . . . . . . . 10 (𝑥Q → ([Q]‘𝑥) = ([Q]‘⟨(1st𝑥), (2nd𝑥)⟩))
2721, 26eqtr3d 2541 . . . . . . . . 9 (𝑥Q𝑥 = ([Q]‘⟨(1st𝑥), (2nd𝑥)⟩))
2827oveq1d 6378 . . . . . . . 8 (𝑥Q → (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = (([Q]‘⟨(1st𝑥), (2nd𝑥)⟩) ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)))
29 mulerpq 9467 . . . . . . . 8 (([Q]‘⟨(1st𝑥), (2nd𝑥)⟩) ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = ([Q]‘(⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩))
3028, 29syl6eq 2555 . . . . . . 7 (𝑥Q → (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = ([Q]‘(⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩)))
31 xp1st 6900 . . . . . . . . . . 11 (𝑥 ∈ (N × N) → (1st𝑥) ∈ N)
3223, 31syl 17 . . . . . . . . . 10 (𝑥Q → (1st𝑥) ∈ N)
33 xp2nd 6901 . . . . . . . . . . 11 (𝑥 ∈ (N × N) → (2nd𝑥) ∈ N)
3423, 33syl 17 . . . . . . . . . 10 (𝑥Q → (2nd𝑥) ∈ N)
35 mulpipq 9450 . . . . . . . . . 10 ((((1st𝑥) ∈ N ∧ (2nd𝑥) ∈ N) ∧ ((2nd𝑥) ∈ N ∧ (1st𝑥) ∈ N)) → (⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩) = ⟨((1st𝑥) ·N (2nd𝑥)), ((2nd𝑥) ·N (1st𝑥))⟩)
3632, 34, 34, 32, 35syl22anc 1309 . . . . . . . . 9 (𝑥Q → (⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩) = ⟨((1st𝑥) ·N (2nd𝑥)), ((2nd𝑥) ·N (1st𝑥))⟩)
37 mulcompi 9406 . . . . . . . . . 10 ((2nd𝑥) ·N (1st𝑥)) = ((1st𝑥) ·N (2nd𝑥))
3837opeq2i 4200 . . . . . . . . 9 ⟨((1st𝑥) ·N (2nd𝑥)), ((2nd𝑥) ·N (1st𝑥))⟩ = ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩
3936, 38syl6eq 2555 . . . . . . . 8 (𝑥Q → (⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩) = ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩)
4039fveq2d 5931 . . . . . . 7 (𝑥Q → ([Q]‘(⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩)) = ([Q]‘⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩))
41 nqerid 9443 . . . . . . . . 9 (1QQ → ([Q]‘1Q) = 1Q)
426, 41ax-mp 5 . . . . . . . 8 ([Q]‘1Q) = 1Q
43 mulclpi 9403 . . . . . . . . . . 11 (((1st𝑥) ∈ N ∧ (2nd𝑥) ∈ N) → ((1st𝑥) ·N (2nd𝑥)) ∈ N)
4432, 34, 43syl2anc 682 . . . . . . . . . 10 (𝑥Q → ((1st𝑥) ·N (2nd𝑥)) ∈ N)
45 1nqenq 9472 . . . . . . . . . 10 (((1st𝑥) ·N (2nd𝑥)) ∈ N → 1Q ~Q ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩)
4644, 45syl 17 . . . . . . . . 9 (𝑥Q → 1Q ~Q ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩)
47 elpqn 9435 . . . . . . . . . . 11 (1QQ → 1Q ∈ (N × N))
486, 47ax-mp 5 . . . . . . . . . 10 1Q ∈ (N × N)
49 opelxpi 4912 . . . . . . . . . . 11 ((((1st𝑥) ·N (2nd𝑥)) ∈ N ∧ ((1st𝑥) ·N (2nd𝑥)) ∈ N) → ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩ ∈ (N × N))
5044, 44, 49syl2anc 682 . . . . . . . . . 10 (𝑥Q → ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩ ∈ (N × N))
51 nqereq 9445 . . . . . . . . . 10 ((1Q ∈ (N × N) ∧ ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩ ∈ (N × N)) → (1Q ~Q ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩ ↔ ([Q]‘1Q) = ([Q]‘⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩)))
5248, 50, 51sylancr 685 . . . . . . . . 9 (𝑥Q → (1Q ~Q ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩ ↔ ([Q]‘1Q) = ([Q]‘⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩)))
5346, 52mpbid 217 . . . . . . . 8 (𝑥Q → ([Q]‘1Q) = ([Q]‘⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩))
5442, 53syl5reqr 2554 . . . . . . 7 (𝑥Q → ([Q]‘⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩) = 1Q)
5530, 40, 543eqtrd 2543 . . . . . 6 (𝑥Q → (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = 1Q)
56 fvex 5937 . . . . . . 7 ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩) ∈ V
57 oveq2 6371 . . . . . . . 8 (𝑦 = ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩) → (𝑥 ·Q 𝑦) = (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)))
5857eqeq1d 2507 . . . . . . 7 (𝑦 = ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩) → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = 1Q))
5956, 58spcev 3162 . . . . . 6 ((𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = 1Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
6055, 59syl 17 . . . . 5 (𝑥Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
61 mulcomnq 9463 . . . . . . 7 (𝑟 ·Q 𝑠) = (𝑠 ·Q 𝑟)
62 mulassnq 9469 . . . . . . 7 ((𝑟 ·Q 𝑠) ·Q 𝑡) = (𝑟 ·Q (𝑠 ·Q 𝑡))
63 mulidnq 9473 . . . . . . 7 (𝑟Q → (𝑟 ·Q 1Q) = 𝑟)
646, 9, 10, 61, 62, 63caovmo 6581 . . . . . 6 ∃*𝑦(𝑥 ·Q 𝑦) = 1Q
65 eu5 2379 . . . . . 6 (∃!𝑦(𝑥 ·Q 𝑦) = 1Q ↔ (∃𝑦(𝑥 ·Q 𝑦) = 1Q ∧ ∃*𝑦(𝑥 ·Q 𝑦) = 1Q))
6664, 65mpbiran2 946 . . . . 5 (∃!𝑦(𝑥 ·Q 𝑦) = 1Q ↔ ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
6760, 66sylibr 219 . . . 4 (𝑥Q → ∃!𝑦(𝑥 ·Q 𝑦) = 1Q)
68 cnvimass 5238 . . . . . . . 8 ( ·Q “ {1Q}) ⊆ dom ·Q
69 df-rq 9427 . . . . . . . 8 *Q = ( ·Q “ {1Q})
709eqcomi 2514 . . . . . . . 8 (Q × Q) = dom ·Q
7168, 69, 703sstr4i 3493 . . . . . . 7 *Q ⊆ (Q × Q)
72 relxp 4989 . . . . . . 7 Rel (Q × Q)
73 relss 4969 . . . . . . 7 (*Q ⊆ (Q × Q) → (Rel (Q × Q) → Rel *Q))
7471, 72, 73mp2 9 . . . . . 6 Rel *Q
7569eleq2i 2575 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ *Q ↔ ⟨𝑥, 𝑦⟩ ∈ ( ·Q “ {1Q}))
76 ffn 5784 . . . . . . . . 9 ( ·Q :(Q × Q)⟶Q → ·Q Fn (Q × Q))
77 fniniseg 6070 . . . . . . . . 9 ( ·Q Fn (Q × Q) → (⟨𝑥, 𝑦⟩ ∈ ( ·Q “ {1Q}) ↔ (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q)))
788, 76, 77mp2b 10 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ ( ·Q “ {1Q}) ↔ (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q))
79 ancom 459 . . . . . . . . 9 ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
80 ancom 459 . . . . . . . . . 10 ((𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q) ↔ ((𝑥 ·Q 𝑦) = 1Q𝑥Q))
81 eleq1 2571 . . . . . . . . . . . . . . 15 ((𝑥 ·Q 𝑦) = 1Q → ((𝑥 ·Q 𝑦) ∈ Q ↔ 1QQ))
826, 81mpbiri 243 . . . . . . . . . . . . . 14 ((𝑥 ·Q 𝑦) = 1Q → (𝑥 ·Q 𝑦) ∈ Q)
839, 10ndmovrcl 6530 . . . . . . . . . . . . . 14 ((𝑥 ·Q 𝑦) ∈ Q → (𝑥Q𝑦Q))
8482, 83syl 17 . . . . . . . . . . . . 13 ((𝑥 ·Q 𝑦) = 1Q → (𝑥Q𝑦Q))
85 opelxpi 4912 . . . . . . . . . . . . 13 ((𝑥Q𝑦Q) → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
8684, 85syl 17 . . . . . . . . . . . 12 ((𝑥 ·Q 𝑦) = 1Q → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
8784simpld 468 . . . . . . . . . . . 12 ((𝑥 ·Q 𝑦) = 1Q𝑥Q)
8886, 872thd 250 . . . . . . . . . . 11 ((𝑥 ·Q 𝑦) = 1Q → (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ↔ 𝑥Q))
8988pm5.32i 658 . . . . . . . . . 10 (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ ((𝑥 ·Q 𝑦) = 1Q𝑥Q))
90 df-ov 6366 . . . . . . . . . . . 12 (𝑥 ·Q 𝑦) = ( ·Q ‘⟨𝑥, 𝑦⟩)
9190eqeq1i 2510 . . . . . . . . . . 11 ((𝑥 ·Q 𝑦) = 1Q ↔ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q)
9291anbi1i 718 . . . . . . . . . 10 (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
9380, 89, 923bitr2ri 284 . . . . . . . . 9 ((( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q))
9479, 93bitri 259 . . . . . . . 8 ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q))
9575, 78, 943bitri 281 . . . . . . 7 (⟨𝑥, 𝑦⟩ ∈ *Q ↔ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q))
9695a1i 11 . . . . . 6 (⊤ → (⟨𝑥, 𝑦⟩ ∈ *Q ↔ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q)))
9774, 96opabbi2dv 5031 . . . . 5 (⊤ → *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q)})
9897trud 1477 . . . 4 *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
9918, 20, 67, 98fvopab3g 6011 . . 3 ((𝐴Q𝐵 ∈ V) → ((*Q𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
10099ex 443 . 2 (𝐴Q → (𝐵 ∈ V → ((*Q𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q)))
1014, 16, 100pm5.21ndd 363 1 (𝐴Q → ((*Q𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191  wa 378   = wceq 1468  wtru 1469  wex 1692  wcel 1937  ∃!weu 2353  ∃*wmo 2354  Vcvv 3066  wss 3426  {csn 3995  cop 4001   class class class wbr 4434  {copab 4492   × cxp 4878  ccnv 4879  dom cdm 4880  cima 4883  Rel wrel 4885   Fn wfn 5628  wf 5629  cfv 5633  (class class class)co 6363  1st c1st 6868  2nd c2nd 6869  Ncnpi 9354   ·N cmi 9356   ·pQ cmpq 9359   ~Q ceq 9361  Qcnq 9362  1Qc1q 9363  [Q]cerq 9364   ·Q cmq 9366  *Qcrq 9367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680  ax-un 6659
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-iun 4309  df-br 4435  df-opab 4494  df-mpt 4495  df-tr 4531  df-eprel 4791  df-id 4795  df-po 4801  df-so 4802  df-fr 4839  df-we 4841  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-pred 5431  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-iota 5597  df-fun 5635  df-fn 5636  df-f 5637  df-f1 5638  df-fo 5639  df-f1o 5640  df-fv 5641  df-ov 6366  df-oprab 6367  df-mpt2 6368  df-om 6770  df-1st 6870  df-2nd 6871  df-wrecs 7105  df-recs 7167  df-rdg 7205  df-1o 7259  df-oadd 7263  df-omul 7264  df-er 7440  df-ni 9382  df-mi 9384  df-lti 9385  df-mpq 9419  df-enq 9421  df-nq 9422  df-erq 9423  df-mq 9425  df-1nq 9426  df-rq 9427
This theorem is referenced by:  recidnq  9475  recrecnq  9477  reclem3pr  9559
  Copyright terms: Public domain W3C validator