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

Theorem recmulnq 10232
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 6551 . . . 4 (*Q𝐴) ∈ V
21a1i 11 . . 3 (𝐴Q → (*Q𝐴) ∈ V)
3 eleq1 2870 . . 3 ((*Q𝐴) = 𝐵 → ((*Q𝐴) ∈ V ↔ 𝐵 ∈ V))
42, 3syl5ibcom 246 . 2 (𝐴Q → ((*Q𝐴) = 𝐵𝐵 ∈ V))
5 id 22 . . . . . 6 ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) = 1Q)
6 1nq 10196 . . . . . 6 1QQ
75, 6syl6eqel 2891 . . . . 5 ((𝐴 ·Q 𝐵) = 1Q → (𝐴 ·Q 𝐵) ∈ Q)
8 mulnqf 10217 . . . . . . 7 ·Q :(Q × Q)⟶Q
98fdmi 6392 . . . . . 6 dom ·Q = (Q × Q)
10 0nnq 10192 . . . . . 6 ¬ ∅ ∈ Q
119, 10ndmovrcl 7190 . . . . 5 ((𝐴 ·Q 𝐵) ∈ Q → (𝐴Q𝐵Q))
127, 11syl 17 . . . 4 ((𝐴 ·Q 𝐵) = 1Q → (𝐴Q𝐵Q))
13 elex 3455 . . . 4 (𝐵Q𝐵 ∈ V)
1412, 13simpl2im 504 . . 3 ((𝐴 ·Q 𝐵) = 1Q𝐵 ∈ V)
1514a1i 11 . 2 (𝐴Q → ((𝐴 ·Q 𝐵) = 1Q𝐵 ∈ V))
16 oveq1 7023 . . . . 5 (𝑥 = 𝐴 → (𝑥 ·Q 𝑦) = (𝐴 ·Q 𝑦))
1716eqeq1d 2797 . . . 4 (𝑥 = 𝐴 → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝑦) = 1Q))
18 oveq2 7024 . . . . 5 (𝑦 = 𝐵 → (𝐴 ·Q 𝑦) = (𝐴 ·Q 𝐵))
1918eqeq1d 2797 . . . 4 (𝑦 = 𝐵 → ((𝐴 ·Q 𝑦) = 1Q ↔ (𝐴 ·Q 𝐵) = 1Q))
20 nqerid 10201 . . . . . . . . . 10 (𝑥Q → ([Q]‘𝑥) = 𝑥)
21 relxp 5461 . . . . . . . . . . . 12 Rel (N × N)
22 elpqn 10193 . . . . . . . . . . . 12 (𝑥Q𝑥 ∈ (N × N))
23 1st2nd 7594 . . . . . . . . . . . 12 ((Rel (N × N) ∧ 𝑥 ∈ (N × N)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
2421, 22, 23sylancr 587 . . . . . . . . . . 11 (𝑥Q𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
2524fveq2d 6542 . . . . . . . . . 10 (𝑥Q → ([Q]‘𝑥) = ([Q]‘⟨(1st𝑥), (2nd𝑥)⟩))
2620, 25eqtr3d 2833 . . . . . . . . 9 (𝑥Q𝑥 = ([Q]‘⟨(1st𝑥), (2nd𝑥)⟩))
2726oveq1d 7031 . . . . . . . 8 (𝑥Q → (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = (([Q]‘⟨(1st𝑥), (2nd𝑥)⟩) ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)))
28 mulerpq 10225 . . . . . . . 8 (([Q]‘⟨(1st𝑥), (2nd𝑥)⟩) ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = ([Q]‘(⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩))
2927, 28syl6eq 2847 . . . . . . 7 (𝑥Q → (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = ([Q]‘(⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩)))
30 xp1st 7577 . . . . . . . . . . 11 (𝑥 ∈ (N × N) → (1st𝑥) ∈ N)
3122, 30syl 17 . . . . . . . . . 10 (𝑥Q → (1st𝑥) ∈ N)
32 xp2nd 7578 . . . . . . . . . . 11 (𝑥 ∈ (N × N) → (2nd𝑥) ∈ N)
3322, 32syl 17 . . . . . . . . . 10 (𝑥Q → (2nd𝑥) ∈ N)
34 mulpipq 10208 . . . . . . . . . 10 ((((1st𝑥) ∈ N ∧ (2nd𝑥) ∈ N) ∧ ((2nd𝑥) ∈ N ∧ (1st𝑥) ∈ N)) → (⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩) = ⟨((1st𝑥) ·N (2nd𝑥)), ((2nd𝑥) ·N (1st𝑥))⟩)
3531, 33, 33, 31, 34syl22anc 835 . . . . . . . . 9 (𝑥Q → (⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩) = ⟨((1st𝑥) ·N (2nd𝑥)), ((2nd𝑥) ·N (1st𝑥))⟩)
36 mulcompi 10164 . . . . . . . . . 10 ((2nd𝑥) ·N (1st𝑥)) = ((1st𝑥) ·N (2nd𝑥))
3736opeq2i 4714 . . . . . . . . 9 ⟨((1st𝑥) ·N (2nd𝑥)), ((2nd𝑥) ·N (1st𝑥))⟩ = ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩
3835, 37syl6eq 2847 . . . . . . . 8 (𝑥Q → (⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩) = ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩)
3938fveq2d 6542 . . . . . . 7 (𝑥Q → ([Q]‘(⟨(1st𝑥), (2nd𝑥)⟩ ·pQ ⟨(2nd𝑥), (1st𝑥)⟩)) = ([Q]‘⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩))
40 nqerid 10201 . . . . . . . . 9 (1QQ → ([Q]‘1Q) = 1Q)
416, 40ax-mp 5 . . . . . . . 8 ([Q]‘1Q) = 1Q
42 mulclpi 10161 . . . . . . . . . . 11 (((1st𝑥) ∈ N ∧ (2nd𝑥) ∈ N) → ((1st𝑥) ·N (2nd𝑥)) ∈ N)
4331, 33, 42syl2anc 584 . . . . . . . . . 10 (𝑥Q → ((1st𝑥) ·N (2nd𝑥)) ∈ N)
44 1nqenq 10230 . . . . . . . . . 10 (((1st𝑥) ·N (2nd𝑥)) ∈ N → 1Q ~Q ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩)
4543, 44syl 17 . . . . . . . . 9 (𝑥Q → 1Q ~Q ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩)
46 elpqn 10193 . . . . . . . . . . 11 (1QQ → 1Q ∈ (N × N))
476, 46ax-mp 5 . . . . . . . . . 10 1Q ∈ (N × N)
4843, 43opelxpd 5481 . . . . . . . . . 10 (𝑥Q → ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩ ∈ (N × N))
49 nqereq 10203 . . . . . . . . . 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𝑥))⟩)))
5047, 48, 49sylancr 587 . . . . . . . . 9 (𝑥Q → (1Q ~Q ⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩ ↔ ([Q]‘1Q) = ([Q]‘⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩)))
5145, 50mpbid 233 . . . . . . . 8 (𝑥Q → ([Q]‘1Q) = ([Q]‘⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩))
5241, 51syl5reqr 2846 . . . . . . 7 (𝑥Q → ([Q]‘⟨((1st𝑥) ·N (2nd𝑥)), ((1st𝑥) ·N (2nd𝑥))⟩) = 1Q)
5329, 39, 523eqtrd 2835 . . . . . 6 (𝑥Q → (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = 1Q)
54 fvex 6551 . . . . . . 7 ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩) ∈ V
55 oveq2 7024 . . . . . . . 8 (𝑦 = ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩) → (𝑥 ·Q 𝑦) = (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)))
5655eqeq1d 2797 . . . . . . 7 (𝑦 = ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩) → ((𝑥 ·Q 𝑦) = 1Q ↔ (𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = 1Q))
5754, 56spcev 3549 . . . . . 6 ((𝑥 ·Q ([Q]‘⟨(2nd𝑥), (1st𝑥)⟩)) = 1Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
5853, 57syl 17 . . . . 5 (𝑥Q → ∃𝑦(𝑥 ·Q 𝑦) = 1Q)
59 mulcomnq 10221 . . . . . 6 (𝑟 ·Q 𝑠) = (𝑠 ·Q 𝑟)
60 mulassnq 10227 . . . . . 6 ((𝑟 ·Q 𝑠) ·Q 𝑡) = (𝑟 ·Q (𝑠 ·Q 𝑡))
61 mulidnq 10231 . . . . . 6 (𝑟Q → (𝑟 ·Q 1Q) = 𝑟)
626, 9, 10, 59, 60, 61caovmo 7241 . . . . 5 ∃*𝑦(𝑥 ·Q 𝑦) = 1Q
63 df-eu 2612 . . . . 5 (∃!𝑦(𝑥 ·Q 𝑦) = 1Q ↔ (∃𝑦(𝑥 ·Q 𝑦) = 1Q ∧ ∃*𝑦(𝑥 ·Q 𝑦) = 1Q))
6458, 62, 63sylanblrc 590 . . . 4 (𝑥Q → ∃!𝑦(𝑥 ·Q 𝑦) = 1Q)
65 cnvimass 5825 . . . . . . . 8 ( ·Q “ {1Q}) ⊆ dom ·Q
66 df-rq 10185 . . . . . . . 8 *Q = ( ·Q “ {1Q})
679eqcomi 2804 . . . . . . . 8 (Q × Q) = dom ·Q
6865, 66, 673sstr4i 3931 . . . . . . 7 *Q ⊆ (Q × Q)
69 relxp 5461 . . . . . . 7 Rel (Q × Q)
70 relss 5542 . . . . . . 7 (*Q ⊆ (Q × Q) → (Rel (Q × Q) → Rel *Q))
7168, 69, 70mp2 9 . . . . . 6 Rel *Q
7266eleq2i 2874 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ *Q ↔ ⟨𝑥, 𝑦⟩ ∈ ( ·Q “ {1Q}))
73 ffn 6382 . . . . . . . . 9 ( ·Q :(Q × Q)⟶Q → ·Q Fn (Q × Q))
74 fniniseg 6695 . . . . . . . . 9 ( ·Q Fn (Q × Q) → (⟨𝑥, 𝑦⟩ ∈ ( ·Q “ {1Q}) ↔ (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q)))
758, 73, 74mp2b 10 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ ( ·Q “ {1Q}) ↔ (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q))
76 ancom 461 . . . . . . . . 9 ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
77 ancom 461 . . . . . . . . . 10 ((𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q) ↔ ((𝑥 ·Q 𝑦) = 1Q𝑥Q))
78 eleq1 2870 . . . . . . . . . . . . . . 15 ((𝑥 ·Q 𝑦) = 1Q → ((𝑥 ·Q 𝑦) ∈ Q ↔ 1QQ))
796, 78mpbiri 259 . . . . . . . . . . . . . 14 ((𝑥 ·Q 𝑦) = 1Q → (𝑥 ·Q 𝑦) ∈ Q)
809, 10ndmovrcl 7190 . . . . . . . . . . . . . 14 ((𝑥 ·Q 𝑦) ∈ Q → (𝑥Q𝑦Q))
8179, 80syl 17 . . . . . . . . . . . . 13 ((𝑥 ·Q 𝑦) = 1Q → (𝑥Q𝑦Q))
82 opelxpi 5480 . . . . . . . . . . . . 13 ((𝑥Q𝑦Q) → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
8381, 82syl 17 . . . . . . . . . . . 12 ((𝑥 ·Q 𝑦) = 1Q → ⟨𝑥, 𝑦⟩ ∈ (Q × Q))
8481simpld 495 . . . . . . . . . . . 12 ((𝑥 ·Q 𝑦) = 1Q𝑥Q)
8583, 842thd 266 . . . . . . . . . . 11 ((𝑥 ·Q 𝑦) = 1Q → (⟨𝑥, 𝑦⟩ ∈ (Q × Q) ↔ 𝑥Q))
8685pm5.32i 575 . . . . . . . . . 10 (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ ((𝑥 ·Q 𝑦) = 1Q𝑥Q))
87 df-ov 7019 . . . . . . . . . . . 12 (𝑥 ·Q 𝑦) = ( ·Q ‘⟨𝑥, 𝑦⟩)
8887eqeq1i 2800 . . . . . . . . . . 11 ((𝑥 ·Q 𝑦) = 1Q ↔ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q)
8988anbi1i 623 . . . . . . . . . 10 (((𝑥 ·Q 𝑦) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ (( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)))
9077, 86, 893bitr2ri 301 . . . . . . . . 9 ((( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q ∧ ⟨𝑥, 𝑦⟩ ∈ (Q × Q)) ↔ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q))
9176, 90bitri 276 . . . . . . . 8 ((⟨𝑥, 𝑦⟩ ∈ (Q × Q) ∧ ( ·Q ‘⟨𝑥, 𝑦⟩) = 1Q) ↔ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q))
9272, 75, 913bitri 298 . . . . . . 7 (⟨𝑥, 𝑦⟩ ∈ *Q ↔ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q))
9392a1i 11 . . . . . 6 (⊤ → (⟨𝑥, 𝑦⟩ ∈ *Q ↔ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q)))
9471, 93opabbi2dv 5606 . . . . 5 (⊤ → *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q)})
9594mptru 1529 . . . 4 *Q = {⟨𝑥, 𝑦⟩ ∣ (𝑥Q ∧ (𝑥 ·Q 𝑦) = 1Q)}
9617, 19, 64, 95fvopab3g 6630 . . 3 ((𝐴Q𝐵 ∈ V) → ((*Q𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
9796ex 413 . 2 (𝐴Q → (𝐵 ∈ V → ((*Q𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q)))
984, 15, 97pm5.21ndd 381 1 (𝐴Q → ((*Q𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1522  wtru 1523  wex 1761  wcel 2081  ∃*wmo 2574  ∃!weu 2611  Vcvv 3437  wss 3859  {csn 4472  cop 4478   class class class wbr 4962  {copab 5024   × cxp 5441  ccnv 5442  dom cdm 5443  cima 5446  Rel wrel 5448   Fn wfn 6220  wf 6221  cfv 6225  (class class class)co 7016  1st c1st 7543  2nd c2nd 7544  Ncnpi 10112   ·N cmi 10114   ·pQ cmpq 10117   ~Q ceq 10119  Qcnq 10120  1Qc1q 10121  [Q]cerq 10122   ·Q cmq 10124  *Qcrq 10125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-oadd 7957  df-omul 7958  df-er 8139  df-ni 10140  df-mi 10142  df-lti 10143  df-mpq 10177  df-enq 10179  df-nq 10180  df-erq 10181  df-mq 10183  df-1nq 10184  df-rq 10185
This theorem is referenced by:  recidnq  10233  recrecnq  10235  reclem3pr  10317
  Copyright terms: Public domain W3C validator