Metamath Proof Explorer

Theorem rmxy1

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

Ref Expression
Assertion rmxy1 ⊢ A ∈ ℤ ≥ 2 → A X rm 1 = A ∧ A Y rm 1 = 1

Proof

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