Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eulerpartlemt Structured version   Visualization version   GIF version

Theorem eulerpartlemt 30561
Description: Lemma for eulerpart 30572. (Contributed by Thierry Arnoux, 19-Sep-2017.)
Hypotheses
Ref Expression
eulerpart.p 𝑃 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ ((𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘) = 𝑁)}
eulerpart.o 𝑂 = {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
eulerpart.d 𝐷 = {𝑔𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔𝑛) ≤ 1}
eulerpart.j 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
eulerpart.f 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
eulerpart.h 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
eulerpart.m 𝑀 = (𝑟𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ (𝑟𝑥))})
eulerpart.r 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
eulerpart.t 𝑇 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
Assertion
Ref Expression
eulerpartlemt ((ℕ0𝑚 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽))
Distinct variable groups:   𝑓,𝑚,𝐽   𝑅,𝑚   𝑇,𝑚
Allowed substitution hints:   𝐷(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑚,𝑛,𝑟)   𝑃(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑚,𝑛,𝑟)   𝑅(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝑇(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑛,𝑟)   𝐹(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑚,𝑛,𝑟)   𝐻(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑚,𝑛,𝑟)   𝐽(𝑥,𝑦,𝑧,𝑔,𝑘,𝑛,𝑟)   𝑀(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑚,𝑛,𝑟)   𝑁(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑚,𝑛,𝑟)   𝑂(𝑥,𝑦,𝑧,𝑓,𝑔,𝑘,𝑚,𝑛,𝑟)

Proof of Theorem eulerpartlemt
Dummy variable 𝑜 is distinct from all other variables.
StepHypRef Expression
1 elmapi 7921 . . . . . . . . . 10 (𝑜 ∈ (ℕ0𝑚 𝐽) → 𝑜:𝐽⟶ℕ0)
21adantr 480 . . . . . . . . 9 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → 𝑜:𝐽⟶ℕ0)
3 c0ex 10072 . . . . . . . . . . 11 0 ∈ V
43fconst 6129 . . . . . . . . . 10 ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0}
54a1i 11 . . . . . . . . 9 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0})
6 disjdif 4073 . . . . . . . . . 10 (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅
76a1i 11 . . . . . . . . 9 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅)
8 fun 6104 . . . . . . . . 9 (((𝑜:𝐽⟶ℕ0 ∧ ((ℕ ∖ 𝐽) × {0}):(ℕ ∖ 𝐽)⟶{0}) ∧ (𝐽 ∩ (ℕ ∖ 𝐽)) = ∅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪ {0}))
92, 5, 7, 8syl21anc 1365 . . . . . . . 8 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪ {0}))
10 eulerpart.j . . . . . . . . . . 11 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}
11 ssrab2 3720 . . . . . . . . . . 11 {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} ⊆ ℕ
1210, 11eqsstri 3668 . . . . . . . . . 10 𝐽 ⊆ ℕ
13 undif 4082 . . . . . . . . . 10 (𝐽 ⊆ ℕ ↔ (𝐽 ∪ (ℕ ∖ 𝐽)) = ℕ)
1412, 13mpbi 220 . . . . . . . . 9 (𝐽 ∪ (ℕ ∖ 𝐽)) = ℕ
15 0nn0 11345 . . . . . . . . . . 11 0 ∈ ℕ0
16 snssi 4371 . . . . . . . . . . 11 (0 ∈ ℕ0 → {0} ⊆ ℕ0)
1715, 16ax-mp 5 . . . . . . . . . 10 {0} ⊆ ℕ0
18 ssequn2 3819 . . . . . . . . . 10 ({0} ⊆ ℕ0 ↔ (ℕ0 ∪ {0}) = ℕ0)
1917, 18mpbi 220 . . . . . . . . 9 (ℕ0 ∪ {0}) = ℕ0
2014, 19feq23i 6077 . . . . . . . 8 ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):(𝐽 ∪ (ℕ ∖ 𝐽))⟶(ℕ0 ∪ {0}) ↔ (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
219, 20sylib 208 . . . . . . 7 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
22 nn0ex 11336 . . . . . . . 8 0 ∈ V
23 nnex 11064 . . . . . . . 8 ℕ ∈ V
2422, 23elmap 7928 . . . . . . 7 ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0𝑚 ℕ) ↔ (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})):ℕ⟶ℕ0)
2521, 24sylibr 224 . . . . . 6 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0𝑚 ℕ))
26 cnvun 5573 . . . . . . . . 9 (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) = (𝑜((ℕ ∖ 𝐽) × {0}))
2726imaeq1i 5498 . . . . . . . 8 ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((𝑜((ℕ ∖ 𝐽) × {0})) “ ℕ)
28 imaundir 5581 . . . . . . . 8 ((𝑜((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((𝑜 “ ℕ) ∪ (((ℕ ∖ 𝐽) × {0}) “ ℕ))
2927, 28eqtri 2673 . . . . . . 7 ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) = ((𝑜 “ ℕ) ∪ (((ℕ ∖ 𝐽) × {0}) “ ℕ))
30 vex 3234 . . . . . . . . . . 11 𝑜 ∈ V
31 cnveq 5328 . . . . . . . . . . . . 13 (𝑓 = 𝑜𝑓 = 𝑜)
3231imaeq1d 5500 . . . . . . . . . . . 12 (𝑓 = 𝑜 → (𝑓 “ ℕ) = (𝑜 “ ℕ))
3332eleq1d 2715 . . . . . . . . . . 11 (𝑓 = 𝑜 → ((𝑓 “ ℕ) ∈ Fin ↔ (𝑜 “ ℕ) ∈ Fin))
34 eulerpart.r . . . . . . . . . . 11 𝑅 = {𝑓 ∣ (𝑓 “ ℕ) ∈ Fin}
3530, 33, 34elab2 3386 . . . . . . . . . 10 (𝑜𝑅 ↔ (𝑜 “ ℕ) ∈ Fin)
3635biimpi 206 . . . . . . . . 9 (𝑜𝑅 → (𝑜 “ ℕ) ∈ Fin)
3736adantl 481 . . . . . . . 8 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → (𝑜 “ ℕ) ∈ Fin)
38 cnvxp 5586 . . . . . . . . . . . . . 14 ((ℕ ∖ 𝐽) × {0}) = ({0} × (ℕ ∖ 𝐽))
3938dmeqi 5357 . . . . . . . . . . . . 13 dom ((ℕ ∖ 𝐽) × {0}) = dom ({0} × (ℕ ∖ 𝐽))
40 2nn 11223 . . . . . . . . . . . . . . 15 2 ∈ ℕ
41 2z 11447 . . . . . . . . . . . . . . . . 17 2 ∈ ℤ
42 iddvds 15042 . . . . . . . . . . . . . . . . 17 (2 ∈ ℤ → 2 ∥ 2)
4341, 42ax-mp 5 . . . . . . . . . . . . . . . 16 2 ∥ 2
44 breq2 4689 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 2 → (2 ∥ 𝑧 ↔ 2 ∥ 2))
4544notbid 307 . . . . . . . . . . . . . . . . . 18 (𝑧 = 2 → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 2))
4645, 10elrab2 3399 . . . . . . . . . . . . . . . . 17 (2 ∈ 𝐽 ↔ (2 ∈ ℕ ∧ ¬ 2 ∥ 2))
4746simprbi 479 . . . . . . . . . . . . . . . 16 (2 ∈ 𝐽 → ¬ 2 ∥ 2)
4843, 47mt2 191 . . . . . . . . . . . . . . 15 ¬ 2 ∈ 𝐽
49 eldif 3617 . . . . . . . . . . . . . . 15 (2 ∈ (ℕ ∖ 𝐽) ↔ (2 ∈ ℕ ∧ ¬ 2 ∈ 𝐽))
5040, 48, 49mpbir2an 975 . . . . . . . . . . . . . 14 2 ∈ (ℕ ∖ 𝐽)
51 ne0i 3954 . . . . . . . . . . . . . 14 (2 ∈ (ℕ ∖ 𝐽) → (ℕ ∖ 𝐽) ≠ ∅)
52 dmxp 5376 . . . . . . . . . . . . . 14 ((ℕ ∖ 𝐽) ≠ ∅ → dom ({0} × (ℕ ∖ 𝐽)) = {0})
5350, 51, 52mp2b 10 . . . . . . . . . . . . 13 dom ({0} × (ℕ ∖ 𝐽)) = {0}
5439, 53eqtri 2673 . . . . . . . . . . . 12 dom ((ℕ ∖ 𝐽) × {0}) = {0}
5554ineq1i 3843 . . . . . . . . . . 11 (dom ((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ({0} ∩ ℕ)
56 incom 3838 . . . . . . . . . . 11 (ℕ ∩ {0}) = ({0} ∩ ℕ)
57 0nnn 11090 . . . . . . . . . . . 12 ¬ 0 ∈ ℕ
58 disjsn 4278 . . . . . . . . . . . 12 ((ℕ ∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ)
5957, 58mpbir 221 . . . . . . . . . . 11 (ℕ ∩ {0}) = ∅
6055, 56, 593eqtr2i 2679 . . . . . . . . . 10 (dom ((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ∅
61 imadisj 5519 . . . . . . . . . 10 ((((ℕ ∖ 𝐽) × {0}) “ ℕ) = ∅ ↔ (dom ((ℕ ∖ 𝐽) × {0}) ∩ ℕ) = ∅)
6260, 61mpbir 221 . . . . . . . . 9 (((ℕ ∖ 𝐽) × {0}) “ ℕ) = ∅
63 0fin 8229 . . . . . . . . 9 ∅ ∈ Fin
6462, 63eqeltri 2726 . . . . . . . 8 (((ℕ ∖ 𝐽) × {0}) “ ℕ) ∈ Fin
65 unfi 8268 . . . . . . . 8 (((𝑜 “ ℕ) ∈ Fin ∧ (((ℕ ∖ 𝐽) × {0}) “ ℕ) ∈ Fin) → ((𝑜 “ ℕ) ∪ (((ℕ ∖ 𝐽) × {0}) “ ℕ)) ∈ Fin)
6637, 64, 65sylancl 695 . . . . . . 7 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → ((𝑜 “ ℕ) ∪ (((ℕ ∖ 𝐽) × {0}) “ ℕ)) ∈ Fin)
6729, 66syl5eqel 2734 . . . . . 6 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ∈ Fin)
68 cnvimass 5520 . . . . . . . . 9 (𝑜 “ ℕ) ⊆ dom 𝑜
69 fdm 6089 . . . . . . . . . 10 (𝑜:𝐽⟶ℕ0 → dom 𝑜 = 𝐽)
702, 69syl 17 . . . . . . . . 9 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → dom 𝑜 = 𝐽)
7168, 70syl5sseq 3686 . . . . . . . 8 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → (𝑜 “ ℕ) ⊆ 𝐽)
72 0ss 4005 . . . . . . . . . 10 ∅ ⊆ 𝐽
7362, 72eqsstri 3668 . . . . . . . . 9 (((ℕ ∖ 𝐽) × {0}) “ ℕ) ⊆ 𝐽
7473a1i 11 . . . . . . . 8 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → (((ℕ ∖ 𝐽) × {0}) “ ℕ) ⊆ 𝐽)
7571, 74unssd 3822 . . . . . . 7 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → ((𝑜 “ ℕ) ∪ (((ℕ ∖ 𝐽) × {0}) “ ℕ)) ⊆ 𝐽)
7629, 75syl5eqss 3682 . . . . . 6 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ⊆ 𝐽)
77 eulerpart.p . . . . . . 7 𝑃 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ ((𝑓 “ ℕ) ∈ Fin ∧ Σ𝑘 ∈ ℕ ((𝑓𝑘) · 𝑘) = 𝑁)}
78 eulerpart.o . . . . . . 7 𝑂 = {𝑔𝑃 ∣ ∀𝑛 ∈ (𝑔 “ ℕ) ¬ 2 ∥ 𝑛}
79 eulerpart.d . . . . . . 7 𝐷 = {𝑔𝑃 ∣ ∀𝑛 ∈ ℕ (𝑔𝑛) ≤ 1}
80 eulerpart.f . . . . . . 7 𝐹 = (𝑥𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))
81 eulerpart.h . . . . . . 7 𝐻 = {𝑟 ∈ ((𝒫 ℕ0 ∩ Fin) ↑𝑚 𝐽) ∣ (𝑟 supp ∅) ∈ Fin}
82 eulerpart.m . . . . . . 7 𝑀 = (𝑟𝐻 ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐽𝑦 ∈ (𝑟𝑥))})
83 eulerpart.t . . . . . . 7 𝑇 = {𝑓 ∈ (ℕ0𝑚 ℕ) ∣ (𝑓 “ ℕ) ⊆ 𝐽}
8477, 78, 79, 10, 80, 81, 82, 34, 83eulerpartlemt0 30559 . . . . . 6 ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇𝑅) ↔ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (ℕ0𝑚 ℕ) ∧ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ∈ Fin ∧ ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) “ ℕ) ⊆ 𝐽))
8525, 67, 76, 84syl3anbrc 1265 . . . . 5 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇𝑅))
86 resundir 5446 . . . . . 6 ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽) = ((𝑜𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽))
87 ffn 6083 . . . . . . . 8 (𝑜:𝐽⟶ℕ0𝑜 Fn 𝐽)
88 fnresdm 6038 . . . . . . . . 9 (𝑜 Fn 𝐽 → (𝑜𝐽) = 𝑜)
89 incom 3838 . . . . . . . . . . . 12 ((ℕ ∖ 𝐽) ∩ 𝐽) = (𝐽 ∩ (ℕ ∖ 𝐽))
9089, 6eqtri 2673 . . . . . . . . . . 11 ((ℕ ∖ 𝐽) ∩ 𝐽) = ∅
91 fnconstg 6131 . . . . . . . . . . . 12 (0 ∈ ℕ0 → ((ℕ ∖ 𝐽) × {0}) Fn (ℕ ∖ 𝐽))
92 fnresdisj 6039 . . . . . . . . . . . 12 (((ℕ ∖ 𝐽) × {0}) Fn (ℕ ∖ 𝐽) → (((ℕ ∖ 𝐽) ∩ 𝐽) = ∅ ↔ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅))
9315, 91, 92mp2b 10 . . . . . . . . . . 11 (((ℕ ∖ 𝐽) ∩ 𝐽) = ∅ ↔ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅)
9490, 93mpbi 220 . . . . . . . . . 10 (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅
9594a1i 11 . . . . . . . . 9 (𝑜 Fn 𝐽 → (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽) = ∅)
9688, 95uneq12d 3801 . . . . . . . 8 (𝑜 Fn 𝐽 → ((𝑜𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = (𝑜 ∪ ∅))
972, 87, 963syl 18 . . . . . . 7 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → ((𝑜𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = (𝑜 ∪ ∅))
98 un0 4000 . . . . . . 7 (𝑜 ∪ ∅) = 𝑜
9997, 98syl6eq 2701 . . . . . 6 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → ((𝑜𝐽) ∪ (((ℕ ∖ 𝐽) × {0}) ↾ 𝐽)) = 𝑜)
10086, 99syl5req 2698 . . . . 5 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽))
101 reseq1 5422 . . . . . . 7 (𝑚 = (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) → (𝑚𝐽) = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽))
102101eqeq2d 2661 . . . . . 6 (𝑚 = (𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) → (𝑜 = (𝑚𝐽) ↔ 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽)))
103102rspcev 3340 . . . . 5 (((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ∈ (𝑇𝑅) ∧ 𝑜 = ((𝑜 ∪ ((ℕ ∖ 𝐽) × {0})) ↾ 𝐽)) → ∃𝑚 ∈ (𝑇𝑅)𝑜 = (𝑚𝐽))
10485, 100, 103syl2anc 694 . . . 4 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) → ∃𝑚 ∈ (𝑇𝑅)𝑜 = (𝑚𝐽))
105 simpr 476 . . . . . . 7 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → 𝑜 = (𝑚𝐽))
106 simpl 472 . . . . . . . . . . . 12 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → 𝑚 ∈ (𝑇𝑅))
10777, 78, 79, 10, 80, 81, 82, 34, 83eulerpartlemt0 30559 . . . . . . . . . . . 12 (𝑚 ∈ (𝑇𝑅) ↔ (𝑚 ∈ (ℕ0𝑚 ℕ) ∧ (𝑚 “ ℕ) ∈ Fin ∧ (𝑚 “ ℕ) ⊆ 𝐽))
108106, 107sylib 208 . . . . . . . . . . 11 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → (𝑚 ∈ (ℕ0𝑚 ℕ) ∧ (𝑚 “ ℕ) ∈ Fin ∧ (𝑚 “ ℕ) ⊆ 𝐽))
109108simp1d 1093 . . . . . . . . . 10 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → 𝑚 ∈ (ℕ0𝑚 ℕ))
11022, 23elmap 7928 . . . . . . . . . 10 (𝑚 ∈ (ℕ0𝑚 ℕ) ↔ 𝑚:ℕ⟶ℕ0)
111109, 110sylib 208 . . . . . . . . 9 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → 𝑚:ℕ⟶ℕ0)
112 fssres 6108 . . . . . . . . 9 ((𝑚:ℕ⟶ℕ0𝐽 ⊆ ℕ) → (𝑚𝐽):𝐽⟶ℕ0)
113111, 12, 112sylancl 695 . . . . . . . 8 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → (𝑚𝐽):𝐽⟶ℕ0)
11410, 23rabex2 4847 . . . . . . . . 9 𝐽 ∈ V
11522, 114elmap 7928 . . . . . . . 8 ((𝑚𝐽) ∈ (ℕ0𝑚 𝐽) ↔ (𝑚𝐽):𝐽⟶ℕ0)
116113, 115sylibr 224 . . . . . . 7 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → (𝑚𝐽) ∈ (ℕ0𝑚 𝐽))
117105, 116eqeltrd 2730 . . . . . 6 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → 𝑜 ∈ (ℕ0𝑚 𝐽))
118 ffun 6086 . . . . . . . . . 10 (𝑚:ℕ⟶ℕ0 → Fun 𝑚)
119 respreima 6384 . . . . . . . . . 10 (Fun 𝑚 → ((𝑚𝐽) “ ℕ) = ((𝑚 “ ℕ) ∩ 𝐽))
120111, 118, 1193syl 18 . . . . . . . . 9 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → ((𝑚𝐽) “ ℕ) = ((𝑚 “ ℕ) ∩ 𝐽))
121108simp2d 1094 . . . . . . . . . 10 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → (𝑚 “ ℕ) ∈ Fin)
122 infi 8225 . . . . . . . . . 10 ((𝑚 “ ℕ) ∈ Fin → ((𝑚 “ ℕ) ∩ 𝐽) ∈ Fin)
123121, 122syl 17 . . . . . . . . 9 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → ((𝑚 “ ℕ) ∩ 𝐽) ∈ Fin)
124120, 123eqeltrd 2730 . . . . . . . 8 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → ((𝑚𝐽) “ ℕ) ∈ Fin)
125 vex 3234 . . . . . . . . . 10 𝑚 ∈ V
126125resex 5478 . . . . . . . . 9 (𝑚𝐽) ∈ V
127 cnveq 5328 . . . . . . . . . . 11 (𝑓 = (𝑚𝐽) → 𝑓 = (𝑚𝐽))
128127imaeq1d 5500 . . . . . . . . . 10 (𝑓 = (𝑚𝐽) → (𝑓 “ ℕ) = ((𝑚𝐽) “ ℕ))
129128eleq1d 2715 . . . . . . . . 9 (𝑓 = (𝑚𝐽) → ((𝑓 “ ℕ) ∈ Fin ↔ ((𝑚𝐽) “ ℕ) ∈ Fin))
130126, 129, 34elab2 3386 . . . . . . . 8 ((𝑚𝐽) ∈ 𝑅 ↔ ((𝑚𝐽) “ ℕ) ∈ Fin)
131124, 130sylibr 224 . . . . . . 7 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → (𝑚𝐽) ∈ 𝑅)
132105, 131eqeltrd 2730 . . . . . 6 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → 𝑜𝑅)
133117, 132jca 553 . . . . 5 ((𝑚 ∈ (𝑇𝑅) ∧ 𝑜 = (𝑚𝐽)) → (𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅))
134133rexlimiva 3057 . . . 4 (∃𝑚 ∈ (𝑇𝑅)𝑜 = (𝑚𝐽) → (𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅))
135104, 134impbii 199 . . 3 ((𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅) ↔ ∃𝑚 ∈ (𝑇𝑅)𝑜 = (𝑚𝐽))
136135abbii 2768 . 2 {𝑜 ∣ (𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅)} = {𝑜 ∣ ∃𝑚 ∈ (𝑇𝑅)𝑜 = (𝑚𝐽)}
137 df-in 3614 . 2 ((ℕ0𝑚 𝐽) ∩ 𝑅) = {𝑜 ∣ (𝑜 ∈ (ℕ0𝑚 𝐽) ∧ 𝑜𝑅)}
138 eqid 2651 . . 3 (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)) = (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽))
139138rnmpt 5403 . 2 ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽)) = {𝑜 ∣ ∃𝑚 ∈ (𝑇𝑅)𝑜 = (𝑚𝐽)}
140136, 137, 1393eqtr4i 2683 1 ((ℕ0𝑚 𝐽) ∩ 𝑅) = ran (𝑚 ∈ (𝑇𝑅) ↦ (𝑚𝐽))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  {cab 2637  wne 2823  wral 2941  wrex 2942  {crab 2945  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  𝒫 cpw 4191  {csn 4210   class class class wbr 4685  {copab 4745  cmpt 4762   × cxp 5141  ccnv 5142  dom cdm 5143  ran crn 5144  cres 5145  cima 5146  Fun wfun 5920   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  cmpt2 6692   supp csupp 7340  𝑚 cmap 7899  Fincfn 7997  0cc0 9974  1c1 9975   · cmul 9979  cle 10113  cn 11058  2c2 11108  0cn0 11330  cz 11415  cexp 12900  Σcsu 14460  cdvds 15027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-dvds 15028
This theorem is referenced by:  eulerpartgbij  30562
  Copyright terms: Public domain W3C validator