Metamath Proof Explorer

Theorem rmxy0

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

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

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 rmxyval ⊢ A ∈ ℤ ≥ 2 ∧ 0 ∈ ℤ → A X rm 0 + A 2 − 1 ⁢ A Y rm 0 = A + A 2 − 1 0
3 1 2 mpan2 ⊢ A ∈ ℤ ≥ 2 → A X rm 0 + A 2 − 1 ⁢ A Y rm 0 = A + A 2 − 1 0
4 rmbaserp ⊢ A ∈ ℤ ≥ 2 → A + A 2 − 1 ∈ ℝ +
5 4 rpcnd ⊢ A ∈ ℤ ≥ 2 → A + A 2 − 1 ∈ ℂ
6 5 exp0d ⊢ A ∈ ℤ ≥ 2 → A + A 2 − 1 0 = 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 mul01d ⊢ A ∈ ℤ ≥ 2 → A 2 − 1 ⋅ 0 = 0
11 10 oveq2d ⊢ A ∈ ℤ ≥ 2 → 1 + A 2 − 1 ⋅ 0 = 1 + 0
12 1p0e1 ⊢ 1 + 0 = 1
13 11 12 eqtr2di ⊢ A ∈ ℤ ≥ 2 → 1 = 1 + A 2 − 1 ⋅ 0
14 3 6 13 3eqtrd ⊢ A ∈ ℤ ≥ 2 → A X rm 0 + A 2 − 1 ⁢ A Y rm 0 = 1 + A 2 − 1 ⋅ 0
15 rmspecsqrtnq ⊢ A ∈ ℤ ≥ 2 → A 2 − 1 ∈ ℂ ∖ ℚ
16 nn0ssq ⊢ ℕ 0 ⊆ ℚ
17 frmx ⊢ X rm : ℤ ≥ 2 × ℤ ⟶ ℕ 0
18 17 fovcl ⊢ A ∈ ℤ ≥ 2 ∧ 0 ∈ ℤ → A X rm 0 ∈ ℕ 0
19 1 18 mpan2 ⊢ A ∈ ℤ ≥ 2 → A X rm 0 ∈ ℕ 0
20 16 19 sselid ⊢ A ∈ ℤ ≥ 2 → A X rm 0 ∈ ℚ
21 zssq ⊢ ℤ ⊆ ℚ
22 frmy ⊢ Y rm : ℤ ≥ 2 × ℤ ⟶ ℤ
23 22 fovcl ⊢ A ∈ ℤ ≥ 2 ∧ 0 ∈ ℤ → A Y rm 0 ∈ ℤ
24 1 23 mpan2 ⊢ A ∈ ℤ ≥ 2 → A Y rm 0 ∈ ℤ
25 21 24 sselid ⊢ A ∈ ℤ ≥ 2 → A Y rm 0 ∈ ℚ
26 1z ⊢ 1 ∈ ℤ
27 21 26 sselii ⊢ 1 ∈ ℚ
28 27 a1i ⊢ A ∈ ℤ ≥ 2 → 1 ∈ ℚ
29 21 1 sselii ⊢ 0 ∈ ℚ
30 29 a1i ⊢ A ∈ ℤ ≥ 2 → 0 ∈ ℚ
31 qirropth ⊢ A 2 − 1 ∈ ℂ ∖ ℚ ∧ A X rm 0 ∈ ℚ ∧ A Y rm 0 ∈ ℚ ∧ 1 ∈ ℚ ∧ 0 ∈ ℚ → A X rm 0 + A 2 − 1 ⁢ A Y rm 0 = 1 + A 2 − 1 ⋅ 0 ↔ A X rm 0 = 1 ∧ A Y rm 0 = 0
32 15 20 25 28 30 31 syl122anc ⊢ A ∈ ℤ ≥ 2 → A X rm 0 + A 2 − 1 ⁢ A Y rm 0 = 1 + A 2 − 1 ⋅ 0 ↔ A X rm 0 = 1 ∧ A Y rm 0 = 0
33 14 32 mpbid ⊢ A ∈ ℤ ≥ 2 → A X rm 0 = 1 ∧ A Y rm 0 = 0