Theorem frmy

Description: The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014)

	Ref	Expression
Assertion	frmy	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ

Proof

Step	Hyp	Ref	Expression
1		rmxyelxp	⊢ ( ( 𝑎 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( ◡ ( 𝑐 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑐 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑐 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑏 ) ) ∈ ( ℕ0 × ℤ ) )
2		xp2nd	⊢ ( ( ◡ ( 𝑐 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑐 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑐 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑏 ) ) ∈ ( ℕ0 × ℤ ) → ( 2nd ‘ ( ◡ ( 𝑐 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑐 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑐 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑏 ) ) ) ∈ ℤ )
3	1 2	syl	⊢ ( ( 𝑎 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑏 ∈ ℤ ) → ( 2nd ‘ ( ◡ ( 𝑐 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑐 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑐 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑏 ) ) ) ∈ ℤ )
4	3	rgen2	⊢ ∀ 𝑎 ∈ ( ℤ≥ ‘ 2 ) ∀ 𝑏 ∈ ℤ ( 2nd ‘ ( ◡ ( 𝑐 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑐 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑐 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑏 ) ) ) ∈ ℤ
5		df-rmy	⊢ Yrm = ( 𝑎 ∈ ( ℤ≥ ‘ 2 ) , 𝑏 ∈ ℤ ↦ ( 2nd ‘ ( ◡ ( 𝑐 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑐 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑐 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑏 ) ) ) )
6	5	fmpo	⊢ ( ∀ 𝑎 ∈ ( ℤ≥ ‘ 2 ) ∀ 𝑏 ∈ ℤ ( 2nd ‘ ( ◡ ( 𝑐 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑐 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑐 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑏 ) ) ) ∈ ℤ ↔ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ )
7	4 6	mpbi	⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