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 syl6req 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 sseldi 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 sseldi 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