Step |
Hyp |
Ref |
Expression |
1 |
|
0z |
|- 0 e. ZZ |
2 |
|
rmxyval |
|- ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ ) -> ( ( A rmX 0 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 0 ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ 0 ) ) |
3 |
1 2
|
mpan2 |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 0 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 0 ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ 0 ) ) |
4 |
|
rmbaserp |
|- ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. RR+ ) |
5 |
4
|
rpcnd |
|- ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. CC ) |
6 |
5
|
exp0d |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ 0 ) = 1 ) |
7 |
|
rmspecpos |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. RR+ ) |
8 |
7
|
rpcnd |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. CC ) |
9 |
8
|
sqrtcld |
|- ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. CC ) |
10 |
9
|
mul01d |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 0 ) = 0 ) |
11 |
10
|
oveq2d |
|- ( A e. ( ZZ>= ` 2 ) -> ( 1 + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 0 ) ) = ( 1 + 0 ) ) |
12 |
|
1p0e1 |
|- ( 1 + 0 ) = 1 |
13 |
11 12
|
eqtr2di |
|- ( A e. ( ZZ>= ` 2 ) -> 1 = ( 1 + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 0 ) ) ) |
14 |
3 6 13
|
3eqtrd |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 0 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 0 ) ) ) = ( 1 + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 0 ) ) ) |
15 |
|
rmspecsqrtnq |
|- ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) ) |
16 |
|
nn0ssq |
|- NN0 C_ QQ |
17 |
|
frmx |
|- rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0 |
18 |
17
|
fovcl |
|- ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ ) -> ( A rmX 0 ) e. NN0 ) |
19 |
1 18
|
mpan2 |
|- ( A e. ( ZZ>= ` 2 ) -> ( A rmX 0 ) e. NN0 ) |
20 |
16 19
|
sseldi |
|- ( A e. ( ZZ>= ` 2 ) -> ( A rmX 0 ) e. QQ ) |
21 |
|
zssq |
|- ZZ C_ QQ |
22 |
|
frmy |
|- rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ |
23 |
22
|
fovcl |
|- ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ ) -> ( A rmY 0 ) e. ZZ ) |
24 |
1 23
|
mpan2 |
|- ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) e. ZZ ) |
25 |
21 24
|
sseldi |
|- ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) e. QQ ) |
26 |
|
1z |
|- 1 e. ZZ |
27 |
21 26
|
sselii |
|- 1 e. QQ |
28 |
27
|
a1i |
|- ( A e. ( ZZ>= ` 2 ) -> 1 e. QQ ) |
29 |
21 1
|
sselii |
|- 0 e. QQ |
30 |
29
|
a1i |
|- ( A e. ( ZZ>= ` 2 ) -> 0 e. QQ ) |
31 |
|
qirropth |
|- ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) /\ ( ( A rmX 0 ) e. QQ /\ ( A rmY 0 ) e. QQ ) /\ ( 1 e. QQ /\ 0 e. QQ ) ) -> ( ( ( A rmX 0 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 0 ) ) ) = ( 1 + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 0 ) ) <-> ( ( A rmX 0 ) = 1 /\ ( A rmY 0 ) = 0 ) ) ) |
32 |
15 20 25 28 30 31
|
syl122anc |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( ( A rmX 0 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 0 ) ) ) = ( 1 + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 0 ) ) <-> ( ( A rmX 0 ) = 1 /\ ( A rmY 0 ) = 0 ) ) ) |
33 |
14 32
|
mpbid |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 0 ) = 1 /\ ( A rmY 0 ) = 0 ) ) |