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	mulridd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 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	mulridd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 𝐴 ↑ 2 ) − 1 ) · 1 ) = ( ( 𝐴 ↑ 2 ) − 1 ) )
35	32 34	eqtrid	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 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 ) ) ) )