Metamath Proof Explorer


Theorem recmulnq

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.)

Ref Expression
Assertion recmulnq A 𝑸 * 𝑸 A = B A 𝑸 B = 1 𝑸

Proof

Step Hyp Ref Expression
1 fvex * 𝑸 A V
2 1 a1i A 𝑸 * 𝑸 A V
3 eleq1 * 𝑸 A = B * 𝑸 A V B V
4 2 3 syl5ibcom A 𝑸 * 𝑸 A = B B V
5 id A 𝑸 B = 1 𝑸 A 𝑸 B = 1 𝑸
6 1nq 1 𝑸 𝑸
7 5 6 eqeltrdi A 𝑸 B = 1 𝑸 A 𝑸 B 𝑸
8 mulnqf 𝑸 : 𝑸 × 𝑸 𝑸
9 8 fdmi dom 𝑸 = 𝑸 × 𝑸
10 0nnq ¬ 𝑸
11 9 10 ndmovrcl A 𝑸 B 𝑸 A 𝑸 B 𝑸
12 7 11 syl A 𝑸 B = 1 𝑸 A 𝑸 B 𝑸
13 elex B 𝑸 B V
14 12 13 simpl2im A 𝑸 B = 1 𝑸 B V
15 14 a1i A 𝑸 A 𝑸 B = 1 𝑸 B V
16 oveq1 x = A x 𝑸 y = A 𝑸 y
17 16 eqeq1d x = A x 𝑸 y = 1 𝑸 A 𝑸 y = 1 𝑸
18 oveq2 y = B A 𝑸 y = A 𝑸 B
19 18 eqeq1d y = B A 𝑸 y = 1 𝑸 A 𝑸 B = 1 𝑸
20 nqerid x 𝑸 / 𝑸 x = x
21 relxp Rel 𝑵 × 𝑵
22 elpqn x 𝑸 x 𝑵 × 𝑵
23 1st2nd Rel 𝑵 × 𝑵 x 𝑵 × 𝑵 x = 1 st x 2 nd x
24 21 22 23 sylancr x 𝑸 x = 1 st x 2 nd x
25 24 fveq2d x 𝑸 / 𝑸 x = / 𝑸 1 st x 2 nd x
26 20 25 eqtr3d x 𝑸 x = / 𝑸 1 st x 2 nd x
27 26 oveq1d x 𝑸 x 𝑸 / 𝑸 2 nd x 1 st x = / 𝑸 1 st x 2 nd x 𝑸 / 𝑸 2 nd x 1 st x
28 mulerpq / 𝑸 1 st x 2 nd x 𝑸 / 𝑸 2 nd x 1 st x = / 𝑸 1 st x 2 nd x 𝑝𝑸 2 nd x 1 st x
29 27 28 eqtrdi x 𝑸 x 𝑸 / 𝑸 2 nd x 1 st x = / 𝑸 1 st x 2 nd x 𝑝𝑸 2 nd x 1 st x
30 xp1st x 𝑵 × 𝑵 1 st x 𝑵
31 22 30 syl x 𝑸 1 st x 𝑵
32 xp2nd x 𝑵 × 𝑵 2 nd x 𝑵
33 22 32 syl x 𝑸 2 nd x 𝑵
34 mulpipq 1 st x 𝑵 2 nd x 𝑵 2 nd x 𝑵 1 st x 𝑵 1 st x 2 nd x 𝑝𝑸 2 nd x 1 st x = 1 st x 𝑵 2 nd x 2 nd x 𝑵 1 st x
35 31 33 33 31 34 syl22anc x 𝑸 1 st x 2 nd x 𝑝𝑸 2 nd x 1 st x = 1 st x 𝑵 2 nd x 2 nd x 𝑵 1 st x
36 mulcompi 2 nd x 𝑵 1 st x = 1 st x 𝑵 2 nd x
37 36 opeq2i 1 st x 𝑵 2 nd x 2 nd x 𝑵 1 st x = 1 st x 𝑵 2 nd x 1 st x 𝑵 2 nd x
38 35 37 eqtrdi x 𝑸 1 st x 2 nd x 𝑝𝑸 2 nd x 1 st x = 1 st x 𝑵 2 nd x 1 st x 𝑵 2 nd x
39 38 fveq2d x 𝑸 / 𝑸 1 st x 2 nd x 𝑝𝑸 2 nd x 1 st x = / 𝑸 1 st x 𝑵 2 nd x 1 st x 𝑵 2 nd x
40 mulclpi 1 st x 𝑵 2 nd x 𝑵 1 st x 𝑵 2 nd x 𝑵
41 31 33 40 syl2anc x 𝑸 1 st x 𝑵 2 nd x 𝑵
42 1nqenq 1 st x 𝑵 2 nd x 𝑵 1 𝑸 ~ 𝑸 1 st x 𝑵 2 nd x 1 st x 𝑵 2 nd x
43 41 42 syl x 𝑸 1 𝑸 ~ 𝑸 1 st x 𝑵 2 nd x 1 st x 𝑵 2 nd x
44 elpqn 1 𝑸 𝑸 1 𝑸 𝑵 × 𝑵
45 6 44 ax-mp 1 𝑸 𝑵 × 𝑵
46 41 41 opelxpd x 𝑸 1 st x 𝑵 2 nd x 1 st x 𝑵 2 nd x 𝑵 × 𝑵
47 nqereq 1 𝑸 𝑵 × 𝑵 1 st x 𝑵 2 nd x 1 st x 𝑵 2 nd x 𝑵 × 𝑵 1 𝑸 ~ 𝑸 1 st x 𝑵 2 nd x 1 st x 𝑵 2 nd x / 𝑸 1 𝑸 = / 𝑸 1 st x 𝑵 2 nd x 1 st x 𝑵 2 nd x
48 45 46 47 sylancr x 𝑸 1 𝑸 ~ 𝑸 1 st x 𝑵 2 nd x 1 st x 𝑵 2 nd x / 𝑸 1 𝑸 = / 𝑸 1 st x 𝑵 2 nd x 1 st x 𝑵 2 nd x
49 43 48 mpbid x 𝑸 / 𝑸 1 𝑸 = / 𝑸 1 st x 𝑵 2 nd x 1 st x 𝑵 2 nd x
50 nqerid 1 𝑸 𝑸 / 𝑸 1 𝑸 = 1 𝑸
51 6 50 ax-mp / 𝑸 1 𝑸 = 1 𝑸
52 49 51 eqtr3di x 𝑸 / 𝑸 1 st x 𝑵 2 nd x 1 st x 𝑵 2 nd x = 1 𝑸
53 29 39 52 3eqtrd x 𝑸 x 𝑸 / 𝑸 2 nd x 1 st x = 1 𝑸
54 fvex / 𝑸 2 nd x 1 st x V
55 oveq2 y = / 𝑸 2 nd x 1 st x x 𝑸 y = x 𝑸 / 𝑸 2 nd x 1 st x
56 55 eqeq1d y = / 𝑸 2 nd x 1 st x x 𝑸 y = 1 𝑸 x 𝑸 / 𝑸 2 nd x 1 st x = 1 𝑸
57 54 56 spcev x 𝑸 / 𝑸 2 nd x 1 st x = 1 𝑸 y x 𝑸 y = 1 𝑸
58 53 57 syl x 𝑸 y x 𝑸 y = 1 𝑸
59 mulcomnq r 𝑸 s = s 𝑸 r
60 mulassnq r 𝑸 s 𝑸 t = r 𝑸 s 𝑸 t
61 mulidnq r 𝑸 r 𝑸 1 𝑸 = r
62 6 9 10 59 60 61 caovmo * y x 𝑸 y = 1 𝑸
63 df-eu ∃! y x 𝑸 y = 1 𝑸 y x 𝑸 y = 1 𝑸 * y x 𝑸 y = 1 𝑸
64 58 62 63 sylanblrc x 𝑸 ∃! y x 𝑸 y = 1 𝑸
65 cnvimass 𝑸 -1 1 𝑸 dom 𝑸
66 df-rq * 𝑸 = 𝑸 -1 1 𝑸
67 9 eqcomi 𝑸 × 𝑸 = dom 𝑸
68 65 66 67 3sstr4i * 𝑸 𝑸 × 𝑸
69 relxp Rel 𝑸 × 𝑸
70 relss * 𝑸 𝑸 × 𝑸 Rel 𝑸 × 𝑸 Rel * 𝑸
71 68 69 70 mp2 Rel * 𝑸
72 66 eleq2i x y * 𝑸 x y 𝑸 -1 1 𝑸
73 ffn 𝑸 : 𝑸 × 𝑸 𝑸 𝑸 Fn 𝑸 × 𝑸
74 fniniseg 𝑸 Fn 𝑸 × 𝑸 x y 𝑸 -1 1 𝑸 x y 𝑸 × 𝑸 𝑸 x y = 1 𝑸
75 8 73 74 mp2b x y 𝑸 -1 1 𝑸 x y 𝑸 × 𝑸 𝑸 x y = 1 𝑸
76 ancom x y 𝑸 × 𝑸 𝑸 x y = 1 𝑸 𝑸 x y = 1 𝑸 x y 𝑸 × 𝑸
77 ancom x 𝑸 x 𝑸 y = 1 𝑸 x 𝑸 y = 1 𝑸 x 𝑸
78 eleq1 x 𝑸 y = 1 𝑸 x 𝑸 y 𝑸 1 𝑸 𝑸
79 6 78 mpbiri x 𝑸 y = 1 𝑸 x 𝑸 y 𝑸
80 9 10 ndmovrcl x 𝑸 y 𝑸 x 𝑸 y 𝑸
81 79 80 syl x 𝑸 y = 1 𝑸 x 𝑸 y 𝑸
82 opelxpi x 𝑸 y 𝑸 x y 𝑸 × 𝑸
83 81 82 syl x 𝑸 y = 1 𝑸 x y 𝑸 × 𝑸
84 81 simpld x 𝑸 y = 1 𝑸 x 𝑸
85 83 84 2thd x 𝑸 y = 1 𝑸 x y 𝑸 × 𝑸 x 𝑸
86 85 pm5.32i x 𝑸 y = 1 𝑸 x y 𝑸 × 𝑸 x 𝑸 y = 1 𝑸 x 𝑸
87 df-ov x 𝑸 y = 𝑸 x y
88 87 eqeq1i x 𝑸 y = 1 𝑸 𝑸 x y = 1 𝑸
89 88 anbi1i x 𝑸 y = 1 𝑸 x y 𝑸 × 𝑸 𝑸 x y = 1 𝑸 x y 𝑸 × 𝑸
90 77 86 89 3bitr2ri 𝑸 x y = 1 𝑸 x y 𝑸 × 𝑸 x 𝑸 x 𝑸 y = 1 𝑸
91 76 90 bitri x y 𝑸 × 𝑸 𝑸 x y = 1 𝑸 x 𝑸 x 𝑸 y = 1 𝑸
92 72 75 91 3bitri x y * 𝑸 x 𝑸 x 𝑸 y = 1 𝑸
93 92 a1i x y * 𝑸 x 𝑸 x 𝑸 y = 1 𝑸
94 71 93 opabbi2dv * 𝑸 = x y | x 𝑸 x 𝑸 y = 1 𝑸
95 94 mptru * 𝑸 = x y | x 𝑸 x 𝑸 y = 1 𝑸
96 17 19 64 95 fvopab3g A 𝑸 B V * 𝑸 A = B A 𝑸 B = 1 𝑸
97 96 ex A 𝑸 B V * 𝑸 A = B A 𝑸 B = 1 𝑸
98 4 15 97 pm5.21ndd A 𝑸 * 𝑸 A = B A 𝑸 B = 1 𝑸