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 33924
Description: Lemma for eulerpart 33938. 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 13962 . . . 4 (⊀ β†’ (1...𝑁) ∈ Fin)
2 fzfi 13961 . . . . . 6 (0...𝑁) ∈ Fin
3 snfi 9060 . . . . . 6 {0} ∈ Fin
42, 3ifcli 4571 . . . . 5 if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin
54a1i 11 . . . 4 ((⊀ ∧ π‘₯ ∈ β„•) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin)
6 eldifn 4123 . . . . . 6 (π‘₯ ∈ (β„• βˆ– (1...𝑁)) β†’ Β¬ π‘₯ ∈ (1...𝑁))
76adantl 481 . . . . 5 ((⊀ ∧ π‘₯ ∈ (β„• βˆ– (1...𝑁))) β†’ Β¬ π‘₯ ∈ (1...𝑁))
8 iffalse 4533 . . . . 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 9366 . . 3 (⊀ β†’ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin)
1211mptru 1541 . 2 Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ∈ Fin
13 eulerpart.p . . . . 5 𝑃 = {𝑓 ∈ (β„•0 ↑m β„•) ∣ ((◑𝑓 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘“β€˜π‘˜) Β· π‘˜) = 𝑁)}
1413eulerpartleme 33919 . . . 4 (𝑔 ∈ 𝑃 ↔ (𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁))
15 ffn 6716 . . . . . 6 (𝑔:β„•βŸΆβ„•0 β†’ 𝑔 Fn β„•)
16153ad2ant1 1131 . . . . 5 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ 𝑔 Fn β„•)
17 ffvelcdm 7085 . . . . . . . . . . . . 13 ((𝑔:β„•βŸΆβ„•0 ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ β„•0)
18173ad2antl1 1183 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ β„•0)
1918nn0red 12555 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ ℝ)
20 nnre 12241 . . . . . . . . . . . . 13 (π‘₯ ∈ β„• β†’ π‘₯ ∈ ℝ)
2120adantl 481 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ ℝ)
2219, 21remulcld 11266 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ∈ ℝ)
23 cnvimass 6079 . . . . . . . . . . . . . . . . . 18 (◑𝑔 β€œ β„•) βŠ† dom 𝑔
24 fdm 6725 . . . . . . . . . . . . . . . . . . 19 (𝑔:β„•βŸΆβ„•0 β†’ dom 𝑔 = β„•)
2524adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ dom 𝑔 = β„•)
2623, 25sseqtrid 4030 . . . . . . . . . . . . . . . . 17 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (◑𝑔 β€œ β„•) βŠ† β„•)
2726sselda 3978 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ π‘˜ ∈ β„•)
28 ffvelcdm 7085 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔:β„•βŸΆβ„•0 ∧ π‘˜ ∈ β„•) β†’ (π‘”β€˜π‘˜) ∈ β„•0)
2928adantlr 714 . . . . . . . . . . . . . . . . . . . 20 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ β„•) β†’ (π‘”β€˜π‘˜) ∈ β„•0)
3027, 29syldan 590 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ (π‘”β€˜π‘˜) ∈ β„•0)
3127nnnn0d 12554 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ π‘˜ ∈ β„•0)
3230, 31nn0mulcld 12559 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
3332nn0cnd 12556 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„‚)
34 simpl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ 𝑔:β„•βŸΆβ„•0)
35 nnex 12240 . . . . . . . . . . . . . . . . . . . . . . 23 β„• ∈ V
36 fcdmnn0supp 12550 . . . . . . . . . . . . . . . . . . . . . . 23 ((β„• ∈ V ∧ 𝑔:β„•βŸΆβ„•0) β†’ (𝑔 supp 0) = (◑𝑔 β€œ β„•))
3735, 36mpan 689 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔:β„•βŸΆβ„•0 β†’ (𝑔 supp 0) = (◑𝑔 β€œ β„•))
3837adantr 480 . . . . . . . . . . . . . . . . . . . . 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 12509 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ β„•0
4342a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ 0 ∈ β„•0)
4434, 40, 41, 43suppssr 8194 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ (π‘”β€˜π‘˜) = 0)
4544oveq1d 7429 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) = (0 Β· π‘˜))
46 eldifi 4122 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•)) β†’ π‘˜ ∈ β„•)
4746adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ π‘˜ ∈ β„•)
48 nncn 12242 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„‚)
49 mul02 11414 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ β„‚ β†’ (0 Β· π‘˜) = 0)
5047, 48, 493syl 18 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ (0 Β· π‘˜) = 0)
5145, 50eqtrd 2767 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) = 0)
52 nnuz 12887 . . . . . . . . . . . . . . . . . . 19 β„• = (β„€β‰₯β€˜1)
5352eqimssi 4038 . . . . . . . . . . . . . . . . . 18 β„• βŠ† (β„€β‰₯β€˜1)
5453a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ β„• βŠ† (β„€β‰₯β€˜1))
5526, 33, 51, 54sumss 15694 . . . . . . . . . . . . . . . 16 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜) = Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
56 simpr 484 . . . . . . . . . . . . . . . . 17 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (◑𝑔 β€œ β„•) ∈ Fin)
5756, 32fsumnn0cl 15706 . . . . . . . . . . . . . . . 16 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
5855, 57eqeltrrd 2829 . . . . . . . . . . . . . . 15 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
59 eleq1 2816 . . . . . . . . . . . . . . 15 (Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁 β†’ (Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0 ↔ 𝑁 ∈ β„•0))
6058, 59syl5ibcom 244 . . . . . . . . . . . . . 14 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ (Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁 β†’ 𝑁 ∈ β„•0))
61603impia 1115 . . . . . . . . . . . . 13 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ 𝑁 ∈ β„•0)
6261adantr 480 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 𝑁 ∈ β„•0)
6362nn0red 12555 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 𝑁 ∈ ℝ)
6418nn0ge0d 12557 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 0 ≀ (π‘”β€˜π‘₯))
65 nnge1 12262 . . . . . . . . . . . . 13 (π‘₯ ∈ β„• β†’ 1 ≀ π‘₯)
6665adantl 481 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 1 ≀ π‘₯)
6719, 21, 64, 66lemulge11d 12173 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ≀ ((π‘”β€˜π‘₯) Β· π‘₯))
6856adantr 480 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ (◑𝑔 β€œ β„•) ∈ Fin)
6932nn0red 12555 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ ℝ)
7069adantlr 714 . . . . . . . . . . . . . . . . 17 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ ℝ)
7132nn0ge0d 12557 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ 0 ≀ ((π‘”β€˜π‘˜) Β· π‘˜))
7271adantlr 714 . . . . . . . . . . . . . . . . 17 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ 0 ≀ ((π‘”β€˜π‘˜) Β· π‘˜))
73 fveq2 6891 . . . . . . . . . . . . . . . . . 18 (π‘˜ = π‘₯ β†’ (π‘”β€˜π‘˜) = (π‘”β€˜π‘₯))
74 id 22 . . . . . . . . . . . . . . . . . 18 (π‘˜ = π‘₯ β†’ π‘˜ = π‘₯)
7573, 74oveq12d 7432 . . . . . . . . . . . . . . . . 17 (π‘˜ = π‘₯ β†’ ((π‘”β€˜π‘˜) Β· π‘˜) = ((π‘”β€˜π‘₯) Β· π‘₯))
76 simprr 772 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ π‘₯ ∈ (◑𝑔 β€œ β„•))
7768, 70, 72, 75, 76fsumge1 15767 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
7877expr 456 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ (π‘₯ ∈ (◑𝑔 β€œ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜)))
79 eldif 3954 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (β„• βˆ– (◑𝑔 β€œ β„•)) ↔ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•)))
8051ralrimiva 3141 . . . . . . . . . . . . . . . . . . 19 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) β†’ βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))((π‘”β€˜π‘˜) Β· π‘˜) = 0)
8175eqeq1d 2729 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ = π‘₯ β†’ (((π‘”β€˜π‘˜) Β· π‘˜) = 0 ↔ ((π‘”β€˜π‘₯) Β· π‘₯) = 0))
8281rspccva 3606 . . . . . . . . . . . . . . . . . . 19 ((βˆ€π‘˜ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))((π‘”β€˜π‘˜) Β· π‘˜) = 0 ∧ π‘₯ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) = 0)
8380, 82sylan 579 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ (β„• βˆ– (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) = 0)
8479, 83sylan2br 594 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) = 0)
8556adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ (◑𝑔 β€œ β„•) ∈ Fin)
8632adantlr 714 . . . . . . . . . . . . . . . . . . . 20 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ β„•0)
8786nn0red 12555 . . . . . . . . . . . . . . . . . . 19 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ ((π‘”β€˜π‘˜) Β· π‘˜) ∈ ℝ)
8886nn0ge0d 12557 . . . . . . . . . . . . . . . . . . 19 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) ∧ π‘˜ ∈ (◑𝑔 β€œ β„•)) β†’ 0 ≀ ((π‘”β€˜π‘˜) Β· π‘˜))
8985, 87, 88fsumge0 15765 . . . . . . . . . . . . . . . . . 18 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ 0 ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9089adantrr 716 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ 0 ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9184, 90eqbrtrd 5164 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ (π‘₯ ∈ β„• ∧ Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•))) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9291expr 456 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ (Β¬ π‘₯ ∈ (◑𝑔 β€œ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜)))
9378, 92pm2.61d 179 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜))
9455adantr 480 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ Ξ£π‘˜ ∈ (◑𝑔 β€œ β„•)((π‘”β€˜π‘˜) Β· π‘˜) = Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
9593, 94breqtrd 5168 . . . . . . . . . . . . 13 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
96953adantl3 1166 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜))
97 simpl3 1191 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁)
9896, 97breqtrd 5168 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ 𝑁)
9919, 22, 63, 67, 98letrd 11393 . . . . . . . . . 10 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ≀ 𝑁)
100 nn0uz 12886 . . . . . . . . . . . 12 β„•0 = (β„€β‰₯β€˜0)
10118, 100eleqtrdi 2838 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ (β„€β‰₯β€˜0))
10262nn0zd 12606 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 𝑁 ∈ β„€)
103 elfz5 13517 . . . . . . . . . . 11 (((π‘”β€˜π‘₯) ∈ (β„€β‰₯β€˜0) ∧ 𝑁 ∈ β„€) β†’ ((π‘”β€˜π‘₯) ∈ (0...𝑁) ↔ (π‘”β€˜π‘₯) ≀ 𝑁))
104101, 102, 103syl2anc 583 . . . . . . . . . 10 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ (0...𝑁) ↔ (π‘”β€˜π‘₯) ≀ 𝑁))
10599, 104mpbird 257 . . . . . . . . 9 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ (0...𝑁))
106105adantr 480 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ (0...𝑁))
107 iftrue 4530 . . . . . . . . 9 (π‘₯ ∈ (1...𝑁) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = (0...𝑁))
108107adantl 481 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ π‘₯ ∈ (1...𝑁)) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = (0...𝑁))
109106, 108eleqtrrd 2831 . . . . . . 7 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
110 nnge1 12262 . . . . . . . . . . . . . 14 ((π‘”β€˜π‘₯) ∈ β„• β†’ 1 ≀ (π‘”β€˜π‘₯))
111 nnnn0 12501 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ β„• β†’ π‘₯ ∈ β„•0)
112111adantl 481 . . . . . . . . . . . . . . . . 17 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ β„•0)
113112nn0ge0d 12557 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ 0 ≀ π‘₯)
114 lemulge12 12099 . . . . . . . . . . . . . . . . 17 (((π‘₯ ∈ ℝ ∧ (π‘”β€˜π‘₯) ∈ ℝ) ∧ (0 ≀ π‘₯ ∧ 1 ≀ (π‘”β€˜π‘₯))) β†’ π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯))
115114expr 456 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ ℝ ∧ (π‘”β€˜π‘₯) ∈ ℝ) ∧ 0 ≀ π‘₯) β†’ (1 ≀ (π‘”β€˜π‘₯) β†’ π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯)))
11621, 19, 113, 115syl21anc 837 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (1 ≀ (π‘”β€˜π‘₯) β†’ π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯)))
117 letr 11330 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ ℝ ∧ ((π‘”β€˜π‘₯) Β· π‘₯) ∈ ℝ ∧ 𝑁 ∈ ℝ) β†’ ((π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯) ∧ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ 𝑁) β†’ π‘₯ ≀ 𝑁))
11821, 22, 63, 117syl3anc 1369 . . . . . . . . . . . . . . . 16 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯) ∧ ((π‘”β€˜π‘₯) Β· π‘₯) ≀ 𝑁) β†’ π‘₯ ≀ 𝑁))
11998, 118mpan2d 693 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘₯ ≀ ((π‘”β€˜π‘₯) Β· π‘₯) β†’ π‘₯ ≀ 𝑁))
120116, 119syld 47 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (1 ≀ (π‘”β€˜π‘₯) β†’ π‘₯ ≀ 𝑁))
121110, 120syl5 34 . . . . . . . . . . . . 13 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ β„• β†’ π‘₯ ≀ 𝑁))
122 simpr 484 . . . . . . . . . . . . . . 15 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ β„•)
123122, 52eleqtrdi 2838 . . . . . . . . . . . . . 14 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ π‘₯ ∈ (β„€β‰₯β€˜1))
124 elfz5 13517 . . . . . . . . . . . . . 14 ((π‘₯ ∈ (β„€β‰₯β€˜1) ∧ 𝑁 ∈ β„€) β†’ (π‘₯ ∈ (1...𝑁) ↔ π‘₯ ≀ 𝑁))
125123, 102, 124syl2anc 583 . . . . . . . . . . . . 13 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘₯ ∈ (1...𝑁) ↔ π‘₯ ≀ 𝑁))
126121, 125sylibrd 259 . . . . . . . . . . . 12 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ ((π‘”β€˜π‘₯) ∈ β„• β†’ π‘₯ ∈ (1...𝑁)))
127126con3d 152 . . . . . . . . . . 11 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (Β¬ π‘₯ ∈ (1...𝑁) β†’ Β¬ (π‘”β€˜π‘₯) ∈ β„•))
128 elnn0 12496 . . . . . . . . . . . . 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 406 . . . . . . . . 9 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) = 0)
133 fvex 6904 . . . . . . . . . 10 (π‘”β€˜π‘₯) ∈ V
134133elsn 4639 . . . . . . . . 9 ((π‘”β€˜π‘₯) ∈ {0} ↔ (π‘”β€˜π‘₯) = 0)
135132, 134sylibr 233 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ {0})
1368adantl 481 . . . . . . . 8 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) = {0})
137135, 136eleqtrrd 2831 . . . . . . 7 ((((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) ∧ Β¬ π‘₯ ∈ (1...𝑁)) β†’ (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
138109, 137pm2.61dan 812 . . . . . 6 (((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) ∧ π‘₯ ∈ β„•) β†’ (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
139138ralrimiva 3141 . . . . 5 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ βˆ€π‘₯ ∈ β„• (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
140 vex 3473 . . . . . 6 𝑔 ∈ V
141140elixp 8914 . . . . 5 (𝑔 ∈ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}) ↔ (𝑔 Fn β„• ∧ βˆ€π‘₯ ∈ β„• (π‘”β€˜π‘₯) ∈ if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0})))
14216, 139, 141sylanbrc 582 . . . 4 ((𝑔:β„•βŸΆβ„•0 ∧ (◑𝑔 β€œ β„•) ∈ Fin ∧ Ξ£π‘˜ ∈ β„• ((π‘”β€˜π‘˜) Β· π‘˜) = 𝑁) β†’ 𝑔 ∈ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
14314, 142sylbi 216 . . 3 (𝑔 ∈ 𝑃 β†’ 𝑔 ∈ Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0}))
144143ssriv 3982 . 2 𝑃 βŠ† Xπ‘₯ ∈ β„• if(π‘₯ ∈ (1...𝑁), (0...𝑁), {0})
145 ssfi 9189 . 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 395   ∨ wo 846   ∧ w3a 1085   = wceq 1534  βŠ€wtru 1535   ∈ wcel 2099  βˆ€wral 3056  {crab 3427  Vcvv 3469   βˆ– cdif 3941   ∩ cin 3943   βŠ† wss 3944  βˆ…c0 4318  ifcif 4524  π’« cpw 4598  {csn 4624   class class class wbr 5142  {copab 5204   ↦ cmpt 5225  β—‘ccnv 5671  dom cdm 5672   β€œ cima 5675   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7414   ∈ cmpo 7416   supp csupp 8159   ↑m cmap 8836  Xcixp 8907  Fincfn 8955  β„‚cc 11128  β„cr 11129  0cc0 11130  1c1 11131   Β· cmul 11135   ≀ cle 11271  β„•cn 12234  2c2 12289  β„•0cn0 12494  β„€cz 12580  β„€β‰₯cuz 12844  ...cfz 13508  β†‘cexp 14050  Ξ£csu 15656   βˆ₯ cdvds 16222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-map 8838  df-pm 8839  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-sup 9457  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-n0 12495  df-z 12581  df-uz 12845  df-rp 12999  df-ico 13354  df-fz 13509  df-fzo 13652  df-seq 13991  df-exp 14051  df-hash 14314  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-clim 15456  df-sum 15657
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator