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=1st⁡x2nd⁡x
24 21 22 23 sylancr ⊢x∈𝑸→x=1st⁡x2nd⁡x
25 24 fveq2d ⊢x∈𝑸→/𝑸⁡x=/𝑸⁡1st⁡x2nd⁡x
26 20 25 eqtr3d ⊢x∈𝑸→x=/𝑸⁡1st⁡x2nd⁡x
27 26 oveq1d ⊢x∈𝑸→x⋅𝑸/𝑸⁡2nd⁡x1st⁡x=/𝑸⁡1st⁡x2nd⁡x⋅𝑸/𝑸⁡2nd⁡x1st⁡x
28 mulerpq ⊢/𝑸⁡1st⁡x2nd⁡x⋅𝑸/𝑸⁡2nd⁡x1st⁡x=/𝑸⁡1st⁡x2nd⁡x⋅𝑝𝑸2nd⁡x1st⁡x
29 27 28 eqtrdi ⊢x∈𝑸→x⋅𝑸/𝑸⁡2nd⁡x1st⁡x=/𝑸⁡1st⁡x2nd⁡x⋅𝑝𝑸2nd⁡x1st⁡x
30 xp1st ⊢x∈𝑵×𝑵→1st⁡x∈𝑵
31 22 30 syl ⊢x∈𝑸→1st⁡x∈𝑵
32 xp2nd ⊢x∈𝑵×𝑵→2nd⁡x∈𝑵
33 22 32 syl ⊢x∈𝑸→2nd⁡x∈𝑵
34 mulpipq ⊢1st⁡x∈𝑵∧2nd⁡x∈𝑵∧2nd⁡x∈𝑵∧1st⁡x∈𝑵→1st⁡x2nd⁡x⋅𝑝𝑸2nd⁡x1st⁡x=1st⁡x⋅𝑵2nd⁡x2nd⁡x⋅𝑵1st⁡x
35 31 33 33 31 34 syl22anc ⊢x∈𝑸→1st⁡x2nd⁡x⋅𝑝𝑸2nd⁡x1st⁡x=1st⁡x⋅𝑵2nd⁡x2nd⁡x⋅𝑵1st⁡x
36 mulcompi ⊢2nd⁡x⋅𝑵1st⁡x=1st⁡x⋅𝑵2nd⁡x
37 36 opeq2i ⊢1st⁡x⋅𝑵2nd⁡x2nd⁡x⋅𝑵1st⁡x=1st⁡x⋅𝑵2nd⁡x1st⁡x⋅𝑵2nd⁡x
38 35 37 eqtrdi ⊢x∈𝑸→1st⁡x2nd⁡x⋅𝑝𝑸2nd⁡x1st⁡x=1st⁡x⋅𝑵2nd⁡x1st⁡x⋅𝑵2nd⁡x
39 38 fveq2d ⊢x∈𝑸→/𝑸⁡1st⁡x2nd⁡x⋅𝑝𝑸2nd⁡x1st⁡x=/𝑸⁡1st⁡x⋅𝑵2nd⁡x1st⁡x⋅𝑵2nd⁡x
40 mulclpi ⊢1st⁡x∈𝑵∧2nd⁡x∈𝑵→1st⁡x⋅𝑵2nd⁡x∈𝑵
41 31 33 40 syl2anc ⊢x∈𝑸→1st⁡x⋅𝑵2nd⁡x∈𝑵
42 1nqenq ⊢1st⁡x⋅𝑵2nd⁡x∈𝑵→1𝑸~𝑸1st⁡x⋅𝑵2nd⁡x1st⁡x⋅𝑵2nd⁡x
43 41 42 syl ⊢x∈𝑸→1𝑸~𝑸1st⁡x⋅𝑵2nd⁡x1st⁡x⋅𝑵2nd⁡x
44 elpqn ⊢1𝑸∈𝑸→1𝑸∈𝑵×𝑵
45 6 44 ax-mp ⊢1𝑸∈𝑵×𝑵
46 41 41 opelxpd ⊢x∈𝑸→1st⁡x⋅𝑵2nd⁡x1st⁡x⋅𝑵2nd⁡x∈𝑵×𝑵
47 nqereq ⊢1𝑸∈𝑵×𝑵∧1st⁡x⋅𝑵2nd⁡x1st⁡x⋅𝑵2nd⁡x∈𝑵×𝑵→1𝑸~𝑸1st⁡x⋅𝑵2nd⁡x1st⁡x⋅𝑵2nd⁡x↔/𝑸⁡1𝑸=/𝑸⁡1st⁡x⋅𝑵2nd⁡x1st⁡x⋅𝑵2nd⁡x
48 45 46 47 sylancr ⊢x∈𝑸→1𝑸~𝑸1st⁡x⋅𝑵2nd⁡x1st⁡x⋅𝑵2nd⁡x↔/𝑸⁡1𝑸=/𝑸⁡1st⁡x⋅𝑵2nd⁡x1st⁡x⋅𝑵2nd⁡x
49 43 48 mpbid ⊢x∈𝑸→/𝑸⁡1𝑸=/𝑸⁡1st⁡x⋅𝑵2nd⁡x1st⁡x⋅𝑵2nd⁡x
50 nqerid ⊢1𝑸∈𝑸→/𝑸⁡1𝑸=1𝑸
51 6 50 ax-mp ⊢/𝑸⁡1𝑸=1𝑸
52 49 51 eqtr3di ⊢x∈𝑸→/𝑸⁡1st⁡x⋅𝑵2nd⁡x1st⁡x⋅𝑵2nd⁡x=1𝑸
53 29 39 52 3eqtrd ⊢x∈𝑸→x⋅𝑸/𝑸⁡2nd⁡x1st⁡x=1𝑸
54 fvex ⊢/𝑸⁡2nd⁡x1st⁡x∈V
55 oveq2 ⊢y=/𝑸⁡2nd⁡x1st⁡x→x⋅𝑸y=x⋅𝑸/𝑸⁡2nd⁡x1st⁡x
56 55 eqeq1d ⊢y=/𝑸⁡2nd⁡x1st⁡x→x⋅𝑸y=1𝑸↔x⋅𝑸/𝑸⁡2nd⁡x1st⁡x=1𝑸
57 54 56 spcev ⊢x⋅𝑸/𝑸⁡2nd⁡x1st⁡x=1𝑸→∃yx⋅𝑸y=1𝑸
58 53 57 syl ⊢x∈𝑸→∃yx⋅𝑸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 ⊢∃*yx⋅𝑸y=1𝑸
63 df-eu ⊢∃!yx⋅𝑸y=1𝑸↔∃yx⋅𝑸y=1𝑸∧∃*yx⋅𝑸y=1𝑸
64 58 62 63 sylanblrc ⊢x∈𝑸→∃!yx⋅𝑸y=1𝑸
65 cnvimass ⊢⋅𝑸-11𝑸⊆dom⁡⋅𝑸
66 df-rq ⊢*𝑸=⋅𝑸-11𝑸
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 ⊢xy∈*𝑸↔xy∈⋅𝑸-11𝑸
73 ffn ⊢⋅𝑸:𝑸×𝑸⟶𝑸→⋅𝑸Fn𝑸×𝑸
74 fniniseg ⊢⋅𝑸Fn𝑸×𝑸→xy∈⋅𝑸-11𝑸↔xy∈𝑸×𝑸∧⋅𝑸⁡xy=1𝑸
75 8 73 74 mp2b ⊢xy∈⋅𝑸-11𝑸↔xy∈𝑸×𝑸∧⋅𝑸⁡xy=1𝑸
76 ancom ⊢xy∈𝑸×𝑸∧⋅𝑸⁡xy=1𝑸↔⋅𝑸⁡xy=1𝑸∧xy∈𝑸×𝑸
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∈𝑸→xy∈𝑸×𝑸
83 81 82 syl ⊢x⋅𝑸y=1𝑸→xy∈𝑸×𝑸
84 81 simpld ⊢x⋅𝑸y=1𝑸→x∈𝑸
85 83 84 2thd ⊢x⋅𝑸y=1𝑸→xy∈𝑸×𝑸↔x∈𝑸
86 85 pm5.32i ⊢x⋅𝑸y=1𝑸∧xy∈𝑸×𝑸↔x⋅𝑸y=1𝑸∧x∈𝑸
87 df-ov ⊢x⋅𝑸y=⋅𝑸⁡xy
88 87 eqeq1i ⊢x⋅𝑸y=1𝑸↔⋅𝑸⁡xy=1𝑸
89 88 anbi1i ⊢x⋅𝑸y=1𝑸∧xy∈𝑸×𝑸↔⋅𝑸⁡xy=1𝑸∧xy∈𝑸×𝑸
90 77 86 89 3bitr2ri ⊢⋅𝑸⁡xy=1𝑸∧xy∈𝑸×𝑸↔x∈𝑸∧x⋅𝑸y=1𝑸
91 76 90 bitri ⊢xy∈𝑸×𝑸∧⋅𝑸⁡xy=1𝑸↔x∈𝑸∧x⋅𝑸y=1𝑸
92 72 75 91 3bitri ⊢xy∈*𝑸↔x∈𝑸∧x⋅𝑸y=1𝑸
93 92 a1i ⊢⊤→xy∈*𝑸↔x∈𝑸∧x⋅𝑸y=1𝑸
94 71 93 opabbi2dv ⊢⊤→*𝑸=xy|x∈𝑸∧x⋅𝑸y=1𝑸
95 94 mptru ⊢*𝑸=xy|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𝑸