Metamath Proof Explorer

Theorem rmxyneg

Description: Negation law for X and Y sequences. JonesMatijasevic is inconsistent on whether the X and Y sequences have domain NN0 or ZZ ; we use ZZ consistently to avoid the need for a separate subtraction law. (Contributed by Stefan O'Rear, 22-Sep-2014)

Ref Expression
Assertion rmxyneg 
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX -u N ) = ( A rmX N ) /\ ( A rmY -u N ) = -u ( A rmY N ) ) )

Proof

Step Hyp Ref Expression
1 znegcl 
 |-  ( N e. ZZ -> -u N e. ZZ )
2 rmxyval 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ -u N e. ZZ ) -> ( ( A rmX -u N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY -u N ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ -u N ) )
3 1 2 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX -u N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY -u N ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ -u N ) )
4 rmxyval 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) )
5 4 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( 1 / ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ) = ( 1 / ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) ) )
6 rmbaserp 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. RR+ )
7 6 rpcnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. CC )
8 7 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. CC )
9 6 rpne0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) =/= 0 )
10 9 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) =/= 0 )
11 simpr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> N e. ZZ )
12 8 10 11 expclzd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) e. CC )
13 4 12 eqeltrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) e. CC )
14 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
15 14 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
16 15 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. CC )
17 rmspecnonsq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )
18 17 eldifad 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. NN )
19 18 nncnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. CC )
20 19 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A ^ 2 ) - 1 ) e. CC )
21 20 sqrtcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. CC )
22 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
23 22 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
24 23 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. CC )
25 24 negcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> -u ( A rmY N ) e. CC )
26 21 25 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. -u ( A rmY N ) ) e. CC )
27 16 26 addcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. -u ( A rmY N ) ) ) e. CC )
28 8 10 11 expne0d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) =/= 0 )
29 4 28 eqnetrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) =/= 0 )
30 21 24 mulneg2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. -u ( A rmY N ) ) = -u ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) )
31 30 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. -u ( A rmY N ) ) ) = ( ( A rmX N ) + -u ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) )
32 21 24 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) e. CC )
33 16 32 negsubd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) + -u ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) = ( ( A rmX N ) - ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) )
34 31 33 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. -u ( A rmY N ) ) ) = ( ( A rmX N ) - ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) )
35 34 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) x. ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. -u ( A rmY N ) ) ) ) = ( ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) x. ( ( A rmX N ) - ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ) )
36 subsq 
 |-  ( ( ( A rmX N ) e. CC /\ ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) e. CC ) -> ( ( ( A rmX N ) ^ 2 ) - ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ 2 ) ) = ( ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) x. ( ( A rmX N ) - ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ) )
37 16 32 36 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmX N ) ^ 2 ) - ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ 2 ) ) = ( ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) x. ( ( A rmX N ) - ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ) )
38 21 24 sqmuld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ 2 ) = ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) x. ( ( A rmY N ) ^ 2 ) ) )
39 20 sqsqrtd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) = ( ( A ^ 2 ) - 1 ) )
40 39 oveq1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ^ 2 ) x. ( ( A rmY N ) ^ 2 ) ) = ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) )
41 38 40 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ 2 ) = ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) )
42 41 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmX N ) ^ 2 ) - ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ 2 ) ) = ( ( ( A rmX N ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) )
43 rmxynorm 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmX N ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) = 1 )
44 42 43 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmX N ) ^ 2 ) - ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ^ 2 ) ) = 1 )
45 35 37 44 3eqtr2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) x. ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. -u ( A rmY N ) ) ) ) = 1 )
46 13 27 29 45 mvllmuld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. -u ( A rmY N ) ) ) = ( 1 / ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ) )
47 8 10 11 expnegd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ -u N ) = ( 1 / ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) ) )
48 5 46 47 3eqtr4rd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ -u N ) = ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. -u ( A rmY N ) ) ) )
49 3 48 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX -u N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY -u N ) ) ) = ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. -u ( A rmY N ) ) ) )
50 rmspecsqrtnq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
51 50 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
52 nn0ssq 
 |-  NN0 C_ QQ
53 14 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ -u N e. ZZ ) -> ( A rmX -u N ) e. NN0 )
54 1 53 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX -u N ) e. NN0 )
55 52 54 sselid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX -u N ) e. QQ )
56 zssq 
 |-  ZZ C_ QQ
57 22 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ -u N e. ZZ ) -> ( A rmY -u N ) e. ZZ )
58 1 57 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY -u N ) e. ZZ )
59 56 58 sselid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY -u N ) e. QQ )
60 52 15 sselid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. QQ )
61 56 23 sselid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. QQ )
62 qnegcl 
 |-  ( ( A rmY N ) e. QQ -> -u ( A rmY N ) e. QQ )
63 61 62 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> -u ( A rmY N ) e. QQ )
64 qirropth 
 |-  ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) /\ ( ( A rmX -u N ) e. QQ /\ ( A rmY -u N ) e. QQ ) /\ ( ( A rmX N ) e. QQ /\ -u ( A rmY N ) e. QQ ) ) -> ( ( ( A rmX -u N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY -u N ) ) ) = ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. -u ( A rmY N ) ) ) <-> ( ( A rmX -u N ) = ( A rmX N ) /\ ( A rmY -u N ) = -u ( A rmY N ) ) ) )
65 51 55 59 60 63 64 syl122anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmX -u N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY -u N ) ) ) = ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. -u ( A rmY N ) ) ) <-> ( ( A rmX -u N ) = ( A rmX N ) /\ ( A rmY -u N ) = -u ( A rmY N ) ) ) )
66 49 65 mpbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX -u N ) = ( A rmX N ) /\ ( A rmY -u N ) = -u ( A rmY N ) ) )