Metamath Proof Explorer

Theorem rmxyelxp

Description: Lemma for frmx and frmy . (Contributed by Stefan O'Rear, 22-Sep-2014)

Ref Expression
Assertion rmxyelxp ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b -1 ⁡ A + A 2 − 1 N ∈ ℕ 0 × ℤ

Proof

Step Hyp Ref Expression
1 rmxypairf1o ⊢ A ∈ ℤ ≥ 2 → b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b : ℕ 0 × ℤ ⟶ 1-1 onto a | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
2 1 adantr ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b : ℕ 0 × ℤ ⟶ 1-1 onto a | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
3 rmxyelqirr ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → A + A 2 − 1 N ∈ a | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d
4 f1ocnvdm ⊢ b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b : ℕ 0 × ℤ ⟶ 1-1 onto a | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d ∧ A + A 2 − 1 N ∈ a | ∃ c ∈ ℕ 0 ∃ d ∈ ℤ a = c + A 2 − 1 ⁢ d → b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b -1 ⁡ A + A 2 − 1 N ∈ ℕ 0 × ℤ
5 2 3 4 syl2anc ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ → b ∈ ℕ 0 × ℤ ⟼ 1 st ⁡ b + A 2 − 1 ⁢ 2 nd ⁡ b -1 ⁡ A + A 2 − 1 N ∈ ℕ 0 × ℤ