# 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}\in {ℤ}_{\ge 2}\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right):{ℕ}_{0}×ℤ\underset{1-1 onto}{⟶}\left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}$

### Proof

Step Hyp Ref Expression
1 ovex ${⊢}{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\in \mathrm{V}$
2 eqid ${⊢}\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)=\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)$
3 1 2 fnmpti ${⊢}\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)Fn\left({ℕ}_{0}×ℤ\right)$
4 3 a1i ${⊢}{A}\in {ℤ}_{\ge 2}\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)Fn\left({ℕ}_{0}×ℤ\right)$
5 2 rnmpt ${⊢}\mathrm{ran}\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)=\left\{{a}|\exists {b}\in \left({ℕ}_{0}×ℤ\right)\phantom{\rule{.4em}{0ex}}{a}={1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right\}$
6 vex ${⊢}{c}\in \mathrm{V}$
7 vex ${⊢}{d}\in \mathrm{V}$
8 6 7 op1std ${⊢}{b}=⟨{c},{d}⟩\to {1}^{st}\left({b}\right)={c}$
9 6 7 op2ndd ${⊢}{b}=⟨{c},{d}⟩\to {2}^{nd}\left({b}\right)={d}$
10 9 oveq2d ${⊢}{b}=⟨{c},{d}⟩\to \sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)=\sqrt{{{A}}^{2}-1}{d}$
11 8 10 oveq12d ${⊢}{b}=⟨{c},{d}⟩\to {1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)={c}+\sqrt{{{A}}^{2}-1}{d}$
12 11 eqeq2d ${⊢}{b}=⟨{c},{d}⟩\to \left({a}={1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)↔{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right)$
13 12 rexxp ${⊢}\exists {b}\in \left({ℕ}_{0}×ℤ\right)\phantom{\rule{.4em}{0ex}}{a}={1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)↔\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}$
14 13 bicomi ${⊢}\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}↔\exists {b}\in \left({ℕ}_{0}×ℤ\right)\phantom{\rule{.4em}{0ex}}{a}={1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)$
15 14 a1i ${⊢}{A}\in {ℤ}_{\ge 2}\to \left(\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}↔\exists {b}\in \left({ℕ}_{0}×ℤ\right)\phantom{\rule{.4em}{0ex}}{a}={1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)$
16 15 abbidv ${⊢}{A}\in {ℤ}_{\ge 2}\to \left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}=\left\{{a}|\exists {b}\in \left({ℕ}_{0}×ℤ\right)\phantom{\rule{.4em}{0ex}}{a}={1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right\}$
17 5 16 eqtr4id ${⊢}{A}\in {ℤ}_{\ge 2}\to \mathrm{ran}\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)=\left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}$
18 fveq2 ${⊢}{b}={c}\to {1}^{st}\left({b}\right)={1}^{st}\left({c}\right)$
19 fveq2 ${⊢}{b}={c}\to {2}^{nd}\left({b}\right)={2}^{nd}\left({c}\right)$
20 19 oveq2d ${⊢}{b}={c}\to \sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)=\sqrt{{{A}}^{2}-1}{2}^{nd}\left({c}\right)$
21 18 20 oveq12d ${⊢}{b}={c}\to {1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)={1}^{st}\left({c}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({c}\right)$
22 ovex ${⊢}{1}^{st}\left({c}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({c}\right)\in \mathrm{V}$
23 21 2 22 fvmpt ${⊢}{c}\in \left({ℕ}_{0}×ℤ\right)\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\left({c}\right)={1}^{st}\left({c}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({c}\right)$
24 23 ad2antrl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\left({c}\right)={1}^{st}\left({c}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({c}\right)$
25 fveq2 ${⊢}{b}={d}\to {1}^{st}\left({b}\right)={1}^{st}\left({d}\right)$
26 fveq2 ${⊢}{b}={d}\to {2}^{nd}\left({b}\right)={2}^{nd}\left({d}\right)$
27 26 oveq2d ${⊢}{b}={d}\to \sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)=\sqrt{{{A}}^{2}-1}{2}^{nd}\left({d}\right)$
28 25 27 oveq12d ${⊢}{b}={d}\to {1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)={1}^{st}\left({d}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({d}\right)$
29 ovex ${⊢}{1}^{st}\left({d}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({d}\right)\in \mathrm{V}$
30 28 2 29 fvmpt ${⊢}{d}\in \left({ℕ}_{0}×ℤ\right)\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\left({d}\right)={1}^{st}\left({d}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({d}\right)$
31 30 ad2antll ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\left({d}\right)={1}^{st}\left({d}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({d}\right)$
32 24 31 eqeq12d ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to \left(\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\left({c}\right)=\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\left({d}\right)↔{1}^{st}\left({c}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({c}\right)={1}^{st}\left({d}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({d}\right)\right)$
33 rmspecsqrtnq ${⊢}{A}\in {ℤ}_{\ge 2}\to \sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)$
34 33 adantr ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to \sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)$
35 nn0ssq ${⊢}{ℕ}_{0}\subseteq ℚ$
36 xp1st ${⊢}{c}\in \left({ℕ}_{0}×ℤ\right)\to {1}^{st}\left({c}\right)\in {ℕ}_{0}$
37 36 ad2antrl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to {1}^{st}\left({c}\right)\in {ℕ}_{0}$
38 35 37 sseldi ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to {1}^{st}\left({c}\right)\in ℚ$
39 xp2nd ${⊢}{c}\in \left({ℕ}_{0}×ℤ\right)\to {2}^{nd}\left({c}\right)\in ℤ$
40 39 ad2antrl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to {2}^{nd}\left({c}\right)\in ℤ$
41 zq ${⊢}{2}^{nd}\left({c}\right)\in ℤ\to {2}^{nd}\left({c}\right)\in ℚ$
42 40 41 syl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to {2}^{nd}\left({c}\right)\in ℚ$
43 xp1st ${⊢}{d}\in \left({ℕ}_{0}×ℤ\right)\to {1}^{st}\left({d}\right)\in {ℕ}_{0}$
44 43 ad2antll ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to {1}^{st}\left({d}\right)\in {ℕ}_{0}$
45 35 44 sseldi ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to {1}^{st}\left({d}\right)\in ℚ$
46 xp2nd ${⊢}{d}\in \left({ℕ}_{0}×ℤ\right)\to {2}^{nd}\left({d}\right)\in ℤ$
47 46 ad2antll ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to {2}^{nd}\left({d}\right)\in ℤ$
48 zq ${⊢}{2}^{nd}\left({d}\right)\in ℤ\to {2}^{nd}\left({d}\right)\in ℚ$
49 47 48 syl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to {2}^{nd}\left({d}\right)\in ℚ$
50 qirropth ${⊢}\left(\sqrt{{{A}}^{2}-1}\in \left(ℂ\setminus ℚ\right)\wedge \left({1}^{st}\left({c}\right)\in ℚ\wedge {2}^{nd}\left({c}\right)\in ℚ\right)\wedge \left({1}^{st}\left({d}\right)\in ℚ\wedge {2}^{nd}\left({d}\right)\in ℚ\right)\right)\to \left({1}^{st}\left({c}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({c}\right)={1}^{st}\left({d}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({d}\right)↔\left({1}^{st}\left({c}\right)={1}^{st}\left({d}\right)\wedge {2}^{nd}\left({c}\right)={2}^{nd}\left({d}\right)\right)\right)$
51 34 38 42 45 49 50 syl122anc ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to \left({1}^{st}\left({c}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({c}\right)={1}^{st}\left({d}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({d}\right)↔\left({1}^{st}\left({c}\right)={1}^{st}\left({d}\right)\wedge {2}^{nd}\left({c}\right)={2}^{nd}\left({d}\right)\right)\right)$
52 51 biimpd ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to \left({1}^{st}\left({c}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({c}\right)={1}^{st}\left({d}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({d}\right)\to \left({1}^{st}\left({c}\right)={1}^{st}\left({d}\right)\wedge {2}^{nd}\left({c}\right)={2}^{nd}\left({d}\right)\right)\right)$
53 xpopth ${⊢}\left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\to \left(\left({1}^{st}\left({c}\right)={1}^{st}\left({d}\right)\wedge {2}^{nd}\left({c}\right)={2}^{nd}\left({d}\right)\right)↔{c}={d}\right)$
54 53 adantl ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to \left(\left({1}^{st}\left({c}\right)={1}^{st}\left({d}\right)\wedge {2}^{nd}\left({c}\right)={2}^{nd}\left({d}\right)\right)↔{c}={d}\right)$
55 52 54 sylibd ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to \left({1}^{st}\left({c}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({c}\right)={1}^{st}\left({d}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({d}\right)\to {c}={d}\right)$
56 32 55 sylbid ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge \left({c}\in \left({ℕ}_{0}×ℤ\right)\wedge {d}\in \left({ℕ}_{0}×ℤ\right)\right)\right)\to \left(\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\left({c}\right)=\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\left({d}\right)\to {c}={d}\right)$
57 56 ralrimivva ${⊢}{A}\in {ℤ}_{\ge 2}\to \forall {c}\in \left({ℕ}_{0}×ℤ\right)\phantom{\rule{.4em}{0ex}}\forall {d}\in \left({ℕ}_{0}×ℤ\right)\phantom{\rule{.4em}{0ex}}\left(\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\left({c}\right)=\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\left({d}\right)\to {c}={d}\right)$
58 dff1o6 ${⊢}\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right):{ℕ}_{0}×ℤ\underset{1-1 onto}{⟶}\left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}↔\left(\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)Fn\left({ℕ}_{0}×ℤ\right)\wedge \mathrm{ran}\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)=\left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}\wedge \forall {c}\in \left({ℕ}_{0}×ℤ\right)\phantom{\rule{.4em}{0ex}}\forall {d}\in \left({ℕ}_{0}×ℤ\right)\phantom{\rule{.4em}{0ex}}\left(\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\left({c}\right)=\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)\left({d}\right)\to {c}={d}\right)\right)$
59 4 17 57 58 syl3anbrc ${⊢}{A}\in {ℤ}_{\ge 2}\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right):{ℕ}_{0}×ℤ\underset{1-1 onto}{⟶}\left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}$