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 ) ) ) )
24 23 ad2antrl
 |-  ( ( 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 ) ) ) )
31 30 ad2antll
 |-  ( ( 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 ) )
34 33 adantr
 |-  ( ( 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 )
37 36 ad2antrl
 |-  ( ( 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 )
40 39 ad2antrl
 |-  ( ( 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 )
44 43 ad2antll
 |-  ( ( 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 )
47 46 ad2antll
 |-  ( ( 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 ) )
54 53 adantl
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( c e. ( NN0 X. ZZ ) /\ d e. ( NN0 X. ZZ ) ) ) -> ( ( ( 1st ` c ) = ( 1st ` d ) /\ ( 2nd ` c ) = ( 2nd ` d ) ) <-> c = d ) )
55 52 54 sylibd
 |-  ( ( 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 ) )
56 32 55 sylbid
 |-  ( ( 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 ) )
57 56 ralrimivva
 |-  ( 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 ) )
58 dff1o6
 |-  ( ( 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 ) ) )
59 4 17 57 58 syl3anbrc
 |-  ( 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 ) ) } )