Theorem rmxy0

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

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

Proof

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