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 33008
Description: Lemma for eulerpart 33022. 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 13885 . . . 4 (⊀ β†’ (1...𝑁) ∈ Fin)
2 fzfi 13884 . . . . . 6 (0...𝑁) ∈ Fin
3 snfi 8995 . . . . . 6 {0} ∈ Fin
42, 3ifcli 4538 . . . . 5 if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin
54a1i 11 . . . 4 ((⊀ ∧ π‘₯ ∈ β„•) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin)
6 eldifn 4092 . . . . . 6 (π‘₯ ∈ (β„• βˆ– (1...𝑁)) β†’ Β¬ π‘₯ ∈ (1...𝑁))
76adantl 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})
107, 8, 93syl 18 . . . 4 ((⊀ ∧ π‘₯ ∈ (β„• βˆ– (1...𝑁))) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) βŠ† {0})
111, 5, 10ixpfi2 9301 . . 3 (⊀ β†’ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin)
1211mptru 1549 . 2 Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin
13 eulerpart.p . . . . 5 𝑃 = {𝑓 ∈ (β„•0 ↑m β„•) ∣ ((◑𝑓 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘“β€˜π‘˜) Β· π‘˜) = 𝑁)}
1413eulerpartleme 33003 . . . 4 (𝑔 ∈ 𝑃 ↔ (𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁))
15 ffn 6673 . . . . . 6 (𝑔:β„•βŸΆβ„•0 β†’ 𝑔 Fn β„•)
16153ad2ant1 1134 . . . . 5 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ 𝑔 Fn β„•)
17 ffvelcdm 7037 . . . . . . . . . . . . 13 ((𝑔:β„•βŸΆβ„•0 ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ β„•0)
18173ad2antl1 1186 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ β„•0)
1918nn0red 12481 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ ℝ)
20 nnre 12167 . . . . . . . . . . . . 13 (π‘₯ ∈ β„• β†’ π‘₯ ∈ ℝ)
2120adantl 483 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ ℝ)
2219, 21remulcld 11192 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ∈ ℝ)
23 cnvimass 6038 . . . . . . . . . . . . . . . . . 18 (◑𝑔 β€œ β„•) βŠ† dom 𝑔
24 fdm 6682 . . . . . . . . . . . . . . . . . . 19 (𝑔:β„•βŸΆβ„•0 β†’ dom 𝑔 = β„•)
2524adantr 482 . . . . . . . . . . . . . . . . . 18 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ dom 𝑔 = β„•)
2623, 25sseqtrid 4001 . . . . . . . . . . . . . . . . 17 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (◑𝑔 β€œ β„•) βŠ† β„•)
2726sselda 3949 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ π‘˜ ∈ β„•)
28 ffvelcdm 7037 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔:β„•βŸΆβ„•0 ∧ π‘˜ ∈ β„•) β†’ (π‘”β€˜π‘˜) ∈ β„•0)
2928adantlr 714 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ β„•) β†’ (π‘”β€˜π‘˜) ∈ β„•0)
3027, 29syldan 592 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ (π‘”β€˜π‘˜) ∈ β„•0)
3127nnnn0d 12480 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ π‘˜ ∈ β„•0)
3230, 31nn0mulcld 12485 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
3332nn0cnd 12482 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„‚)
34 simpl 484 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ 𝑔:β„•βŸΆβ„•0)
35 nnex 12166 . . . . . . . . . . . . . . . . . . . . . . 23 β„• ∈ V
36 fcdmnn0supp 12476 . . . . . . . . . . . . . . . . . . . . . . 23 ((β„• ∈ V ∧ 𝑔:β„•βŸΆβ„•0) β†’ (𝑔 supp 0) = (◑𝑔 β€œ β„•))
3735, 36mpan 689 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:β„•βŸΆβ„•0 β†’ (𝑔 supp 0) = (◑𝑔 β€œ β„•))
3837adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (𝑔 supp 0) = (◑𝑔 β€œ β„•))
39 eqimss 4005 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 supp 0) = (◑𝑔 β€œ β„•) β†’ (𝑔 supp 0) βŠ† (◑𝑔 β€œ β„•))
4038, 39syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (𝑔 supp 0) βŠ† (◑𝑔 β€œ β„•))
4135a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ β„• ∈ V)
42 0nn0 12435 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ β„•0
4342a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ 0 ∈ β„•0)
4434, 40, 41, 43suppssr 8132 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ (π‘”β€˜π‘˜) = 0)
4544oveq1d 7377 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) = (0 Β· π‘˜))
46 eldifi 4091 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•)) β†’ π‘˜ ∈ β„•)
4746adantl 483 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ π‘˜ ∈ β„•)
48 nncn 12168 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„‚)
49 mul02 11340 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ β„‚ β†’ (0 Β· π‘˜) = 0)
5047, 48, 493syl 18 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ (0 Β· π‘˜) = 0)
5145, 50eqtrd 2777 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) = 0)
52 nnuz 12813 . . . . . . . . . . . . . . . . . . 19 β„• = (β„€β‰₯β€˜1)
5352eqimssi 4007 . . . . . . . . . . . . . . . . . 18 β„• βŠ† (β„€β‰₯β€˜1)
5453a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ β„• βŠ† (β„€β‰₯β€˜1))
5526, 33, 51, 54sumss 15616 . . . . . . . . . . . . . . . 16 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜) = Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
56 simpr 486 . . . . . . . . . . . . . . . . 17 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (◑𝑔 β€œ β„•) ∈ Fin)
5756, 32fsumnn0cl 15628 . . . . . . . . . . . . . . . 16 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
5855, 57eqeltrrd 2839 . . . . . . . . . . . . . . 15 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
59 eleq1 2826 . . . . . . . . . . . . . . 15 (Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁 β†’ (Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0 ↔ 𝑁 ∈ β„•0))
6058, 59syl5ibcom 244 . . . . . . . . . . . . . 14 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁 β†’ 𝑁 ∈ β„•0))
61603impia 1118 . . . . . . . . . . . . 13 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ 𝑁 ∈ β„•0)
6261adantr 482 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 𝑁 ∈ β„•0)
6362nn0red 12481 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 𝑁 ∈ ℝ)
6418nn0ge0d 12483 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 0 ≀ (π‘”β€˜π‘₯))
65 nnge1 12188 . . . . . . . . . . . . 13 (π‘₯ ∈ β„• β†’ 1 ≀ π‘₯)
6665adantl 483 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 1 ≀ π‘₯)
6719, 21, 64, 66lemulge11d 12099 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ≀ ((π‘”β€˜π‘₯) Β· π‘₯))
6856adantr 482 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ (◑𝑔 β€œ β„•) ∈ Fin)
6932nn0red 12481 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ ℝ)
7069adantlr 714 . . . . . . . . . . . . . . . . 17 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ ℝ)
7132nn0ge0d 12483 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ 0 ≀ ((π‘”β€˜π‘˜) Β· π‘˜))
7271adantlr 714 . . . . . . . . . . . . . . . . 17 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ 0 ≀ ((π‘”β€˜π‘˜) Β· π‘˜))
73 fveq2 6847 . . . . . . . . . . . . . . . . . 18 (π‘˜ = π‘₯ β†’ (π‘”β€˜π‘˜) = (π‘”β€˜π‘₯))
74 id 22 . . . . . . . . . . . . . . . . . 18 (π‘˜ = π‘₯ β†’ π‘˜ = π‘₯)
7573, 74oveq12d 7380 . . . . . . . . . . . . . . . . 17 (π‘˜ = π‘₯ β†’ ((π‘”β€˜π‘˜) Β· π‘˜) = ((π‘”β€˜π‘₯) Β· π‘₯))
76 simprr 772 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ π‘₯ ∈ (◑𝑔 β€œ β„•))
7768, 70, 72, 75, 76fsumge1 15689 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
7877expr 458 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ (π‘₯ ∈ (◑𝑔 β€œ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜)))
79 eldif 3925 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (β„• βˆ– (◑𝑔 β€œ β„•)) ↔ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•)))
8051ralrimiva 3144 . . . . . . . . . . . . . . . . . . 19 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))((π‘”β€˜π‘˜) Β· π‘˜) = 0)
8175eqeq1d 2739 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = π‘₯ β†’ (((π‘”β€˜π‘˜) Β· π‘˜) = 0 ↔ ((π‘”β€˜π‘₯) Β· π‘₯) = 0))
8281rspccva 3583 . . . . . . . . . . . . . . . . . . 19 ((βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))((π‘”β€˜π‘˜) Β· π‘˜) = 0 ∧ π‘₯ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) = 0)
8380, 82sylan 581 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) = 0)
8479, 83sylan2br 596 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) = 0)
8556adantr 482 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ (◑𝑔 β€œ β„•) ∈ Fin)
8632adantlr 714 . . . . . . . . . . . . . . . . . . . 20 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
8786nn0red 12481 . . . . . . . . . . . . . . . . . . 19 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ ℝ)
8886nn0ge0d 12483 . . . . . . . . . . . . . . . . . . 19 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ 0 ≀ ((π‘”β€˜π‘˜) Β· π‘˜))
8985, 87, 88fsumge0 15687 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ 0 ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9089adantrr 716 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ 0 ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9184, 90eqbrtrd 5132 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9291expr 458 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ (Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜)))
9378, 92pm2.61d 179 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9455adantr 482 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜) = Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
9593, 94breqtrd 5136 . . . . . . . . . . . . 13 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
96953adantl3 1169 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
97 simpl3 1194 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁)
9896, 97breqtrd 5136 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ 𝑁)
9919, 22, 63, 67, 98letrd 11319 . . . . . . . . . 10 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ≀ 𝑁)
100 nn0uz 12812 . . . . . . . . . . . 12 β„•0 = (β„€β‰₯β€˜0)
10118, 100eleqtrdi 2848 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ (β„€β‰₯β€˜0))
10262nn0zd 12532 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 𝑁 ∈ β„€)
103 elfz5 13440 . . . . . . . . . . 11 (((π‘”β€˜π‘₯) ∈ (β„€β‰₯β€˜0) ∧ 𝑁 ∈ β„€) β†’ ((π‘”β€˜π‘₯) ∈ (0...𝑁) ↔ (π‘”β€˜π‘₯) ≀ 𝑁))
104101, 102, 103syl2anc 585 . . . . . . . . . 10 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ (0...𝑁) ↔ (π‘”β€˜π‘₯) ≀ 𝑁))
10599, 104mpbird 257 . . . . . . . . 9 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ (0...𝑁))
106105adantr 482 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ (0...𝑁))
107 iftrue 4497 . . . . . . . . 9 (π‘₯ ∈ (1...𝑁) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = (0...𝑁))
108107adantl 483 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ π‘₯ ∈ (1...𝑁)) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = (0...𝑁))
109106, 108eleqtrrd 2841 . . . . . . 7 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
110 nnge1 12188 . . . . . . . . . . . . . 14 ((π‘”β€˜π‘₯) ∈ β„• β†’ 1 ≀ (π‘”β€˜π‘₯))
111 nnnn0 12427 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ β„• β†’ π‘₯ ∈ β„•0)
112111adantl 483 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ β„•0)
113112nn0ge0d 12483 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 0 ≀ π‘₯)
114 lemulge12 12025 . . . . . . . . . . . . . . . . 17 (((π‘₯ ∈ ℝ ∧ (π‘”β€˜π‘₯) ∈ ℝ) ∧ (0 ≀ π‘₯ ∧ 1 ≀ (π‘”β€˜π‘₯))) β†’ π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯))
115114expr 458 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ ℝ ∧ (π‘”β€˜π‘₯) ∈ ℝ) ∧ 0 ≀ π‘₯) β†’ (1 ≀ (π‘”β€˜π‘₯) β†’ π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯)))
11621, 19, 113, 115syl21anc 837 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (1 ≀ (π‘”β€˜π‘₯) β†’ π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯)))
117 letr 11256 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ ℝ ∧ ((π‘”β€˜π‘₯) Β· π‘₯) ∈ ℝ ∧ 𝑁 ∈ ℝ) β†’ ((π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯) ∧ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ 𝑁) β†’ π‘₯ ≀ 𝑁))
11821, 22, 63, 117syl3anc 1372 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯) ∧ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ 𝑁) β†’ π‘₯ ≀ 𝑁))
11998, 118mpan2d 693 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯) β†’ π‘₯ ≀ 𝑁))
120116, 119syld 47 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (1 ≀ (π‘”β€˜π‘₯) β†’ π‘₯ ≀ 𝑁))
121110, 120syl5 34 . . . . . . . . . . . . 13 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ β„• β†’ π‘₯ ≀ 𝑁))
122 simpr 486 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ β„•)
123122, 52eleqtrdi 2848 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ (β„€β‰₯β€˜1))
124 elfz5 13440 . . . . . . . . . . . . . 14 ((π‘₯ ∈ (β„€β‰₯β€˜1) ∧ 𝑁 ∈ β„€) β†’ (π‘₯ ∈ (1...𝑁) ↔ π‘₯ ≀ 𝑁))
125123, 102, 124syl2anc 585 . . . . . . . . . . . . 13 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘₯ ∈ (1...𝑁) ↔ π‘₯ ≀ 𝑁))
126121, 125sylibrd 259 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ β„• β†’ π‘₯ ∈ (1...𝑁)))
127126con3d 152 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (Β¬ π‘₯ ∈ (1...𝑁) β†’ Β¬ (π‘”β€˜π‘₯) ∈ β„•))
128 elnn0 12422 . . . . . . . . . . . . 13 ((π‘”β€˜π‘₯) ∈ β„•0 ↔ ((π‘”β€˜π‘₯) ∈ β„• ∨ (π‘”β€˜π‘₯) = 0))
12918, 128sylib 217 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ β„• ∨ (π‘”β€˜π‘₯) = 0))
130129ord 863 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (Β¬ (π‘”β€˜π‘₯) ∈ β„• β†’ (π‘”β€˜π‘₯) = 0))
131127, 130syld 47 . . . . . . . . . 10 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (Β¬ π‘₯ ∈ (1...𝑁) β†’ (π‘”β€˜π‘₯) = 0))
132131imp 408 . . . . . . . . 9 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) = 0)
133 fvex 6860 . . . . . . . . . 10 (π‘”β€˜π‘₯) ∈ V
134133elsn 4606 . . . . . . . . 9 ((π‘”β€˜π‘₯) ∈ {0} ↔ (π‘”β€˜π‘₯) = 0)
135132, 134sylibr 233 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ {0})
1368adantl 483 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = {0})
137135, 136eleqtrrd 2841 . . . . . . 7 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
138109, 137pm2.61dan 812 . . . . . 6 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
139138ralrimiva 3144 . . . . 5 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ βˆ€π‘₯ ∈ β„• (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
140 vex 3452 . . . . . 6 𝑔 ∈ V
141140elixp 8849 . . . . 5 (𝑔 ∈ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ↔ (𝑔 Fn β„• ∧ βˆ€π‘₯ ∈ β„• (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0})))
14216, 139, 141sylanbrc 584 . . . 4 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ 𝑔 ∈ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
14314, 142sylbi 216 . . 3 (𝑔 ∈ 𝑃 β†’ 𝑔 ∈ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
144143ssriv 3953 . 2 𝑃 βŠ† Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0})
145 ssfi 9124 . 2 ((Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin ∧ 𝑃 βŠ† Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0})) β†’ 𝑃 ∈ Fin)
14612, 144, 145mp2an 691 1 𝑃 ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107  βˆ€wral 3065  {crab 3410  Vcvv 3448   βˆ– cdif 3912   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287  ifcif 4491  π’« cpw 4565  {csn 4591   class class class wbr 5110  {copab 5172   ↦ cmpt 5193  β—‘ccnv 5637  dom cdm 5638   β€œ cima 5641   Fn wfn 6496  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   ∈ cmpo 7364   supp csupp 8097   ↑m cmap 8772  Xcixp 8842  Fincfn 8890  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   Β· cmul 11063   ≀ cle 11197  β„•cn 12160  2c2 12215  β„•0cn0 12420  β„€cz 12506  β„€β‰₯cuz 12770  ...cfz 13431  β†‘cexp 13974  Ξ£csu 15577   βˆ₯ cdvds 16143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-rp 12923  df-ico 13277  df-fz 13432  df-fzo 13575  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-sum 15578
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator