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

Theorem recmulnq 9540
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 5996 . . . 4 (*Q𝐴) ∈ V
21a1i 11 . . 3 (𝐴Q → (*Q𝐴) ∈ V)
3 eleq1 2580 . . 3 ((*Q𝐴) = 𝐵 → ((*Q𝐴) ∈ V ↔ 𝐵 ∈ V))
42, 3syl5ibcom 233 . 2 (𝐴Q → ((*Q𝐴) = 𝐵𝐵 ∈ V))
5 id 22 . . . . . . 7 ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) = 1Q)
6 1nq 9504 . . . . . . 7 1QQ
75, 6syl6eqel 2600 . . . . . 6 ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) ∈ Q)
8 mulnqf 9525 . . . . . . . 8 ·Q :(Q × Q)⟶Q
98fdmi 5850 . . . . . . 7 dom ·Q = (Q × Q)
10 0nnq 9500 . . . . . . 7 ¬ ∅ ∈ Q
119, 10ndmovrcl 6593 . . . . . 6 ((𝐴 ·Q 𝐵) ∈ Q → (𝐴Q𝐵Q))
127, 11syl 17 . . . . 5 ((𝐴 ·Q 𝐵) = 1Q → (𝐴Q𝐵Q))
1312simprd 477 . . . 4 ((𝐴 ·Q 𝐵) = 1Q𝐵Q)
14 elex 3089 . . . 4 (𝐵Q𝐵 ∈ V)
1513, 14syl 17 . . 3 ((𝐴 ·Q 𝐵) = 1Q𝐵 ∈ V)
1615a1i 11 . 2 (𝐴Q → ((𝐴 ·Q 𝐵) = 1Q𝐵 ∈ V))
17 oveq1 6432 . . . . 5 (𝑥 = 𝐴 → (𝑥 ·Q 𝑦) = (𝐴 ·Q 𝑦))
1817eqeq1d 2516 . . . 4 (𝑥 = 𝐴 → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝑦) = 1Q))
19 oveq2 6433 . . . . 5 (𝑦 = 𝐵 → (𝐴 ·Q 𝑦) = (𝐴 ·Q 𝐵))
2019eqeq1d 2516 . . . 4 (𝑦 = 𝐵 → ((𝐴 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝐵) = 1Q))
21 nqerid 9509 . . . . . . . . . 10 (𝑥Q → ([Q]‘𝑥) = 𝑥)
22 relxp 5043 . . . . . . . . . . . 12 Rel (N × N)
23 elpqn 9501 . . . . . . . . . . . 12 (𝑥Q𝑥 ∈ (N × N))
24 1st2nd 6979 . . . . . . . . . . . 12 ((Rel (N × N) ∧ 𝑥 ∈ (N × N)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
2522, 23, 24sylancr 693 . . . . . . . . . . 11 (𝑥Q𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
2625fveq2d 5990 . . . . . . . . . 10 (𝑥Q → ([Q]‘𝑥) = ([Q]‘⟨(1st𝑥), (2nd𝑥)⟩))
2721, 26eqtr3d 2550 . . . . . . . . 9 (𝑥Q𝑥 = ([Q]‘⟨(1st𝑥), (2nd𝑥)⟩))
2827oveq1d 6440 . . . . . . . 8 (𝑥Q → (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = (([Q]‘⟨(1st𝑥), (2nd𝑥)⟩) ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)))
29 mulerpq 9533 . . . . . . . 8 (([Q]‘⟨(1st𝑥), (2nd𝑥)⟩) ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = ([Q]‘(⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩))
3028, 29syl6eq 2564 . . . . . . 7 (𝑥Q → (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = ([Q]‘(⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩)))
31 xp1st 6963 . . . . . . . . . . 11 (𝑥 ∈ (N × N) → (1st𝑥) ∈ N)
3223, 31syl 17 . . . . . . . . . 10 (𝑥Q → (1st𝑥) ∈ N)
33 xp2nd 6964 . . . . . . . . . . 11 (𝑥 ∈ (N × N) → (2nd𝑥) ∈ N)
3423, 33syl 17 . . . . . . . . . 10 (𝑥Q → (2nd𝑥) ∈ N)
35 mulpipq 9516 . . . . . . . . . 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 1318 . . . . . . . . 9 (𝑥Q → (⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩) = ⟨((1st𝑥) ·N (2nd𝑥)), ((2nd𝑥) ·N (1st𝑥))⟩)
37 mulcompi 9472 . . . . . . . . . 10 ((2nd𝑥) ·N (1st𝑥)) = ((1st𝑥) ·N (2nd𝑥))
3837opeq2i 4242 . . . . . . . . 9 ⟨((1st𝑥) ·N (2nd𝑥)), ((2nd𝑥) ·N (1st𝑥))⟩ = ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩
3936, 38syl6eq 2564 . . . . . . . 8 (𝑥Q → (⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩) = ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩)
4039fveq2d 5990 . . . . . . 7 (𝑥Q → ([Q]‘(⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩)) = ([Q]‘⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩))
41 nqerid 9509 . . . . . . . . 9 (1QQ → ([Q]‘1Q) = 1Q)
426, 41ax-mp 5 . . . . . . . 8 ([Q]‘1Q) = 1Q
43 mulclpi 9469 . . . . . . . . . . 11 (((1st𝑥) ∈ N ∧ (2nd𝑥) ∈ N) → ((1st𝑥) ·N (2nd𝑥)) ∈ N)
4432, 34, 43syl2anc 690 . . . . . . . . . 10 (𝑥Q → ((1st𝑥) ·N (2nd𝑥)) ∈ N)
45 1nqenq 9538 . . . . . . . . . 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 9501 . . . . . . . . . . 11 (1QQ → 1Q ∈ (N × N))
486, 47ax-mp 5 . . . . . . . . . 10 1Q ∈ (N × N)
49 opelxpi 4966 . . . . . . . . . . 11 ((((1st𝑥) ·N (2nd𝑥)) ∈ N ∧ ((1st𝑥) ·N (2nd𝑥)) ∈ N) → ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩ ∈ (N × N))
5044, 44, 49syl2anc 690 . . . . . . . . . 10 (𝑥Q → ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩ ∈ (N × N))
51 nqereq 9511 . . . . . . . . . 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 693 . . . . . . . . 9 (𝑥Q → (1Q ~Q ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩ ↔ ([Q]‘1Q) = ([Q]‘⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩)))
5346, 52mpbid 220 . . . . . . . 8 (𝑥Q → ([Q]‘1Q) = ([Q]‘⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩))
5442, 53syl5reqr 2563 . . . . . . 7 (𝑥Q → ([Q]‘⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩) = 1Q)
5530, 40, 543eqtrd 2552 . . . . . 6 (𝑥Q → (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = 1Q)
56 fvex 5996 . . . . . . 7 ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩) ∈ V
57 oveq2 6433 . . . . . . . 8 (𝑦 = ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩) → (𝑥 ·Q 𝑦) = (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)))
5857eqeq1d 2516 . . . . . . 7 (𝑦 = ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩) → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = 1Q))
5956, 58spcev 3177 . . . . . 6 ((𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = 1Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
6055, 59syl 17 . . . . 5 (𝑥Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
61 mulcomnq 9529 . . . . . . 7 (𝑟 ·Q 𝑠) = (𝑠 ·Q 𝑟)
62 mulassnq 9535 . . . . . . 7 ((𝑟 ·Q 𝑠) ·Q 𝑡) = (𝑟 ·Q (𝑠 ·Q 𝑡))
63 mulidnq 9539 . . . . . . 7 (𝑟Q → (𝑟 ·Q 1Q) = 𝑟)
646, 9, 10, 61, 62, 63caovmo 6644 . . . . . 6 ∃*𝑦(𝑥 ·Q 𝑦) = 1Q
65 eu5 2388 . . . . . 6 (∃!𝑦(𝑥 ·Q 𝑦) = 1Q ↔ (∃𝑦(𝑥 ·Q 𝑦) = 1Q ∧ ∃*𝑦(𝑥 ·Q 𝑦) = 1Q))
6664, 65mpbiran2 955 . . . . 5 (∃!𝑦(𝑥 ·Q 𝑦) = 1Q ↔ ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
6760, 66sylibr 222 . . . 4 (𝑥Q → ∃!𝑦(𝑥 ·Q 𝑦) = 1Q)
68 cnvimass 5295 . . . . . . . 8 ( ·Q “ {1Q}) ⊆ dom ·Q
69 df-rq 9493 . . . . . . . 8 *Q = ( ·Q “ {1Q})
709eqcomi 2523 . . . . . . . 8 (Q × Q) = dom ·Q
7168, 69, 703sstr4i 3511 . . . . . . 7 *Q ⊆ (Q × Q)
72 relxp 5043 . . . . . . 7 Rel (Q × Q)
73 relss 5023 . . . . . . 7 (*Q ⊆ (Q × Q) → (Rel (Q × Q) → Rel *Q))
7471, 72, 73mp2 9 . . . . . 6 Rel *Q
7569eleq2i 2584 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ *Q ↔ ⟨𝑥, 𝑦⟩ ∈ ( ·Q “ {1Q}))
76 ffn 5843 . . . . . . . . 9 ( ·Q :(Q × Q)⟶Q → ·Q Fn (Q × Q))
77 fniniseg 6129 . . . . . . . . 9 ( ·Q Fn (Q × Q) → (⟨𝑥, 𝑦⟩ ∈ ( ·Q “ {1Q}) ↔ (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q)))
788, 76, 77mp2b 10 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ ( ·Q “ {1Q}) ↔ (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q))
79 ancom 464 . . . . . . . . 9 ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
80 ancom 464 . . . . . . . . . 10 ((𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q) ↔ ((𝑥 ·Q 𝑦) = 1Q𝑥Q))
81 eleq1 2580 . . . . . . . . . . . . . . 15 ((𝑥 ·Q 𝑦) = 1Q → ((𝑥 ·Q 𝑦) ∈ Q ↔ 1QQ))
826, 81mpbiri 246 . . . . . . . . . . . . . 14 ((𝑥 ·Q 𝑦) = 1Q → (𝑥 ·Q 𝑦) ∈ Q)
839, 10ndmovrcl 6593 . . . . . . . . . . . . . 14 ((𝑥 ·Q 𝑦) ∈ Q → (𝑥Q𝑦Q))
8482, 83syl 17 . . . . . . . . . . . . 13 ((𝑥 ·Q 𝑦) = 1Q → (𝑥Q𝑦Q))
85 opelxpi 4966 . . . . . . . . . . . . 13 ((𝑥Q𝑦Q) → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
8684, 85syl 17 . . . . . . . . . . . 12 ((𝑥 ·Q 𝑦) = 1Q → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
8784simpld 473 . . . . . . . . . . . 12 ((𝑥 ·Q 𝑦) = 1Q𝑥Q)
8886, 872thd 253 . . . . . . . . . . 11 ((𝑥 ·Q 𝑦) = 1Q → (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ↔ 𝑥Q))
8988pm5.32i 666 . . . . . . . . . 10 (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ ((𝑥 ·Q 𝑦) = 1Q𝑥Q))
90 df-ov 6428 . . . . . . . . . . . 12 (𝑥 ·Q 𝑦) = ( ·Q ‘⟨𝑥, 𝑦⟩)
9190eqeq1i 2519 . . . . . . . . . . 11 ((𝑥 ·Q 𝑦) = 1Q ↔ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q)
9291anbi1i 726 . . . . . . . . . 10 (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
9380, 89, 923bitr2ri 287 . . . . . . . . 9 ((( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q))
9479, 93bitri 262 . . . . . . . 8 ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q))
9575, 78, 943bitri 284 . . . . . . 7 (⟨𝑥, 𝑦⟩ ∈ *Q ↔ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q))
9695a1i 11 . . . . . 6 (⊤ → (⟨𝑥, 𝑦⟩ ∈ *Q ↔ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q)))
9774, 96opabbi2dv 5085 . . . . 5 (⊤ → *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q)})
9897trud 1483 . . . 4 *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
9918, 20, 67, 98fvopab3g 6070 . . 3 ((𝐴Q𝐵 ∈ V) → ((*Q𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
10099ex 448 . 2 (𝐴Q → (𝐵 ∈ V → ((*Q𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q)))
1014, 16, 100pm5.21ndd 367 1 (𝐴Q → ((*Q𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wtru 1475  wex 1694  wcel 1938  ∃!weu 2362  ∃*wmo 2363  Vcvv 3077  wss 3444  {csn 4028  cop 4034   class class class wbr 4481  {copab 4540   × cxp 4930  ccnv 4931  dom cdm 4932  cima 4935  Rel wrel 4937   Fn wfn 5684  wf 5685  cfv 5689  (class class class)co 6425  1st c1st 6931  2nd c2nd 6932  Ncnpi 9420   ·N cmi 9422   ·pQ cmpq 9425   ~Q ceq 9427  Qcnq 9428  1Qc1q 9429  [Q]cerq 9430   ·Q cmq 9432  *Qcrq 9433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6722
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-ov 6428  df-oprab 6429  df-mpt2 6430  df-om 6833  df-1st 6933  df-2nd 6934  df-wrecs 7168  df-recs 7230  df-rdg 7268  df-1o 7322  df-oadd 7326  df-omul 7327  df-er 7504  df-ni 9448  df-mi 9450  df-lti 9451  df-mpq 9485  df-enq 9487  df-nq 9488  df-erq 9489  df-mq 9491  df-1nq 9492  df-rq 9493
This theorem is referenced by:  recidnq  9541  recrecnq  9543  reclem3pr  9625
  Copyright terms: Public domain W3C validator