# 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 e. ( ZZ>= ` 2 ) -> ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) : ( NN0 X. ZZ ) -1-1-onto-> { a | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } )`

### Proof

Step Hyp Ref Expression
1 ovex
` |-  ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) e. _V`
2 eqid
` |-  ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) = ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) )`
3 1 2 fnmpti
` |-  ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) Fn ( NN0 X. ZZ )`
4 3 a1i
` |-  ( A e. ( ZZ>= ` 2 ) -> ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) Fn ( NN0 X. ZZ ) )`
5 vex
` |-  c e. _V`
6 vex
` |-  d e. _V`
7 5 6 op1std
` |-  ( b = <. c , d >. -> ( 1st ` b ) = c )`
8 5 6 op2ndd
` |-  ( b = <. c , d >. -> ( 2nd ` b ) = d )`
9 8 oveq2d
` |-  ( b = <. c , d >. -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) )`
10 7 9 oveq12d
` |-  ( b = <. c , d >. -> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) )`
11 10 eqeq2d
` |-  ( b = <. c , d >. -> ( a = ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) <-> a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) ) )`
12 11 rexxp
` |-  ( E. b e. ( NN0 X. ZZ ) a = ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) <-> E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) )`
13 12 bicomi
` |-  ( E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) <-> E. b e. ( NN0 X. ZZ ) a = ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) )`
14 13 a1i
` |-  ( A e. ( ZZ>= ` 2 ) -> ( E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) <-> E. b e. ( NN0 X. ZZ ) a = ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) )`
15 14 abbidv
` |-  ( A e. ( ZZ>= ` 2 ) -> { a | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } = { a | E. b e. ( NN0 X. ZZ ) a = ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) } )`
16 2 rnmpt
` |-  ran ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) = { a | E. b e. ( NN0 X. ZZ ) a = ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) }`
17 15 16 syl6reqr
` |-  ( A e. ( ZZ>= ` 2 ) -> ran ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) = { a | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } )`
18 fveq2
` |-  ( b = c -> ( 1st ` b ) = ( 1st ` c ) )`
19 fveq2
` |-  ( b = c -> ( 2nd ` b ) = ( 2nd ` c ) )`
20 19 oveq2d
` |-  ( b = c -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) )`
21 18 20 oveq12d
` |-  ( b = c -> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) = ( ( 1st ` c ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) )`
22 ovex
` |-  ( ( 1st ` c ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) e. _V`
23 21 2 22 fvmpt
` |-  ( c e. ( NN0 X. ZZ ) -> ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` c ) = ( ( 1st ` c ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` c ) = ( ( 1st ` c ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) )`
25 fveq2
` |-  ( b = d -> ( 1st ` b ) = ( 1st ` d ) )`
26 fveq2
` |-  ( b = d -> ( 2nd ` b ) = ( 2nd ` d ) )`
27 26 oveq2d
` |-  ( b = d -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` d ) ) )`
28 25 27 oveq12d
` |-  ( b = d -> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) = ( ( 1st ` d ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` d ) ) ) )`
29 ovex
` |-  ( ( 1st ` d ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` d ) ) ) e. _V`
30 28 2 29 fvmpt
` |-  ( d e. ( NN0 X. ZZ ) -> ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` d ) = ( ( 1st ` d ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` d ) ) ) )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` d ) = ( ( 1st ` d ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` d ) ) ) )`
32 24 31 eqeq12d
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` c ) = ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` d ) <-> ( ( 1st ` c ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) = ( ( 1st ` d ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` d ) ) ) ) )`
33 rmspecsqrtnq
` |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )`
35 nn0ssq
` |-  NN0 C_ QQ`
36 xp1st
` |-  ( c e. ( NN0 X. ZZ ) -> ( 1st ` c ) e. NN0 )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( 1st ` c ) e. NN0 )`
38 35 37 sseldi
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( 1st ` c ) e. QQ )`
39 xp2nd
` |-  ( c e. ( NN0 X. ZZ ) -> ( 2nd ` c ) e. ZZ )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( 2nd ` c ) e. ZZ )`
41 zq
` |-  ( ( 2nd ` c ) e. ZZ -> ( 2nd ` c ) e. QQ )`
42 40 41 syl
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( 2nd ` c ) e. QQ )`
43 xp1st
` |-  ( d e. ( NN0 X. ZZ ) -> ( 1st ` d ) e. NN0 )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( 1st ` d ) e. NN0 )`
45 35 44 sseldi
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( 1st ` d ) e. QQ )`
46 xp2nd
` |-  ( d e. ( NN0 X. ZZ ) -> ( 2nd ` d ) e. ZZ )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( 2nd ` d ) e. ZZ )`
48 zq
` |-  ( ( 2nd ` d ) e. ZZ -> ( 2nd ` d ) e. QQ )`
49 47 48 syl
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( 2nd ` d ) e. QQ )`
50 qirropth
` |-  ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) /\ ( ( 1st ` c ) e. QQ /\ ( 2nd ` c ) e. QQ ) /\ ( ( 1st ` d ) e. QQ /\ ( 2nd ` d ) e. QQ ) ) -> ( ( ( 1st ` c ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) = ( ( 1st ` d ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` d ) ) ) <-> ( ( 1st ` c ) = ( 1st ` d ) /\ ( 2nd ` c ) = ( 2nd ` d ) ) ) )`
51 34 38 42 45 49 50 syl122anc
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( ( ( 1st ` c ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) = ( ( 1st ` d ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` d ) ) ) <-> ( ( 1st ` c ) = ( 1st ` d ) /\ ( 2nd ` c ) = ( 2nd ` d ) ) ) )`
52 51 biimpd
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( ( ( 1st ` c ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) = ( ( 1st ` d ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` d ) ) ) -> ( ( 1st ` c ) = ( 1st ` d ) /\ ( 2nd ` c ) = ( 2nd ` d ) ) ) )`
53 xpopth
` |-  ( ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) -> ( ( ( 1st ` c ) = ( 1st ` d ) /\ ( 2nd ` c ) = ( 2nd ` d ) ) <-> c = d ) )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( ( ( 1st ` c ) = ( 1st ` d ) /\ ( 2nd ` c ) = ( 2nd ` d ) ) <-> c = d ) )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( ( ( 1st ` c ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) = ( ( 1st ` d ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` d ) ) ) -> c = d ) )`
` |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` c ) = ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` d ) -> c = d ) )`
` |-  ( A e. ( ZZ>= ` 2 ) -> A. c e. ( NN0 X. ZZ ) A. d e. ( NN0 X. ZZ ) ( ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` c ) = ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` d ) -> c = d ) )`
` |-  ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) : ( NN0 X. ZZ ) -1-1-onto-> { a | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } <-> ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) Fn ( NN0 X. ZZ ) /\ ran ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) = { a | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } /\ A. c e. ( NN0 X. ZZ ) A. d e. ( NN0 X. ZZ ) ( ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` c ) = ( ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` d ) -> c = d ) ) )`
` |-  ( A e. ( ZZ>= ` 2 ) -> ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) : ( NN0 X. ZZ ) -1-1-onto-> { a | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } )`