Metamath Proof Explorer

Theorem rmxycomplete

Description: The X and Y sequences taken together enumerate all solutions to the corresponding Pell equation in the right half-plane. This is Metamath 100 proof #39. (Contributed by Stefan O'Rear, 22-Sep-2014)

Ref Expression
Assertion rmxycomplete 
|- ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 <-> E. n e. ZZ ( X = ( A rmX n ) /\ Y = ( A rmY n ) ) ) )

Proof

Step Hyp Ref Expression
1 rmspecnonsq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )
2 1 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )
3 pellfund14b 
 |-  ( ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) -> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) e. ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) <-> E. n e. ZZ ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ n ) ) )
4 2 3 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) e. ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) <-> E. n e. ZZ ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ n ) ) )
5 nn0re 
 |-  ( X e. NN0 -> X e. RR )
6 5 3ad2ant2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> X e. RR )
7 rmspecpos 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. RR+ )
8 7 rpsqrtcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. RR+ )
9 8 rpred 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. RR )
10 9 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. RR )
11 zre 
 |-  ( Y e. ZZ -> Y e. RR )
12 11 3ad2ant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> Y e. RR )
13 10 12 remulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) e. RR )
14 6 13 readdcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) e. RR )
15 14 biantrurd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( E. x e. NN0 E. y e. ZZ ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) <-> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) e. RR /\ E. x e. NN0 E. y e. ZZ ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) ) ) )
16 simpl2 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 ) -> X e. NN0 )
17 simpl3 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 ) -> Y e. ZZ )
18 eqidd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 ) -> ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) )
19 simpr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 ) -> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 )
20 oveq1 
 |-  ( x = X -> ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) = ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) )
21 20 eqeq2d 
 |-  ( x = X -> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) <-> ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) ) )
22 oveq1 
 |-  ( x = X -> ( x ^ 2 ) = ( X ^ 2 ) )
23 22 oveq1d 
 |-  ( x = X -> ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) )
24 23 eqeq1d 
 |-  ( x = X -> ( ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 <-> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) )
25 21 24 anbi12d 
 |-  ( x = X -> ( ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) <-> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) ) )
26 oveq2 
 |-  ( y = Y -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) )
27 26 oveq2d 
 |-  ( y = Y -> ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) = ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) )
28 27 eqeq2d 
 |-  ( y = Y -> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) <-> ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) ) )
29 oveq1 
 |-  ( y = Y -> ( y ^ 2 ) = ( Y ^ 2 ) )
30 29 oveq2d 
 |-  ( y = Y -> ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) = ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) )
31 30 oveq2d 
 |-  ( y = Y -> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) )
32 31 eqeq1d 
 |-  ( y = Y -> ( ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 <-> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 ) )
33 28 32 anbi12d 
 |-  ( y = Y -> ( ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) <-> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 ) ) )
34 25 33 rspc2ev 
 |-  ( ( X e. NN0 /\ Y e. ZZ /\ ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 ) ) -> E. x e. NN0 E. y e. ZZ ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) )
35 16 17 18 19 34 syl112anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 ) -> E. x e. NN0 E. y e. ZZ ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) )
36 35 ex 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 -> E. x e. NN0 E. y e. ZZ ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) ) )
37 rmspecsqrtnq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
38 37 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
39 38 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( x e. NN0 /\ y e. ZZ ) ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
40 nn0ssq 
 |-  NN0 C_ QQ
41 simp2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> X e. NN0 )
42 40 41 sselid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> X e. QQ )
43 42 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( x e. NN0 /\ y e. ZZ ) ) -> X e. QQ )
44 zq 
 |-  ( Y e. ZZ -> Y e. QQ )
45 44 3ad2ant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> Y e. QQ )
46 45 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( x e. NN0 /\ y e. ZZ ) ) -> Y e. QQ )
47 40 sseli 
 |-  ( x e. NN0 -> x e. QQ )
48 47 ad2antrl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( x e. NN0 /\ y e. ZZ ) ) -> x e. QQ )
49 zq 
 |-  ( y e. ZZ -> y e. QQ )
50 49 ad2antll 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( x e. NN0 /\ y e. ZZ ) ) -> y e. QQ )
51 qirropth 
 |-  ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) /\ ( X e. QQ /\ Y e. QQ ) /\ ( x e. QQ /\ y e. QQ ) ) -> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) <-> ( X = x /\ Y = y ) ) )
