Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . . 4
β’ (β€
β (1...π) β
Fin) |
2 | | fzfi 13884 |
. . . . . 6
β’
(0...π) β
Fin |
3 | | snfi 8995 |
. . . . . 6
β’ {0}
β Fin |
4 | 2, 3 | ifcli 4538 |
. . . . 5
β’ if(π₯ β (1...π), (0...π), {0}) β Fin |
5 | 4 | a1i 11 |
. . . 4
β’
((β€ β§ π₯
β β) β if(π₯
β (1...π), (0...π), {0}) β
Fin) |
6 | | eldifn 4092 |
. . . . . 6
β’ (π₯ β (β β
(1...π)) β Β¬ π₯ β (1...π)) |
7 | 6 | adantl 483 |
. . . . 5
β’
((β€ β§ π₯
β (β β (1...π))) β Β¬ π₯ β (1...π)) |
8 | | iffalse 4500 |
. . . . 5
β’ (Β¬
π₯ β (1...π) β if(π₯ β (1...π), (0...π), {0}) = {0}) |
9 | | eqimss 4005 |
. . . . 5
β’ (if(π₯ β (1...π), (0...π), {0}) = {0} β if(π₯ β (1...π), (0...π), {0}) β {0}) |
10 | 7, 8, 9 | 3syl 18 |
. . . 4
β’
((β€ β§ π₯
β (β β (1...π))) β if(π₯ β (1...π), (0...π), {0}) β {0}) |
11 | 1, 5, 10 | ixpfi2 9301 |
. . 3
β’ (β€
β Xπ₯ β β if(π₯ β (1...π), (0...π), {0}) β Fin) |
12 | 11 | mptru 1549 |
. 2
β’ Xπ₯ β
β if(π₯ β
(1...π), (0...π), {0}) β
Fin |
13 | | eulerpart.p |
. . . . 5
β’ π = {π β (β0
βm β) β£ ((β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π)} |
14 | 13 | eulerpartleme 33003 |
. . . 4
β’ (π β π β (π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π)) |
15 | | ffn 6673 |
. . . . . 6
β’ (π:ββΆβ0 β
π Fn
β) |
16 | 15 | 3ad2ant1 1134 |
. . . . 5
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β π Fn β) |
17 | | ffvelcdm 7037 |
. . . . . . . . . . . . 13
β’ ((π:ββΆβ0 β§
π₯ β β) β
(πβπ₯) β
β0) |
18 | 17 | 3ad2antl1 1186 |
. . . . . . . . . . . 12
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (πβπ₯) β
β0) |
19 | 18 | nn0red 12481 |
. . . . . . . . . . 11
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (πβπ₯) β β) |
20 | | nnre 12167 |
. . . . . . . . . . . . 13
β’ (π₯ β β β π₯ β
β) |
21 | 20 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β π₯ β β) |
22 | 19, 21 | remulcld 11192 |
. . . . . . . . . . 11
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β ((πβπ₯) Β· π₯) β β) |
23 | | cnvimass 6038 |
. . . . . . . . . . . . . . . . . 18
β’ (β‘π β β) β dom π |
24 | | fdm 6682 |
. . . . . . . . . . . . . . . . . . 19
β’ (π:ββΆβ0 β
dom π =
β) |
25 | 24 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β dom
π =
β) |
26 | 23, 25 | sseqtrid 4001 |
. . . . . . . . . . . . . . . . 17
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β (β‘π β β) β
β) |
27 | 26 | sselda 3949 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π β (β‘π β β)) β π β β) |
28 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π:ββΆβ0 β§
π β β) β
(πβπ) β
β0) |
29 | 28 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π β β) β (πβπ) β
β0) |
30 | 27, 29 | syldan 592 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π β (β‘π β β)) β (πβπ) β
β0) |
31 | 27 | nnnn0d 12480 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π β (β‘π β β)) β π β β0) |
32 | 30, 31 | nn0mulcld 12485 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π β (β‘π β β)) β ((πβπ) Β· π) β
β0) |
33 | 32 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . 17
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π β (β‘π β β)) β ((πβπ) Β· π) β β) |
34 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β π:ββΆβ0) |
35 | | nnex 12166 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ β
β V |
36 | | fcdmnn0supp 12476 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((β
β V β§ π:ββΆβ0) β
(π supp 0) = (β‘π β β)) |
37 | 35, 36 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π:ββΆβ0 β
(π supp 0) = (β‘π β β)) |
38 | 37 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β (π supp 0) = (β‘π β β)) |
39 | | eqimss 4005 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π supp 0) = (β‘π β β) β (π supp 0) β (β‘π β β)) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β (π supp 0) β (β‘π β β)) |
41 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β β
β V) |
42 | | 0nn0 12435 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 β
β0 |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β 0 β
β0) |
44 | 34, 40, 41, 43 | suppssr 8132 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π β (β β (β‘π β β))) β (πβπ) = 0) |
45 | 44 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π β (β β (β‘π β β))) β ((πβπ) Β· π) = (0 Β· π)) |
46 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β β (β‘π β β)) β π β β) |
47 | 46 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π β (β β (β‘π β β))) β π β β) |
48 | | nncn 12168 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β) |
49 | | mul02 11340 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β (0
Β· π) =
0) |
50 | 47, 48, 49 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π β (β β (β‘π β β))) β (0 Β· π) = 0) |
51 | 45, 50 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π β (β β (β‘π β β))) β ((πβπ) Β· π) = 0) |
52 | | nnuz 12813 |
. . . . . . . . . . . . . . . . . . 19
β’ β =
(β€β₯β1) |
53 | 52 | eqimssi 4007 |
. . . . . . . . . . . . . . . . . 18
β’ β
β (β€β₯β1) |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β β
β (β€β₯β1)) |
55 | 26, 33, 51, 54 | sumss 15616 |
. . . . . . . . . . . . . . . 16
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β
Ξ£π β (β‘π β β)((πβπ) Β· π) = Ξ£π β β ((πβπ) Β· π)) |
56 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β (β‘π β β) β
Fin) |
57 | 56, 32 | fsumnn0cl 15628 |
. . . . . . . . . . . . . . . 16
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β
Ξ£π β (β‘π β β)((πβπ) Β· π) β
β0) |
58 | 55, 57 | eqeltrrd 2839 |
. . . . . . . . . . . . . . 15
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β
Ξ£π β β
((πβπ) Β· π) β
β0) |
59 | | eleq1 2826 |
. . . . . . . . . . . . . . 15
β’
(Ξ£π β
β ((πβπ) Β· π) = π β (Ξ£π β β ((πβπ) Β· π) β β0 β π β
β0)) |
60 | 58, 59 | syl5ibcom 244 |
. . . . . . . . . . . . . 14
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β
(Ξ£π β β
((πβπ) Β· π) = π β π β
β0)) |
61 | 60 | 3impia 1118 |
. . . . . . . . . . . . 13
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β π β
β0) |
62 | 61 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β π β
β0) |
63 | 62 | nn0red 12481 |
. . . . . . . . . . 11
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β π β β) |
64 | 18 | nn0ge0d 12483 |
. . . . . . . . . . . 12
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β 0 β€ (πβπ₯)) |
65 | | nnge1 12188 |
. . . . . . . . . . . . 13
β’ (π₯ β β β 1 β€
π₯) |
66 | 65 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β 1 β€ π₯) |
67 | 19, 21, 64, 66 | lemulge11d 12099 |
. . . . . . . . . . 11
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (πβπ₯) β€ ((πβπ₯) Β· π₯)) |
68 | 56 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ (π₯ β β β§ π₯ β (β‘π β β))) β (β‘π β β) β
Fin) |
69 | 32 | nn0red 12481 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π β (β‘π β β)) β ((πβπ) Β· π) β β) |
70 | 69 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ ((((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ (π₯ β β β§ π₯ β (β‘π β β))) β§ π β (β‘π β β)) β ((πβπ) Β· π) β β) |
71 | 32 | nn0ge0d 12483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π β (β‘π β β)) β 0 β€ ((πβπ) Β· π)) |
72 | 71 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ ((((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ (π₯ β β β§ π₯ β (β‘π β β))) β§ π β (β‘π β β)) β 0 β€ ((πβπ) Β· π)) |
73 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π₯ β (πβπ) = (πβπ₯)) |
74 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π₯ β π = π₯) |
75 | 73, 74 | oveq12d 7380 |
. . . . . . . . . . . . . . . . 17
β’ (π = π₯ β ((πβπ) Β· π) = ((πβπ₯) Β· π₯)) |
76 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ (π₯ β β β§ π₯ β (β‘π β β))) β π₯ β (β‘π β β)) |
77 | 68, 70, 72, 75, 76 | fsumge1 15689 |
. . . . . . . . . . . . . . . 16
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ (π₯ β β β§ π₯ β (β‘π β β))) β ((πβπ₯) Β· π₯) β€ Ξ£π β (β‘π β β)((πβπ) Β· π)) |
78 | 77 | expr 458 |
. . . . . . . . . . . . . . 15
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π₯ β β) β (π₯ β (β‘π β β) β ((πβπ₯) Β· π₯) β€ Ξ£π β (β‘π β β)((πβπ) Β· π))) |
79 | | eldif 3925 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (β β (β‘π β β)) β (π₯ β β β§ Β¬ π₯ β (β‘π β β))) |
80 | 51 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin) β
βπ β (β
β (β‘π β β))((πβπ) Β· π) = 0) |
81 | 75 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π₯ β (((πβπ) Β· π) = 0 β ((πβπ₯) Β· π₯) = 0)) |
82 | 81 | rspccva 3583 |
. . . . . . . . . . . . . . . . . . 19
β’
((βπ β
(β β (β‘π β β))((πβπ) Β· π) = 0 β§ π₯ β (β β (β‘π β β))) β ((πβπ₯) Β· π₯) = 0) |
83 | 80, 82 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π₯ β (β β (β‘π β β))) β ((πβπ₯) Β· π₯) = 0) |
84 | 79, 83 | sylan2br 596 |
. . . . . . . . . . . . . . . . 17
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ (π₯ β β β§ Β¬
π₯ β (β‘π β β))) β ((πβπ₯) Β· π₯) = 0) |
85 | 56 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π₯ β β) β (β‘π β β) β
Fin) |
86 | 32 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π₯ β β) β§ π β (β‘π β β)) β ((πβπ) Β· π) β
β0) |
87 | 86 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π₯ β β) β§ π β (β‘π β β)) β ((πβπ) Β· π) β β) |
88 | 86 | nn0ge0d 12483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π₯ β β) β§ π β (β‘π β β)) β 0 β€ ((πβπ) Β· π)) |
89 | 85, 87, 88 | fsumge0 15687 |
. . . . . . . . . . . . . . . . . 18
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π₯ β β) β 0 β€
Ξ£π β (β‘π β β)((πβπ) Β· π)) |
90 | 89 | adantrr 716 |
. . . . . . . . . . . . . . . . 17
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ (π₯ β β β§ Β¬
π₯ β (β‘π β β))) β 0 β€
Ξ£π β (β‘π β β)((πβπ) Β· π)) |
91 | 84, 90 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . 16
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ (π₯ β β β§ Β¬
π₯ β (β‘π β β))) β ((πβπ₯) Β· π₯) β€ Ξ£π β (β‘π β β)((πβπ) Β· π)) |
92 | 91 | expr 458 |
. . . . . . . . . . . . . . 15
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π₯ β β) β (Β¬
π₯ β (β‘π β β) β ((πβπ₯) Β· π₯) β€ Ξ£π β (β‘π β β)((πβπ) Β· π))) |
93 | 78, 92 | pm2.61d 179 |
. . . . . . . . . . . . . 14
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π₯ β β) β ((πβπ₯) Β· π₯) β€ Ξ£π β (β‘π β β)((πβπ) Β· π)) |
94 | 55 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π₯ β β) β
Ξ£π β (β‘π β β)((πβπ) Β· π) = Ξ£π β β ((πβπ) Β· π)) |
95 | 93, 94 | breqtrd 5136 |
. . . . . . . . . . . . 13
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin) β§ π₯ β β) β ((πβπ₯) Β· π₯) β€ Ξ£π β β ((πβπ) Β· π)) |
96 | 95 | 3adantl3 1169 |
. . . . . . . . . . . 12
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β ((πβπ₯) Β· π₯) β€ Ξ£π β β ((πβπ) Β· π)) |
97 | | simpl3 1194 |
. . . . . . . . . . . 12
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β Ξ£π β β ((πβπ) Β· π) = π) |
98 | 96, 97 | breqtrd 5136 |
. . . . . . . . . . 11
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β ((πβπ₯) Β· π₯) β€ π) |
99 | 19, 22, 63, 67, 98 | letrd 11319 |
. . . . . . . . . 10
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (πβπ₯) β€ π) |
100 | | nn0uz 12812 |
. . . . . . . . . . . 12
β’
β0 = (β€β₯β0) |
101 | 18, 100 | eleqtrdi 2848 |
. . . . . . . . . . 11
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (πβπ₯) β
(β€β₯β0)) |
102 | 62 | nn0zd 12532 |
. . . . . . . . . . 11
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β π β β€) |
103 | | elfz5 13440 |
. . . . . . . . . . 11
β’ (((πβπ₯) β (β€β₯β0)
β§ π β β€)
β ((πβπ₯) β (0...π) β (πβπ₯) β€ π)) |
104 | 101, 102,
103 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β ((πβπ₯) β (0...π) β (πβπ₯) β€ π)) |
105 | 99, 104 | mpbird 257 |
. . . . . . . . 9
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (πβπ₯) β (0...π)) |
106 | 105 | adantr 482 |
. . . . . . . 8
β’ ((((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β§ π₯ β (1...π)) β (πβπ₯) β (0...π)) |
107 | | iftrue 4497 |
. . . . . . . . 9
β’ (π₯ β (1...π) β if(π₯ β (1...π), (0...π), {0}) = (0...π)) |
108 | 107 | adantl 483 |
. . . . . . . 8
β’ ((((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β§ π₯ β (1...π)) β if(π₯ β (1...π), (0...π), {0}) = (0...π)) |
109 | 106, 108 | eleqtrrd 2841 |
. . . . . . 7
β’ ((((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β§ π₯ β (1...π)) β (πβπ₯) β if(π₯ β (1...π), (0...π), {0})) |
110 | | nnge1 12188 |
. . . . . . . . . . . . . 14
β’ ((πβπ₯) β β β 1 β€ (πβπ₯)) |
111 | | nnnn0 12427 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β π₯ β
β0) |
112 | 111 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β π₯ β β0) |
113 | 112 | nn0ge0d 12483 |
. . . . . . . . . . . . . . . 16
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β 0 β€ π₯) |
114 | | lemulge12 12025 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β β§ (πβπ₯) β β) β§ (0 β€ π₯ β§ 1 β€ (πβπ₯))) β π₯ β€ ((πβπ₯) Β· π₯)) |
115 | 114 | expr 458 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β β§ (πβπ₯) β β) β§ 0 β€ π₯) β (1 β€ (πβπ₯) β π₯ β€ ((πβπ₯) Β· π₯))) |
116 | 21, 19, 113, 115 | syl21anc 837 |
. . . . . . . . . . . . . . 15
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (1 β€ (πβπ₯) β π₯ β€ ((πβπ₯) Β· π₯))) |
117 | | letr 11256 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ ((πβπ₯) Β· π₯) β β β§ π β β) β ((π₯ β€ ((πβπ₯) Β· π₯) β§ ((πβπ₯) Β· π₯) β€ π) β π₯ β€ π)) |
118 | 21, 22, 63, 117 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β ((π₯ β€ ((πβπ₯) Β· π₯) β§ ((πβπ₯) Β· π₯) β€ π) β π₯ β€ π)) |
119 | 98, 118 | mpan2d 693 |
. . . . . . . . . . . . . . 15
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (π₯ β€ ((πβπ₯) Β· π₯) β π₯ β€ π)) |
120 | 116, 119 | syld 47 |
. . . . . . . . . . . . . 14
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (1 β€ (πβπ₯) β π₯ β€ π)) |
121 | 110, 120 | syl5 34 |
. . . . . . . . . . . . 13
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β ((πβπ₯) β β β π₯ β€ π)) |
122 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β π₯ β β) |
123 | 122, 52 | eleqtrdi 2848 |
. . . . . . . . . . . . . 14
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β π₯ β
(β€β₯β1)) |
124 | | elfz5 13440 |
. . . . . . . . . . . . . 14
β’ ((π₯ β
(β€β₯β1) β§ π β β€) β (π₯ β (1...π) β π₯ β€ π)) |
125 | 123, 102,
124 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (π₯ β (1...π) β π₯ β€ π)) |
126 | 121, 125 | sylibrd 259 |
. . . . . . . . . . . 12
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β ((πβπ₯) β β β π₯ β (1...π))) |
127 | 126 | con3d 152 |
. . . . . . . . . . 11
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (Β¬ π₯ β (1...π) β Β¬ (πβπ₯) β β)) |
128 | | elnn0 12422 |
. . . . . . . . . . . . 13
β’ ((πβπ₯) β β0 β ((πβπ₯) β β β¨ (πβπ₯) = 0)) |
129 | 18, 128 | sylib 217 |
. . . . . . . . . . . 12
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β ((πβπ₯) β β β¨ (πβπ₯) = 0)) |
130 | 129 | ord 863 |
. . . . . . . . . . 11
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (Β¬ (πβπ₯) β β β (πβπ₯) = 0)) |
131 | 127, 130 | syld 47 |
. . . . . . . . . 10
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (Β¬ π₯ β (1...π) β (πβπ₯) = 0)) |
132 | 131 | imp 408 |
. . . . . . . . 9
β’ ((((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β§ Β¬ π₯ β (1...π)) β (πβπ₯) = 0) |
133 | | fvex 6860 |
. . . . . . . . . 10
β’ (πβπ₯) β V |
134 | 133 | elsn 4606 |
. . . . . . . . 9
β’ ((πβπ₯) β {0} β (πβπ₯) = 0) |
135 | 132, 134 | sylibr 233 |
. . . . . . . 8
β’ ((((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β§ Β¬ π₯ β (1...π)) β (πβπ₯) β {0}) |
136 | 8 | adantl 483 |
. . . . . . . 8
β’ ((((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β§ Β¬ π₯ β (1...π)) β if(π₯ β (1...π), (0...π), {0}) = {0}) |
137 | 135, 136 | eleqtrrd 2841 |
. . . . . . 7
β’ ((((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β§ Β¬ π₯ β (1...π)) β (πβπ₯) β if(π₯ β (1...π), (0...π), {0})) |
138 | 109, 137 | pm2.61dan 812 |
. . . . . 6
β’ (((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β§ π₯ β β) β (πβπ₯) β if(π₯ β (1...π), (0...π), {0})) |
139 | 138 | ralrimiva 3144 |
. . . . 5
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β βπ₯ β β (πβπ₯) β if(π₯ β (1...π), (0...π), {0})) |
140 | | vex 3452 |
. . . . . 6
β’ π β V |
141 | 140 | elixp 8849 |
. . . . 5
β’ (π β Xπ₯ β
β if(π₯ β
(1...π), (0...π), {0}) β (π Fn β β§ βπ₯ β β (πβπ₯) β if(π₯ β (1...π), (0...π), {0}))) |
142 | 16, 139, 141 | sylanbrc 584 |
. . . 4
β’ ((π:ββΆβ0 β§
(β‘π β β) β Fin β§
Ξ£π β β
((πβπ) Β· π) = π) β π β Xπ₯ β β if(π₯ β (1...π), (0...π), {0})) |
143 | 14, 142 | sylbi 216 |
. . 3
β’ (π β π β π β Xπ₯ β β if(π₯ β (1...π), (0...π), {0})) |
144 | 143 | ssriv 3953 |
. 2
β’ π β Xπ₯ β
β if(π₯ β
(1...π), (0...π), {0}) |
145 | | ssfi 9124 |
. 2
β’ ((Xπ₯ β
β if(π₯ β
(1...π), (0...π), {0}) β Fin β§ π β Xπ₯ β
β if(π₯ β
(1...π), (0...π), {0})) β π β Fin) |
146 | 12, 144, 145 | mp2an 691 |
1
β’ π β Fin |