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 33355
Description: Lemma for eulerpart 33369. 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 13934 . . . 4 (⊀ β†’ (1...𝑁) ∈ Fin)
2 fzfi 13933 . . . . . 6 (0...𝑁) ∈ Fin
3 snfi 9040 . . . . . 6 {0} ∈ Fin
42, 3ifcli 4574 . . . . 5 if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin
54a1i 11 . . . 4 ((⊀ ∧ π‘₯ ∈ β„•) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin)
6 eldifn 4126 . . . . . 6 (π‘₯ ∈ (β„• βˆ– (1...𝑁)) β†’ Β¬ π‘₯ ∈ (1...𝑁))
76adantl 482 . . . . 5 ((⊀ ∧ π‘₯ ∈ (β„• βˆ– (1...𝑁))) β†’ Β¬ π‘₯ ∈ (1...𝑁))
8 iffalse 4536 . . . . 5 (Β¬ π‘₯ ∈ (1...𝑁) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = {0})
9 eqimss 4039 . . . . 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 9346 . . 3 (⊀ β†’ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin)
1211mptru 1548 . 2 Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin
13 eulerpart.p . . . . 5 𝑃 = {𝑓 ∈ (β„•0 ↑m β„•) ∣ ((◑𝑓 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘“β€˜π‘˜) Β· π‘˜) = 𝑁)}
1413eulerpartleme 33350 . . . 4 (𝑔 ∈ 𝑃 ↔ (𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁))
15 ffn 6714 . . . . . 6 (𝑔:β„•βŸΆβ„•0 β†’ 𝑔 Fn β„•)
16153ad2ant1 1133 . . . . 5 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ 𝑔 Fn β„•)
17 ffvelcdm 7080 . . . . . . . . . . . . 13 ((𝑔:β„•βŸΆβ„•0 ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ β„•0)
18173ad2antl1 1185 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ β„•0)
1918nn0red 12529 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ ℝ)
20 nnre 12215 . . . . . . . . . . . . 13 (π‘₯ ∈ β„• β†’ π‘₯ ∈ ℝ)
2120adantl 482 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ ℝ)
2219, 21remulcld 11240 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ∈ ℝ)
23 cnvimass 6077 . . . . . . . . . . . . . . . . . 18 (◑𝑔 β€œ β„•) βŠ† dom 𝑔
24 fdm 6723 . . . . . . . . . . . . . . . . . . 19 (𝑔:β„•βŸΆβ„•0 β†’ dom 𝑔 = β„•)
2524adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ dom 𝑔 = β„•)
2623, 25sseqtrid 4033 . . . . . . . . . . . . . . . . 17 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (◑𝑔 β€œ β„•) βŠ† β„•)
2726sselda 3981 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ π‘˜ ∈ β„•)
28 ffvelcdm 7080 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔:β„•βŸΆβ„•0 ∧ π‘˜ ∈ β„•) β†’ (π‘”β€˜π‘˜) ∈ β„•0)
2928adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ β„•) β†’ (π‘”β€˜π‘˜) ∈ β„•0)
3027, 29syldan 591 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ (π‘”β€˜π‘˜) ∈ β„•0)
3127nnnn0d 12528 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ π‘˜ ∈ β„•0)
3230, 31nn0mulcld 12533 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
3332nn0cnd 12530 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„‚)
34 simpl 483 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ 𝑔:β„•βŸΆβ„•0)
35 nnex 12214 . . . . . . . . . . . . . . . . . . . . . . 23 β„• ∈ V
36 fcdmnn0supp 12524 . . . . . . . . . . . . . . . . . . . . . . 23 ((β„• ∈ V ∧ 𝑔:β„•βŸΆβ„•0) β†’ (𝑔 supp 0) = (◑𝑔 β€œ β„•))
3735, 36mpan 688 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:β„•βŸΆβ„•0 β†’ (𝑔 supp 0) = (◑𝑔 β€œ β„•))
3837adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (𝑔 supp 0) = (◑𝑔 β€œ β„•))
39 eqimss 4039 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 supp 0) = (◑𝑔 β€œ β„•) β†’ (𝑔 supp 0) βŠ† (◑𝑔 β€œ β„•))
4038, 39syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (𝑔 supp 0) βŠ† (◑𝑔 β€œ β„•))
4135a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ β„• ∈ V)
42 0nn0 12483 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ β„•0
4342a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ 0 ∈ β„•0)
4434, 40, 41, 43suppssr 8177 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ (π‘”β€˜π‘˜) = 0)
4544oveq1d 7420 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) = (0 Β· π‘˜))
46 eldifi 4125 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•)) β†’ π‘˜ ∈ β„•)
4746adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ π‘˜ ∈ β„•)
48 nncn 12216 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„‚)
49 mul02 11388 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ β„‚ β†’ (0 Β· π‘˜) = 0)
5047, 48, 493syl 18 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ (0 Β· π‘˜) = 0)
5145, 50eqtrd 2772 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) = 0)
52 nnuz 12861 . . . . . . . . . . . . . . . . . . 19 β„• = (β„€β‰₯β€˜1)
5352eqimssi 4041 . . . . . . . . . . . . . . . . . 18 β„• βŠ† (β„€β‰₯β€˜1)
5453a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ β„• βŠ† (β„€β‰₯β€˜1))
5526, 33, 51, 54sumss 15666 . . . . . . . . . . . . . . . 16 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜) = Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
56 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (◑𝑔 β€œ β„•) ∈ Fin)
5756, 32fsumnn0cl 15678 . . . . . . . . . . . . . . . 16 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
5855, 57eqeltrrd 2834 . . . . . . . . . . . . . . 15 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
59 eleq1 2821 . . . . . . . . . . . . . . 15 (Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁 β†’ (Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0 ↔ 𝑁 ∈ β„•0))
6058, 59syl5ibcom 244 . . . . . . . . . . . . . 14 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁 β†’ 𝑁 ∈ β„•0))
61603impia 1117 . . . . . . . . . . . . 13 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ 𝑁 ∈ β„•0)
6261adantr 481 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 𝑁 ∈ β„•0)
6362nn0red 12529 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 𝑁 ∈ ℝ)
6418nn0ge0d 12531 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 0 ≀ (π‘”β€˜π‘₯))
65 nnge1 12236 . . . . . . . . . . . . 13 (π‘₯ ∈ β„• β†’ 1 ≀ π‘₯)
6665adantl 482 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 1 ≀ π‘₯)
6719, 21, 64, 66lemulge11d 12147 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ≀ ((π‘”β€˜π‘₯) Β· π‘₯))
6856adantr 481 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ (◑𝑔 β€œ β„•) ∈ Fin)
6932nn0red 12529 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ ℝ)
7069adantlr 713 . . . . . . . . . . . . . . . . 17 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ ℝ)
7132nn0ge0d 12531 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ 0 ≀ ((π‘”β€˜π‘˜) Β· π‘˜))
7271adantlr 713 . . . . . . . . . . . . . . . . 17 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ 0 ≀ ((π‘”β€˜π‘˜) Β· π‘˜))
73 fveq2 6888 . . . . . . . . . . . . . . . . . 18 (π‘˜ = π‘₯ β†’ (π‘”β€˜π‘˜) = (π‘”β€˜π‘₯))
74 id 22 . . . . . . . . . . . . . . . . . 18 (π‘˜ = π‘₯ β†’ π‘˜ = π‘₯)
7573, 74oveq12d 7423 . . . . . . . . . . . . . . . . 17 (π‘˜ = π‘₯ β†’ ((π‘”β€˜π‘˜) Β· π‘˜) = ((π‘”β€˜π‘₯) Β· π‘₯))
76 simprr 771 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ π‘₯ ∈ (◑𝑔 β€œ β„•))
7768, 70, 72, 75, 76fsumge1 15739 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
7877expr 457 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ (π‘₯ ∈ (◑𝑔 β€œ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜)))
79 eldif 3957 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (β„• βˆ– (◑𝑔 β€œ β„•)) ↔ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•)))
8051ralrimiva 3146 . . . . . . . . . . . . . . . . . . 19 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))((π‘”β€˜π‘˜) Β· π‘˜) = 0)
8175eqeq1d 2734 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = π‘₯ β†’ (((π‘”β€˜π‘˜) Β· π‘˜) = 0 ↔ ((π‘”β€˜π‘₯) Β· π‘₯) = 0))
8281rspccva 3611 . . . . . . . . . . . . . . . . . . 19 ((βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))((π‘”β€˜π‘˜) Β· π‘˜) = 0 ∧ π‘₯ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) = 0)
8380, 82sylan 580 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) = 0)
8479, 83sylan2br 595 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) = 0)
8556adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ (◑𝑔 β€œ β„•) ∈ Fin)
8632adantlr 713 . . . . . . . . . . . . . . . . . . . 20 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
8786nn0red 12529 . . . . . . . . . . . . . . . . . . 19 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ ℝ)
8886nn0ge0d 12531 . . . . . . . . . . . . . . . . . . 19 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ 0 ≀ ((π‘”β€˜π‘˜) Β· π‘˜))
8985, 87, 88fsumge0 15737 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ 0 ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9089adantrr 715 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ 0 ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9184, 90eqbrtrd 5169 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9291expr 457 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ (Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜)))
9378, 92pm2.61d 179 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9455adantr 481 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜) = Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
9593, 94breqtrd 5173 . . . . . . . . . . . . 13 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
96953adantl3 1168 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
97 simpl3 1193 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁)
9896, 97breqtrd 5173 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ 𝑁)
9919, 22, 63, 67, 98letrd 11367 . . . . . . . . . 10 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ≀ 𝑁)
100 nn0uz 12860 . . . . . . . . . . . 12 β„•0 = (β„€β‰₯β€˜0)
10118, 100eleqtrdi 2843 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ (β„€β‰₯β€˜0))
10262nn0zd 12580 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 𝑁 ∈ β„€)
103 elfz5 13489 . . . . . . . . . . 11 (((π‘”β€˜π‘₯) ∈ (β„€β‰₯β€˜0) ∧ 𝑁 ∈ β„€) β†’ ((π‘”β€˜π‘₯) ∈ (0...𝑁) ↔ (π‘”β€˜π‘₯) ≀ 𝑁))
104101, 102, 103syl2anc 584 . . . . . . . . . 10 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ (0...𝑁) ↔ (π‘”β€˜π‘₯) ≀ 𝑁))
10599, 104mpbird 256 . . . . . . . . 9 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ (0...𝑁))
106105adantr 481 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ (0...𝑁))
107 iftrue 4533 . . . . . . . . 9 (π‘₯ ∈ (1...𝑁) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = (0...𝑁))
108107adantl 482 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ π‘₯ ∈ (1...𝑁)) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = (0...𝑁))
109106, 108eleqtrrd 2836 . . . . . . 7 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
110 nnge1 12236 . . . . . . . . . . . . . 14 ((π‘”β€˜π‘₯) ∈ β„• β†’ 1 ≀ (π‘”β€˜π‘₯))
111 nnnn0 12475 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ β„• β†’ π‘₯ ∈ β„•0)
112111adantl 482 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ β„•0)
113112nn0ge0d 12531 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 0 ≀ π‘₯)
114 lemulge12 12073 . . . . . . . . . . . . . . . . 17 (((π‘₯ ∈ ℝ ∧ (π‘”β€˜π‘₯) ∈ ℝ) ∧ (0 ≀ π‘₯ ∧ 1 ≀ (π‘”β€˜π‘₯))) β†’ π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯))
115114expr 457 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ ℝ ∧ (π‘”β€˜π‘₯) ∈ ℝ) ∧ 0 ≀ π‘₯) β†’ (1 ≀ (π‘”β€˜π‘₯) β†’ π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯)))
11621, 19, 113, 115syl21anc 836 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (1 ≀ (π‘”β€˜π‘₯) β†’ π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯)))
117 letr 11304 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ ℝ ∧ ((π‘”β€˜π‘₯) Β· π‘₯) ∈ ℝ ∧ 𝑁 ∈ ℝ) β†’ ((π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯) ∧ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ 𝑁) β†’ π‘₯ ≀ 𝑁))
11821, 22, 63, 117syl3anc 1371 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯) ∧ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ 𝑁) β†’ π‘₯ ≀ 𝑁))
11998, 118mpan2d 692 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯) β†’ π‘₯ ≀ 𝑁))
120116, 119syld 47 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (1 ≀ (π‘”β€˜π‘₯) β†’ π‘₯ ≀ 𝑁))
121110, 120syl5 34 . . . . . . . . . . . . 13 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ β„• β†’ π‘₯ ≀ 𝑁))
122 simpr 485 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ β„•)
123122, 52eleqtrdi 2843 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ (β„€β‰₯β€˜1))
124 elfz5 13489 . . . . . . . . . . . . . 14 ((π‘₯ ∈ (β„€β‰₯β€˜1) ∧ 𝑁 ∈ β„€) β†’ (π‘₯ ∈ (1...𝑁) ↔ π‘₯ ≀ 𝑁))
125123, 102, 124syl2anc 584 . . . . . . . . . . . . 13 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘₯ ∈ (1...𝑁) ↔ π‘₯ ≀ 𝑁))
126121, 125sylibrd 258 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ β„• β†’ π‘₯ ∈ (1...𝑁)))
127126con3d 152 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (Β¬ π‘₯ ∈ (1...𝑁) β†’ Β¬ (π‘”β€˜π‘₯) ∈ β„•))
128 elnn0 12470 . . . . . . . . . . . . 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 407 . . . . . . . . 9 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) = 0)
133 fvex 6901 . . . . . . . . . 10 (π‘”β€˜π‘₯) ∈ V
134133elsn 4642 . . . . . . . . 9 ((π‘”β€˜π‘₯) ∈ {0} ↔ (π‘”β€˜π‘₯) = 0)
135132, 134sylibr 233 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ {0})
1368adantl 482 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = {0})
137135, 136eleqtrrd 2836 . . . . . . 7 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
138109, 137pm2.61dan 811 . . . . . 6 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
139138ralrimiva 3146 . . . . 5 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ βˆ€π‘₯ ∈ β„• (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
140 vex 3478 . . . . . 6 𝑔 ∈ V
141140elixp 8894 . . . . 5 (𝑔 ∈ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ↔ (𝑔 Fn β„• ∧ βˆ€π‘₯ ∈ β„• (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0})))
14216, 139, 141sylanbrc 583 . . . 4 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ 𝑔 ∈ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
14314, 142sylbi 216 . . 3 (𝑔 ∈ 𝑃 β†’ 𝑔 ∈ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
144143ssriv 3985 . 2 𝑃 βŠ† Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0})
145 ssfi 9169 . 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 396   ∨ wo 845   ∧ w3a 1087   = wceq 1541  βŠ€wtru 1542   ∈ wcel 2106  βˆ€wral 3061  {crab 3432  Vcvv 3474   βˆ– cdif 3944   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  ifcif 4527  π’« cpw 4601  {csn 4627   class class class wbr 5147  {copab 5209   ↦ cmpt 5230  β—‘ccnv 5674  dom cdm 5675   β€œ cima 5678   Fn wfn 6535  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405   ∈ cmpo 7407   supp csupp 8142   ↑m cmap 8816  Xcixp 8887  Fincfn 8935  β„‚cc 11104  β„cr 11105  0cc0 11106  1c1 11107   Β· cmul 11111   ≀ cle 11245  β„•cn 12208  2c2 12263  β„•0cn0 12468  β„€cz 12554  β„€β‰₯cuz 12818  ...cfz 13480  β†‘cexp 14023  Ξ£csu 15628   βˆ₯ cdvds 16193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-oi 9501  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-ico 13326  df-fz 13481  df-fzo 13624  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-sum 15629
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator