Step |
Hyp |
Ref |
Expression |
1 |
|
1z |
|- 1 e. ZZ |
2 |
|
rmxyval |
|- ( ( A e. ( ZZ>= ` 2 ) /\ 1 e. ZZ ) -> ( ( A rmX 1 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 1 ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ 1 ) ) |
3 |
1 2
|
mpan2 |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 1 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 1 ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ 1 ) ) |
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
|
exp1d |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ 1 ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 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
|
mulid1d |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) = ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) |
11 |
10
|
eqcomd |
|- ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) ) |
12 |
11
|
oveq2d |
|- ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) = ( A + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) ) ) |
13 |
3 6 12
|
3eqtrd |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 1 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 1 ) ) ) = ( A + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) ) ) |
14 |
|
rmspecsqrtnq |
|- ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) ) |
15 |
|
nn0ssq |
|- NN0 C_ QQ |
16 |
|
frmx |
|- rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0 |
17 |
16
|
fovcl |
|- ( ( A e. ( ZZ>= ` 2 ) /\ 1 e. ZZ ) -> ( A rmX 1 ) e. NN0 ) |
18 |
1 17
|
mpan2 |
|- ( A e. ( ZZ>= ` 2 ) -> ( A rmX 1 ) e. NN0 ) |
19 |
15 18
|
sseldi |
|- ( A e. ( ZZ>= ` 2 ) -> ( A rmX 1 ) e. QQ ) |
20 |
|
zssq |
|- ZZ C_ QQ |
21 |
|
frmy |
|- rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ |
22 |
21
|
fovcl |
|- ( ( A e. ( ZZ>= ` 2 ) /\ 1 e. ZZ ) -> ( A rmY 1 ) e. ZZ ) |
23 |
1 22
|
mpan2 |
|- ( A e. ( ZZ>= ` 2 ) -> ( A rmY 1 ) e. ZZ ) |
24 |
20 23
|
sseldi |
|- ( A e. ( ZZ>= ` 2 ) -> ( A rmY 1 ) e. QQ ) |
25 |
|
eluzelz |
|- ( A e. ( ZZ>= ` 2 ) -> A e. ZZ ) |
26 |
|
zq |
|- ( A e. ZZ -> A e. QQ ) |
27 |
25 26
|
syl |
|- ( A e. ( ZZ>= ` 2 ) -> A e. QQ ) |
28 |
20 1
|
sselii |
|- 1 e. QQ |
29 |
28
|
a1i |
|- ( A e. ( ZZ>= ` 2 ) -> 1 e. QQ ) |
30 |
|
qirropth |
|- ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) /\ ( ( A rmX 1 ) e. QQ /\ ( A rmY 1 ) e. QQ ) /\ ( A e. QQ /\ 1 e. QQ ) ) -> ( ( ( A rmX 1 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 1 ) ) ) = ( A + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) ) <-> ( ( A rmX 1 ) = A /\ ( A rmY 1 ) = 1 ) ) ) |
31 |
14 19 24 27 29 30
|
syl122anc |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( ( A rmX 1 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 1 ) ) ) = ( A + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) ) <-> ( ( A rmX 1 ) = A /\ ( A rmY 1 ) = 1 ) ) ) |
32 |
13 31
|
mpbid |
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 1 ) = A /\ ( A rmY 1 ) = 1 ) ) |