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