52 39 43 46 48 50 51 syl122anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( x e. NN0 /\ y e. ZZ ) ) -> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) <-> ( X = x /\ Y = y ) ) )
53 52 biimpd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( x e. NN0 /\ y e. ZZ ) ) -> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) -> ( X = x /\ Y = y ) ) )
54 53 anim1d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( x e. NN0 /\ y e. ZZ ) ) -> ( ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) -> ( ( X = x /\ Y = y ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) ) )
55 oveq1 
 |-  ( X = x -> ( X ^ 2 ) = ( x ^ 2 ) )
56 oveq1 
 |-  ( Y = y -> ( Y ^ 2 ) = ( y ^ 2 ) )
57 56 oveq2d 
 |-  ( Y = y -> ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) = ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) )
58 55 57 oveqan12d 
 |-  ( ( X = x /\ Y = y ) -> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) )
59 58 eqcomd 
 |-  ( ( X = x /\ Y = y ) -> ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) )
60 59 eqeq1d 
 |-  ( ( X = x /\ Y = y ) -> ( ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 <-> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 ) )
61 60 biimpa 
 |-  ( ( ( X = x /\ Y = y ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) -> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 )
62 54 61 syl6 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ ( x e. NN0 /\ y e. ZZ ) ) -> ( ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) -> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 ) )
63 62 rexlimdvva 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( E. x e. NN0 E. y e. ZZ ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) -> ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 ) )
64 36 63 impbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 <-> E. x e. NN0 E. y e. ZZ ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) ) )
65 elpell14qr 
 |-  ( ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) -> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) e. ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) <-> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) e. RR /\ E. x e. NN0 E. y e. ZZ ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) ) ) )
66 2 65 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) e. ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) <-> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) e. RR /\ E. x e. NN0 E. y e. ZZ ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( x + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. y ) ) /\ ( ( x ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) ) ) )
67 15 64 66 3bitr4d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 <-> ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) e. ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) ) )
68 38 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
69 42 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> X e. QQ )
70 45 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> Y e. QQ )
71 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
72 71 a1i 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0 )
73 simpl1 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> A e. ( ZZ>= ` 2 ) )
74 simpr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> n e. ZZ )
75 72 73 74 fovrnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> ( A rmX n ) e. NN0 )
76 40 75 sselid 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> ( A rmX n ) e. QQ )
77 zssq 
 |-  ZZ C_ QQ
78 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
79 78 a1i 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ )
80 79 73 74 fovrnd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> ( A rmY n ) e. ZZ )
81 77 80 sselid 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> ( A rmY n ) e. QQ )
82 qirropth 
 |-  ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) /\ ( X e. QQ /\ Y e. QQ ) /\ ( ( A rmX n ) e. QQ /\ ( A rmY n ) e. QQ ) ) -> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( ( A rmX n ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY n ) ) ) <-> ( X = ( A rmX n ) /\ Y = ( A rmY n ) ) ) )
83 68 69 70 76 81 82 syl122anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( ( A rmX n ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY n ) ) ) <-> ( X = ( A rmX n ) /\ Y = ( A rmY n ) ) ) )
84 rmxyval 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ n e. ZZ ) -> ( ( A rmX n ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY n ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ n ) )
85 84 3ad2antl1 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> ( ( A rmX n ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY n ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ n ) )
86 rmspecfund 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
87 86 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
88 87 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
89 88 oveq1d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ n ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ n ) )
90 85 89 eqtr4d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> ( ( A rmX n ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY n ) ) ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ n ) )
91 90 eqeq2d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> ( ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( ( A rmX n ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY n ) ) ) <-> ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ n ) ) )
92 83 91 bitr3d 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) /\ n e. ZZ ) -> ( ( X = ( A rmX n ) /\ Y = ( A rmY n ) ) <-> ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ n ) ) )
93 92 rexbidva 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( E. n e. ZZ ( X = ( A rmX n ) /\ Y = ( A rmY n ) ) <-> E. n e. ZZ ( X + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. Y ) ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ n ) ) )
94 4 67 93 3bitr4d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 <-> E. n e. ZZ ( X = ( A rmX n ) /\ Y = ( A rmY n ) ) ) )