Step | Hyp | Ref
| Expression |
1 | | fzfi 13884 |
. . . . . 6
β’
(3...π½) β
Fin |
2 | | ssrab2 4042 |
. . . . . 6
β’ {π β (3...π½) β£ Β¬ 2 β₯ π} β (3...π½) |
3 | | ssfi 9124 |
. . . . . 6
β’
(((3...π½) β Fin
β§ {π β (3...π½) β£ Β¬ 2 β₯ π} β (3...π½)) β {π β (3...π½) β£ Β¬ 2 β₯ π} β Fin) |
4 | 1, 2, 3 | mp2an 691 |
. . . . 5
β’ {π β (3...π½) β£ Β¬ 2 β₯ π} β Fin |
5 | 4 | a1i 11 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β {π β (3...π½) β£ Β¬ 2 β₯ π} β Fin) |
6 | | nnnn0 12427 |
. . . . . . . 8
β’ (π½ β β β π½ β
β0) |
7 | 6 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β π½ β
β0) |
8 | 2 | sseli 3945 |
. . . . . . . 8
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β π β (3...π½)) |
9 | | elfzelz 13448 |
. . . . . . . 8
β’ (π β (3...π½) β π β β€) |
10 | 8, 9 | syl 17 |
. . . . . . 7
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β π β β€) |
11 | | bccl 14229 |
. . . . . . 7
β’ ((π½ β β0
β§ π β β€)
β (π½Cπ) β
β0) |
12 | 7, 10, 11 | syl2an 597 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (π½Cπ) β
β0) |
13 | 12 | nn0zd 12532 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (π½Cπ) β β€) |
14 | | simpl1 1192 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β π΄ β
(β€β₯β2)) |
15 | | simpl2 1193 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β π β β€) |
16 | | frmx 41266 |
. . . . . . . . . 10
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
17 | 16 | fovcl 7489 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
18 | 14, 15, 17 | syl2anc 585 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (π΄ Xrm π) β
β0) |
19 | 18 | nn0zd 12532 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (π΄ Xrm π) β β€) |
20 | 8 | adantl 483 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β π β (3...π½)) |
21 | | fznn0sub 13480 |
. . . . . . . 8
β’ (π β (3...π½) β (π½ β π) β
β0) |
22 | 20, 21 | syl 17 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (π½ β π) β
β0) |
23 | | zexpcl 13989 |
. . . . . . 7
β’ (((π΄ Xrm π) β β€ β§ (π½ β π) β β0) β ((π΄ Xrm π)β(π½ β π)) β β€) |
24 | 19, 22, 23 | syl2anc 585 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((π΄ Xrm π)β(π½ β π)) β β€) |
25 | | rmspecnonsq 41259 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β (β β
β»NN)) |
26 | 25 | eldifad 3927 |
. . . . . . . . . 10
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β) |
27 | 26 | nnzd 12533 |
. . . . . . . . 9
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β€) |
28 | 27 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π΄β2) β 1) β
β€) |
29 | | breq2 5114 |
. . . . . . . . . . . . . 14
β’ (π = π β (2 β₯ π β 2 β₯ π)) |
30 | 29 | notbid 318 |
. . . . . . . . . . . . 13
β’ (π = π β (Β¬ 2 β₯ π β Β¬ 2 β₯ π)) |
31 | 30 | elrab 3650 |
. . . . . . . . . . . 12
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β (π β (3...π½) β§ Β¬ 2 β₯ π)) |
32 | 31 | simprbi 498 |
. . . . . . . . . . 11
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β Β¬ 2 β₯ π) |
33 | | 1zzd 12541 |
. . . . . . . . . . 11
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β 1 β β€) |
34 | | n2dvds1 16257 |
. . . . . . . . . . . 12
β’ Β¬ 2
β₯ 1 |
35 | 34 | a1i 11 |
. . . . . . . . . . 11
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β Β¬ 2 β₯ 1) |
36 | | omoe 16253 |
. . . . . . . . . . 11
β’ (((π β β€ β§ Β¬ 2
β₯ π) β§ (1 β
β€ β§ Β¬ 2 β₯ 1)) β 2 β₯ (π β 1)) |
37 | 10, 32, 33, 35, 36 | syl22anc 838 |
. . . . . . . . . 10
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β 2 β₯ (π β 1)) |
38 | | 2z 12542 |
. . . . . . . . . . . 12
β’ 2 β
β€ |
39 | 38 | a1i 11 |
. . . . . . . . . . 11
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β 2 β β€) |
40 | | 2ne0 12264 |
. . . . . . . . . . . 12
β’ 2 β
0 |
41 | 40 | a1i 11 |
. . . . . . . . . . 11
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β 2 β 0) |
42 | | peano2zm 12553 |
. . . . . . . . . . . 12
β’ (π β β€ β (π β 1) β
β€) |
43 | 10, 42 | syl 17 |
. . . . . . . . . . 11
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β (π β 1) β β€) |
44 | | dvdsval2 16146 |
. . . . . . . . . . 11
β’ ((2
β β€ β§ 2 β 0 β§ (π β 1) β β€) β (2 β₯
(π β 1) β
((π β 1) / 2) β
β€)) |
45 | 39, 41, 43, 44 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β (2 β₯ (π β 1) β ((π β 1) / 2) β
β€)) |
46 | 37, 45 | mpbid 231 |
. . . . . . . . 9
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β ((π β 1) / 2) β
β€) |
47 | 43 | zred 12614 |
. . . . . . . . . 10
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β (π β 1) β β) |
48 | | 0red 11165 |
. . . . . . . . . . . . . . 15
β’ (π β (3...π½) β 0 β β) |
49 | | 3re 12240 |
. . . . . . . . . . . . . . . 16
β’ 3 β
β |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β (3...π½) β 3 β β) |
51 | 9 | zred 12614 |
. . . . . . . . . . . . . . 15
β’ (π β (3...π½) β π β β) |
52 | | 3pos 12265 |
. . . . . . . . . . . . . . . 16
β’ 0 <
3 |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β (3...π½) β 0 < 3) |
54 | | elfzle1 13451 |
. . . . . . . . . . . . . . 15
β’ (π β (3...π½) β 3 β€ π) |
55 | 48, 50, 51, 53, 54 | ltletrd 11322 |
. . . . . . . . . . . . . 14
β’ (π β (3...π½) β 0 < π) |
56 | | elnnz 12516 |
. . . . . . . . . . . . . 14
β’ (π β β β (π β β€ β§ 0 <
π)) |
57 | 9, 55, 56 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ (π β (3...π½) β π β β) |
58 | | nnm1nn0 12461 |
. . . . . . . . . . . . 13
β’ (π β β β (π β 1) β
β0) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (3...π½) β (π β 1) β
β0) |
60 | 59 | nn0ge0d 12483 |
. . . . . . . . . . 11
β’ (π β (3...π½) β 0 β€ (π β 1)) |
61 | 8, 60 | syl 17 |
. . . . . . . . . 10
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β 0 β€ (π β 1)) |
62 | | 2re 12234 |
. . . . . . . . . . 11
β’ 2 β
β |
63 | 62 | a1i 11 |
. . . . . . . . . 10
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β 2 β β) |
64 | | 2pos 12263 |
. . . . . . . . . . 11
β’ 0 <
2 |
65 | 64 | a1i 11 |
. . . . . . . . . 10
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β 0 < 2) |
66 | | divge0 12031 |
. . . . . . . . . 10
β’ ((((π β 1) β β β§
0 β€ (π β 1)) β§
(2 β β β§ 0 < 2)) β 0 β€ ((π β 1) / 2)) |
67 | 47, 61, 63, 65, 66 | syl22anc 838 |
. . . . . . . . 9
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β 0 β€ ((π β 1) / 2)) |
68 | | elnn0z 12519 |
. . . . . . . . 9
β’ (((π β 1) / 2) β
β0 β (((π β 1) / 2) β β€ β§ 0 β€
((π β 1) /
2))) |
69 | 46, 67, 68 | sylanbrc 584 |
. . . . . . . 8
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β ((π β 1) / 2) β
β0) |
70 | | zexpcl 13989 |
. . . . . . . 8
β’ ((((π΄β2) β 1) β
β€ β§ ((π β
1) / 2) β β0) β (((π΄β2) β 1)β((π β 1) / 2)) β
β€) |
71 | 28, 69, 70 | syl2an 597 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (((π΄β2) β 1)β((π β 1) / 2)) β
β€) |
72 | | frmy 41267 |
. . . . . . . . . 10
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
73 | 72 | fovcl 7489 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
74 | 14, 15, 73 | syl2anc 585 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (π΄ Yrm π) β β€) |
75 | | elfzel1 13447 |
. . . . . . . . . . . 12
β’ (π β (3...π½) β 3 β β€) |
76 | 9, 75 | zsubcld 12619 |
. . . . . . . . . . 11
β’ (π β (3...π½) β (π β 3) β β€) |
77 | | subge0 11675 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 3 β
β) β (0 β€ (π
β 3) β 3 β€ π)) |
78 | 51, 49, 77 | sylancl 587 |
. . . . . . . . . . . 12
β’ (π β (3...π½) β (0 β€ (π β 3) β 3 β€ π)) |
79 | 54, 78 | mpbird 257 |
. . . . . . . . . . 11
β’ (π β (3...π½) β 0 β€ (π β 3)) |
80 | | elnn0z 12519 |
. . . . . . . . . . 11
β’ ((π β 3) β
β0 β ((π β 3) β β€ β§ 0 β€
(π β
3))) |
81 | 76, 79, 80 | sylanbrc 584 |
. . . . . . . . . 10
β’ (π β (3...π½) β (π β 3) β
β0) |
82 | 8, 81 | syl 17 |
. . . . . . . . 9
β’ (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β (π β 3) β
β0) |
83 | 82 | adantl 483 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (π β 3) β
β0) |
84 | | zexpcl 13989 |
. . . . . . . 8
β’ (((π΄ Yrm π) β β€ β§ (π β 3) β
β0) β ((π΄ Yrm π)β(π β 3)) β β€) |
85 | 74, 83, 84 | syl2anc 585 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((π΄ Yrm π)β(π β 3)) β β€) |
86 | 71, 85 | zmulcld 12620 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))) β
β€) |
87 | 24, 86 | zmulcld 12620 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3)))) β
β€) |
88 | 13, 87 | zmulcld 12620 |
. . . 4
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) β
β€) |
89 | 5, 88 | fsumzcl 15627 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) β
β€) |
90 | 73 | 3adant3 1133 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (π΄ Yrm π) β β€) |
91 | | 3nn0 12438 |
. . . 4
β’ 3 β
β0 |
92 | | zexpcl 13989 |
. . . 4
β’ (((π΄ Yrm π) β β€ β§ 3 β
β0) β ((π΄ Yrm π)β3) β β€) |
93 | 90, 91, 92 | sylancl 587 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π΄ Yrm π)β3) β β€) |
94 | | dvdsmul2 16168 |
. . 3
β’
((Ξ£π β
{π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) β β€ β§ ((π΄ Yrm π)β3) β β€) β
((π΄ Yrm π)β3) β₯ (Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3))) |
95 | 89, 93, 94 | syl2anc 585 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π΄ Yrm π)β3) β₯ (Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3))) |
96 | | jm2.22 41348 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β0) β (π΄ Yrm (π Β· π½)) = Ξ£π β {π β (0...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) /
2)))))) |
97 | 6, 96 | syl3an3 1166 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (π΄ Yrm (π Β· π½)) = Ξ£π β {π β (0...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) /
2)))))) |
98 | | 1lt3 12333 |
. . . . . . . . . . . 12
β’ 1 <
3 |
99 | | 1re 11162 |
. . . . . . . . . . . . 13
β’ 1 β
β |
100 | 99, 49 | ltnlei 11283 |
. . . . . . . . . . . 12
β’ (1 < 3
β Β¬ 3 β€ 1) |
101 | 98, 100 | mpbi 229 |
. . . . . . . . . . 11
β’ Β¬ 3
β€ 1 |
102 | | elfzle1 13451 |
. . . . . . . . . . 11
β’ (1 β
(3...π½) β 3 β€
1) |
103 | 101, 102 | mto 196 |
. . . . . . . . . 10
β’ Β¬ 1
β (3...π½) |
104 | 103 | a1i 11 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β Β¬ 1 β
(3...π½)) |
105 | 104 | intnanrd 491 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β Β¬ (1 β
(3...π½) β§ Β¬ 2
β₯ 1)) |
106 | | breq2 5114 |
. . . . . . . . . 10
β’ (π = 1 β (2 β₯ π β 2 β₯
1)) |
107 | 106 | notbid 318 |
. . . . . . . . 9
β’ (π = 1 β (Β¬ 2 β₯
π β Β¬ 2 β₯
1)) |
108 | 107 | elrab 3650 |
. . . . . . . 8
β’ (1 β
{π β (3...π½) β£ Β¬ 2 β₯ π} β (1 β (3...π½) β§ Β¬ 2 β₯
1)) |
109 | 105, 108 | sylnibr 329 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β Β¬ 1 β
{π β (3...π½) β£ Β¬ 2 β₯ π}) |
110 | | disjsn 4677 |
. . . . . . 7
β’ (({π β (3...π½) β£ Β¬ 2 β₯ π} β© {1}) = β
β Β¬ 1 β
{π β (3...π½) β£ Β¬ 2 β₯ π}) |
111 | 109, 110 | sylibr 233 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ({π β (3...π½) β£ Β¬ 2 β₯ π} β© {1}) = β
) |
112 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β§ π = 1) β π = 1) |
113 | 112 | olcd 873 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β§ π = 1) β ((π β (3...π½) β§ Β¬ 2 β₯ π) β¨ π = 1)) |
114 | | 3z 12543 |
. . . . . . . . . . . . . 14
β’ 3 β
β€ |
115 | 114 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β§ π β 1) β 3 β
β€) |
116 | | nnz 12527 |
. . . . . . . . . . . . . . 15
β’ (π½ β β β π½ β
β€) |
117 | 116 | 3ad2ant3 1136 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β π½ β β€) |
118 | 117 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β§ π β 1) β π½ β β€) |
119 | | elfzelz 13448 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π½) β π β β€) |
120 | 119 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β (0...π½) β§ Β¬ 2 β₯ π) β π β β€) |
121 | 120 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β§ π β 1) β π β β€) |
122 | | elfznn0 13541 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...π½) β π β β0) |
123 | 122 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β (0...π½) β§ Β¬ 2 β₯ π) β π β β0) |
124 | 123 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β§ π β 1) β π β β0) |
125 | | simplrr 777 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β§ π β 1) β Β¬ 2 β₯ π) |
126 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β§ π β 1) β π β 1) |
127 | | elnn1uz2 12857 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π = 1 β¨ π β
(β€β₯β2))) |
128 | | df-ne 2945 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β 1 β Β¬ π = 1) |
129 | 128 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β 1 β Β¬ π = 1) |
130 | 129 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β
Β¬ π =
1) |
131 | 130 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β
(π = 1 β 3 β€ π)) |
132 | 131 | imp 408 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β§ π = 1) β 3 β€ π) |
133 | | uzp1 12811 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯β2) β (π = 2 β¨ π β (β€β₯β(2 +
1)))) |
134 | | 1z 12540 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 1 β
β€ |
135 | | dvdsmul1 16167 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((2
β β€ β§ 1 β β€) β 2 β₯ (2 Β·
1)) |
136 | 38, 134, 135 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 2 β₯
(2 Β· 1) |
137 | | 2t1e2 12323 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (2
Β· 1) = 2 |
138 | 136, 137 | breqtri 5135 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 2 β₯
2 |
139 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = 2 β (2 β₯ π β 2 β₯
2)) |
140 | 139 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β§ π = 2) β (2 β₯ π β 2 β₯
2)) |
141 | 138, 140 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β§ π = 2) β 2 β₯ π) |
142 | | simpl2 1193 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β§ π = 2) β Β¬ 2 β₯
π) |
143 | 141, 142 | pm2.21dd 194 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β§ π = 2) β 3 β€ π) |
144 | | eluzle 12783 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(β€β₯β3) β 3 β€ π) |
145 | | 2p1e3 12302 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (2 + 1) =
3 |
146 | 145 | fveq2i 6850 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(β€β₯β(2 + 1)) =
(β€β₯β3) |
147 | 144, 146 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β
(β€β₯β(2 + 1)) β 3 β€ π) |
148 | 147 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β§ π β
(β€β₯β(2 + 1))) β 3 β€ π) |
149 | 143, 148 | jaodan 957 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β§
(π = 2 β¨ π β
(β€β₯β(2 + 1)))) β 3 β€ π) |
150 | 133, 149 | sylan2 594 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β§ π β
(β€β₯β2)) β 3 β€ π) |
151 | 132, 150 | jaodan 957 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β§
(π = 1 β¨ π β
(β€β₯β2))) β 3 β€ π) |
152 | 127, 151 | sylan2b 595 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β§ π β β) β 3 β€
π) |
153 | | dvds0 16161 |
. . . . . . . . . . . . . . . . . . 19
β’ (2 β
β€ β 2 β₯ 0) |
154 | 38, 153 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β₯
0 |
155 | | breq2 5114 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 0 β (2 β₯ π β 2 β₯
0)) |
156 | 154, 155 | mpbiri 258 |
. . . . . . . . . . . . . . . . 17
β’ (π = 0 β 2 β₯ π) |
157 | 156 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β§ π = 0) β 2 β₯ π) |
158 | | simpl2 1193 |
. . . . . . . . . . . . . . . 16
β’ (((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β§ π = 0) β Β¬ 2 β₯
π) |
159 | 157, 158 | pm2.21dd 194 |
. . . . . . . . . . . . . . 15
β’ (((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β§ π = 0) β 3 β€ π) |
160 | | elnn0 12422 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β (π β β
β¨ π =
0)) |
161 | 160 | biimpi 215 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β (π β β
β¨ π =
0)) |
162 | 161 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β
(π β β β¨
π = 0)) |
163 | 152, 159,
162 | mpjaodan 958 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ Β¬ 2 β₯ π
β§ π β 1) β 3
β€ π) |
164 | 124, 125,
126, 163 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β§ π β 1) β 3 β€ π) |
165 | | elfzle2 13452 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π½) β π β€ π½) |
166 | 165 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β (0...π½) β§ Β¬ 2 β₯ π) β π β€ π½) |
167 | 166 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β§ π β 1) β π β€ π½) |
168 | 115, 118,
121, 164, 167 | elfzd 13439 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β§ π β 1) β π β (3...π½)) |
169 | 168, 125 | jca 513 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β§ π β 1) β (π β (3...π½) β§ Β¬ 2 β₯ π)) |
170 | 169 | orcd 872 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β§ π β 1) β ((π β (3...π½) β§ Β¬ 2 β₯ π) β¨ π = 1)) |
171 | 113, 170 | pm2.61dane 3033 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (0...π½) β§ Β¬ 2 β₯ π)) β ((π β (3...π½) β§ Β¬ 2 β₯ π) β¨ π = 1)) |
172 | | nn0uz 12812 |
. . . . . . . . . . . . . . 15
β’
β0 = (β€β₯β0) |
173 | 91, 172 | eleqtri 2836 |
. . . . . . . . . . . . . 14
β’ 3 β
(β€β₯β0) |
174 | | fzss1 13487 |
. . . . . . . . . . . . . 14
β’ (3 β
(β€β₯β0) β (3...π½) β (0...π½)) |
175 | 173, 174 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
(3...π½) β
(0...π½) |
176 | 175 | sseli 3945 |
. . . . . . . . . . . 12
β’ (π β (3...π½) β π β (0...π½)) |
177 | 176 | anim1i 616 |
. . . . . . . . . . 11
β’ ((π β (3...π½) β§ Β¬ 2 β₯ π) β (π β (0...π½) β§ Β¬ 2 β₯ π)) |
178 | 177 | adantl 483 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ (π β (3...π½) β§ Β¬ 2 β₯ π)) β (π β (0...π½) β§ Β¬ 2 β₯ π)) |
179 | | 0zd 12518 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π = 1) β 0 β
β€) |
180 | 117 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π = 1) β π½ β β€) |
181 | | 1zzd 12541 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π = 1) β 1 β
β€) |
182 | | 0le1 11685 |
. . . . . . . . . . . . 13
β’ 0 β€
1 |
183 | 182 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π = 1) β 0 β€ 1) |
184 | | nnge1 12188 |
. . . . . . . . . . . . . 14
β’ (π½ β β β 1 β€
π½) |
185 | 184 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β 1 β€ π½) |
186 | 185 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π = 1) β 1 β€ π½) |
187 | 179, 180,
181, 183, 186 | elfzd 13439 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π = 1) β 1 β (0...π½)) |
188 | 34 | a1i 11 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π = 1) β Β¬ 2 β₯
1) |
189 | | eleq1 2826 |
. . . . . . . . . . . . 13
β’ (π = 1 β (π β (0...π½) β 1 β (0...π½))) |
190 | | breq2 5114 |
. . . . . . . . . . . . . 14
β’ (π = 1 β (2 β₯ π β 2 β₯
1)) |
191 | 190 | notbid 318 |
. . . . . . . . . . . . 13
β’ (π = 1 β (Β¬ 2 β₯
π β Β¬ 2 β₯
1)) |
192 | 189, 191 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π = 1 β ((π β (0...π½) β§ Β¬ 2 β₯ π) β (1 β (0...π½) β§ Β¬ 2 β₯
1))) |
193 | 192 | adantl 483 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π = 1) β ((π β (0...π½) β§ Β¬ 2 β₯ π) β (1 β (0...π½) β§ Β¬ 2 β₯
1))) |
194 | 187, 188,
193 | mpbir2and 712 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π = 1) β (π β (0...π½) β§ Β¬ 2 β₯ π)) |
195 | 178, 194 | jaodan 957 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ ((π β (3...π½) β§ Β¬ 2 β₯ π) β¨ π = 1)) β (π β (0...π½) β§ Β¬ 2 β₯ π)) |
196 | 171, 195 | impbida 800 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π β (0...π½) β§ Β¬ 2 β₯ π) β ((π β (3...π½) β§ Β¬ 2 β₯ π) β¨ π = 1))) |
197 | 30 | elrab 3650 |
. . . . . . . 8
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β (π β (0...π½) β§ Β¬ 2 β₯ π)) |
198 | | elun 4113 |
. . . . . . . . 9
β’ (π β ({π β (3...π½) β£ Β¬ 2 β₯ π} βͺ {1}) β (π β {π β (3...π½) β£ Β¬ 2 β₯ π} β¨ π β {1})) |
199 | | velsn 4607 |
. . . . . . . . . 10
β’ (π β {1} β π = 1) |
200 | 31, 199 | orbi12i 914 |
. . . . . . . . 9
β’ ((π β {π β (3...π½) β£ Β¬ 2 β₯ π} β¨ π β {1}) β ((π β (3...π½) β§ Β¬ 2 β₯ π) β¨ π = 1)) |
201 | 198, 200 | bitri 275 |
. . . . . . . 8
β’ (π β ({π β (3...π½) β£ Β¬ 2 β₯ π} βͺ {1}) β ((π β (3...π½) β§ Β¬ 2 β₯ π) β¨ π = 1)) |
202 | 196, 197,
201 | 3bitr4g 314 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β π β ({π β (3...π½) β£ Β¬ 2 β₯ π} βͺ {1}))) |
203 | 202 | eqrdv 2735 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β {π β (0...π½) β£ Β¬ 2 β₯ π} = ({π β (3...π½) β£ Β¬ 2 β₯ π} βͺ {1})) |
204 | | fzfi 13884 |
. . . . . . . 8
β’
(0...π½) β
Fin |
205 | | ssrab2 4042 |
. . . . . . . 8
β’ {π β (0...π½) β£ Β¬ 2 β₯ π} β (0...π½) |
206 | | ssfi 9124 |
. . . . . . . 8
β’
(((0...π½) β Fin
β§ {π β (0...π½) β£ Β¬ 2 β₯ π} β (0...π½)) β {π β (0...π½) β£ Β¬ 2 β₯ π} β Fin) |
207 | 204, 205,
206 | mp2an 691 |
. . . . . . 7
β’ {π β (0...π½) β£ Β¬ 2 β₯ π} β Fin |
208 | 207 | a1i 11 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β {π β (0...π½) β£ Β¬ 2 β₯ π} β Fin) |
209 | 205 | sseli 3945 |
. . . . . . . . . 10
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β π β (0...π½)) |
210 | 209, 119 | syl 17 |
. . . . . . . . 9
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β π β β€) |
211 | 7, 210, 11 | syl2an 597 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (0...π½) β£ Β¬ 2 β₯ π}) β (π½Cπ) β
β0) |
212 | 211 | nn0cnd 12482 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (0...π½) β£ Β¬ 2 β₯ π}) β (π½Cπ) β β) |
213 | 17 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (π΄ Xrm π) β
β0) |
214 | 213 | nn0cnd 12482 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (π΄ Xrm π) β β) |
215 | 214 | adantr 482 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (0...π½) β£ Β¬ 2 β₯ π}) β (π΄ Xrm π) β β) |
216 | 209 | adantl 483 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (0...π½) β£ Β¬ 2 β₯ π}) β π β (0...π½)) |
217 | | fznn0sub 13480 |
. . . . . . . . . 10
β’ (π β (0...π½) β (π½ β π) β
β0) |
218 | 216, 217 | syl 17 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (0...π½) β£ Β¬ 2 β₯ π}) β (π½ β π) β
β0) |
219 | 215, 218 | expcld 14058 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (0...π½) β£ Β¬ 2 β₯ π}) β ((π΄ Xrm π)β(π½ β π)) β β) |
220 | 90 | zcnd 12615 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (π΄ Yrm π) β β) |
221 | 209, 122 | syl 17 |
. . . . . . . . . 10
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β π β β0) |
222 | | expcl 13992 |
. . . . . . . . . 10
β’ (((π΄ Yrm π) β β β§ π β β0)
β ((π΄ Yrm
π)βπ) β β) |
223 | 220, 221,
222 | syl2an 597 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (0...π½) β£ Β¬ 2 β₯ π}) β ((π΄ Yrm π)βπ) β β) |
224 | | rmspecpos 41269 |
. . . . . . . . . . . 12
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β+) |
225 | 224 | rpcnd 12966 |
. . . . . . . . . . 11
β’ (π΄ β
(β€β₯β2) β ((π΄β2) β 1) β
β) |
226 | 225 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π΄β2) β 1) β
β) |
227 | 197 | simprbi 498 |
. . . . . . . . . . . . 13
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β Β¬ 2 β₯ π) |
228 | | 1zzd 12541 |
. . . . . . . . . . . . 13
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β 1 β β€) |
229 | 34 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β Β¬ 2 β₯ 1) |
230 | 210, 227,
228, 229, 36 | syl22anc 838 |
. . . . . . . . . . . 12
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β 2 β₯ (π β 1)) |
231 | 38 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β 2 β β€) |
232 | 40 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β 2 β 0) |
233 | 210, 42 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β (π β 1) β β€) |
234 | 231, 232,
233, 44 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β (2 β₯ (π β 1) β ((π β 1) / 2) β
β€)) |
235 | 230, 234 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β ((π β 1) / 2) β
β€) |
236 | 233 | zred 12614 |
. . . . . . . . . . . 12
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β (π β 1) β β) |
237 | 156 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...π½) β (π = 0 β 2 β₯ π)) |
238 | 237 | con3dimp 410 |
. . . . . . . . . . . . . . . 16
β’ ((π β (0...π½) β§ Β¬ 2 β₯ π) β Β¬ π = 0) |
239 | 197, 238 | sylbi 216 |
. . . . . . . . . . . . . . 15
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β Β¬ π = 0) |
240 | 221, 161 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β (π β β β¨ π = 0)) |
241 | | orel2 890 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π = 0 β ((π β β β¨ π = 0) β π β β)) |
242 | 239, 240,
241 | sylc 65 |
. . . . . . . . . . . . . 14
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β π β β) |
243 | 242, 58 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β (π β 1) β
β0) |
244 | 243 | nn0ge0d 12483 |
. . . . . . . . . . . 12
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β 0 β€ (π β 1)) |
245 | 62 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β 2 β β) |
246 | 64 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β 0 < 2) |
247 | 236, 244,
245, 246, 66 | syl22anc 838 |
. . . . . . . . . . 11
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β 0 β€ ((π β 1) / 2)) |
248 | 235, 247,
68 | sylanbrc 584 |
. . . . . . . . . 10
β’ (π β {π β (0...π½) β£ Β¬ 2 β₯ π} β ((π β 1) / 2) β
β0) |
249 | | expcl 13992 |
. . . . . . . . . 10
β’ ((((π΄β2) β 1) β
β β§ ((π β
1) / 2) β β0) β (((π΄β2) β 1)β((π β 1) / 2)) β
β) |
250 | 226, 248,
249 | syl2an 597 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (0...π½) β£ Β¬ 2 β₯ π}) β (((π΄β2) β 1)β((π β 1) / 2)) β
β) |
251 | 223, 250 | mulcld 11182 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (0...π½) β£ Β¬ 2 β₯ π}) β (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) / 2))) β
β) |
252 | 219, 251 | mulcld 11182 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (0...π½) β£ Β¬ 2 β₯ π}) β (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) / 2)))) β
β) |
253 | 212, 252 | mulcld 11182 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (0...π½) β£ Β¬ 2 β₯ π}) β ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) / 2))))) β
β) |
254 | 111, 203,
208, 253 | fsumsplit 15633 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β Ξ£π β {π β (0...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) / 2))))) =
(Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) / 2))))) +
Ξ£π β {1} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) /
2))))))) |
255 | | expcl 13992 |
. . . . . . . . 9
β’ (((π΄ Yrm π) β β β§ 3 β
β0) β ((π΄ Yrm π)β3) β β) |
256 | 220, 91, 255 | sylancl 587 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π΄ Yrm π)β3) β β) |
257 | 88 | zcnd 12615 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) β
β) |
258 | 5, 256, 257 | fsummulc1 15677 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3)) = Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} (((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3))) |
259 | 12 | nn0cnd 12482 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (π½Cπ) β β) |
260 | 214 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (π΄ Xrm π) β β) |
261 | 260, 22 | expcld 14058 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((π΄ Xrm π)β(π½ β π)) β β) |
262 | 226, 69, 249 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (((π΄β2) β 1)β((π β 1) / 2)) β
β) |
263 | | expcl 13992 |
. . . . . . . . . . . . 13
β’ (((π΄ Yrm π) β β β§ (π β 3) β
β0) β ((π΄ Yrm π)β(π β 3)) β β) |
264 | 220, 82, 263 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((π΄ Yrm π)β(π β 3)) β β) |
265 | 262, 264 | mulcld 11182 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))) β
β) |
266 | 261, 265 | mulcld 11182 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3)))) β
β) |
267 | 256 | adantr 482 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((π΄ Yrm π)β3) β β) |
268 | 259, 266,
267 | mulassd 11185 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3)) = ((π½Cπ) Β· ((((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3)))) Β· ((π΄ Yrm π)β3)))) |
269 | 261, 265,
267 | mulassd 11185 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3)))) Β· ((π΄ Yrm π)β3)) = (((π΄ Xrm π)β(π½ β π)) Β· (((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))) Β· ((π΄ Yrm π)β3)))) |
270 | 262, 264,
267 | mulassd 11185 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))) Β· ((π΄ Yrm π)β3)) = ((((π΄β2) β 1)β((π β 1) / 2)) Β·
(((π΄ Yrm π)β(π β 3)) Β· ((π΄ Yrm π)β3)))) |
271 | 264, 267 | mulcld 11182 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (((π΄ Yrm π)β(π β 3)) Β· ((π΄ Yrm π)β3)) β β) |
272 | 262, 271 | mulcomd 11183 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((((π΄β2) β 1)β((π β 1) / 2)) Β·
(((π΄ Yrm π)β(π β 3)) Β· ((π΄ Yrm π)β3))) = ((((π΄ Yrm π)β(π β 3)) Β· ((π΄ Yrm π)β3)) Β· (((π΄β2) β 1)β((π β 1) /
2)))) |
273 | 220 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (π΄ Yrm π) β β) |
274 | 91 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β 3 β
β0) |
275 | 273, 274,
83 | expaddd 14060 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((π΄ Yrm π)β((π β 3) + 3)) = (((π΄ Yrm π)β(π β 3)) Β· ((π΄ Yrm π)β3))) |
276 | 10 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β π β β€) |
277 | 276 | zcnd 12615 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β π β β) |
278 | | 3cn 12241 |
. . . . . . . . . . . . . . . . 17
β’ 3 β
β |
279 | | npcan 11417 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ 3 β
β) β ((π β
3) + 3) = π) |
280 | 277, 278,
279 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((π β 3) + 3) = π) |
281 | 280 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((π΄ Yrm π)β((π β 3) + 3)) = ((π΄ Yrm π)βπ)) |
282 | 275, 281 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (((π΄ Yrm π)β(π β 3)) Β· ((π΄ Yrm π)β3)) = ((π΄ Yrm π)βπ)) |
283 | 282 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((((π΄ Yrm π)β(π β 3)) Β· ((π΄ Yrm π)β3)) Β· (((π΄β2) β 1)β((π β 1) / 2))) = (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) /
2)))) |
284 | 270, 272,
283 | 3eqtrd 2781 |
. . . . . . . . . . . 12
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))) Β· ((π΄ Yrm π)β3)) = (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) /
2)))) |
285 | 284 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (((π΄ Xrm π)β(π½ β π)) Β· (((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))) Β· ((π΄ Yrm π)β3))) = (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) /
2))))) |
286 | 269, 285 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3)))) Β· ((π΄ Yrm π)β3)) = (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) /
2))))) |
287 | 286 | oveq2d 7378 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β ((π½Cπ) Β· ((((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3)))) Β· ((π΄ Yrm π)β3))) = ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) /
2)))))) |
288 | 268, 287 | eqtrd 2777 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β§ π β {π β (3...π½) β£ Β¬ 2 β₯ π}) β (((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3)) = ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) /
2)))))) |
289 | 288 | sumeq2dv 15595 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} (((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3)) = Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) /
2)))))) |
290 | 258, 289 | eqtr2d 2778 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) / 2))))) =
(Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3))) |
291 | | 1nn 12171 |
. . . . . . 7
β’ 1 β
β |
292 | | bccl 14229 |
. . . . . . . . . . 11
β’ ((π½ β β0
β§ 1 β β€) β (π½C1) β
β0) |
293 | 6, 134, 292 | sylancl 587 |
. . . . . . . . . 10
β’ (π½ β β β (π½C1) β
β0) |
294 | 293 | nn0cnd 12482 |
. . . . . . . . 9
β’ (π½ β β β (π½C1) β
β) |
295 | 294 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (π½C1) β β) |
296 | | nnm1nn0 12461 |
. . . . . . . . . . 11
β’ (π½ β β β (π½ β 1) β
β0) |
297 | 296 | 3ad2ant3 1136 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (π½ β 1) β
β0) |
298 | 214, 297 | expcld 14058 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π΄ Xrm π)β(π½ β 1)) β
β) |
299 | | 1nn0 12436 |
. . . . . . . . . . 11
β’ 1 β
β0 |
300 | | expcl 13992 |
. . . . . . . . . . 11
β’ (((π΄ Yrm π) β β β§ 1 β
β0) β ((π΄ Yrm π)β1) β β) |
301 | 220, 299,
300 | sylancl 587 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π΄ Yrm π)β1) β β) |
302 | | 1m1e0 12232 |
. . . . . . . . . . . . . 14
β’ (1
β 1) = 0 |
303 | 302 | oveq1i 7372 |
. . . . . . . . . . . . 13
β’ ((1
β 1) / 2) = (0 / 2) |
304 | | 2cn 12235 |
. . . . . . . . . . . . . 14
β’ 2 β
β |
305 | 304, 40 | div0i 11896 |
. . . . . . . . . . . . 13
β’ (0 / 2) =
0 |
306 | 303, 305 | eqtri 2765 |
. . . . . . . . . . . 12
β’ ((1
β 1) / 2) = 0 |
307 | | 0nn0 12435 |
. . . . . . . . . . . 12
β’ 0 β
β0 |
308 | 306, 307 | eqeltri 2834 |
. . . . . . . . . . 11
β’ ((1
β 1) / 2) β β0 |
309 | | expcl 13992 |
. . . . . . . . . . 11
β’ ((((π΄β2) β 1) β
β β§ ((1 β 1) / 2) β β0) β (((π΄β2) β 1)β((1
β 1) / 2)) β β) |
310 | 226, 308,
309 | sylancl 587 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (((π΄β2) β 1)β((1 β 1) /
2)) β β) |
311 | 301, 310 | mulcld 11182 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2))) β β) |
312 | 298, 311 | mulcld 11182 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (((π΄ Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2)))) β β) |
313 | 295, 312 | mulcld 11182 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π½C1) Β· (((π΄ Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2))))) β β) |
314 | | oveq2 7370 |
. . . . . . . . 9
β’ (π = 1 β (π½Cπ) = (π½C1)) |
315 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = 1 β (π½ β π) = (π½ β 1)) |
316 | 315 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = 1 β ((π΄ Xrm π)β(π½ β π)) = ((π΄ Xrm π)β(π½ β 1))) |
317 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = 1 β ((π΄ Yrm π)βπ) = ((π΄ Yrm π)β1)) |
318 | | oveq1 7369 |
. . . . . . . . . . . . 13
β’ (π = 1 β (π β 1) = (1 β 1)) |
319 | 318 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (π = 1 β ((π β 1) / 2) = ((1 β 1) /
2)) |
320 | 319 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (π = 1 β (((π΄β2) β 1)β((π β 1) / 2)) = (((π΄β2) β 1)β((1
β 1) / 2))) |
321 | 317, 320 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π = 1 β (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) / 2))) = (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1
β 1) / 2)))) |
322 | 316, 321 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = 1 β (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) / 2)))) = (((π΄ Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2))))) |
323 | 314, 322 | oveq12d 7380 |
. . . . . . . 8
β’ (π = 1 β ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) / 2))))) = ((π½C1) Β· (((π΄ Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2)))))) |
324 | 323 | sumsn 15638 |
. . . . . . 7
β’ ((1
β β β§ ((π½C1)
Β· (((π΄
Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2))))) β β) β Ξ£π β {1} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) / 2))))) = ((π½C1) Β· (((π΄ Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2)))))) |
325 | 291, 313,
324 | sylancr 588 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β Ξ£π β {1} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) / 2))))) = ((π½C1) Β· (((π΄ Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2)))))) |
326 | 290, 325 | oveq12d 7380 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) / 2))))) +
Ξ£π β {1} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· (((π΄ Yrm π)βπ) Β· (((π΄β2) β 1)β((π β 1) / 2)))))) =
((Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3)) + ((π½C1) Β· (((π΄ Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2))))))) |
327 | 97, 254, 326 | 3eqtrd 2781 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (π΄ Yrm (π Β· π½)) = ((Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3)) + ((π½C1) Β· (((π΄ Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2))))))) |
328 | | bcn1 14220 |
. . . . . . 7
β’ (π½ β β0
β (π½C1) = π½) |
329 | 7, 328 | syl 17 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (π½C1) = π½) |
330 | 329 | eqcomd 2743 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β π½ = (π½C1)) |
331 | 220 | exp1d 14053 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π΄ Yrm π)β1) = (π΄ Yrm π)) |
332 | 306 | a1i 11 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((1 β 1) / 2)
= 0) |
333 | 332 | oveq2d 7378 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (((π΄β2) β 1)β((1 β 1) /
2)) = (((π΄β2) β
1)β0)) |
334 | 226 | exp0d 14052 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (((π΄β2) β 1)β0) =
1) |
335 | 333, 334 | eqtrd 2777 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (((π΄β2) β 1)β((1 β 1) /
2)) = 1) |
336 | 331, 335 | oveq12d 7380 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2))) = ((π΄ Yrm
π) Β·
1)) |
337 | 220 | mulid1d 11179 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π΄ Yrm π) Β· 1) = (π΄ Yrm π)) |
338 | 336, 337 | eqtr2d 2778 |
. . . . . 6
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (π΄ Yrm π) = (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2)))) |
339 | 338 | oveq2d 7378 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (((π΄ Xrm π)β(π½ β 1)) Β· (π΄ Yrm π)) = (((π΄ Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2))))) |
340 | 330, 339 | oveq12d 7380 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (π½ Β· (((π΄ Xrm π)β(π½ β 1)) Β· (π΄ Yrm π))) = ((π½C1) Β· (((π΄ Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2)))))) |
341 | 327, 340 | oveq12d 7380 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π΄ Yrm (π Β· π½)) β (π½ Β· (((π΄ Xrm π)β(π½ β 1)) Β· (π΄ Yrm π)))) = (((Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3)) + ((π½C1) Β· (((π΄ Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2)))))) β ((π½C1)
Β· (((π΄
Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2))))))) |
342 | 5, 257 | fsumcl 15625 |
. . . . 5
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) β
β) |
343 | 342, 256 | mulcld 11182 |
. . . 4
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3)) β β) |
344 | 343, 313 | pncand 11520 |
. . 3
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β (((Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3)) + ((π½C1) Β· (((π΄ Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2)))))) β ((π½C1)
Β· (((π΄
Xrm π)β(π½ β 1)) Β· (((π΄ Yrm π)β1) Β· (((π΄β2) β 1)β((1 β 1) /
2)))))) = (Ξ£π β
{π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3))) |
345 | 341, 344 | eqtrd 2777 |
. 2
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π΄ Yrm (π Β· π½)) β (π½ Β· (((π΄ Xrm π)β(π½ β 1)) Β· (π΄ Yrm π)))) = (Ξ£π β {π β (3...π½) β£ Β¬ 2 β₯ π} ((π½Cπ) Β· (((π΄ Xrm π)β(π½ β π)) Β· ((((π΄β2) β 1)β((π β 1) / 2)) Β·
((π΄ Yrm π)β(π β 3))))) Β· ((π΄ Yrm π)β3))) |
346 | 95, 345 | breqtrrd 5138 |
1
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π½ β β) β ((π΄ Yrm π)β3) β₯ ((π΄ Yrm (π Β· π½)) β (π½ Β· (((π΄ Xrm π)β(π½ β 1)) Β· (π΄ Yrm π))))) |