Step | Hyp | Ref
| Expression |
1 | | nn0sqcl 14001 |
. . . . . 6
β’ (π β β0
β (πβ2) β
β0) |
2 | 1 | 3ad2ant3 1136 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (πβ2) β
β0) |
3 | 2 | nn0cnd 12480 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (πβ2) β
β) |
4 | | simp1 1137 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β π΄ β
(β€β₯β2)) |
5 | | nn0z 12529 |
. . . . . . . 8
β’ (π β β0
β π β
β€) |
6 | 5 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β π β
β€) |
7 | | frmx 41280 |
. . . . . . . 8
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
8 | 7 | fovcl 7485 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
9 | 4, 6, 8 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (π΄ Xrm
π) β
β0) |
10 | | nn0sqcl 14001 |
. . . . . 6
β’ ((π΄ Xrm π) β β0
β ((π΄ Xrm
π)β2) β
β0) |
11 | 9, 10 | syl 17 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β ((π΄ Xrm
π)β2) β
β0) |
12 | 11 | nn0cnd 12480 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β ((π΄ Xrm
π)β2) β
β) |
13 | | rmspecnonsq 41273 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β (β β
β»NN)) |
14 | 13 | eldifad 3923 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β) |
15 | 14 | nnnn0d 12478 |
. . . . . . 7
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β0) |
16 | 15 | 3ad2ant1 1134 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β ((π΄β2) β
1) β β0) |
17 | | rmynn0 41324 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β0) β (π΄ Yrm π) β
β0) |
18 | 17 | 3adant3 1133 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (π΄ Yrm
π) β
β0) |
19 | | nn0sqcl 14001 |
. . . . . . 7
β’ ((π΄ Yrm π) β β0
β ((π΄ Yrm
π)β2) β
β0) |
20 | 18, 19 | syl 17 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β ((π΄ Yrm
π)β2) β
β0) |
21 | 16, 20 | nn0mulcld 12483 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (((π΄β2) β
1) Β· ((π΄
Yrm π)β2))
β β0) |
22 | 21 | nn0cnd 12480 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (((π΄β2) β
1) Β· ((π΄
Yrm π)β2))
β β) |
23 | 3, 12, 22 | subcan2ad 11562 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (((πβ2) β
(((π΄β2) β 1)
Β· ((π΄ Yrm
π)β2))) = (((π΄ Xrm π)β2) β (((π΄β2) β 1) Β·
((π΄ Yrm π)β2))) β (πβ2) = ((π΄ Xrm π)β2))) |
24 | | rmxynorm 41285 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (((π΄ Xrm π)β2) β (((π΄β2) β 1) Β· ((π΄ Yrm π)β2))) =
1) |
25 | 4, 6, 24 | syl2anc 585 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (((π΄ Xrm
π)β2) β (((π΄β2) β 1) Β·
((π΄ Yrm π)β2))) =
1) |
26 | 25 | eqeq2d 2744 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (((πβ2) β
(((π΄β2) β 1)
Β· ((π΄ Yrm
π)β2))) = (((π΄ Xrm π)β2) β (((π΄β2) β 1) Β·
((π΄ Yrm π)β2))) β ((πβ2) β (((π΄β2) β 1) Β·
((π΄ Yrm π)β2))) =
1)) |
27 | | nn0re 12427 |
. . . . . 6
β’ (π β β0
β π β
β) |
28 | | nn0ge0 12443 |
. . . . . 6
β’ (π β β0
β 0 β€ π) |
29 | 27, 28 | jca 513 |
. . . . 5
β’ (π β β0
β (π β β
β§ 0 β€ π)) |
30 | 29 | 3ad2ant3 1136 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (π β β
β§ 0 β€ π)) |
31 | | nn0re 12427 |
. . . . . 6
β’ ((π΄ Xrm π) β β0
β (π΄ Xrm
π) β
β) |
32 | | nn0ge0 12443 |
. . . . . 6
β’ ((π΄ Xrm π) β β0
β 0 β€ (π΄
Xrm π)) |
33 | 31, 32 | jca 513 |
. . . . 5
β’ ((π΄ Xrm π) β β0
β ((π΄ Xrm
π) β β β§ 0
β€ (π΄ Xrm
π))) |
34 | 9, 33 | syl 17 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β ((π΄ Xrm
π) β β β§ 0
β€ (π΄ Xrm
π))) |
35 | | sq11 14042 |
. . . 4
β’ (((π β β β§ 0 β€
π) β§ ((π΄ Xrm π) β β β§ 0 β€
(π΄ Xrm π))) β ((πβ2) = ((π΄ Xrm π)β2) β π = (π΄ Xrm π))) |
36 | 30, 34, 35 | syl2anc 585 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β ((πβ2) =
((π΄ Xrm π)β2) β π = (π΄ Xrm π))) |
37 | 23, 26, 36 | 3bitr3rd 310 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (π = (π΄ Xrm π) β ((πβ2) β (((π΄β2) β 1) Β· ((π΄ Yrm π)β2))) =
1)) |
38 | | oveq1 7365 |
. . . . . . 7
β’ (π¦ = (π΄ Yrm π) β (π¦β2) = ((π΄ Yrm π)β2)) |
39 | 38 | oveq2d 7374 |
. . . . . 6
β’ (π¦ = (π΄ Yrm π) β (((π΄β2) β 1) Β· (π¦β2)) = (((π΄β2) β 1) Β· ((π΄ Yrm π)β2))) |
40 | 39 | oveq2d 7374 |
. . . . 5
β’ (π¦ = (π΄ Yrm π) β ((πβ2) β (((π΄β2) β 1) Β· (π¦β2))) = ((πβ2) β (((π΄β2) β 1) Β· ((π΄ Yrm π)β2)))) |
41 | 40 | eqeq1d 2735 |
. . . 4
β’ (π¦ = (π΄ Yrm π) β (((πβ2) β (((π΄β2) β 1) Β· (π¦β2))) = 1 β ((πβ2) β (((π΄β2) β 1) Β·
((π΄ Yrm π)β2))) =
1)) |
42 | 41 | ceqsrexv 3606 |
. . 3
β’ ((π΄ Yrm π) β β0
β (βπ¦ β
β0 (π¦ =
(π΄ Yrm π) β§ ((πβ2) β (((π΄β2) β 1) Β· (π¦β2))) = 1) β ((πβ2) β (((π΄β2) β 1) Β·
((π΄ Yrm π)β2))) =
1)) |
43 | 18, 42 | syl 17 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (βπ¦ β
β0 (π¦ =
(π΄ Yrm π) β§ ((πβ2) β (((π΄β2) β 1) Β· (π¦β2))) = 1) β ((πβ2) β (((π΄β2) β 1) Β·
((π΄ Yrm π)β2))) =
1)) |
44 | 37, 43 | bitr4d 282 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β0 β§ π β β0)
β (π = (π΄ Xrm π) β βπ¦ β β0
(π¦ = (π΄ Yrm π) β§ ((πβ2) β (((π΄β2) β 1) Β· (π¦β2))) =
1))) |