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 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 ) ) ) }
6 vex 
 |-  c e. _V
7 vex 
 |-  d e. _V
8 6 7 op1std 
 |-  ( b = <. c , d >. -> ( 1st ` b ) = c )
9 6 7 op2ndd 
 |-  ( b = <. c , d >. -> ( 2nd ` b ) = d )
10 9 oveq2d 
 |-  ( b = <. c , d >. -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) )
11 8 10 oveq12d 
 |-  ( b = <. c , d >. -> ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) )
12 11 eqeq2d 
 |-  ( b = <. c , d >. -> ( a = ( ( 1st ` b ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) <-> a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) ) )
13 12 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 ) ) )
14 13 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 ) ) ) )
15 14 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 ) ) ) ) )
16 15 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 ) ) ) } )
17 5 16 eqtr4id 
 |-  ( 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 sselid 
 |-  ( ( 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 sselid 
 |-  ( ( 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 ) ) } )