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
|
sseldi |
|- ( ( 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
|
sseldi |
|- ( ( ( 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
|
sseldi |
|- ( ( ( 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 ) ) ) ) |