Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eulerpartlemb Structured version   Visualization version   GIF version
Theorem eulerpartlemb 34058
Description: Lemma for eulerpart 34072. The set of all partitions of 𝑁 is finite. (Contributed by Mario Carneiro, 26-Jan-2015.)
Hypotheses
Ref Expression
eulerpart.p 𝑃 = {𝑓 ∈ (β„•0 ↑m β„•) ∣ ((◑𝑓 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘“β€˜π‘˜) Β· π‘˜) = 𝑁)}
eulerpart.o 𝑂 = {𝑔 ∈ 𝑃 ∣ βˆ€π‘› ∈ (◑𝑔 β€œ β„•) Β¬ 2 βˆ₯ 𝑛}
eulerpart.d 𝐷 = {𝑔 ∈ 𝑃 ∣ βˆ€π‘› ∈ β„• (π‘”β€˜π‘›) ≀ 1}
eulerpart.j 𝐽 = {𝑧 ∈ β„• ∣ Β¬ 2 βˆ₯ 𝑧}
eulerpart.f 𝐹 = (π‘₯ ∈ 𝐽, 𝑦 ∈ β„•0 ↦ ((2↑𝑦) Β· π‘₯))
eulerpart.h 𝐻 = {π‘Ÿ ∈ ((𝒫 β„•0 ∩ Fin) ↑m 𝐽) ∣ (π‘Ÿ supp βˆ…) ∈ Fin}
eulerpart.m 𝑀 = (π‘Ÿ ∈ 𝐻 ↦ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ 𝐽 ∧ 𝑦 ∈ (π‘Ÿβ€˜π‘₯))})
Assertion
Ref Expression
eulerpartlemb 𝑃 ∈ Fin
Distinct variable groups:   𝑓,𝑔,π‘˜,π‘₯,𝑦   𝑓,𝑁,𝑔,π‘₯   𝑃,𝑔
Allowed substitution hints:   𝐷(π‘₯,𝑦,𝑧,𝑓,𝑔,π‘˜,𝑛,π‘Ÿ)   𝑃(π‘₯,𝑦,𝑧,𝑓,π‘˜,𝑛,π‘Ÿ)   𝐹(π‘₯,𝑦,𝑧,𝑓,𝑔,π‘˜,𝑛,π‘Ÿ)   𝐻(π‘₯,𝑦,𝑧,𝑓,𝑔,π‘˜,𝑛,π‘Ÿ)   𝐽(π‘₯,𝑦,𝑧,𝑓,𝑔,π‘˜,𝑛,π‘Ÿ)   𝑀(π‘₯,𝑦,𝑧,𝑓,𝑔,π‘˜,𝑛,π‘Ÿ)   𝑁(𝑦,𝑧,π‘˜,𝑛,π‘Ÿ)   𝑂(π‘₯,𝑦,𝑧,𝑓,𝑔,π‘˜,𝑛,π‘Ÿ)
Proof of Theorem eulerpartlemb
StepHypRef Expression
1 fzfid 13970 . . . 4 (⊀ β†’ (1...𝑁) ∈ Fin)
2 fzfi 13969 . . . . . 6 (0...𝑁) ∈ Fin
3 snfi 9067 . . . . . 6 {0} ∈ Fin
42, 3ifcli 4576 . . . . 5 if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin
54a1i 11 . . . 4 ((⊀ ∧ π‘₯ ∈ β„•) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin)
6 eldifn 4125 . . . . . 6 (π‘₯ ∈ (β„• βˆ– (1...𝑁)) β†’ Β¬ π‘₯ ∈ (1...𝑁))
76adantl 480 . . . . 5 ((⊀ ∧ π‘₯ ∈ (β„• βˆ– (1...𝑁))) β†’ Β¬ π‘₯ ∈ (1...𝑁))
8 iffalse 4538 . . . . 5 (Β¬ π‘₯ ∈ (1...𝑁) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = {0})
9 eqimss 4036 . . . . 5 (if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = {0} β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) βŠ† {0})
107, 8, 93syl 18 . . . 4 ((⊀ ∧ π‘₯ ∈ (β„• βˆ– (1...𝑁))) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) βŠ† {0})
111, 5, 10ixpfi2 9374 . . 3 (⊀ β†’ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin)
1211mptru 1540 . 2 Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin
13 eulerpart.p . . . . 5 𝑃 = {𝑓 ∈ (β„•0 ↑m β„•) ∣ ((◑𝑓 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘“β€˜π‘˜) Β· π‘˜) = 𝑁)}
1413eulerpartleme 34053 . . . 4 (𝑔 ∈ 𝑃 ↔ (𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁))
15 ffn 6721 . . . . . 6 (𝑔:β„•βŸΆβ„•0 β†’ 𝑔 Fn β„•)
16153ad2ant1 1130 . . . . 5 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ 𝑔 Fn β„•)
17 ffvelcdm 7088 . . . . . . . . . . . . 13 ((𝑔:β„•βŸΆβ„•0 ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ β„•0)
18173ad2antl1 1182 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ β„•0)
1918nn0red 12563 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ ℝ)
20 nnre 12249 . . . . . . . . . . . . 13 (π‘₯ ∈ β„• β†’ π‘₯ ∈ ℝ)
2120adantl 480 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ ℝ)
2219, 21remulcld 11274 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ∈ ℝ)
23 cnvimass 6085 . . . . . . . . . . . . . . . . . 18 (◑𝑔 β€œ β„•) βŠ† dom 𝑔
24 fdm 6730 . . . . . . . . . . . . . . . . . . 19 (𝑔:β„•βŸΆβ„•0 β†’ dom 𝑔 = β„•)
2524adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ dom 𝑔 = β„•)
2623, 25sseqtrid 4030 . . . . . . . . . . . . . . . . 17 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (◑𝑔 β€œ β„•) βŠ† β„•)
2726sselda 3977 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ π‘˜ ∈ β„•)
28 ffvelcdm 7088 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔:β„•βŸΆβ„•0 ∧ π‘˜ ∈ β„•) β†’ (π‘”β€˜π‘˜) ∈ β„•0)
2928adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ β„•) β†’ (π‘”β€˜π‘˜) ∈ β„•0)
3027, 29syldan 589 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ (π‘”β€˜π‘˜) ∈ β„•0)
3127nnnn0d 12562 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ π‘˜ ∈ β„•0)
3230, 31nn0mulcld 12567 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
3332nn0cnd 12564 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„‚)
34 simpl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ 𝑔:β„•βŸΆβ„•0)
35 nnex 12248 . . . . . . . . . . . . . . . . . . . . . . 23 β„• ∈ V
36 fcdmnn0supp 12558 . . . . . . . . . . . . . . . . . . . . . . 23 ((β„• ∈ V ∧ 𝑔:β„•βŸΆβ„•0) β†’ (𝑔 supp 0) = (◑𝑔 β€œ β„•))
3735, 36mpan 688 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:β„•βŸΆβ„•0 β†’ (𝑔 supp 0) = (◑𝑔 β€œ β„•))
3837adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (𝑔 supp 0) = (◑𝑔 β€œ β„•))
39 eqimss 4036 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 supp 0) = (◑𝑔 β€œ β„•) β†’ (𝑔 supp 0) βŠ† (◑𝑔 β€œ β„•))
4038, 39syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (𝑔 supp 0) βŠ† (◑𝑔 β€œ β„•))
4135a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ β„• ∈ V)
42 0nn0 12517 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ β„•0
4342a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ 0 ∈ β„•0)
4434, 40, 41, 43suppssr 8199 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ (π‘”β€˜π‘˜) = 0)
4544oveq1d 7432 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) = (0 Β· π‘˜))
46 eldifi 4124 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•)) β†’ π‘˜ ∈ β„•)
4746adantl 480 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ π‘˜ ∈ β„•)
48 nncn 12250 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„‚)
49 mul02 11422 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ β„‚ β†’ (0 Β· π‘˜) = 0)
5047, 48, 493syl 18 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ (0 Β· π‘˜) = 0)
5145, 50eqtrd 2765 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) = 0)
52 nnuz 12895 . . . . . . . . . . . . . . . . . . 19 β„• = (β„€β‰₯β€˜1)
5352eqimssi 4038 . . . . . . . . . . . . . . . . . 18 β„• βŠ† (β„€β‰₯β€˜1)
5453a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ β„• βŠ† (β„€β‰₯β€˜1))
5526, 33, 51, 54sumss 15702 . . . . . . . . . . . . . . . 16 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜) = Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
56 simpr 483 . . . . . . . . . . . . . . . . 17 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (◑𝑔 β€œ β„•) ∈ Fin)
5756, 32fsumnn0cl 15714 . . . . . . . . . . . . . . . 16 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
5855, 57eqeltrrd 2826 . . . . . . . . . . . . . . 15 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
59 eleq1 2813 . . . . . . . . . . . . . . 15 (Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁 β†’ (Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0 ↔ 𝑁 ∈ β„•0))
6058, 59syl5ibcom 244 . . . . . . . . . . . . . 14 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁 β†’ 𝑁 ∈ β„•0))
61603impia 1114 . . . . . . . . . . . . 13 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ 𝑁 ∈ β„•0)
6261adantr 479 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 𝑁 ∈ β„•0)
6362nn0red 12563 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 𝑁 ∈ ℝ)
6418nn0ge0d 12565 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 0 ≀ (π‘”β€˜π‘₯))
65 nnge1 12270 . . . . . . . . . . . . 13 (π‘₯ ∈ β„• β†’ 1 ≀ π‘₯)
6665adantl 480 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 1 ≀ π‘₯)
6719, 21, 64, 66lemulge11d 12181 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ≀ ((π‘”β€˜π‘₯) Β· π‘₯))
6856adantr 479 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ (◑𝑔 β€œ β„•) ∈ Fin)
6932nn0red 12563 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ ℝ)
7069adantlr 713 . . . . . . . . . . . . . . . . 17 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ ℝ)
7132nn0ge0d 12565 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ 0 ≀ ((π‘”β€˜π‘˜) Β· π‘˜))
7271adantlr 713 . . . . . . . . . . . . . . . . 17 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ 0 ≀ ((π‘”β€˜π‘˜) Β· π‘˜))
73 fveq2 6894 . . . . . . . . . . . . . . . . . 18 (π‘˜ = π‘₯ β†’ (π‘”β€˜π‘˜) = (π‘”β€˜π‘₯))
74 id 22 . . . . . . . . . . . . . . . . . 18 (π‘˜ = π‘₯ β†’ π‘˜ = π‘₯)
7573, 74oveq12d 7435 . . . . . . . . . . . . . . . . 17 (π‘˜ = π‘₯ β†’ ((π‘”β€˜π‘˜) Β· π‘˜) = ((π‘”β€˜π‘₯) Β· π‘₯))
76 simprr 771 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ π‘₯ ∈ (◑𝑔 β€œ β„•))
7768, 70, 72, 75, 76fsumge1 15775 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
7877expr 455 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ (π‘₯ ∈ (◑𝑔 β€œ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜)))
79 eldif 3955 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (β„• βˆ– (◑𝑔 β€œ β„•)) ↔ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•)))
8051ralrimiva 3136 . . . . . . . . . . . . . . . . . . 19 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))((π‘”β€˜π‘˜) Β· π‘˜) = 0)
8175eqeq1d 2727 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = π‘₯ β†’ (((π‘”β€˜π‘˜) Β· π‘˜) = 0 ↔ ((π‘”β€˜π‘₯) Β· π‘₯) = 0))
8281rspccva 3606 . . . . . . . . . . . . . . . . . . 19 ((βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))((π‘”β€˜π‘˜) Β· π‘˜) = 0 ∧ π‘₯ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) = 0)
8380, 82sylan 578 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) = 0)
8479, 83sylan2br 593 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) = 0)
8556adantr 479 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ (◑𝑔 β€œ β„•) ∈ Fin)
8632adantlr 713 . . . . . . . . . . . . . . . . . . . 20 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
8786nn0red 12563 . . . . . . . . . . . . . . . . . . 19 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ ℝ)
8886nn0ge0d 12565 . . . . . . . . . . . . . . . . . . 19 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ 0 ≀ ((π‘”β€˜π‘˜) Β· π‘˜))
8985, 87, 88fsumge0 15773 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ 0 ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9089adantrr 715 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ 0 ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9184, 90eqbrtrd 5170 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9291expr 455 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ (Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜)))
9378, 92pm2.61d 179 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9455adantr 479 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜) = Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
9593, 94breqtrd 5174 . . . . . . . . . . . . 13 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
96953adantl3 1165 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
97 simpl3 1190 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁)
9896, 97breqtrd 5174 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ 𝑁)
9919, 22, 63, 67, 98letrd 11401 . . . . . . . . . 10 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ≀ 𝑁)
100 nn0uz 12894 . . . . . . . . . . . 12 β„•0 = (β„€β‰₯β€˜0)
10118, 100eleqtrdi 2835 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ (β„€β‰₯β€˜0))
10262nn0zd 12614 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 𝑁 ∈ β„€)
103 elfz5 13525 . . . . . . . . . . 11 (((π‘”β€˜π‘₯) ∈ (β„€β‰₯β€˜0) ∧ 𝑁 ∈ β„€) β†’ ((π‘”β€˜π‘₯) ∈ (0...𝑁) ↔ (π‘”β€˜π‘₯) ≀ 𝑁))
104101, 102, 103syl2anc 582 . . . . . . . . . 10 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ (0...𝑁) ↔ (π‘”β€˜π‘₯) ≀ 𝑁))
10599, 104mpbird 256 . . . . . . . . 9 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ (0...𝑁))
106105adantr 479 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ (0...𝑁))
107 iftrue 4535 . . . . . . . . 9 (π‘₯ ∈ (1...𝑁) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = (0...𝑁))
108107adantl 480 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ π‘₯ ∈ (1...𝑁)) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = (0...𝑁))
109106, 108eleqtrrd 2828 . . . . . . 7 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
110 nnge1 12270 . . . . . . . . . . . . . 14 ((π‘”β€˜π‘₯) ∈ β„• β†’ 1 ≀ (π‘”β€˜π‘₯))
111 nnnn0 12509 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ β„• β†’ π‘₯ ∈ β„•0)
112111adantl 480 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ β„•0)
113112nn0ge0d 12565 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 0 ≀ π‘₯)
114 lemulge12 12107 . . . . . . . . . . . . . . . . 17 (((π‘₯ ∈ ℝ ∧ (π‘”β€˜π‘₯) ∈ ℝ) ∧ (0 ≀ π‘₯ ∧ 1 ≀ (π‘”β€˜π‘₯))) β†’ π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯))
115114expr 455 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ ℝ ∧ (π‘”β€˜π‘₯) ∈ ℝ) ∧ 0 ≀ π‘₯) β†’ (1 ≀ (π‘”β€˜π‘₯) β†’ π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯)))
11621, 19, 113, 115syl21anc 836 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (1 ≀ (π‘”β€˜π‘₯) β†’ π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯)))
117 letr 11338 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ ℝ ∧ ((π‘”β€˜π‘₯) Β· π‘₯) ∈ ℝ ∧ 𝑁 ∈ ℝ) β†’ ((π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯) ∧ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ 𝑁) β†’ π‘₯ ≀ 𝑁))
11821, 22, 63, 117syl3anc 1368 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯) ∧ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ 𝑁) β†’ π‘₯ ≀ 𝑁))
11998, 118mpan2d 692 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯) β†’ π‘₯ ≀ 𝑁))
120116, 119syld 47 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (1 ≀ (π‘”β€˜π‘₯) β†’ π‘₯ ≀ 𝑁))
121110, 120syl5 34 . . . . . . . . . . . . 13 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ β„• β†’ π‘₯ ≀ 𝑁))
122 simpr 483 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ β„•)
123122, 52eleqtrdi 2835 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ (β„€β‰₯β€˜1))
124 elfz5 13525 . . . . . . . . . . . . . 14 ((π‘₯ ∈ (β„€β‰₯β€˜1) ∧ 𝑁 ∈ β„€) β†’ (π‘₯ ∈ (1...𝑁) ↔ π‘₯ ≀ 𝑁))
125123, 102, 124syl2anc 582 . . . . . . . . . . . . 13 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘₯ ∈ (1...𝑁) ↔ π‘₯ ≀ 𝑁))
126121, 125sylibrd 258 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ β„• β†’ π‘₯ ∈ (1...𝑁)))
127126con3d 152 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (Β¬ π‘₯ ∈ (1...𝑁) β†’ Β¬ (π‘”β€˜π‘₯) ∈ β„•))
128 elnn0 12504 . . . . . . . . . . . . 13 ((π‘”β€˜π‘₯) ∈ β„•0 ↔ ((π‘”β€˜π‘₯) ∈ β„• ∨ (π‘”β€˜π‘₯) = 0))
12918, 128sylib 217 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ β„• ∨ (π‘”β€˜π‘₯) = 0))
130129ord 862 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (Β¬ (π‘”β€˜π‘₯) ∈ β„• β†’ (π‘”β€˜π‘₯) = 0))
131127, 130syld 47 . . . . . . . . . 10 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (Β¬ π‘₯ ∈ (1...𝑁) β†’ (π‘”β€˜π‘₯) = 0))
132131imp 405 . . . . . . . . 9 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) = 0)
133 fvex 6907 . . . . . . . . . 10 (π‘”β€˜π‘₯) ∈ V
134133elsn 4644 . . . . . . . . 9 ((π‘”β€˜π‘₯) ∈ {0} ↔ (π‘”β€˜π‘₯) = 0)
135132, 134sylibr 233 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ {0})
1368adantl 480 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = {0})
137135, 136eleqtrrd 2828 . . . . . . 7 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
138109, 137pm2.61dan 811 . . . . . 6 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
139138ralrimiva 3136 . . . . 5 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ βˆ€π‘₯ ∈ β„• (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
140 vex 3467 . . . . . 6 𝑔 ∈ V
141140elixp 8921 . . . . 5 (𝑔 ∈ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ↔ (𝑔 Fn β„• ∧ βˆ€π‘₯ ∈ β„• (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0})))
14216, 139, 141sylanbrc 581 . . . 4 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ 𝑔 ∈ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
14314, 142sylbi 216 . . 3 (𝑔 ∈ 𝑃 β†’ 𝑔 ∈ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
144143ssriv 3981 . 2 𝑃 βŠ† Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0})
145 ssfi 9196 . 2 ((Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin ∧ 𝑃 βŠ† Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0})) β†’ 𝑃 ∈ Fin)
14612, 144, 145mp2an 690 1 𝑃 ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∧ w3a 1084   = wceq 1533  βŠ€wtru 1534   ∈ wcel 2098  βˆ€wral 3051  {crab 3419  Vcvv 3463   βˆ– cdif 3942   ∩ cin 3944   βŠ† wss 3945  βˆ…c0 4323  ifcif 4529  π’« cpw 4603  {csn 4629   class class class wbr 5148  {copab 5210   ↦ cmpt 5231  β—‘ccnv 5676  dom cdm 5677   β€œ cima 5680   Fn wfn 6542  βŸΆwf 6543  β€˜cfv 6547  (class class class)co 7417   ∈ cmpo 7419   supp csupp 8163   ↑m cmap 8843  Xcixp 8914  Fincfn 8962  β„‚cc 11136  β„cr 11137  0cc0 11138  1c1 11139   Β· cmul 11143   ≀ cle 11279  β„•cn 12242  2c2 12297  β„•0cn0 12502  β„€cz 12588  β„€β‰₯cuz 12852  ...cfz 13516  β†‘cexp 14058  Ξ£csu 15664   βˆ₯ cdvds 16230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428  ax-un 7739  ax-inf2 9664  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215  ax-pre-sup 11216
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3965  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-isom 6556  df-riota 7373  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7870  df-1st 7992  df-2nd 7993  df-supp 8164  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8723  df-map 8845  df-pm 8846  df-ixp 8915  df-en 8963  df-dom 8964  df-sdom 8965  df-fin 8966  df-sup 9465  df-oi 9533  df-card 9962  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-div 11902  df-nn 12243  df-2 12305  df-3 12306  df-n0 12503  df-z 12589  df-uz 12853  df-rp 13007  df-ico 13362  df-fz 13517  df-fzo 13660  df-seq 13999  df-exp 14059  df-hash 14322  df-cj 15078  df-re 15079  df-im 15080  df-sqrt 15214  df-abs 15215  df-clim 15464  df-sum 15665
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator