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∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→∃x∈ℤA=PellFund⁡Dx

Proof

Step Hyp Ref Expression
1 pell14qrrp ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→A∈ℝ+
2 pellfundrp ⊢D∈ℕ∖◻ℕ→PellFund⁡D∈ℝ+
3 2 adantr ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡D∈ℝ+
4 pellfundne1 ⊢D∈ℕ∖◻ℕ→PellFund⁡D≠1
5 4 adantr ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡D≠1
6 reglogcl ⊢A∈ℝ+∧PellFund⁡D∈ℝ+∧PellFund⁡D≠1→log⁡Alog⁡PellFund⁡D∈ℝ
7 1 3 5 6 syl3anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡Alog⁡PellFund⁡D∈ℝ
8 7 flcld ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡Alog⁡PellFund⁡D∈ℤ
9 pell14qrre ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→A∈ℝ
10 9 recnd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→A∈ℂ
11 3 8 rpexpcld ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡Dlog⁡Alog⁡PellFund⁡D∈ℝ+
12 11 rpcnd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡Dlog⁡Alog⁡PellFund⁡D∈ℂ
13 8 znegcld ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→−log⁡Alog⁡PellFund⁡D∈ℤ
14 3 13 rpexpcld ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡D−log⁡Alog⁡PellFund⁡D∈ℝ+
15 14 rpcnd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡D−log⁡Alog⁡PellFund⁡D∈ℂ
16 14 rpne0d ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡D−log⁡Alog⁡PellFund⁡D≠0
17 simpl ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→D∈ℕ∖◻ℕ
18 pell1qrss14 ⊢D∈ℕ∖◻ℕ→Pell1QR⁡D⊆Pell14QR⁡D
19 pellfundex ⊢D∈ℕ∖◻ℕ→PellFund⁡D∈Pell1QR⁡D
20 18 19 sseldd ⊢D∈ℕ∖◻ℕ→PellFund⁡D∈Pell14QR⁡D
21 20 adantr ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡D∈Pell14QR⁡D
22 pell14qrexpcl ⊢D∈ℕ∖◻ℕ∧PellFund⁡D∈Pell14QR⁡D∧−log⁡Alog⁡PellFund⁡D∈ℤ→PellFund⁡D−log⁡Alog⁡PellFund⁡D∈Pell14QR⁡D
23 17 21 13 22 syl3anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡D−log⁡Alog⁡PellFund⁡D∈Pell14QR⁡D
24 pell14qrmulcl ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧PellFund⁡D−log⁡Alog⁡PellFund⁡D∈Pell14QR⁡D→A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D∈Pell14QR⁡D
25 23 24 mpd3an3 ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D∈Pell14QR⁡D
26 1rp ⊢1∈ℝ+
27 26 a1i ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→1∈ℝ+
28 modge0 ⊢log⁡Alog⁡PellFund⁡D∈ℝ∧1∈ℝ+→0≤log⁡Alog⁡PellFund⁡Dmod1
29 7 27 28 syl2anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→0≤log⁡Alog⁡PellFund⁡Dmod1
30 7 recnd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡Alog⁡PellFund⁡D∈ℂ
31 8 zcnd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡Alog⁡PellFund⁡D∈ℂ
32 30 31 negsubd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡Alog⁡PellFund⁡D+−log⁡Alog⁡PellFund⁡D=log⁡Alog⁡PellFund⁡D−log⁡Alog⁡PellFund⁡D
33 modfrac ⊢log⁡Alog⁡PellFund⁡D∈ℝ→log⁡Alog⁡PellFund⁡Dmod1=log⁡Alog⁡PellFund⁡D−log⁡Alog⁡PellFund⁡D
34 7 33 syl ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡Alog⁡PellFund⁡Dmod1=log⁡Alog⁡PellFund⁡D−log⁡Alog⁡PellFund⁡D
35 32 34 eqtr4d ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡Alog⁡PellFund⁡D+−log⁡Alog⁡PellFund⁡D=log⁡Alog⁡PellFund⁡Dmod1
36 29 35 breqtrrd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→0≤log⁡Alog⁡PellFund⁡D+−log⁡Alog⁡PellFund⁡D
37 reglog1 ⊢PellFund⁡D∈ℝ+∧PellFund⁡D≠1→log⁡1log⁡PellFund⁡D=0
38 3 5 37 syl2anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡1log⁡PellFund⁡D=0
39 reglogmul ⊢A∈ℝ+∧PellFund⁡D−log⁡Alog⁡PellFund⁡D∈ℝ+∧PellFund⁡D∈ℝ+∧PellFund⁡D≠1→log⁡A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D=log⁡Alog⁡PellFund⁡D+log⁡PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D
40 1 14 3 5 39 syl112anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D=log⁡Alog⁡PellFund⁡D+log⁡PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D
41 reglogexpbas ⊢−log⁡Alog⁡PellFund⁡D∈ℤ∧PellFund⁡D∈ℝ+∧PellFund⁡D≠1→log⁡PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D=−log⁡Alog⁡PellFund⁡D
42 13 3 5 41 syl12anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D=−log⁡Alog⁡PellFund⁡D
43 42 oveq2d ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡Alog⁡PellFund⁡D+log⁡PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D=log⁡Alog⁡PellFund⁡D+−log⁡Alog⁡PellFund⁡D
44 40 43 eqtrd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D=log⁡Alog⁡PellFund⁡D+−log⁡Alog⁡PellFund⁡D
45 36 38 44 3brtr4d ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡1log⁡PellFund⁡D≤log⁡A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D
46 1 14 rpmulcld ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D∈ℝ+
47 pellfundgt1 ⊢D∈ℕ∖◻ℕ→1<PellFund⁡D
48 47 adantr ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→1<PellFund⁡D
49 reglogleb ⊢1∈ℝ+∧A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D∈ℝ+∧PellFund⁡D∈ℝ+∧1<PellFund⁡D→1≤A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D↔log⁡1log⁡PellFund⁡D≤log⁡A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D
50 27 46 3 48 49 syl22anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→1≤A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D↔log⁡1log⁡PellFund⁡D≤log⁡A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D
51 45 50 mpbird ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→1≤A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D
52 modlt ⊢log⁡Alog⁡PellFund⁡D∈ℝ∧1∈ℝ+→log⁡Alog⁡PellFund⁡Dmod1<1
53 7 27 52 syl2anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡Alog⁡PellFund⁡Dmod1<1
54 35 53 eqbrtrd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡Alog⁡PellFund⁡D+−log⁡Alog⁡PellFund⁡D<1
55 reglogbas ⊢PellFund⁡D∈ℝ+∧PellFund⁡D≠1→log⁡PellFund⁡Dlog⁡PellFund⁡D=1
56 3 5 55 syl2anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡PellFund⁡Dlog⁡PellFund⁡D=1
57 54 44 56 3brtr4d ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D<log⁡PellFund⁡Dlog⁡PellFund⁡D
58 reglogltb ⊢A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D∈ℝ+∧PellFund⁡D∈ℝ+∧PellFund⁡D∈ℝ+∧1<PellFund⁡D→A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D<PellFund⁡D↔log⁡A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D<log⁡PellFund⁡Dlog⁡PellFund⁡D
59 46 3 3 48 58 syl22anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D<PellFund⁡D↔log⁡A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡Dlog⁡PellFund⁡D<log⁡PellFund⁡Dlog⁡PellFund⁡D
60 57 59 mpbird ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D<PellFund⁡D
61 pellfund14gap ⊢D∈ℕ∖◻ℕ∧A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D∈Pell14QR⁡D∧1≤A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D∧A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D<PellFund⁡D→A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D=1
62 17 25 51 60 61 syl112anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D=1
63 31 negidd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→log⁡Alog⁡PellFund⁡D+−log⁡Alog⁡PellFund⁡D=0
64 63 oveq2d ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡Dlog⁡Alog⁡PellFund⁡D+−log⁡Alog⁡PellFund⁡D=PellFund⁡D0
65 3 rpcnd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡D∈ℂ
66 3 rpne0d ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡D≠0
67 expaddz ⊢PellFund⁡D∈ℂ∧PellFund⁡D≠0∧log⁡Alog⁡PellFund⁡D∈ℤ∧−log⁡Alog⁡PellFund⁡D∈ℤ→PellFund⁡Dlog⁡Alog⁡PellFund⁡D+−log⁡Alog⁡PellFund⁡D=PellFund⁡Dlog⁡Alog⁡PellFund⁡D⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D
68 65 66 8 13 67 syl22anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡Dlog⁡Alog⁡PellFund⁡D+−log⁡Alog⁡PellFund⁡D=PellFund⁡Dlog⁡Alog⁡PellFund⁡D⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D
69 65 exp0d ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→PellFund⁡D0=1
70 64 68 69 3eqtr3rd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→1=PellFund⁡Dlog⁡Alog⁡PellFund⁡D⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D
71 62 70 eqtrd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→A⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D=PellFund⁡Dlog⁡Alog⁡PellFund⁡D⁢PellFund⁡D−log⁡Alog⁡PellFund⁡D
72 10 12 15 16 71 mulcan2ad ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→A=PellFund⁡Dlog⁡Alog⁡PellFund⁡D
73 oveq2 ⊢x=log⁡Alog⁡PellFund⁡D→PellFund⁡Dx=PellFund⁡Dlog⁡Alog⁡PellFund⁡D
74 73 rspceeqv ⊢log⁡Alog⁡PellFund⁡D∈ℤ∧A=PellFund⁡Dlog⁡Alog⁡PellFund⁡D→∃x∈ℤA=PellFund⁡Dx
75 8 72 74 syl2anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→∃x∈ℤA=PellFund⁡Dx