Metamath Proof Explorer


Theorem addnqf

Description: Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995) (Revised by Mario Carneiro, 10-Jul-2014) (New usage is discouraged.)

Ref Expression
Assertion addnqf + 𝑸 : 𝑸 × 𝑸 𝑸

Proof

Step Hyp Ref Expression
1 nqerf / 𝑸 : 𝑵 × 𝑵 𝑸
2 addpqf + 𝑝𝑸 : 𝑵 × 𝑵 × 𝑵 × 𝑵 𝑵 × 𝑵
3 fco / 𝑸 : 𝑵 × 𝑵 𝑸 + 𝑝𝑸 : 𝑵 × 𝑵 × 𝑵 × 𝑵 𝑵 × 𝑵 / 𝑸 + 𝑝𝑸 : 𝑵 × 𝑵 × 𝑵 × 𝑵 𝑸
4 1 2 3 mp2an / 𝑸 + 𝑝𝑸 : 𝑵 × 𝑵 × 𝑵 × 𝑵 𝑸
5 elpqn x 𝑸 x 𝑵 × 𝑵
6 5 ssriv 𝑸 𝑵 × 𝑵
7 xpss12 𝑸 𝑵 × 𝑵 𝑸 𝑵 × 𝑵 𝑸 × 𝑸 𝑵 × 𝑵 × 𝑵 × 𝑵
8 6 6 7 mp2an 𝑸 × 𝑸 𝑵 × 𝑵 × 𝑵 × 𝑵
9 fssres / 𝑸 + 𝑝𝑸 : 𝑵 × 𝑵 × 𝑵 × 𝑵 𝑸 𝑸 × 𝑸 𝑵 × 𝑵 × 𝑵 × 𝑵 / 𝑸 + 𝑝𝑸 𝑸 × 𝑸 : 𝑸 × 𝑸 𝑸
10 4 8 9 mp2an / 𝑸 + 𝑝𝑸 𝑸 × 𝑸 : 𝑸 × 𝑸 𝑸
11 df-plq + 𝑸 = / 𝑸 + 𝑝𝑸 𝑸 × 𝑸
12 11 feq1i + 𝑸 : 𝑸 × 𝑸 𝑸 / 𝑸 + 𝑝𝑸 𝑸 × 𝑸 : 𝑸 × 𝑸 𝑸
13 10 12 mpbir + 𝑸 : 𝑸 × 𝑸 𝑸