Metamath Proof Explorer

Theorem pellfund14

Description: Every positive Pell solution is a power of the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014)

Ref Expression
Assertion pellfund14 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> E. x e. ZZ A = ( ( PellFund ` D ) ^ x ) )

Proof

Step Hyp Ref Expression
1 pell14qrrp 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. RR+ )
2 pellfundrp 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. RR+ )
3 2 adantr 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( PellFund ` D ) e. RR+ )
4 pellfundne1 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) =/= 1 )
5 4 adantr 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( PellFund ` D ) =/= 1 )
6 reglogcl 
 |-  ( ( A e. RR+ /\ ( PellFund ` D ) e. RR+ /\ ( PellFund ` D ) =/= 1 ) -> ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) e. RR )
7 1 3 5 6 syl3anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) e. RR )
8 7 flcld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) e. ZZ )
9 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. RR )
10 9 recnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. CC )
11 3 8 rpexpcld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( PellFund ` D ) ^ ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) e. RR+ )
12 11 rpcnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( PellFund ` D ) ^ ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) e. CC )
13 8 znegcld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) e. ZZ )
14 3 13 rpexpcld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) e. RR+ )
15 14 rpcnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) e. CC )
16 14 rpne0d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) =/= 0 )
17 simpl 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> D e. ( NN \ []NN ) )
18 pell1qrss14 
 |-  ( D e. ( NN \ []NN ) -> ( Pell1QR ` D ) C_ ( Pell14QR ` D ) )
19 pellfundex 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. ( Pell1QR ` D ) )
20 18 19 sseldd 
 |-  ( D e. ( NN \ []NN ) -> ( PellFund ` D ) e. ( Pell14QR ` D ) )
21 20 adantr 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( PellFund ` D ) e. ( Pell14QR ` D ) )
22 pell14qrexpcl 
 |-  ( ( D e. ( NN \ []NN ) /\ ( PellFund ` D ) e. ( Pell14QR ` D ) /\ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) e. ZZ ) -> ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) e. ( Pell14QR ` D ) )
23 17 21 13 22 syl3anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) e. ( Pell14QR ` D ) )
24 pell14qrmulcl 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) e. ( Pell14QR ` D ) ) -> ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) e. ( Pell14QR ` D ) )
25 23 24 mpd3an3 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) e. ( Pell14QR ` D ) )
26 1rp 
 |-  1 e. RR+
27 26 a1i 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> 1 e. RR+ )
28 modge0 
 |-  ( ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) e. RR /\ 1 e. RR+ ) -> 0 <_ ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) mod 1 ) )
29 7 27 28 syl2anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> 0 <_ ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) mod 1 ) )
30 7 recnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) e. CC )
31 8 zcnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) e. CC )
32 30 31 negsubd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) + -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) = ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) - ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) )
33 modfrac 
 |-  ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) e. RR -> ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) mod 1 ) = ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) - ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) )
34 7 33 syl 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) mod 1 ) = ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) - ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) )
35 32 34 eqtr4d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) + -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) = ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) mod 1 ) )
36 29 35 breqtrrd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> 0 <_ ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) + -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) )
37 reglog1 
 |-  ( ( ( PellFund ` D ) e. RR+ /\ ( PellFund ` D ) =/= 1 ) -> ( ( log ` 1 ) / ( log ` ( PellFund ` D ) ) ) = 0 )
38 3 5 37 syl2anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( log ` 1 ) / ( log ` ( PellFund ` D ) ) ) = 0 )
39 reglogmul 
 |-  ( ( A e. RR+ /\ ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) e. RR+ /\ ( ( PellFund ` D ) e. RR+ /\ ( PellFund ` D ) =/= 1 ) ) -> ( ( log ` ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) = ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) + ( ( log ` ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) ) )
40 1 14 3 5 39 syl112anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( log ` ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) = ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) + ( ( log ` ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) ) )
41 reglogexpbas 
 |-  ( ( -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) e. ZZ /\ ( ( PellFund ` D ) e. RR+ /\ ( PellFund ` D ) =/= 1 ) ) -> ( ( log ` ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) = -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) )
42 13 3 5 41 syl12anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( log ` ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) = -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) )
43 42 oveq2d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) + ( ( log ` ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) ) = ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) + -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) )
44 40 43 eqtrd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( log ` ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) = ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) + -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) )
45 36 38 44 3brtr4d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( log ` 1 ) / ( log ` ( PellFund ` D ) ) ) <_ ( ( log ` ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) )
46 1 14 rpmulcld 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) e. RR+ )
47 pellfundgt1 
 |-  ( D e. ( NN \ []NN ) -> 1 < ( PellFund ` D ) )
