Step | Hyp | Ref
| Expression |
1 | | eulerpartlems.r |
. . . . . 6
β’ π
= {π β£ (β‘π β β) β
Fin} |
2 | | eulerpartlems.s |
. . . . . 6
β’ π = (π β ((β0
βm β) β© π
) β¦ Ξ£π β β ((πβπ) Β· π)) |
3 | 1, 2 | eulerpartlemsf 33915 |
. . . . 5
β’ π:((β0
βm β) β© π
)βΆβ0 |
4 | 3 | ffvelcdmi 7087 |
. . . 4
β’ (π΄ β ((β0
βm β) β© π
) β (πβπ΄) β
β0) |
5 | | nndiffz1 32538 |
. . . . 5
β’ ((πβπ΄) β β0 β (β
β (1...(πβπ΄))) =
(β€β₯β((πβπ΄) + 1))) |
6 | 5 | eleq2d 2814 |
. . . 4
β’ ((πβπ΄) β β0 β (π‘ β (β β
(1...(πβπ΄))) β π‘ β (β€β₯β((πβπ΄) + 1)))) |
7 | 4, 6 | syl 17 |
. . 3
β’ (π΄ β ((β0
βm β) β© π
) β (π‘ β (β β (1...(πβπ΄))) β π‘ β (β€β₯β((πβπ΄) + 1)))) |
8 | 7 | pm5.32i 574 |
. 2
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β (π΄ β ((β0
βm β) β© π
) β§ π‘ β (β€β₯β((πβπ΄) + 1)))) |
9 | | simpr 484 |
. . . . . 6
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β π‘ β (β β (1...(πβπ΄)))) |
10 | | eldif 3954 |
. . . . . 6
β’ (π‘ β (β β
(1...(πβπ΄))) β (π‘ β β β§ Β¬ π‘ β (1...(πβπ΄)))) |
11 | 9, 10 | sylib 217 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β (π‘ β β β§ Β¬ π‘ β (1...(πβπ΄)))) |
12 | 11 | simpld 494 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β π‘ β β) |
13 | 1, 2 | eulerpartlemelr 33913 |
. . . . . 6
β’ (π΄ β ((β0
βm β) β© π
) β (π΄:ββΆβ0 β§
(β‘π΄ β β) β
Fin)) |
14 | 13 | simpld 494 |
. . . . 5
β’ (π΄ β ((β0
βm β) β© π
) β π΄:ββΆβ0) |
15 | 14 | ffvelcdmda 7088 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β β) β (π΄βπ‘) β
β0) |
16 | 12, 15 | syldan 590 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β (π΄βπ‘) β
β0) |
17 | | simpl 482 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β π΄ β ((β0
βm β) β© π
)) |
18 | 4 | adantr 480 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β (πβπ΄) β
β0) |
19 | 11 | simprd 495 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β Β¬ π‘ β (1...(πβπ΄))) |
20 | | simpl 482 |
. . . . . . . . . 10
β’ ((π‘ β β β§ (πβπ΄) β β0) β π‘ β
β) |
21 | | nnuz 12887 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
22 | 20, 21 | eleqtrdi 2838 |
. . . . . . . . 9
β’ ((π‘ β β β§ (πβπ΄) β β0) β π‘ β
(β€β₯β1)) |
23 | | simpr 484 |
. . . . . . . . . 10
β’ ((π‘ β β β§ (πβπ΄) β β0) β (πβπ΄) β
β0) |
24 | 23 | nn0zd 12606 |
. . . . . . . . 9
β’ ((π‘ β β β§ (πβπ΄) β β0) β (πβπ΄) β β€) |
25 | | elfz5 13517 |
. . . . . . . . 9
β’ ((π‘ β
(β€β₯β1) β§ (πβπ΄) β β€) β (π‘ β (1...(πβπ΄)) β π‘ β€ (πβπ΄))) |
26 | 22, 24, 25 | syl2anc 583 |
. . . . . . . 8
β’ ((π‘ β β β§ (πβπ΄) β β0) β (π‘ β (1...(πβπ΄)) β π‘ β€ (πβπ΄))) |
27 | 26 | notbid 318 |
. . . . . . 7
β’ ((π‘ β β β§ (πβπ΄) β β0) β (Β¬
π‘ β (1...(πβπ΄)) β Β¬ π‘ β€ (πβπ΄))) |
28 | 23 | nn0red 12555 |
. . . . . . . 8
β’ ((π‘ β β β§ (πβπ΄) β β0) β (πβπ΄) β β) |
29 | 20 | nnred 12249 |
. . . . . . . 8
β’ ((π‘ β β β§ (πβπ΄) β β0) β π‘ β
β) |
30 | 28, 29 | ltnled 11383 |
. . . . . . 7
β’ ((π‘ β β β§ (πβπ΄) β β0) β ((πβπ΄) < π‘ β Β¬ π‘ β€ (πβπ΄))) |
31 | 27, 30 | bitr4d 282 |
. . . . . 6
β’ ((π‘ β β β§ (πβπ΄) β β0) β (Β¬
π‘ β (1...(πβπ΄)) β (πβπ΄) < π‘)) |
32 | 31 | biimpa 476 |
. . . . 5
β’ (((π‘ β β β§ (πβπ΄) β β0) β§ Β¬
π‘ β (1...(πβπ΄))) β (πβπ΄) < π‘) |
33 | 12, 18, 19, 32 | syl21anc 837 |
. . . 4
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β (πβπ΄) < π‘) |
34 | 1, 2 | eulerpartlemsv1 33912 |
. . . . . . . . . 10
β’ (π΄ β ((β0
βm β) β© π
) β (πβπ΄) = Ξ£π β β ((π΄βπ) Β· π)) |
35 | | fveq2 6891 |
. . . . . . . . . . . 12
β’ (π = π‘ β (π΄βπ) = (π΄βπ‘)) |
36 | | id 22 |
. . . . . . . . . . . 12
β’ (π = π‘ β π = π‘) |
37 | 35, 36 | oveq12d 7432 |
. . . . . . . . . . 11
β’ (π = π‘ β ((π΄βπ) Β· π) = ((π΄βπ‘) Β· π‘)) |
38 | 37 | cbvsumv 15666 |
. . . . . . . . . 10
β’
Ξ£π β
β ((π΄βπ) Β· π) = Ξ£π‘ β β ((π΄βπ‘) Β· π‘) |
39 | 34, 38 | eqtr2di 2784 |
. . . . . . . . 9
β’ (π΄ β ((β0
βm β) β© π
) β Ξ£π‘ β β ((π΄βπ‘) Β· π‘) = (πβπ΄)) |
40 | | breq2 5146 |
. . . . . . . . . . . . 13
β’ (π‘ = π β ((πβπ΄) < π‘ β (πβπ΄) < π)) |
41 | | fveq2 6891 |
. . . . . . . . . . . . . 14
β’ (π‘ = π β (π΄βπ‘) = (π΄βπ)) |
42 | 41 | breq2d 5154 |
. . . . . . . . . . . . 13
β’ (π‘ = π β (0 < (π΄βπ‘) β 0 < (π΄βπ))) |
43 | 40, 42 | anbi12d 630 |
. . . . . . . . . . . 12
β’ (π‘ = π β (((πβπ΄) < π‘ β§ 0 < (π΄βπ‘)) β ((πβπ΄) < π β§ 0 < (π΄βπ)))) |
44 | 43 | cbvrexvw 3230 |
. . . . . . . . . . 11
β’
(βπ‘ β
β ((πβπ΄) < π‘ β§ 0 < (π΄βπ‘)) β βπ β β ((πβπ΄) < π β§ 0 < (π΄βπ))) |
45 | 4 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((π΄ β ((β0
βm β) β© π
) β§ βπ β β ((πβπ΄) < π β§ 0 < (π΄βπ))) β (πβπ΄) β
β0) |
46 | 45 | nn0red 12555 |
. . . . . . . . . . . . 13
β’ ((π΄ β ((β0
βm β) β© π
) β§ βπ β β ((πβπ΄) < π β§ 0 < (π΄βπ))) β (πβπ΄) β β) |
47 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β (πβπ΄) β
β0) |
48 | 47 | nn0red 12555 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β (πβπ΄) β β) |
49 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β π β β) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β π β β) |
51 | 50 | nnred 12249 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β π β β) |
52 | | 1zzd 12615 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β 1 β
β€) |
53 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ π‘ β β) β π΄:ββΆβ0) |
54 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ π‘ β β) β π‘ β β) |
55 | | eqidd 2728 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄:ββΆβ0 β§
π‘ β β) β
(π β β β¦
((π΄βπ) Β· π)) = (π β β β¦ ((π΄βπ) Β· π))) |
56 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΄:ββΆβ0 β§
π‘ β β) β§
π = π‘) β π = π‘) |
57 | 56 | fveq2d 6895 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΄:ββΆβ0 β§
π‘ β β) β§
π = π‘) β (π΄βπ) = (π΄βπ‘)) |
58 | 57, 56 | oveq12d 7432 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄:ββΆβ0 β§
π‘ β β) β§
π = π‘) β ((π΄βπ) Β· π) = ((π΄βπ‘) Β· π‘)) |
59 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄:ββΆβ0 β§
π‘ β β) β
π‘ β
β) |
60 | | ffvelcdm 7085 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄:ββΆβ0 β§
π‘ β β) β
(π΄βπ‘) β
β0) |
61 | 59 | nnnn0d 12554 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄:ββΆβ0 β§
π‘ β β) β
π‘ β
β0) |
62 | 60, 61 | nn0mulcld 12559 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄:ββΆβ0 β§
π‘ β β) β
((π΄βπ‘) Β· π‘) β
β0) |
63 | 55, 58, 59, 62 | fvmptd 7006 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄:ββΆβ0 β§
π‘ β β) β
((π β β β¦
((π΄βπ) Β· π))βπ‘) = ((π΄βπ‘) Β· π‘)) |
64 | 53, 54, 63 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ π‘ β β) β ((π β β β¦ ((π΄βπ) Β· π))βπ‘) = ((π΄βπ‘) Β· π‘)) |
65 | 14 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β π΄:ββΆβ0) |
66 | 65 | ffvelcdmda 7088 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ π‘ β β) β (π΄βπ‘) β
β0) |
67 | 54 | nnnn0d 12554 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ π‘ β β) β π‘ β β0) |
68 | 66, 67 | nn0mulcld 12559 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ π‘ β β) β ((π΄βπ‘) Β· π‘) β
β0) |
69 | 68 | nn0red 12555 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ π‘ β β) β ((π΄βπ‘) Β· π‘) β β) |
70 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π‘ β (π΄βπ) = (π΄βπ‘)) |
71 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π‘ β π = π‘) |
72 | 70, 71 | oveq12d 7432 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π‘ β ((π΄βπ) Β· π) = ((π΄βπ‘) Β· π‘)) |
73 | 72 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β¦ ((π΄βπ) Β· π)) = (π‘ β β β¦ ((π΄βπ‘) Β· π‘)) |
74 | 68, 73 | fmptd 7118 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β (π β β β¦ ((π΄βπ) Β· π)):ββΆβ0) |
75 | | nn0sscn 12499 |
. . . . . . . . . . . . . . . . . . 19
β’
β0 β β |
76 | | fss 6733 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β¦ ((π΄βπ) Β· π)):ββΆβ0 β§
β0 β β) β (π β β β¦ ((π΄βπ) Β· π)):ββΆβ) |
77 | 74, 75, 76 | sylancl 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β (π β β β¦ ((π΄βπ) Β· π)):ββΆβ) |
78 | | nnex 12240 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β
β V |
79 | | 0nn0 12509 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 β
β0 |
80 | | eqid 2727 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β
β {0}) = (β β {0}) |
81 | 80 | ffs2 32494 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((β
β V β§ 0 β β0 β§ (π β β β¦ ((π΄βπ) Β· π)):ββΆβ) β ((π β β β¦ ((π΄βπ) Β· π)) supp 0) = (β‘(π β β β¦ ((π΄βπ) Β· π)) β (β β
{0}))) |
82 | 78, 79, 81 | mp3an12 1448 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β¦ ((π΄βπ) Β· π)):ββΆβ β ((π β β β¦ ((π΄βπ) Β· π)) supp 0) = (β‘(π β β β¦ ((π΄βπ) Β· π)) β (β β
{0}))) |
83 | 77, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β ((π β β β¦ ((π΄βπ) Β· π)) supp 0) = (β‘(π β β β¦ ((π΄βπ) Β· π)) β (β β
{0}))) |
84 | | fcdmnn0supp 12550 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((β
β V β§ π΄:ββΆβ0) β
(π΄ supp 0) = (β‘π΄ β β)) |
85 | 78, 65, 84 | sylancr 586 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β (π΄ supp 0) = (β‘π΄ β β)) |
86 | 13 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄ β ((β0
βm β) β© π
) β (β‘π΄ β β) β
Fin) |
87 | 86 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β (β‘π΄ β β) β
Fin) |
88 | 85, 87 | eqeltrd 2828 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β (π΄ supp 0) β Fin) |
89 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄:ββΆβ0 β
β β V) |
90 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄:ββΆβ0 β 0
β β0) |
91 | | ffn 6716 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΄:ββΆβ0 β
π΄ Fn
β) |
92 | | simp3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π΄:ββΆβ0 β§
π‘ β β β§
(π΄βπ‘) = 0) β (π΄βπ‘) = 0) |
93 | 92 | oveq1d 7429 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π΄:ββΆβ0 β§
π‘ β β β§
(π΄βπ‘) = 0) β ((π΄βπ‘) Β· π‘) = (0 Β· π‘)) |
94 | | simp2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π΄:ββΆβ0 β§
π‘ β β β§
(π΄βπ‘) = 0) β π‘ β β) |
95 | 94 | nncnd 12250 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π΄:ββΆβ0 β§
π‘ β β β§
(π΄βπ‘) = 0) β π‘ β β) |
96 | 95 | mul02d 11434 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π΄:ββΆβ0 β§
π‘ β β β§
(π΄βπ‘) = 0) β (0 Β· π‘) = 0) |
97 | 93, 96 | eqtrd 2767 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄:ββΆβ0 β§
π‘ β β β§
(π΄βπ‘) = 0) β ((π΄βπ‘) Β· π‘) = 0) |
98 | 73, 89, 90, 91, 97 | suppss3 32490 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π΄:ββΆβ0 β
((π β β β¦
((π΄βπ) Β· π)) supp 0) β (π΄ supp 0)) |
99 | 65, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β ((π β β β¦ ((π΄βπ) Β· π)) supp 0) β (π΄ supp 0)) |
100 | | ssfi 9189 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΄ supp 0) β Fin β§
((π β β β¦
((π΄βπ) Β· π)) supp 0) β (π΄ supp 0)) β ((π β β β¦ ((π΄βπ) Β· π)) supp 0) β Fin) |
101 | 88, 99, 100 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β ((π β β β¦ ((π΄βπ) Β· π)) supp 0) β Fin) |
102 | 83, 101 | eqeltrrd 2829 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β (β‘(π β β β¦ ((π΄βπ) Β· π)) β (β β {0})) β
Fin) |
103 | 21, 52, 77, 102 | fsumcvg4 33487 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β seq1( + , (π β β β¦ ((π΄βπ) Β· π))) β dom β ) |
104 | 21, 52, 64, 69, 103 | isumrecl 15735 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β Ξ£π‘ β β ((π΄βπ‘) Β· π‘) β β) |
105 | 104 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β Ξ£π‘ β β ((π΄βπ‘) Β· π‘) β β) |
106 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β (πβπ΄) < π) |
107 | 14 | ffvelcdmda 7088 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β (π΄βπ) β
β0) |
108 | 107 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β (π΄βπ) β
β0) |
109 | 108 | nn0red 12555 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β (π΄βπ) β β) |
110 | 109, 51 | remulcld 11266 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β ((π΄βπ) Β· π) β β) |
111 | 50 | nnnn0d 12554 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β π β β0) |
112 | 111 | nn0ge0d 12557 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β 0 β€ π) |
113 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β 0 < (π΄βπ)) |
114 | | elnnnn0b 12538 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄βπ) β β β ((π΄βπ) β β0 β§ 0 <
(π΄βπ))) |
115 | | nnge1 12262 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄βπ) β β β 1 β€ (π΄βπ)) |
116 | 114, 115 | sylbir 234 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄βπ) β β0 β§ 0 <
(π΄βπ)) β 1 β€ (π΄βπ)) |
117 | 108, 113,
116 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β 1 β€ (π΄βπ)) |
118 | 51, 109, 112, 117 | lemulge12d 12174 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β π β€ ((π΄βπ) Β· π)) |
119 | 107 | nn0cnd 12556 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β (π΄βπ) β β) |
120 | 49 | nncnd 12250 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β π β β) |
121 | 119, 120 | mulcld 11256 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β ((π΄βπ) Β· π) β β) |
122 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ = π β π‘ = π) |
123 | 41, 122 | oveq12d 7432 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π‘ = π β ((π΄βπ‘) Β· π‘) = ((π΄βπ) Β· π)) |
124 | 123 | sumsn 15716 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ ((π΄βπ) Β· π) β β) β Ξ£π‘ β {π} ((π΄βπ‘) Β· π‘) = ((π΄βπ) Β· π)) |
125 | 49, 121, 124 | syl2anc 583 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β Ξ£π‘ β {π} ((π΄βπ‘) Β· π‘) = ((π΄βπ) Β· π)) |
126 | | snfi 9060 |
. . . . . . . . . . . . . . . . . . . 20
β’ {π} β Fin |
127 | 126 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β {π} β Fin) |
128 | 49 | snssd 4808 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β {π} β β) |
129 | 68 | nn0ge0d 12557 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ π‘ β β) β 0 β€ ((π΄βπ‘) Β· π‘)) |
130 | 21, 52, 127, 128, 64, 69, 129, 103 | isumless 15815 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β Ξ£π‘ β {π} ((π΄βπ‘) Β· π‘) β€ Ξ£π‘ β β ((π΄βπ‘) Β· π‘)) |
131 | 125, 130 | eqbrtrrd 5166 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β ((β0
βm β) β© π
) β§ π β β) β ((π΄βπ) Β· π) β€ Ξ£π‘ β β ((π΄βπ‘) Β· π‘)) |
132 | 131 | adantr 480 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β ((π΄βπ) Β· π) β€ Ξ£π‘ β β ((π΄βπ‘) Β· π‘)) |
133 | 51, 110, 105, 118, 132 | letrd 11393 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β π β€ Ξ£π‘ β β ((π΄βπ‘) Β· π‘)) |
134 | 48, 51, 105, 106, 133 | ltletrd 11396 |
. . . . . . . . . . . . . 14
β’ (((π΄ β ((β0
βm β) β© π
) β§ π β β) β§ ((πβπ΄) < π β§ 0 < (π΄βπ))) β (πβπ΄) < Ξ£π‘ β β ((π΄βπ‘) Β· π‘)) |
135 | 134 | r19.29an 3153 |
. . . . . . . . . . . . 13
β’ ((π΄ β ((β0
βm β) β© π
) β§ βπ β β ((πβπ΄) < π β§ 0 < (π΄βπ))) β (πβπ΄) < Ξ£π‘ β β ((π΄βπ‘) Β· π‘)) |
136 | 46, 135 | gtned 11371 |
. . . . . . . . . . . 12
β’ ((π΄ β ((β0
βm β) β© π
) β§ βπ β β ((πβπ΄) < π β§ 0 < (π΄βπ))) β Ξ£π‘ β β ((π΄βπ‘) Β· π‘) β (πβπ΄)) |
137 | 136 | ex 412 |
. . . . . . . . . . 11
β’ (π΄ β ((β0
βm β) β© π
) β (βπ β β ((πβπ΄) < π β§ 0 < (π΄βπ)) β Ξ£π‘ β β ((π΄βπ‘) Β· π‘) β (πβπ΄))) |
138 | 44, 137 | biimtrid 241 |
. . . . . . . . . 10
β’ (π΄ β ((β0
βm β) β© π
) β (βπ‘ β β ((πβπ΄) < π‘ β§ 0 < (π΄βπ‘)) β Ξ£π‘ β β ((π΄βπ‘) Β· π‘) β (πβπ΄))) |
139 | 138 | necon2bd 2951 |
. . . . . . . . 9
β’ (π΄ β ((β0
βm β) β© π
) β (Ξ£π‘ β β ((π΄βπ‘) Β· π‘) = (πβπ΄) β Β¬ βπ‘ β β ((πβπ΄) < π‘ β§ 0 < (π΄βπ‘)))) |
140 | 39, 139 | mpd 15 |
. . . . . . . 8
β’ (π΄ β ((β0
βm β) β© π
) β Β¬ βπ‘ β β ((πβπ΄) < π‘ β§ 0 < (π΄βπ‘))) |
141 | | ralnex 3067 |
. . . . . . . 8
β’
(βπ‘ β
β Β¬ ((πβπ΄) < π‘ β§ 0 < (π΄βπ‘)) β Β¬ βπ‘ β β ((πβπ΄) < π‘ β§ 0 < (π΄βπ‘))) |
142 | 140, 141 | sylibr 233 |
. . . . . . 7
β’ (π΄ β ((β0
βm β) β© π
) β βπ‘ β β Β¬ ((πβπ΄) < π‘ β§ 0 < (π΄βπ‘))) |
143 | | imnan 399 |
. . . . . . . 8
β’ (((πβπ΄) < π‘ β Β¬ 0 < (π΄βπ‘)) β Β¬ ((πβπ΄) < π‘ β§ 0 < (π΄βπ‘))) |
144 | 143 | ralbii 3088 |
. . . . . . 7
β’
(βπ‘ β
β ((πβπ΄) < π‘ β Β¬ 0 < (π΄βπ‘)) β βπ‘ β β Β¬ ((πβπ΄) < π‘ β§ 0 < (π΄βπ‘))) |
145 | 142, 144 | sylibr 233 |
. . . . . 6
β’ (π΄ β ((β0
βm β) β© π
) β βπ‘ β β ((πβπ΄) < π‘ β Β¬ 0 < (π΄βπ‘))) |
146 | 145 | r19.21bi 3243 |
. . . . 5
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β β) β ((πβπ΄) < π‘ β Β¬ 0 < (π΄βπ‘))) |
147 | 146 | imp 406 |
. . . 4
β’ (((π΄ β ((β0
βm β) β© π
) β§ π‘ β β) β§ (πβπ΄) < π‘) β Β¬ 0 < (π΄βπ‘)) |
148 | 17, 12, 33, 147 | syl21anc 837 |
. . 3
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β Β¬ 0 < (π΄βπ‘)) |
149 | | nn0re 12503 |
. . . . . 6
β’ ((π΄βπ‘) β β0 β (π΄βπ‘) β β) |
150 | | 0red 11239 |
. . . . . 6
β’ ((π΄βπ‘) β β0 β 0 β
β) |
151 | 149, 150 | lenltd 11382 |
. . . . 5
β’ ((π΄βπ‘) β β0 β ((π΄βπ‘) β€ 0 β Β¬ 0 < (π΄βπ‘))) |
152 | | nn0le0eq0 12522 |
. . . . 5
β’ ((π΄βπ‘) β β0 β ((π΄βπ‘) β€ 0 β (π΄βπ‘) = 0)) |
153 | 151, 152 | bitr3d 281 |
. . . 4
β’ ((π΄βπ‘) β β0 β (Β¬ 0
< (π΄βπ‘) β (π΄βπ‘) = 0)) |
154 | 153 | biimpa 476 |
. . 3
β’ (((π΄βπ‘) β β0 β§ Β¬ 0
< (π΄βπ‘)) β (π΄βπ‘) = 0) |
155 | 16, 148, 154 | syl2anc 583 |
. 2
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β β (1...(πβπ΄)))) β (π΄βπ‘) = 0) |
156 | 8, 155 | sylbir 234 |
1
β’ ((π΄ β ((β0
βm β) β© π
) β§ π‘ β (β€β₯β((πβπ΄) + 1))) β (π΄βπ‘) = 0) |