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→AXrm1=A∧AYrm1=1

Proof

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