Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β π΄ β
(β€β₯β2)) |
2 | | zaddcl 12402 |
. . . . 5
β’ ((π β β€ β§ π β β€) β (π + π) β β€) |
3 | 2 | 3adant1 1130 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π + π) β β€) |
4 | | rmxyval 40774 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ (π + π) β β€) β ((π΄ Xrm (π + π)) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm (π + π)))) = ((π΄ + (ββ((π΄β2) β 1)))β(π + π))) |
5 | 1, 3, 4 | syl2anc 585 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm (π + π)) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm (π + π)))) = ((π΄ + (ββ((π΄β2) β 1)))β(π + π))) |
6 | | eluzelz 12634 |
. . . . . . . 8
β’ (π΄ β
(β€β₯β2) β π΄ β β€) |
7 | 6 | 3ad2ant1 1133 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β π΄ β β€) |
8 | 7 | zcnd 12469 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β π΄ β β) |
9 | | zq 12736 |
. . . . . . . . . 10
β’ (π΄ β β€ β π΄ β
β) |
10 | | qsqcl 13891 |
. . . . . . . . . 10
β’ (π΄ β β β (π΄β2) β
β) |
11 | 7, 9, 10 | 3syl 18 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄β2) β β) |
12 | | zssq 12738 |
. . . . . . . . . . 11
β’ β€
β β |
13 | | 1z 12392 |
. . . . . . . . . . 11
β’ 1 β
β€ |
14 | 12, 13 | sselii 3923 |
. . . . . . . . . 10
β’ 1 β
β |
15 | 14 | a1i 11 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β 1 β
β) |
16 | | qsubcl 12750 |
. . . . . . . . 9
β’ (((π΄β2) β β β§ 1
β β) β ((π΄β2) β 1) β
β) |
17 | 11, 15, 16 | syl2anc 585 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄β2) β 1) β
β) |
18 | | qcn 12745 |
. . . . . . . 8
β’ (((π΄β2) β 1) β
β β ((π΄β2)
β 1) β β) |
19 | 17, 18 | syl 17 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄β2) β 1) β
β) |
20 | 19 | sqrtcld 15190 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β
(ββ((π΄β2)
β 1)) β β) |
21 | 8, 20 | addcld 11036 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ + (ββ((π΄β2) β 1))) β
β) |
22 | | rmbaserp 40778 |
. . . . . . 7
β’ (π΄ β
(β€β₯β2) β (π΄ + (ββ((π΄β2) β 1))) β
β+) |
23 | 22 | rpne0d 12819 |
. . . . . 6
β’ (π΄ β
(β€β₯β2) β (π΄ + (ββ((π΄β2) β 1))) β
0) |
24 | 23 | 3ad2ant1 1133 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ + (ββ((π΄β2) β 1))) β
0) |
25 | | simp2 1137 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β π β β€) |
26 | | simp3 1138 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β π β β€) |
27 | | expaddz 13869 |
. . . . 5
β’ ((((π΄ + (ββ((π΄β2) β 1))) β
β β§ (π΄ +
(ββ((π΄β2)
β 1))) β 0) β§ (π β β€ β§ π β β€)) β ((π΄ + (ββ((π΄β2) β 1)))β(π + π)) = (((π΄ + (ββ((π΄β2) β 1)))βπ) Β· ((π΄ + (ββ((π΄β2) β 1)))βπ))) |
28 | 21, 24, 25, 26, 27 | syl22anc 837 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ + (ββ((π΄β2) β 1)))β(π + π)) = (((π΄ + (ββ((π΄β2) β 1)))βπ) Β· ((π΄ + (ββ((π΄β2) β 1)))βπ))) |
29 | | frmx 40772 |
. . . . . . . . 9
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
30 | 29 | a1i 11 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β Xrm
:((β€β₯β2) Γ
β€)βΆβ0) |
31 | 30, 1, 25 | fovcdmd 7472 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β
β0) |
32 | 31 | nn0cnd 12337 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β β) |
33 | | frmy 40773 |
. . . . . . . . . 10
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
34 | 33 | a1i 11 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β Yrm
:((β€β₯β2) Γ
β€)βΆβ€) |
35 | 34, 1, 25 | fovcdmd 7472 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β€) |
36 | 35 | zcnd 12469 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β) |
37 | 20, 36 | mulcld 11037 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π)) β
β) |
38 | 30, 1, 26 | fovcdmd 7472 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β
β0) |
39 | 38 | nn0cnd 12337 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β β) |
40 | 34, 1, 26 | fovcdmd 7472 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β€) |
41 | 40 | zcnd 12469 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β) |
42 | 20, 41 | mulcld 11037 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π)) β
β) |
43 | 32, 37, 39, 42 | muladdd 11475 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) Β· ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π)))) = ((((π΄ Xrm π) Β· (π΄ Xrm π)) + (((ββ((π΄β2) β 1)) Β· (π΄ Yrm π)) Β·
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π)))) +
(((π΄ Xrm π) Β·
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π))) +
((π΄ Xrm π) Β·
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π)))))) |
44 | | rmxyval 40774 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) = ((π΄ + (ββ((π΄β2) β 1)))βπ)) |
45 | 1, 25, 44 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) = ((π΄ + (ββ((π΄β2) β 1)))βπ)) |
46 | | rmxyval 40774 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) = ((π΄ + (ββ((π΄β2) β 1)))βπ)) |
47 | 1, 26, 46 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) = ((π΄ + (ββ((π΄β2) β 1)))βπ)) |
48 | 45, 47 | oveq12d 7321 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π))) Β· ((π΄ Xrm π) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm π)))) = (((π΄ + (ββ((π΄β2) β 1)))βπ) Β· ((π΄ + (ββ((π΄β2) β 1)))βπ))) |
49 | 43, 48 | eqtr3d 2778 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((((π΄ Xrm π) Β· (π΄ Xrm π)) + (((ββ((π΄β2) β 1)) Β· (π΄ Yrm π)) Β·
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π)))) +
(((π΄ Xrm π) Β·
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π))) +
((π΄ Xrm π) Β·
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π))))) =
(((π΄ +
(ββ((π΄β2)
β 1)))βπ)
Β· ((π΄ +
(ββ((π΄β2)
β 1)))βπ))) |
50 | 20, 41, 20, 36 | mul4d 11229 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β
(((ββ((π΄β2) β 1)) Β· (π΄ Yrm π)) Β·
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π))) =
(((ββ((π΄β2) β 1)) Β·
(ββ((π΄β2)
β 1))) Β· ((π΄
Yrm π) Β·
(π΄ Yrm π)))) |
51 | 19 | msqsqrtd 15193 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β
((ββ((π΄β2)
β 1)) Β· (ββ((π΄β2) β 1))) = ((π΄β2) β 1)) |
52 | 41, 36 | mulcomd 11038 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) Β· (π΄ Yrm π)) = ((π΄ Yrm π) Β· (π΄ Yrm π))) |
53 | 51, 52 | oveq12d 7321 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β
(((ββ((π΄β2) β 1)) Β·
(ββ((π΄β2)
β 1))) Β· ((π΄
Yrm π) Β·
(π΄ Yrm π))) = (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π)))) |
54 | 50, 53 | eqtrd 2776 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β
(((ββ((π΄β2) β 1)) Β· (π΄ Yrm π)) Β·
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π))) =
(((π΄β2) β 1)
Β· ((π΄ Yrm
π) Β· (π΄ Yrm π)))) |
55 | 54 | oveq2d 7319 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Xrm π) Β· (π΄ Xrm π)) + (((ββ((π΄β2) β 1)) Β· (π΄ Yrm π)) Β·
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π)))) =
(((π΄ Xrm π) Β· (π΄ Xrm π)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π))))) |
56 | 32, 20, 41 | mul12d 11226 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) Β· ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))) = ((ββ((π΄β2) β 1)) Β·
((π΄ Xrm π) Β· (π΄ Yrm π)))) |
57 | 39, 20, 36 | mul12d 11226 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) Β· ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))) = ((ββ((π΄β2) β 1)) Β·
((π΄ Xrm π) Β· (π΄ Yrm π)))) |
58 | 56, 57 | oveq12d 7321 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Xrm π) Β· ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))) + ((π΄ Xrm π) Β· ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π)))) = (((ββ((π΄β2) β 1)) Β·
((π΄ Xrm π) Β· (π΄ Yrm π))) + ((ββ((π΄β2) β 1)) Β· ((π΄ Xrm π) Β· (π΄ Yrm π))))) |
59 | 32, 41 | mulcld 11037 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) Β· (π΄ Yrm π)) β β) |
60 | 39, 36 | mulcld 11037 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) Β· (π΄ Yrm π)) β β) |
61 | 20, 59, 60 | adddid 11041 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β
((ββ((π΄β2)
β 1)) Β· (((π΄
Xrm π) Β·
(π΄ Yrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))) = (((ββ((π΄β2) β 1)) Β· ((π΄ Xrm π) Β· (π΄ Yrm π))) + ((ββ((π΄β2) β 1)) Β· ((π΄ Xrm π) Β· (π΄ Yrm π))))) |
62 | 59, 60 | addcomd 11219 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π))) = (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))) |
63 | 39, 36 | mulcomd 11038 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) Β· (π΄ Yrm π)) = ((π΄ Yrm π) Β· (π΄ Xrm π))) |
64 | 63 | oveq1d 7318 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π))) = (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))) |
65 | 62, 64 | eqtrd 2776 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Xrm π) Β· (π΄ Yrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π))) = (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))) |
66 | 65 | oveq2d 7319 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β
((ββ((π΄β2)
β 1)) Β· (((π΄
Xrm π) Β·
(π΄ Yrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))) = ((ββ((π΄β2) β 1)) Β· (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π))))) |
67 | 58, 61, 66 | 3eqtr2d 2782 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Xrm π) Β· ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π))) + ((π΄ Xrm π) Β· ((ββ((π΄β2) β 1)) Β·
(π΄ Yrm π)))) = ((ββ((π΄β2) β 1)) Β·
(((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π))))) |
68 | 55, 67 | oveq12d 7321 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((((π΄ Xrm π) Β· (π΄ Xrm π)) + (((ββ((π΄β2) β 1)) Β· (π΄ Yrm π)) Β·
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π)))) +
(((π΄ Xrm π) Β·
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π))) +
((π΄ Xrm π) Β·
((ββ((π΄β2)
β 1)) Β· (π΄
Yrm π))))) =
((((π΄ Xrm π) Β· (π΄ Xrm π)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π)))) + ((ββ((π΄β2) β 1)) Β· (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))))) |
69 | 28, 49, 68 | 3eqtr2d 2782 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ + (ββ((π΄β2) β 1)))β(π + π)) = ((((π΄ Xrm π) Β· (π΄ Xrm π)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π)))) + ((ββ((π΄β2) β 1)) Β· (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))))) |
70 | 5, 69 | eqtrd 2776 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm (π + π)) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm (π + π)))) = ((((π΄ Xrm π) Β· (π΄ Xrm π)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π)))) + ((ββ((π΄β2) β 1)) Β· (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))))) |
71 | | rmspecsqrtnq 40764 |
. . . 4
β’ (π΄ β
(β€β₯β2) β (ββ((π΄β2) β 1)) β (β β
β)) |
72 | 71 | 3ad2ant1 1133 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β
(ββ((π΄β2)
β 1)) β (β β β)) |
73 | | nn0ssq 12739 |
. . . 4
β’
β0 β β |
74 | 30, 1, 3 | fovcdmd 7472 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm (π + π)) β
β0) |
75 | 73, 74 | sselid 3924 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm (π + π)) β β) |
76 | 34, 1, 3 | fovcdmd 7472 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm (π + π)) β β€) |
77 | 12, 76 | sselid 3924 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm (π + π)) β β) |
78 | 73, 31 | sselid 3924 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β β) |
79 | 73, 38 | sselid 3924 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Xrm π) β β) |
80 | | qmulcl 12749 |
. . . . 5
β’ (((π΄ Xrm π) β β β§ (π΄ Xrm π) β β) β ((π΄ Xrm π) Β· (π΄ Xrm π)) β β) |
81 | 78, 79, 80 | syl2anc 585 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) Β· (π΄ Xrm π)) β β) |
82 | 12, 35 | sselid 3924 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β) |
83 | 12, 40 | sselid 3924 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm π) β β) |
84 | | qmulcl 12749 |
. . . . . 6
β’ (((π΄ Yrm π) β β β§ (π΄ Yrm π) β β) β ((π΄ Yrm π) Β· (π΄ Yrm π)) β β) |
85 | 82, 83, 84 | syl2anc 585 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) Β· (π΄ Yrm π)) β β) |
86 | | qmulcl 12749 |
. . . . 5
β’ ((((π΄β2) β 1) β
β β§ ((π΄
Yrm π) Β·
(π΄ Yrm π)) β β) β
(((π΄β2) β 1)
Β· ((π΄ Yrm
π) Β· (π΄ Yrm π))) β
β) |
87 | 17, 85, 86 | syl2anc 585 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π))) β β) |
88 | | qaddcl 12747 |
. . . 4
β’ ((((π΄ Xrm π) Β· (π΄ Xrm π)) β β β§ (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π))) β β) β (((π΄ Xrm π) Β· (π΄ Xrm π)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π)))) β β) |
89 | 81, 87, 88 | syl2anc 585 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Xrm π) Β· (π΄ Xrm π)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π)))) β β) |
90 | | qmulcl 12749 |
. . . . 5
β’ (((π΄ Yrm π) β β β§ (π΄ Xrm π) β β) β ((π΄ Yrm π) Β· (π΄ Xrm π)) β β) |
91 | 82, 79, 90 | syl2anc 585 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Yrm π) Β· (π΄ Xrm π)) β β) |
92 | | qmulcl 12749 |
. . . . 5
β’ (((π΄ Xrm π) β β β§ (π΄ Yrm π) β β) β ((π΄ Xrm π) Β· (π΄ Yrm π)) β β) |
93 | 78, 83, 92 | syl2anc 585 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm π) Β· (π΄ Yrm π)) β β) |
94 | | qaddcl 12747 |
. . . 4
β’ ((((π΄ Yrm π) Β· (π΄ Xrm π)) β β β§ ((π΄ Xrm π) Β· (π΄ Yrm π)) β β) β (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π))) β β) |
95 | 91, 93, 94 | syl2anc 585 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π))) β β) |
96 | | qirropth 40766 |
. . 3
β’
(((ββ((π΄β2) β 1)) β (β β
β) β§ ((π΄
Xrm (π + π)) β β β§ (π΄ Yrm (π + π)) β β) β§ ((((π΄ Xrm π) Β· (π΄ Xrm π)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π)))) β β β§ (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π))) β β)) β (((π΄ Xrm (π + π)) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm (π + π)))) = ((((π΄ Xrm π) Β· (π΄ Xrm π)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π)))) + ((ββ((π΄β2) β 1)) Β· (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π))))) β ((π΄ Xrm (π + π)) = (((π΄ Xrm π) Β· (π΄ Xrm π)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π)))) β§ (π΄ Yrm (π + π)) = (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))))) |
97 | 72, 75, 77, 89, 95, 96 | syl122anc 1379 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (((π΄ Xrm (π + π)) + ((ββ((π΄β2) β 1)) Β· (π΄ Yrm (π + π)))) = ((((π΄ Xrm π) Β· (π΄ Xrm π)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π)))) + ((ββ((π΄β2) β 1)) Β· (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π))))) β ((π΄ Xrm (π + π)) = (((π΄ Xrm π) Β· (π΄ Xrm π)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π)))) β§ (π΄ Yrm (π + π)) = (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))))) |
98 | 70, 97 | mpbid 232 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β ((π΄ Xrm (π + π)) = (((π΄ Xrm π) Β· (π΄ Xrm π)) + (((π΄β2) β 1) Β· ((π΄ Yrm π) Β· (π΄ Yrm π)))) β§ (π΄ Yrm (π + π)) = (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π))))) |