Metamath Proof Explorer


Theorem rmxypairf1o

Description: The function used to extract rational and irrational parts in df-rmx and df-rmy in fact achieves a one-to-one mapping from the quadratic irrationals to pairs of integers. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion rmxypairf1o A 2 b 0 × 1 st b + A 2 1 2 nd b : 0 × 1-1 onto a | c 0 d a = c + A 2 1 d

Proof

Step Hyp Ref Expression
1 ovex 1 st b + A 2 1 2 nd b V
2 eqid b 0 × 1 st b + A 2 1 2 nd b = b 0 × 1 st b + A 2 1 2 nd b
3 1 2 fnmpti b 0 × 1 st b + A 2 1 2 nd b Fn 0 ×
4 3 a1i A 2 b 0 × 1 st b + A 2 1 2 nd b Fn 0 ×
5 vex c V
6 vex d V
7 5 6 op1std b = c d 1 st b = c
8 5 6 op2ndd b = c d 2 nd b = d
9 8 oveq2d b = c d A 2 1 2 nd b = A 2 1 d
10 7 9 oveq12d b = c d 1 st b + A 2 1 2 nd b = c + A 2 1 d
11 10 eqeq2d b = c d a = 1 st b + A 2 1 2 nd b a = c + A 2 1 d
12 11 rexxp b 0 × a = 1 st b + A 2 1 2 nd b c 0 d a = c + A 2 1 d
13 12 bicomi c 0 d a = c + A 2 1 d b 0 × a = 1 st b + A 2 1 2 nd b
14 13 a1i A 2 c 0 d a = c + A 2 1 d b 0 × a = 1 st b + A 2 1 2 nd b
15 14 abbidv A 2 a | c 0 d a = c + A 2 1 d = a | b 0 × a = 1 st b + A 2 1 2 nd b
16 2 rnmpt ran b 0 × 1 st b + A 2 1 2 nd b = a | b 0 × a = 1 st b + A 2 1 2 nd b
17 15 16 syl6reqr A 2 ran b 0 × 1 st b + A 2 1 2 nd b = a | c 0 d a = c + A 2 1 d
18 fveq2 b = c 1 st b = 1 st c
19 fveq2 b = c 2 nd b = 2 nd c
20 19 oveq2d b = c A 2 1 2 nd b = A 2 1 2 nd c
21 18 20 oveq12d b = c 1 st b + A 2 1 2 nd b = 1 st c + A 2 1 2 nd c
22 ovex 1 st c + A 2 1 2 nd c V
23 21 2 22 fvmpt c 0 × b 0 × 1 st b + A 2 1 2 nd b c = 1 st c + A 2 1 2 nd c
24 23 ad2antrl A 2 c 0 × d 0 × b 0 × 1 st b + A 2 1 2 nd b c = 1 st c + A 2 1 2 nd c
25 fveq2 b = d 1 st b = 1 st d
26 fveq2 b = d 2 nd b = 2 nd d
27 26 oveq2d b = d A 2 1 2 nd b = A 2 1 2 nd d
28 25 27 oveq12d b = d 1 st b + A 2 1 2 nd b = 1 st d + A 2 1 2 nd d
29 ovex 1 st d + A 2 1 2 nd d V
30 28 2 29 fvmpt d 0 × b 0 × 1 st b + A 2 1 2 nd b d = 1 st d + A 2 1 2 nd d
31 30 ad2antll A 2 c 0 × d 0 × b 0 × 1 st b + A 2 1 2 nd b d = 1 st d + A 2 1 2 nd d
32 24 31 eqeq12d A 2 c 0 × d 0 × b 0 × 1 st b + A 2 1 2 nd b c = b 0 × 1 st b + A 2 1 2 nd b d 1 st c + A 2 1 2 nd c = 1 st d + A 2 1 2 nd d
33 rmspecsqrtnq A 2 A 2 1
34 33 adantr A 2 c 0 × d 0 × A 2 1
35 nn0ssq 0
36 xp1st c 0 × 1 st c 0
37 36 ad2antrl A 2 c 0 × d 0 × 1 st c 0
38 35 37 sseldi A 2 c 0 × d 0 × 1 st c
39 xp2nd c 0 × 2 nd c
40 39 ad2antrl A 2 c 0 × d 0 × 2 nd c
41 zq 2 nd c 2 nd c
42 40 41 syl A 2 c 0 × d 0 × 2 nd c
43 xp1st d 0 × 1 st d 0
44 43 ad2antll A 2 c 0 × d 0 × 1 st d 0
45 35 44 sseldi A 2 c 0 × d 0 × 1 st d
46 xp2nd d 0 × 2 nd d
47 46 ad2antll A 2 c 0 × d 0 × 2 nd d
48 zq 2 nd d 2 nd d
49 47 48 syl A 2 c 0 × d 0 × 2 nd d
50 qirropth A 2 1 1 st c 2 nd c 1 st d 2 nd d 1 st c + A 2 1 2 nd c = 1 st d + A 2 1 2 nd d 1 st c = 1 st d 2 nd c = 2 nd d
51 34 38 42 45 49 50 syl122anc A 2 c 0 × d 0 × 1 st c + A 2 1 2 nd c = 1 st d + A 2 1 2 nd d 1 st c = 1 st d 2 nd c = 2 nd d
52 51 biimpd A 2 c 0 × d 0 × 1 st c + A 2 1 2 nd c = 1 st d + A 2 1 2 nd d 1 st c = 1 st d 2 nd c = 2 nd d
53 xpopth c 0 × d 0 × 1 st c = 1 st d 2 nd c = 2 nd d c = d
54 53 adantl A 2 c 0 × d 0 × 1 st c = 1 st d 2 nd c = 2 nd d c = d
55 52 54 sylibd A 2 c 0 × d 0 × 1 st c + A 2 1 2 nd c = 1 st d + A 2 1 2 nd d c = d
56 32 55 sylbid A 2 c 0 × d 0 × b 0 × 1 st b + A 2 1 2 nd b c = b 0 × 1 st b + A 2 1 2 nd b d c = d
57 56 ralrimivva A 2 c 0 × d 0 × b 0 × 1 st b + A 2 1 2 nd b c = b 0 × 1 st b + A 2 1 2 nd b d c = d
58 dff1o6 b 0 × 1 st b + A 2 1 2 nd b : 0 × 1-1 onto a | c 0 d a = c + A 2 1 d b 0 × 1 st b + A 2 1 2 nd b Fn 0 × ran b 0 × 1 st b + A 2 1 2 nd b = a | c 0 d a = c + A 2 1 d c 0 × d 0 × b 0 × 1 st b + A 2 1 2 nd b c = b 0 × 1 st b + A 2 1 2 nd b d c = d
59 4 17 57 58 syl3anbrc A 2 b 0 × 1 st b + A 2 1 2 nd b : 0 × 1-1 onto a | c 0 d a = c + A 2 1 d