Definition df-rmx

Description: Define the X sequence as the rational part of some solution of a special Pell equation. See frmx and rmxyval for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014)

	Ref	Expression
Assertion	df-rmx	⊢ Xrm = ( 𝑎 ∈ ( ℤ≥ ‘ 2 ) , 𝑛 ∈ ℤ ↦ ( 1st ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crmx	⊢ Xrm
1		va	⊢ 𝑎
2		cuz	⊢ ℤ≥
3		c2	⊢ 2
4	3 2	cfv	⊢ ( ℤ≥ ‘ 2 )
5		vn	⊢ 𝑛
6		cz	⊢ ℤ
7		c1st	⊢ 1st
8		vb	⊢ 𝑏
9		cn0	⊢ ℕ0
10	9 6	cxp	⊢ ( ℕ0 × ℤ )
11	8	cv	⊢ 𝑏
12	11 7	cfv	⊢ ( 1st ‘ 𝑏 )
13		caddc	⊢ +
14		csqrt	⊢ √
15	1	cv	⊢ 𝑎
16		cexp	⊢ ↑
17	15 3 16	co	⊢ ( 𝑎 ↑ 2 )
18		cmin	⊢ −
19		c1	⊢ 1
20	17 19 18	co	⊢ ( ( 𝑎 ↑ 2 ) − 1 )
21	20 14	cfv	⊢ ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) )
22		cmul	⊢ ·
23		c2nd	⊢ 2nd
24	11 23	cfv	⊢ ( 2nd ‘ 𝑏 )
25	21 24 22	co	⊢ ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) )
26	12 25 13	co	⊢ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) )
27	8 10 26	cmpt	⊢ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) )
28	27	ccnv	⊢ ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) )
29	15 21 13	co	⊢ ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) )
30	5	cv	⊢ 𝑛
31	29 30 16	co	⊢ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 )
32	31 28	cfv	⊢ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) )
33	32 7	cfv	⊢ ( 1st ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) )
34	1 5 4 6 33	cmpo	⊢ ( 𝑎 ∈ ( ℤ≥ ‘ 2 ) , 𝑛 ∈ ℤ ↦ ( 1st ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) )
35	0 34	wceq	⊢ Xrm = ( 𝑎 ∈ ( ℤ≥ ‘ 2 ) , 𝑛 ∈ ℤ ↦ ( 1st ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) )