Theorem frmx

Description: The X sequence is a nonnegative integer. See rmxnn for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014)

	Ref	Expression
Assertion	frmx	⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0

Proof

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