Metamath Proof Explorer

Theorem rmspecfund

Description: The base of exponent used to define the X and Y sequences is the fundamental solution of the corresponding Pell equation. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion rmspecfund ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 rmspecnonsq ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )
2 eluzelz ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℤ )
3 zsqcl ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
4 2 3 syl ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 ↑ 2 ) ∈ ℤ )
5 4 zred ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
6 1red ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℝ )
7 5 6 resubcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℝ )
8 sq1 ⊢ ( 1 ↑ 2 ) = 1
9 8 a1i ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 1 ↑ 2 ) = 1 )
10 eluz2b2 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐴 ∈ ℕ ∧ 1 < 𝐴 ) )
11 10 simprbi ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐴 )
12 eluzelre ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℝ )
13 0le1 ⊢ 0 ≤ 1
14 13 a1i ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ 1 )
15 eluzge2nn0 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ0 )
16 15 nn0ge0d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ 𝐴 )
17 6 12 14 16 lt2sqd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 1 < 𝐴 ↔ ( 1 ↑ 2 ) < ( 𝐴 ↑ 2 ) ) )
18 11 17 mpbid ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 1 ↑ 2 ) < ( 𝐴 ↑ 2 ) )
19 9 18 eqbrtrrd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 < ( 𝐴 ↑ 2 ) )
20 6 5 posdifd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 1 < ( 𝐴 ↑ 2 ) ↔ 0 < ( ( 𝐴 ↑ 2 ) − 1 ) ) )
21 19 20 mpbid ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 0 < ( ( 𝐴 ↑ 2 ) − 1 ) )
22 7 21 elrpd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℝ+ )
23 22 rpsqrtcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℝ+ )
24 23 rpred ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℝ )
25 24 recnd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℂ )
26 25 mulid1d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 1 ) = ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
27 26 oveq2d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 1 ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
28 pell1qrss14 ⊢ ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) → ( Pell1QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ⊆ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
29 1 28 syl ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( Pell1QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ⊆ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
30 1nn0 ⊢ 1 ∈ ℕ0
31 30 a1i ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℕ0 )
32 8 oveq2i ⊢ ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 1 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) − 1 ) · 1 )
33 7 recnd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
34 33 mulid1d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · 1 ) = ( ( 𝐴 ↑ 2 ) − 1 ) )
35 32 34 syl5eq ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 1 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) − 1 ) )
36 35 oveq2d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 1 ↑ 2 ) ) ) = ( ( 𝐴 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) − 1 ) ) )
37 5 recnd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
38 1cnd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℂ )
39 37 38 nncand ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) − 1 ) ) = 1 )
40 36 39 eqtrd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 1 ↑ 2 ) ) ) = 1 )
41 pellqrexplicit ⊢ ( ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( ( 𝐴 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 1 ↑ 2 ) ) ) = 1 ) → ( 𝐴 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 1 ) ) ∈ ( Pell1QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
42 1 15 31 40 41 syl31anc ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 1 ) ) ∈ ( Pell1QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
43 29 42 sseldd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 1 ) ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
44 27 43 eqeltrrd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
45 6 24 readdcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 1 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ∈ ℝ )
46 12 24 readdcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ∈ ℝ )
47 6 23 ltaddrpd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 < ( 1 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
48 6 12 24 11 ltadd1dd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 1 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) < ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
49 6 45 46 47 48 lttrd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 < ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
50 pellfundlb ⊢ ( ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∧ 1 < ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ) → ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ≤ ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
51 1 44 49 50 syl3anc ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ≤ ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
52 37 38 npcand ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) + 1 ) = ( 𝐴 ↑ 2 ) )
53 52 fveq2d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( ( 𝐴 ↑ 2 ) − 1 ) + 1 ) ) = ( √ ‘ ( 𝐴 ↑ 2 ) ) )
54 12 16 sqrtsqd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) = 𝐴 )
55 53 54 eqtrd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( ( 𝐴 ↑ 2 ) − 1 ) + 1 ) ) = 𝐴 )
56 55 oveq1d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( √ ‘ ( ( ( 𝐴 ↑ 2 ) − 1 ) + 1 ) ) + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
57 pellfundge ⊢ ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) → ( ( √ ‘ ( ( ( 𝐴 ↑ 2 ) − 1 ) + 1 ) ) + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ≤ ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
58 1 57 syl ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( √ ‘ ( ( ( 𝐴 ↑ 2 ) − 1 ) + 1 ) ) + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ≤ ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
59 56 58 eqbrtrrd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ≤ ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
60 pellfundre ⊢ ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℝ )
61 1 60 syl ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℝ )
62 61 46 letri3d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↔ ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ≤ ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ∧ ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ≤ ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ) )
63 51 59 62 mpbir2and ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )