Step | Hyp | Ref
| Expression |
1 | | znegcl 12546 |
. . . 4
β’ (π β β€ β -π β
β€) |
2 | | rmxyval 41286 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ -π β β€) β ((π΄ Xrm -π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm -π))) = ((π΄ + (ββ((π΄β2) β 1)))β-π)) |
3 | 1, 2 | sylan2 594 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm -π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm -π))) = ((π΄ + (ββ((π΄β2) β 1)))β-π)) |
4 | | rmxyval 41286 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) = ((π΄ + (ββ((π΄β2) β 1)))βπ)) |
5 | 4 | oveq2d 7377 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (1 / ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π)))) = (1 / ((π΄ + (ββ((π΄β2) β 1)))βπ))) |
6 | | rmbaserp 41290 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯β2) β (π΄ + (ββ((π΄β2) β 1))) β
β+) |
7 | 6 | rpcnd 12967 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β (π΄ + (ββ((π΄β2) β 1))) β
β) |
8 | 7 | adantr 482 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ + (ββ((π΄β2) β 1))) β
β) |
9 | 6 | rpne0d 12970 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β (π΄ + (ββ((π΄β2) β 1))) β
0) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ + (ββ((π΄β2) β 1))) β
0) |
11 | | simpr 486 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β π β β€) |
12 | 8, 10, 11 | expclzd 14065 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ + (ββ((π΄β2) β 1)))βπ) β β) |
13 | 4, 12 | eqeltrd 2834 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) β
β) |
14 | | frmx 41284 |
. . . . . . . 8
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
15 | 14 | fovcl 7488 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
16 | 15 | nn0cnd 12483 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β β) |
17 | | rmspecnonsq 41277 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β (β β
β»NN)) |
18 | 17 | eldifad 3926 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β) |
19 | 18 | nncnd 12177 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β) |
20 | 19 | adantr 482 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄β2) β 1) β
β) |
21 | 20 | sqrtcld 15331 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β
(ββ((π΄β2)
β 1)) β β) |
22 | | frmy 41285 |
. . . . . . . . . 10
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
23 | 22 | fovcl 7488 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
24 | 23 | zcnd 12616 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β) |
25 | 24 | negcld 11507 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β -(π΄ Yrm π) β β) |
26 | 21, 25 | mulcld 11183 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β
((ββ((π΄β2)
β 1)) Β· -(π΄
Yrm π)) β
β) |
27 | 16, 26 | addcld 11182 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· -(π΄ Yrm π))) β
β) |
28 | 8, 10, 11 | expne0d 14066 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ + (ββ((π΄β2) β 1)))βπ) β 0) |
29 | 4, 28 | eqnetrd 3008 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) β 0) |
30 | 21, 24 | mulneg2d 11617 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β
((ββ((π΄β2)
β 1)) Β· -(π΄
Yrm π)) =
-((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) |
31 | 30 | oveq2d 7377 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· -(π΄ Yrm π))) = ((π΄ Xrm π) + -((ββ((π΄β2) β 1)) Β· (π΄ Yrm π)))) |
32 | 21, 24 | mulcld 11183 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π)) β
β) |
33 | 16, 32 | negsubd 11526 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) + -((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) = ((π΄ Xrm π) β ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π)))) |
34 | 31, 33 | eqtrd 2773 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· -(π΄ Yrm π))) = ((π΄ Xrm π) β ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π)))) |
35 | 34 | oveq2d 7377 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) Β· ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· -(π΄ Yrm π)))) = (((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) Β· ((π΄ Xrm π) β ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))))) |
36 | | subsq 14123 |
. . . . . . 7
β’ (((π΄ Xrm π) β β β§
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π)) β
β) β (((π΄
Xrm π)β2)
β (((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))β2)) = (((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))) Β· ((π΄ Xrm π) β ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))))) |
37 | 16, 32, 36 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄ Xrm π)β2) β (((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))β2)) = (((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))) Β· ((π΄ Xrm π) β ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))))) |
38 | 21, 24 | sqmuld 14072 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β
(((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))β2) =
(((ββ((π΄β2) β 1))β2) Β·
((π΄ Yrm π)β2))) |
39 | 20 | sqsqrtd 15333 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β
((ββ((π΄β2)
β 1))β2) = ((π΄β2) β 1)) |
40 | 39 | oveq1d 7376 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β
(((ββ((π΄β2) β 1))β2) Β·
((π΄ Yrm π)β2)) = (((π΄β2) β 1) Β·
((π΄ Yrm π)β2))) |
41 | 38, 40 | eqtrd 2773 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β
(((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))β2) = (((π΄β2) β 1) Β·
((π΄ Yrm π)β2))) |
42 | 41 | oveq2d 7377 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄ Xrm π)β2) β (((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))β2)) = (((π΄ Xrm π)β2) β (((π΄β2) β 1) Β·
((π΄ Yrm π)β2)))) |
43 | | rmxynorm 41289 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄ Xrm π)β2) β (((π΄β2) β 1) Β· ((π΄ Yrm π)β2))) =
1) |
44 | 42, 43 | eqtrd 2773 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄ Xrm π)β2) β (((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))β2)) =
1) |
45 | 35, 37, 44 | 3eqtr2d 2779 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) Β· ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· -(π΄ Yrm π)))) = 1) |
46 | 13, 27, 29, 45 | mvllmuld 11995 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· -(π΄ Yrm π))) = (1 / ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))))) |
47 | 8, 10, 11 | expnegd 14067 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ + (ββ((π΄β2) β 1)))β-π) = (1 / ((π΄ + (ββ((π΄β2) β 1)))βπ))) |
48 | 5, 46, 47 | 3eqtr4rd 2784 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ + (ββ((π΄β2) β 1)))β-π) = ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· -(π΄ Yrm π)))) |
49 | 3, 48 | eqtrd 2773 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm -π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm -π))) = ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· -(π΄ Yrm π)))) |
50 | | rmspecsqrtnq 41276 |
. . . 4
β’ (π΄ β
(β€β₯β2) β (ββ((π΄β2) β 1)) β (β β
β)) |
51 | 50 | adantr 482 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β
(ββ((π΄β2)
β 1)) β (β β β)) |
52 | | nn0ssq 12890 |
. . . 4
β’
β0 β β |
53 | 14 | fovcl 7488 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ -π β β€) β (π΄ Xrm -π) β
β0) |
54 | 1, 53 | sylan2 594 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm -π) β
β0) |
55 | 52, 54 | sselid 3946 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm -π) β β) |
56 | | zssq 12889 |
. . . 4
β’ β€
β β |
57 | 22 | fovcl 7488 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ -π β β€) β (π΄ Yrm -π) β β€) |
58 | 1, 57 | sylan2 594 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm -π) β β€) |
59 | 56, 58 | sselid 3946 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm -π) β β) |
60 | 52, 15 | sselid 3946 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β β) |
61 | 56, 23 | sselid 3946 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β) |
62 | | qnegcl 12899 |
. . . 4
β’ ((π΄ Yrm π) β β β -(π΄ Yrm π) β
β) |
63 | 61, 62 | syl 17 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β -(π΄ Yrm π) β β) |
64 | | qirropth 41278 |
. . 3
β’
(((ββ((π΄β2) β 1)) β (β β
β) β§ ((π΄
Xrm -π) β
β β§ (π΄
Yrm -π) β
β) β§ ((π΄
Xrm π) β
β β§ -(π΄
Yrm π) β
β)) β (((π΄
Xrm -π) +
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm -π))) =
((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β·
-(π΄ Yrm π))) β ((π΄ Xrm -π) = (π΄ Xrm π) β§ (π΄ Yrm -π) = -(π΄ Yrm π)))) |
65 | 51, 55, 59, 60, 63, 64 | syl122anc 1380 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄ Xrm -π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm -π))) = ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· -(π΄ Yrm π))) β ((π΄ Xrm -π) = (π΄ Xrm π) β§ (π΄ Yrm -π) = -(π΄ Yrm π)))) |
66 | 49, 65 | mpbid 231 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm -π) = (π΄ Xrm π) β§ (π΄ Yrm -π) = -(π΄ Yrm π))) |