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→AXrm0=1∧AYrm0=0

Proof

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