Step | Hyp | Ref
| Expression |
1 | | uzuzle23 12870 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β3) β π β
(β€β₯β2)) |
2 | 1 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β π β
(β€β₯β2)) |
3 | | fzss2 13538 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β2) β (1...2) β (1...π)) |
4 | 2, 3 | syl 17 |
. . . . . . . . . 10
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β (1...2) β
(1...π)) |
5 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β π β (1...2)) |
6 | 4, 5 | sseldd 3983 |
. . . . . . . . 9
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β π β (1...π)) |
7 | | fznuz 13580 |
. . . . . . . . . . 11
β’ (π β (1...2) β Β¬
π β
(β€β₯β(2 + 1))) |
8 | 7 | adantl 483 |
. . . . . . . . . 10
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β Β¬ π β
(β€β₯β(2 + 1))) |
9 | | 3z 12592 |
. . . . . . . . . . . . . 14
β’ 3 β
β€ |
10 | | uzid 12834 |
. . . . . . . . . . . . . 14
β’ (3 β
β€ β 3 β (β€β₯β3)) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ 3 β
(β€β₯β3) |
12 | | df-3 12273 |
. . . . . . . . . . . . . 14
β’ 3 = (2 +
1) |
13 | 12 | fveq2i 6892 |
. . . . . . . . . . . . 13
β’
(β€β₯β3) = (β€β₯β(2 +
1)) |
14 | 11, 13 | eleqtri 2832 |
. . . . . . . . . . . 12
β’ 3 β
(β€β₯β(2 + 1)) |
15 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π = 3 β (π β (β€β₯β(2 +
1)) β 3 β (β€β₯β(2 + 1)))) |
16 | 14, 15 | mpbiri 258 |
. . . . . . . . . . 11
β’ (π = 3 β π β (β€β₯β(2 +
1))) |
17 | 16 | necon3bi 2968 |
. . . . . . . . . 10
β’ (Β¬
π β
(β€β₯β(2 + 1)) β π β 3) |
18 | 8, 17 | syl 17 |
. . . . . . . . 9
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β π β 3) |
19 | | axlowdimlem16.1 |
. . . . . . . . . 10
β’ π = ({β¨3, -1β©} βͺ
(((1...π) β {3})
Γ {0})) |
20 | 19 | axlowdimlem9 28198 |
. . . . . . . . 9
β’ ((π β (1...π) β§ π β 3) β (πβπ) = 0) |
21 | 6, 18, 20 | syl2anc 585 |
. . . . . . . 8
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β (πβπ) = 0) |
22 | | elfzuz 13494 |
. . . . . . . . . . . . . 14
β’ (πΌ β (2...(π β 1)) β πΌ β
(β€β₯β2)) |
23 | 22 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β πΌ β
(β€β₯β2)) |
24 | | eluzp1p1 12847 |
. . . . . . . . . . . . 13
β’ (πΌ β
(β€β₯β2) β (πΌ + 1) β
(β€β₯β(2 + 1))) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β (πΌ + 1) β
(β€β₯β(2 + 1))) |
26 | | uzss 12842 |
. . . . . . . . . . . 12
β’ ((πΌ + 1) β
(β€β₯β(2 + 1)) β
(β€β₯β(πΌ + 1)) β
(β€β₯β(2 + 1))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . 11
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β
(β€β₯β(πΌ + 1)) β
(β€β₯β(2 + 1))) |
28 | 27, 8 | ssneldd 3985 |
. . . . . . . . . 10
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β Β¬ π β
(β€β₯β(πΌ + 1))) |
29 | | eluzelz 12829 |
. . . . . . . . . . . . . 14
β’ ((πΌ + 1) β
(β€β₯β(2 + 1)) β (πΌ + 1) β β€) |
30 | 25, 29 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β (πΌ + 1) β β€) |
31 | | uzid 12834 |
. . . . . . . . . . . . 13
β’ ((πΌ + 1) β β€ β
(πΌ + 1) β
(β€β₯β(πΌ + 1))) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β (πΌ + 1) β
(β€β₯β(πΌ + 1))) |
33 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π = (πΌ + 1) β (π β (β€β₯β(πΌ + 1)) β (πΌ + 1) β
(β€β₯β(πΌ + 1)))) |
34 | 32, 33 | syl5ibrcom 246 |
. . . . . . . . . . 11
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β (π = (πΌ + 1) β π β (β€β₯β(πΌ + 1)))) |
35 | 34 | necon3bd 2955 |
. . . . . . . . . 10
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β (Β¬ π β
(β€β₯β(πΌ + 1)) β π β (πΌ + 1))) |
36 | 28, 35 | mpd 15 |
. . . . . . . . 9
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β π β (πΌ + 1)) |
37 | | axlowdimlem16.2 |
. . . . . . . . . 10
β’ π = ({β¨(πΌ + 1), 1β©} βͺ (((1...π) β {(πΌ + 1)}) Γ {0})) |
38 | 37 | axlowdimlem12 28201 |
. . . . . . . . 9
β’ ((π β (1...π) β§ π β (πΌ + 1)) β (πβπ) = 0) |
39 | 6, 36, 38 | syl2anc 585 |
. . . . . . . 8
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β (πβπ) = 0) |
40 | 21, 39 | eqtr4d 2776 |
. . . . . . 7
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β (πβπ) = (πβπ)) |
41 | 40 | oveq1d 7421 |
. . . . . 6
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β ((πβπ) β (π΄βπ)) = ((πβπ) β (π΄βπ))) |
42 | 41 | oveq1d 7421 |
. . . . 5
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...2)) β (((πβπ) β (π΄βπ))β2) = (((πβπ) β (π΄βπ))β2)) |
43 | 42 | sumeq2dv 15646 |
. . . 4
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β Ξ£π β (1...2)(((πβπ) β (π΄βπ))β2) = Ξ£π β (1...2)(((πβπ) β (π΄βπ))β2)) |
44 | 19, 37 | axlowdimlem16 28205 |
. . . . 5
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β Ξ£π β (3...π)((πβπ)β2) = Ξ£π β (3...π)((πβπ)β2)) |
45 | | axlowdimlem17.3 |
. . . . . . . . . . . . 13
β’ π΄ = ({β¨1, πβ©, β¨2, πβ©} βͺ ((3...π) Γ {0})) |
46 | 45 | fveq1i 6890 |
. . . . . . . . . . . 12
β’ (π΄βπ) = (({β¨1, πβ©, β¨2, πβ©} βͺ ((3...π) Γ {0}))βπ) |
47 | | axlowdimlem2 28191 |
. . . . . . . . . . . . 13
β’ ((1...2)
β© (3...π)) =
β
|
48 | | axlowdimlem17.4 |
. . . . . . . . . . . . . . . 16
β’ π β β |
49 | | axlowdimlem17.5 |
. . . . . . . . . . . . . . . 16
β’ π β β |
50 | 48, 49 | axlowdimlem4 28193 |
. . . . . . . . . . . . . . 15
β’ {β¨1,
πβ©, β¨2, πβ©}:(1...2)βΆβ |
51 | | ffn 6715 |
. . . . . . . . . . . . . . 15
β’
({β¨1, πβ©,
β¨2, πβ©}:(1...2)βΆβ β
{β¨1, πβ©, β¨2,
πβ©} Fn
(1...2)) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ {β¨1,
πβ©, β¨2, πβ©} Fn
(1...2) |
53 | | axlowdimlem1 28190 |
. . . . . . . . . . . . . . 15
β’
((3...π) Γ
{0}):(3...π)βΆβ |
54 | | ffn 6715 |
. . . . . . . . . . . . . . 15
β’
(((3...π) Γ
{0}):(3...π)βΆβ
β ((3...π) Γ
{0}) Fn (3...π)) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
((3...π) Γ
{0}) Fn (3...π) |
56 | | fvun2 6981 |
. . . . . . . . . . . . . 14
β’
(({β¨1, πβ©,
β¨2, πβ©} Fn
(1...2) β§ ((3...π)
Γ {0}) Fn (3...π)
β§ (((1...2) β© (3...π)) = β
β§ π β (3...π))) β (({β¨1, πβ©, β¨2, πβ©} βͺ ((3...π) Γ {0}))βπ) = (((3...π) Γ {0})βπ)) |
57 | 52, 55, 56 | mp3an12 1452 |
. . . . . . . . . . . . 13
β’
((((1...2) β© (3...π)) = β
β§ π β (3...π)) β (({β¨1, πβ©, β¨2, πβ©} βͺ ((3...π) Γ {0}))βπ) = (((3...π) Γ {0})βπ)) |
58 | 47, 57 | mpan 689 |
. . . . . . . . . . . 12
β’ (π β (3...π) β (({β¨1, πβ©, β¨2, πβ©} βͺ ((3...π) Γ {0}))βπ) = (((3...π) Γ {0})βπ)) |
59 | 46, 58 | eqtrid 2785 |
. . . . . . . . . . 11
β’ (π β (3...π) β (π΄βπ) = (((3...π) Γ {0})βπ)) |
60 | | c0ex 11205 |
. . . . . . . . . . . 12
β’ 0 β
V |
61 | 60 | fvconst2 7202 |
. . . . . . . . . . 11
β’ (π β (3...π) β (((3...π) Γ {0})βπ) = 0) |
62 | 59, 61 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π β (3...π) β (π΄βπ) = 0) |
63 | 62 | adantl 483 |
. . . . . . . . 9
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (3...π)) β (π΄βπ) = 0) |
64 | 63 | oveq2d 7422 |
. . . . . . . 8
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (3...π)) β ((πβπ) β (π΄βπ)) = ((πβπ) β 0)) |
65 | 19 | axlowdimlem7 28196 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β3) β π β (πΌβπ)) |
66 | 65 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (3...π)) β π β (πΌβπ)) |
67 | | 3nn 12288 |
. . . . . . . . . . . . . 14
β’ 3 β
β |
68 | | nnuz 12862 |
. . . . . . . . . . . . . 14
β’ β =
(β€β₯β1) |
69 | 67, 68 | eleqtri 2832 |
. . . . . . . . . . . . 13
β’ 3 β
(β€β₯β1) |
70 | | fzss1 13537 |
. . . . . . . . . . . . 13
β’ (3 β
(β€β₯β1) β (3...π) β (1...π)) |
71 | 69, 70 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(3...π) β
(1...π) |
72 | 71 | sseli 3978 |
. . . . . . . . . . 11
β’ (π β (3...π) β π β (1...π)) |
73 | 72 | adantl 483 |
. . . . . . . . . 10
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (3...π)) β π β (1...π)) |
74 | | fveecn 28150 |
. . . . . . . . . 10
β’ ((π β (πΌβπ) β§ π β (1...π)) β (πβπ) β β) |
75 | 66, 73, 74 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (3...π)) β (πβπ) β β) |
76 | 75 | subid1d 11557 |
. . . . . . . 8
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (3...π)) β ((πβπ) β 0) = (πβπ)) |
77 | 64, 76 | eqtrd 2773 |
. . . . . . 7
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (3...π)) β ((πβπ) β (π΄βπ)) = (πβπ)) |
78 | 77 | oveq1d 7421 |
. . . . . 6
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (3...π)) β (((πβπ) β (π΄βπ))β2) = ((πβπ)β2)) |
79 | 78 | sumeq2dv 15646 |
. . . . 5
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β Ξ£π β (3...π)(((πβπ) β (π΄βπ))β2) = Ξ£π β (3...π)((πβπ)β2)) |
80 | 63 | oveq2d 7422 |
. . . . . . . 8
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (3...π)) β ((πβπ) β (π΄βπ)) = ((πβπ) β 0)) |
81 | | eluzge3nn 12871 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β3) β π β β) |
82 | | 2eluzge1 12875 |
. . . . . . . . . . . . 13
β’ 2 β
(β€β₯β1) |
83 | | fzss1 13537 |
. . . . . . . . . . . . 13
β’ (2 β
(β€β₯β1) β (2...(π β 1)) β (1...(π β 1))) |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . . . . 12
β’
(2...(π β 1))
β (1...(π β
1)) |
85 | 84 | sseli 3978 |
. . . . . . . . . . 11
β’ (πΌ β (2...(π β 1)) β πΌ β (1...(π β 1))) |
86 | 37 | axlowdimlem10 28199 |
. . . . . . . . . . 11
β’ ((π β β β§ πΌ β (1...(π β 1))) β π β (πΌβπ)) |
87 | 81, 85, 86 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β π β (πΌβπ)) |
88 | | fveecn 28150 |
. . . . . . . . . 10
β’ ((π β (πΌβπ) β§ π β (1...π)) β (πβπ) β β) |
89 | 87, 72, 88 | syl2an 597 |
. . . . . . . . 9
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (3...π)) β (πβπ) β β) |
90 | 89 | subid1d 11557 |
. . . . . . . 8
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (3...π)) β ((πβπ) β 0) = (πβπ)) |
91 | 80, 90 | eqtrd 2773 |
. . . . . . 7
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (3...π)) β ((πβπ) β (π΄βπ)) = (πβπ)) |
92 | 91 | oveq1d 7421 |
. . . . . 6
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (3...π)) β (((πβπ) β (π΄βπ))β2) = ((πβπ)β2)) |
93 | 92 | sumeq2dv 15646 |
. . . . 5
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β Ξ£π β (3...π)(((πβπ) β (π΄βπ))β2) = Ξ£π β (3...π)((πβπ)β2)) |
94 | 44, 79, 93 | 3eqtr4d 2783 |
. . . 4
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β Ξ£π β (3...π)(((πβπ) β (π΄βπ))β2) = Ξ£π β (3...π)(((πβπ) β (π΄βπ))β2)) |
95 | 43, 94 | oveq12d 7424 |
. . 3
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β (Ξ£π β (1...2)(((πβπ) β (π΄βπ))β2) + Ξ£π β (3...π)(((πβπ) β (π΄βπ))β2)) = (Ξ£π β (1...2)(((πβπ) β (π΄βπ))β2) + Ξ£π β (3...π)(((πβπ) β (π΄βπ))β2))) |
96 | 47 | a1i 11 |
. . . 4
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β ((1...2) β©
(3...π)) =
β
) |
97 | | eluzelre 12830 |
. . . . . . . . . 10
β’ (π β
(β€β₯β3) β π β β) |
98 | | eluzle 12832 |
. . . . . . . . . 10
β’ (π β
(β€β₯β3) β 3 β€ π) |
99 | | 2re 12283 |
. . . . . . . . . . . 12
β’ 2 β
β |
100 | | 3re 12289 |
. . . . . . . . . . . 12
β’ 3 β
β |
101 | | 2lt3 12381 |
. . . . . . . . . . . 12
β’ 2 <
3 |
102 | 99, 100, 101 | ltleii 11334 |
. . . . . . . . . . 11
β’ 2 β€
3 |
103 | | letr 11305 |
. . . . . . . . . . . 12
β’ ((2
β β β§ 3 β β β§ π β β) β ((2 β€ 3 β§ 3
β€ π) β 2 β€ π)) |
104 | 99, 100, 103 | mp3an12 1452 |
. . . . . . . . . . 11
β’ (π β β β ((2 β€
3 β§ 3 β€ π) β 2
β€ π)) |
105 | 102, 104 | mpani 695 |
. . . . . . . . . 10
β’ (π β β β (3 β€
π β 2 β€ π)) |
106 | 97, 98, 105 | sylc 65 |
. . . . . . . . 9
β’ (π β
(β€β₯β3) β 2 β€ π) |
107 | | 1le2 12418 |
. . . . . . . . 9
β’ 1 β€
2 |
108 | 106, 107 | jctil 521 |
. . . . . . . 8
β’ (π β
(β€β₯β3) β (1 β€ 2 β§ 2 β€ π)) |
109 | 108 | adantr 482 |
. . . . . . 7
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β (1 β€ 2 β§ 2 β€
π)) |
110 | | eluzelz 12829 |
. . . . . . . . 9
β’ (π β
(β€β₯β3) β π β β€) |
111 | 110 | adantr 482 |
. . . . . . . 8
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β π β β€) |
112 | | 2z 12591 |
. . . . . . . . 9
β’ 2 β
β€ |
113 | | 1z 12589 |
. . . . . . . . 9
β’ 1 β
β€ |
114 | | elfz 13487 |
. . . . . . . . 9
β’ ((2
β β€ β§ 1 β β€ β§ π β β€) β (2 β (1...π) β (1 β€ 2 β§ 2 β€
π))) |
115 | 112, 113,
114 | mp3an12 1452 |
. . . . . . . 8
β’ (π β β€ β (2 β
(1...π) β (1 β€ 2
β§ 2 β€ π))) |
116 | 111, 115 | syl 17 |
. . . . . . 7
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β (2 β (1...π) β (1 β€ 2 β§ 2 β€
π))) |
117 | 109, 116 | mpbird 257 |
. . . . . 6
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β 2 β (1...π)) |
118 | | fzsplit 13524 |
. . . . . 6
β’ (2 β
(1...π) β (1...π) = ((1...2) βͺ ((2 +
1)...π))) |
119 | 117, 118 | syl 17 |
. . . . 5
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β (1...π) = ((1...2) βͺ ((2 + 1)...π))) |
120 | 12 | oveq1i 7416 |
. . . . . 6
β’
(3...π) = ((2 +
1)...π) |
121 | 120 | uneq2i 4160 |
. . . . 5
β’ ((1...2)
βͺ (3...π)) = ((1...2)
βͺ ((2 + 1)...π)) |
122 | 119, 121 | eqtr4di 2791 |
. . . 4
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β (1...π) = ((1...2) βͺ (3...π))) |
123 | | fzfid 13935 |
. . . 4
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β (1...π) β Fin) |
124 | 65 | ad2antrr 725 |
. . . . . . 7
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...π)) β π β (πΌβπ)) |
125 | 124, 74 | sylancom 589 |
. . . . . 6
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...π)) β (πβπ) β β) |
126 | 48, 49 | axlowdimlem5 28194 |
. . . . . . . . . 10
β’ (π β
(β€β₯β2) β ({β¨1, πβ©, β¨2, πβ©} βͺ ((3...π) Γ {0})) β (πΌβπ)) |
127 | 45, 126 | eqeltrid 2838 |
. . . . . . . . 9
β’ (π β
(β€β₯β2) β π΄ β (πΌβπ)) |
128 | 1, 127 | syl 17 |
. . . . . . . 8
β’ (π β
(β€β₯β3) β π΄ β (πΌβπ)) |
129 | 128 | ad2antrr 725 |
. . . . . . 7
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...π)) β π΄ β (πΌβπ)) |
130 | | fveecn 28150 |
. . . . . . 7
β’ ((π΄ β (πΌβπ) β§ π β (1...π)) β (π΄βπ) β β) |
131 | 129, 130 | sylancom 589 |
. . . . . 6
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...π)) β (π΄βπ) β β) |
132 | 125, 131 | subcld 11568 |
. . . . 5
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...π)) β ((πβπ) β (π΄βπ)) β β) |
133 | 132 | sqcld 14106 |
. . . 4
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...π)) β (((πβπ) β (π΄βπ))β2) β β) |
134 | 96, 122, 123, 133 | fsumsplit 15684 |
. . 3
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β Ξ£π β (1...π)(((πβπ) β (π΄βπ))β2) = (Ξ£π β (1...2)(((πβπ) β (π΄βπ))β2) + Ξ£π β (3...π)(((πβπ) β (π΄βπ))β2))) |
135 | 87, 88 | sylan 581 |
. . . . . 6
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...π)) β (πβπ) β β) |
136 | 135, 131 | subcld 11568 |
. . . . 5
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...π)) β ((πβπ) β (π΄βπ)) β β) |
137 | 136 | sqcld 14106 |
. . . 4
β’ (((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β§ π β (1...π)) β (((πβπ) β (π΄βπ))β2) β β) |
138 | 96, 122, 123, 137 | fsumsplit 15684 |
. . 3
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β Ξ£π β (1...π)(((πβπ) β (π΄βπ))β2) = (Ξ£π β (1...2)(((πβπ) β (π΄βπ))β2) + Ξ£π β (3...π)(((πβπ) β (π΄βπ))β2))) |
139 | 95, 134, 138 | 3eqtr4d 2783 |
. 2
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β Ξ£π β (1...π)(((πβπ) β (π΄βπ))β2) = Ξ£π β (1...π)(((πβπ) β (π΄βπ))β2)) |
140 | 65 | adantr 482 |
. . 3
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β π β (πΌβπ)) |
141 | 128 | adantr 482 |
. . 3
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β π΄ β (πΌβπ)) |
142 | | brcgr 28148 |
. . 3
β’ (((π β (πΌβπ) β§ π΄ β (πΌβπ)) β§ (π β (πΌβπ) β§ π΄ β (πΌβπ))) β (β¨π, π΄β©Cgrβ¨π, π΄β© β Ξ£π β (1...π)(((πβπ) β (π΄βπ))β2) = Ξ£π β (1...π)(((πβπ) β (π΄βπ))β2))) |
143 | 140, 141,
87, 141, 142 | syl22anc 838 |
. 2
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β (β¨π, π΄β©Cgrβ¨π, π΄β© β Ξ£π β (1...π)(((πβπ) β (π΄βπ))β2) = Ξ£π β (1...π)(((πβπ) β (π΄βπ))β2))) |
144 | 139, 143 | mpbird 257 |
1
β’ ((π β
(β€β₯β3) β§ πΌ β (2...(π β 1))) β β¨π, π΄β©Cgrβ¨π, π΄β©) |