Theorem rmxy1

Description: Value of the X and Y sequences at 1. (Contributed by Stefan O'Rear, 22-Sep-2014)

	Ref	Expression
Assertion	rmxy1	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 Xrm 1 ) = 𝐴 ∧ ( 𝐴 Yrm 1 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		1z	⊢ 1 ∈ ℤ
2		rmxyval	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 ∈ ℤ ) → ( ( 𝐴 Xrm 1 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 1 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 1 ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 Xrm 1 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 1 ) ) ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 1 ) )
4		rmbaserp	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ∈ ℝ+ )
5	4	rpcnd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ∈ ℂ )
6	5	exp1d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 1 ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
7		rmspecpos	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℝ+ )
8	7	rpcnd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ℂ )
9	8	sqrtcld	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ℂ )
10	9	mulid1d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 1 ) = ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
11	10	eqcomd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 1 ) )
12	11	oveq2d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) = ( 𝐴 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 1 ) ) )
13	3 6 12	3eqtrd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 Xrm 1 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 1 ) ) ) = ( 𝐴 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 1 ) ) )
14		rmspecsqrtnq	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) )
15		nn0ssq	⊢ ℕ0 ⊆ ℚ
16		frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
17	16	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 ∈ ℤ ) → ( 𝐴 Xrm 1 ) ∈ ℕ0 )
18	1 17	mpan2	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm 1 ) ∈ ℕ0 )
19	15 18	sseldi	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Xrm 1 ) ∈ ℚ )
20		zssq	⊢ ℤ ⊆ ℚ
21		frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
22	21	fovcl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 1 ∈ ℤ ) → ( 𝐴 Yrm 1 ) ∈ ℤ )
23	1 22	mpan2	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 1 ) ∈ ℤ )
24	20 23	sseldi	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 Yrm 1 ) ∈ ℚ )
25		eluzelz	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℤ )
26		zq	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℚ )
27	25 26	syl	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℚ )
28	20 1	sselii	⊢ 1 ∈ ℚ
29	28	a1i	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℚ )
30		qirropth	⊢ ( ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ∈ ( ℂ ∖ ℚ ) ∧ ( ( 𝐴 Xrm 1 ) ∈ ℚ ∧ ( 𝐴 Yrm 1 ) ∈ ℚ ) ∧ ( 𝐴 ∈ ℚ ∧ 1 ∈ ℚ ) ) → ( ( ( 𝐴 Xrm 1 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 1 ) ) ) = ( 𝐴 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 1 ) ) ↔ ( ( 𝐴 Xrm 1 ) = 𝐴 ∧ ( 𝐴 Yrm 1 ) = 1 ) ) )
31	14 19 24 27 29 30	syl122anc	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 𝐴 Xrm 1 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 𝐴 Yrm 1 ) ) ) = ( 𝐴 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 1 ) ) ↔ ( ( 𝐴 Xrm 1 ) = 𝐴 ∧ ( 𝐴 Yrm 1 ) = 1 ) ) )
32	13 31	mpbid	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 Xrm 1 ) = 𝐴 ∧ ( 𝐴 Yrm 1 ) = 1 ) )