48 47 adantr 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> 1 < ( PellFund ` D ) )
49 reglogleb 
 |-  ( ( ( 1 e. RR+ /\ ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) e. RR+ ) /\ ( ( PellFund ` D ) e. RR+ /\ 1 < ( PellFund ` D ) ) ) -> ( 1 <_ ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) <-> ( ( log ` 1 ) / ( log ` ( PellFund ` D ) ) ) <_ ( ( log ` ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) ) )
50 27 46 3 48 49 syl22anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( 1 <_ ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) <-> ( ( log ` 1 ) / ( log ` ( PellFund ` D ) ) ) <_ ( ( log ` ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) ) )
51 45 50 mpbird 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> 1 <_ ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) )
52 modlt 
 |-  ( ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) e. RR /\ 1 e. RR+ ) -> ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) mod 1 ) < 1 )
53 7 27 52 syl2anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) mod 1 ) < 1 )
54 35 53 eqbrtrd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) + -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) < 1 )
55 reglogbas 
 |-  ( ( ( PellFund ` D ) e. RR+ /\ ( PellFund ` D ) =/= 1 ) -> ( ( log ` ( PellFund ` D ) ) / ( log ` ( PellFund ` D ) ) ) = 1 )
56 3 5 55 syl2anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( log ` ( PellFund ` D ) ) / ( log ` ( PellFund ` D ) ) ) = 1 )
57 54 44 56 3brtr4d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( log ` ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) < ( ( log ` ( PellFund ` D ) ) / ( log ` ( PellFund ` D ) ) ) )
58 reglogltb 
 |-  ( ( ( ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) e. RR+ /\ ( PellFund ` D ) e. RR+ ) /\ ( ( PellFund ` D ) e. RR+ /\ 1 < ( PellFund ` D ) ) ) -> ( ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) < ( PellFund ` D ) <-> ( ( log ` ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) < ( ( log ` ( PellFund ` D ) ) / ( log ` ( PellFund ` D ) ) ) ) )
59 46 3 3 48 58 syl22anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) < ( PellFund ` D ) <-> ( ( log ` ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) ) / ( log ` ( PellFund ` D ) ) ) < ( ( log ` ( PellFund ` D ) ) / ( log ` ( PellFund ` D ) ) ) ) )
60 57 59 mpbird 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) < ( PellFund ` D ) )
61 pellfund14gap 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) e. ( Pell14QR ` D ) /\ ( 1 <_ ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) /\ ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) < ( PellFund ` D ) ) ) -> ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) = 1 )
62 17 25 51 60 61 syl112anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) = 1 )
63 31 negidd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) + -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) = 0 )
64 63 oveq2d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( PellFund ` D ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) + -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) = ( ( PellFund ` D ) ^ 0 ) )
65 3 rpcnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( PellFund ` D ) e. CC )
66 3 rpne0d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( PellFund ` D ) =/= 0 )
67 expaddz 
 |-  ( ( ( ( PellFund ` D ) e. CC /\ ( PellFund ` D ) =/= 0 ) /\ ( ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) e. ZZ /\ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) e. ZZ ) ) -> ( ( PellFund ` D ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) + -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) = ( ( ( PellFund ` D ) ^ ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) )
68 65 66 8 13 67 syl22anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( PellFund ` D ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) + -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) = ( ( ( PellFund ` D ) ^ ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) )
69 65 exp0d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( PellFund ` D ) ^ 0 ) = 1 )
70 64 68 69 3eqtr3rd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> 1 = ( ( ( PellFund ` D ) ^ ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) )
71 62 70 eqtrd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) = ( ( ( PellFund ` D ) ^ ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) x. ( ( PellFund ` D ) ^ -u ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) )
72 10 12 15 16 71 mulcan2ad 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A = ( ( PellFund ` D ) ^ ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) )
73 oveq2 
 |-  ( x = ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) -> ( ( PellFund ` D ) ^ x ) = ( ( PellFund ` D ) ^ ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) )
74 73 rspceeqv 
 |-  ( ( ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) e. ZZ /\ A = ( ( PellFund ` D ) ^ ( |_ ` ( ( log ` A ) / ( log ` ( PellFund ` D ) ) ) ) ) ) -> E. x e. ZZ A = ( ( PellFund ` D ) ^ x ) )
75 8 72 74 syl2anc 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> E. x e. ZZ A = ( ( PellFund ` D ) ^ x ) )