Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvnprodlem1 Structured version   Visualization version   GIF version

Theorem dvnprodlem1 39930
Description: 𝐷 is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
dvnprodlem1.c 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
dvnprodlem1.j (𝜑𝐽 ∈ ℕ0)
dvnprodlem1.d 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
dvnprodlem1.t (𝜑𝑇 ∈ Fin)
dvnprodlem1.z (𝜑𝑍𝑇)
dvnprodlem1.zr (𝜑 → ¬ 𝑍𝑅)
dvnprodlem1.rzt (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
Assertion
Ref Expression
dvnprodlem1 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
Distinct variable groups:   𝐶,𝑐,𝑘   𝐷,𝑐,𝑡   𝐽,𝑐,𝑘,𝑛,𝑡   𝑅,𝑐,𝑘,𝑛,𝑡   𝑅,𝑠,𝑐,𝑛,𝑡   𝑡,𝑇,𝑠   𝑍,𝑐,𝑘,𝑛,𝑡   𝑍,𝑠   𝜑,𝑐,𝑛,𝑡,𝑘   𝜑,𝑠
Allowed substitution hints:   𝐶(𝑡,𝑛,𝑠)   𝐷(𝑘,𝑛,𝑠)   𝑇(𝑘,𝑛,𝑐)   𝐽(𝑠)

Proof of Theorem dvnprodlem1
Dummy variables 𝑑 𝑒 𝑚 𝑝 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqidd 2622 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
2 0zd 11386 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ∈ ℤ)
3 dvnprodlem1.j . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ ℕ0)
43nn0zd 11477 . . . . . . . . . . . . . 14 (𝜑𝐽 ∈ ℤ)
54adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℤ)
6 fzssz 12340 . . . . . . . . . . . . . . . 16 (0...𝐽) ⊆ ℤ
76a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℤ)
8 dvnprodlem1.c . . . . . . . . . . . . . . . . . . . . . . 23 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
98a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})))
10 oveq2 6655 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})))
11 rabeq 3190 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
1210, 11syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
13 sumeq1 14413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
1413eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛))
1514rabbidv 3187 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
1612, 15eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
1716mpteq2dv 4743 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
1817adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠 = (𝑅 ∪ {𝑍})) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
19 dvnprodlem1.rzt . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
20 dvnprodlem1.t . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑇 ∈ Fin)
21 ssexg 4802 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∪ {𝑍}) ⊆ 𝑇𝑇 ∈ Fin) → (𝑅 ∪ {𝑍}) ∈ V)
2219, 20, 21syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
23 elpwg 4164 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 ∪ {𝑍}) ∈ V → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
2422, 23syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
2519, 24mpbird 247 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
26 nn0ex 11295 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
2726mptex 6483 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V
2827a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V)
299, 18, 25, 28fvmptd 6286 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
30 oveq2 6655 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
3130oveq1d 6662 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝐽 → ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
32 rabeq 3190 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
3331, 32syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
34 eqeq2 2632 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
3534rabbidv 3187 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
3633, 35eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
3736adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑛 = 𝐽) → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
38 ovex 6675 . . . . . . . . . . . . . . . . . . . . . . 23 ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∈ V
3938rabex 4811 . . . . . . . . . . . . . . . . . . . . . 22 {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V
4039a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V)
4129, 37, 3, 40fvmptd 6286 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
42 ssrab2 3685 . . . . . . . . . . . . . . . . . . . . 21 {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍}))
4342a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
4441, 43eqsstrd 3637 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
4544adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
46 simpr 477 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
4745, 46sseldd 3602 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
48 elmapi 7876 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
4947, 48syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
50 dvnprodlem1.z . . . . . . . . . . . . . . . . . . 19 (𝜑𝑍𝑇)
51 snidg 4204 . . . . . . . . . . . . . . . . . . 19 (𝑍𝑇𝑍 ∈ {𝑍})
5250, 51syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑍 ∈ {𝑍})
53 elun2 3779 . . . . . . . . . . . . . . . . . 18 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
5452, 53syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑍 ∈ (𝑅 ∪ {𝑍}))
5554adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
5649, 55ffvelrnd 6358 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝐽))
577, 56sseldd 3602 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℤ)
585, 57zsubcld 11484 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
592, 5, 583jca 1241 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ))
60 elfzle2 12342 . . . . . . . . . . . . . 14 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ≤ 𝐽)
6156, 60syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ≤ 𝐽)
625zred 11479 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℝ)
6357zred 11479 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℝ)
6462, 63subge0d 10614 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝐽 − (𝑐𝑍)) ↔ (𝑐𝑍) ≤ 𝐽))
6561, 64mpbird 247 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝐽 − (𝑐𝑍)))
66 elfzle1 12341 . . . . . . . . . . . . . 14 ((𝑐𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐𝑍))
6756, 66syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝑐𝑍))
6862, 63subge02d 10616 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝑐𝑍) ↔ (𝐽 − (𝑐𝑍)) ≤ 𝐽))
6967, 68mpbid 222 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ≤ 𝐽)
7059, 65, 69jca32 558 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐𝑍)) ∧ (𝐽 − (𝑐𝑍)) ≤ 𝐽)))
71 elfz2 12330 . . . . . . . . . . 11 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐𝑍)) ∧ (𝐽 − (𝑐𝑍)) ≤ 𝐽)))
7270, 71sylibr 224 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
73 elmapfn 7877 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) → 𝑐 Fn (𝑅 ∪ {𝑍}))
7447, 73syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
75 ssun1 3774 . . . . . . . . . . . . . . . . . 18 𝑅 ⊆ (𝑅 ∪ {𝑍})
7675a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
77 fnssres 6002 . . . . . . . . . . . . . . . . 17 ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑅 ⊆ (𝑅 ∪ {𝑍})) → (𝑐𝑅) Fn 𝑅)
7874, 76, 77syl2anc 693 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) Fn 𝑅)
79 nfv 1842 . . . . . . . . . . . . . . . . . 18 𝑡𝜑
80 nfcv 2763 . . . . . . . . . . . . . . . . . . 19 𝑡𝑐
81 nfcv 2763 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡𝒫 𝑇
82 nfcv 2763 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡0
83 nfcv 2763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡𝑠
8483nfsum1 14414 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡Σ𝑡𝑠 (𝑐𝑡)
85 nfcv 2763 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡𝑛
8684, 85nfeq 2775 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡Σ𝑡𝑠 (𝑐𝑡) = 𝑛
87 nfcv 2763 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡((0...𝑛) ↑𝑚 𝑠)
8886, 87nfrab 3121 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡{𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}
8982, 88nfmpt 4744 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
9081, 89nfmpt 4744 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
918, 90nfcxfr 2761 . . . . . . . . . . . . . . . . . . . . 21 𝑡𝐶
92 nfcv 2763 . . . . . . . . . . . . . . . . . . . . 21 𝑡(𝑅 ∪ {𝑍})
9391, 92nffv 6196 . . . . . . . . . . . . . . . . . . . 20 𝑡(𝐶‘(𝑅 ∪ {𝑍}))
94 nfcv 2763 . . . . . . . . . . . . . . . . . . . 20 𝑡𝐽
9593, 94nffv 6196 . . . . . . . . . . . . . . . . . . 19 𝑡((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
9680, 95nfel 2776 . . . . . . . . . . . . . . . . . 18 𝑡 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
9779, 96nfan 1827 . . . . . . . . . . . . . . . . 17 𝑡(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
98 fvres 6205 . . . . . . . . . . . . . . . . . . . 20 (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
9998adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
1002adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 0 ∈ ℤ)
10158adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
1026a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ ℤ)
10349adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
10476sselda 3601 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
105103, 104ffvelrnd 6358 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝐽))
106102, 105sseldd 3602 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℤ)
107100, 101, 1063jca 1241 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ ∧ (𝑐𝑡) ∈ ℤ))
108 elfzle1 12341 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑐𝑡) ∈ (0...𝐽) → 0 ≤ (𝑐𝑡))
109105, 108syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 0 ≤ (𝑐𝑡))
11019unssad 3788 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑅𝑇)
111 ssfi 8177 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑇 ∈ Fin ∧ 𝑅𝑇) → 𝑅 ∈ Fin)
11220, 110, 111syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅 ∈ Fin)
113112ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑅 ∈ Fin)
114 zssre 11381 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℤ ⊆ ℝ
1156, 114sstri 3610 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0...𝐽) ⊆ ℝ
116115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (0...𝐽) ⊆ ℝ)
11749adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
11876sselda 3601 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 𝑟 ∈ (𝑅 ∪ {𝑍}))
119117, 118ffvelrnd 6358 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ (0...𝐽))
120116, 119sseldd 3602 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℝ)
121120adantlr 751 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℝ)
122 elfzle1 12341 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑐𝑟) ∈ (0...𝐽) → 0 ≤ (𝑐𝑟))
123119, 122syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 0 ≤ (𝑐𝑟))
124123adantlr 751 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) ∧ 𝑟𝑅) → 0 ≤ (𝑐𝑟))
125 fveq2 6189 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 = 𝑡 → (𝑐𝑟) = (𝑐𝑡))
126 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡𝑅)
127113, 121, 124, 125, 126fsumge1 14523 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ≤ Σ𝑟𝑅 (𝑐𝑟))
128112adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
129120recnd 10065 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℂ)
130128, 129fsumcl 14458 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) ∈ ℂ)
13163recnd 10065 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℂ)
132130, 131pncand 10390 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) − (𝑐𝑍)) = Σ𝑟𝑅 (𝑐𝑟))
133 nfv 1842 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑟(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
134 nfcv 2763 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑟(𝑐𝑍)
13550adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
136 dvnprodlem1.zr . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ¬ 𝑍𝑅)
137136adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
138 fveq2 6189 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑟 = 𝑍 → (𝑐𝑟) = (𝑐𝑍))
139133, 134, 128, 135, 137, 129, 138, 131fsumsplitsn 14468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)))
140139eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) = Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟))
141125cbvsumv 14420 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡)
142141a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
14341adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
14446, 143eleqtrd 2702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
145 rabid 3114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ↔ (𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
146144, 145sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
147146simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽)
148142, 147eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = 𝐽)
149140, 148eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) = 𝐽)
150149oveq1d 6662 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) − (𝑐𝑍)) = (𝐽 − (𝑐𝑍)))
151132, 150eqtr3d 2657 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
152151adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
153127, 152breqtrd 4677 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ≤ (𝐽 − (𝑐𝑍)))
154107, 109, 153jca32 558 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((0 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ ∧ (𝑐𝑡) ∈ ℤ) ∧ (0 ≤ (𝑐𝑡) ∧ (𝑐𝑡) ≤ (𝐽 − (𝑐𝑍)))))
155 elfz2 12330 . . . . . . . . . . . . . . . . . . . 20 ((𝑐𝑡) ∈ (0...(𝐽 − (𝑐𝑍))) ↔ ((0 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ ∧ (𝑐𝑡) ∈ ℤ) ∧ (0 ≤ (𝑐𝑡) ∧ (𝑐𝑡) ≤ (𝐽 − (𝑐𝑍)))))
156154, 155sylibr 224 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
15799, 156eqeltrd 2700 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
158157ex 450 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡𝑅 → ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍)))))
15997, 158ralrimi 2956 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
16078, 159jca 554 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅) Fn 𝑅 ∧ ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍)))))
161 ffnfv 6386 . . . . . . . . . . . . . . 15 ((𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍))) ↔ ((𝑐𝑅) Fn 𝑅 ∧ ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍)))))
162160, 161sylibr 224 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍))))
163 ovexd 6677 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...(𝐽 − (𝑐𝑍))) ∈ V)
16420, 110ssexd 4803 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ V)
165164adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ V)
166163, 165elmapd 7868 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ↔ (𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍)))))
167162, 166mpbird 247 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅))
16898a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡)))
16997, 168ralrimi 2956 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
170169sumeq2d 14426 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = Σ𝑡𝑅 (𝑐𝑡))
171125cbvsumv 14420 . . . . . . . . . . . . . . . 16 Σ𝑟𝑅 (𝑐𝑟) = Σ𝑡𝑅 (𝑐𝑡)
172171eqcomi 2630 . . . . . . . . . . . . . . 15 Σ𝑡𝑅 (𝑐𝑡) = Σ𝑟𝑅 (𝑐𝑟)
173172a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑟𝑅 (𝑐𝑟))
174151idi 2 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
175170, 173, 1743eqtrd 2659 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍)))
176167, 175jca 554 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∧ Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍))))
177 eqidd 2622 . . . . . . . . . . . . . . 15 (𝑒 = (𝑐𝑅) → 𝑅 = 𝑅)
178 simpl 473 . . . . . . . . . . . . . . . 16 ((𝑒 = (𝑐𝑅) ∧ 𝑡𝑅) → 𝑒 = (𝑐𝑅))
179178fveq1d 6191 . . . . . . . . . . . . . . 15 ((𝑒 = (𝑐𝑅) ∧ 𝑡𝑅) → (𝑒𝑡) = ((𝑐𝑅)‘𝑡))
180177, 179sumeq12rdv 14432 . . . . . . . . . . . . . 14 (𝑒 = (𝑐𝑅) → Σ𝑡𝑅 (𝑒𝑡) = Σ𝑡𝑅 ((𝑐𝑅)‘𝑡))
181180eqeq1d 2623 . . . . . . . . . . . . 13 (𝑒 = (𝑐𝑅) → (Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍)) ↔ Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍))))
182181elrab 3361 . . . . . . . . . . . 12 ((𝑐𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ↔ ((𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∧ Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍))))
183176, 182sylibr 224 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
184 oveq2 6655 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑅 → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑅))
185 rabeq 3190 . . . . . . . . . . . . . . . . . . . 20 (((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
186184, 185syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
187 sumeq1 14413 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑅 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑅 (𝑐𝑡))
188187eqeq1d 2623 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑅 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑛))
189188rabbidv 3187 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
190186, 189eqtrd 2655 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
191190mpteq2dv 4743 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑅 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
192191adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 = 𝑅) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
193 elpwg 4164 . . . . . . . . . . . . . . . . . 18 (𝑅 ∈ V → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
194164, 193syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
195110, 194mpbird 247 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ 𝒫 𝑇)
19626mptex 6483 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V
197196a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V)
1989, 192, 195, 197fvmptd 6286 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
199198adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
200 oveq2 6655 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑚 → (0...𝑛) = (0...𝑚))
201200oveq1d 6662 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → ((0...𝑛) ↑𝑚 𝑅) = ((0...𝑚) ↑𝑚 𝑅))
202 rabeq 3190 . . . . . . . . . . . . . . . . . 18 (((0...𝑛) ↑𝑚 𝑅) = ((0...𝑚) ↑𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
203201, 202syl 17 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
204 eqeq2 2632 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑚))
205204rabbidv 3187 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
206203, 205eqtrd 2655 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
207206cbvmptv 4748 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
208207a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚}))
209199, 208eqtrd 2655 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶𝑅) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚}))
210 fveq1 6188 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑒 → (𝑐𝑡) = (𝑒𝑡))
211210sumeq2ad 14428 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑒 → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑡𝑅 (𝑒𝑡))
212211eqeq1d 2623 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑒 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑚 ↔ Σ𝑡𝑅 (𝑒𝑡) = 𝑚))
213212cbvrabv 3197 . . . . . . . . . . . . . . . 16 {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚}
214213a1i 11 . . . . . . . . . . . . . . 15 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
215 oveq2 6655 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝐽 − (𝑐𝑍)) → (0...𝑚) = (0...(𝐽 − (𝑐𝑍))))
216215oveq1d 6662 . . . . . . . . . . . . . . . 16 (𝑚 = (𝐽 − (𝑐𝑍)) → ((0...𝑚) ↑𝑚 𝑅) = ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅))
217 rabeq 3190 . . . . . . . . . . . . . . . 16 (((0...𝑚) ↑𝑚 𝑅) = ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) → {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
218216, 217syl 17 . . . . . . . . . . . . . . 15 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑒 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
219 eqeq2 2632 . . . . . . . . . . . . . . . 16 (𝑚 = (𝐽 − (𝑐𝑍)) → (Σ𝑡𝑅 (𝑒𝑡) = 𝑚 ↔ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))))
220219rabbidv 3187 . . . . . . . . . . . . . . 15 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
221214, 218, 2203eqtrd 2659 . . . . . . . . . . . . . 14 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
222221adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑚 = (𝐽 − (𝑐𝑍))) → {𝑐 ∈ ((0...𝑚) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
22358, 65jca 554 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐𝑍))))
224 elnn0z 11387 . . . . . . . . . . . . . 14 ((𝐽 − (𝑐𝑍)) ∈ ℕ0 ↔ ((𝐽 − (𝑐𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐𝑍))))
225223, 224sylibr 224 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
226 ovex 6675 . . . . . . . . . . . . . . 15 ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∈ V
227226rabex 4811 . . . . . . . . . . . . . 14 {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ∈ V
228227a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ∈ V)
229209, 222, 225, 228fvmptd 6286 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))) = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
230229eqcomd 2627 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
231183, 230eleqtrd 2702 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
23272, 231jca 554 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))
2331, 232jca 554 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))))
234 ovexd 6677 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ V)
235 vex 3201 . . . . . . . . . . 11 𝑐 ∈ V
236235resex 5441 . . . . . . . . . 10 (𝑐𝑅) ∈ V
237236a1i 11 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ V)
238 opeq12 4402 . . . . . . . . . . . 12 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ⟨𝑘, 𝑑⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
239238eqeq2d 2631 . . . . . . . . . . 11 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ↔ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
240 eleq1 2688 . . . . . . . . . . . . 13 (𝑘 = (𝐽 − (𝑐𝑍)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐𝑍)) ∈ (0...𝐽)))
241240adantr 481 . . . . . . . . . . . 12 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐𝑍)) ∈ (0...𝐽)))
242 simpr 477 . . . . . . . . . . . . 13 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → 𝑑 = (𝑐𝑅))
243 fveq2 6189 . . . . . . . . . . . . . 14 (𝑘 = (𝐽 − (𝑐𝑍)) → ((𝐶𝑅)‘𝑘) = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
244243adantr 481 . . . . . . . . . . . . 13 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((𝐶𝑅)‘𝑘) = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
245242, 244eleq12d 2694 . . . . . . . . . . . 12 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (𝑑 ∈ ((𝐶𝑅)‘𝑘) ↔ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))
246241, 245anbi12d 747 . . . . . . . . . . 11 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)) ↔ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))))
247239, 246anbi12d 747 . . . . . . . . . 10 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))) ↔ (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))))
248247spc2egv 3293 . . . . . . . . 9 (((𝐽 − (𝑐𝑍)) ∈ V ∧ (𝑐𝑅) ∈ V) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)))))
249234, 237, 248syl2anc 693 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)))))
250233, 249mpd 15 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))))
251 eliunxp 5257 . . . . . . 7 (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))))
252250, 251sylibr 224 . . . . . 6 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
253 dvnprodlem1.d . . . . . 6 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
254252, 253fmptd 6383 . . . . 5 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
25595nfcri 2757 . . . . . . . . . . . 12 𝑡 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
25696, 255nfan 1827 . . . . . . . . . . 11 𝑡(𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
25779, 256nfan 1827 . . . . . . . . . 10 𝑡(𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
258 nfv 1842 . . . . . . . . . 10 𝑡(𝐷𝑐) = (𝐷𝑒)
259257, 258nfan 1827 . . . . . . . . 9 𝑡((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒))
26099eqcomd 2627 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
261260adantlrr 757 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
262261adantlr 751 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
263253a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
264 opex 4930 . . . . . . . . . . . . . . . . . . . 20 ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V
265264a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V)
266263, 265fvmpt2d 6291 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
267266fveq2d 6193 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
268267fveq1d 6191 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2nd ‘(𝐷𝑐))‘𝑡) = ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡))
269 ovex 6675 . . . . . . . . . . . . . . . . . . 19 (𝐽 − (𝑐𝑍)) ∈ V
270269, 236op2nd 7174 . . . . . . . . . . . . . . . . . 18 (2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝑐𝑅)
271270fveq1i 6190 . . . . . . . . . . . . . . . . 17 ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡) = ((𝑐𝑅)‘𝑡)
272271a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡) = ((𝑐𝑅)‘𝑡))
273268, 272eqtr2d 2656 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
274273adantrr 753 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
275274ad2antrr 762 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
276 simpr 477 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑐) = (𝐷𝑒))
277253a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
278 fveq1 6188 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑒 → (𝑐𝑍) = (𝑒𝑍))
279278oveq2d 6663 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝑒𝑍)))
280 reseq1 5388 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → (𝑐𝑅) = (𝑒𝑅))
281279, 280opeq12d 4408 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑒 → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
282281adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑐 = 𝑒) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
283 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
284 opex 4930 . . . . . . . . . . . . . . . . . . . . . . 23 ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩ ∈ V
285284a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩ ∈ V)
286277, 282, 283, 285fvmptd 6286 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑒) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
287286adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑒) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
288276, 287eqtrd 2655 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑐) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
289288fveq2d 6193 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
290289adantlrl 756 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
291290adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
292 ovex 6675 . . . . . . . . . . . . . . . . . 18 (𝐽 − (𝑒𝑍)) ∈ V
293 vex 3201 . . . . . . . . . . . . . . . . . . 19 𝑒 ∈ V
294293resex 5441 . . . . . . . . . . . . . . . . . 18 (𝑒𝑅) ∈ V
295292, 294op2nd 7174 . . . . . . . . . . . . . . . . 17 (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝑒𝑅)
296295a1i 11 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝑒𝑅))
297291, 296eqtrd 2655 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘(𝐷𝑐)) = (𝑒𝑅))
298297fveq1d 6191 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((2nd ‘(𝐷𝑐))‘𝑡) = ((𝑒𝑅)‘𝑡))
299 fvres 6205 . . . . . . . . . . . . . . 15 (𝑡𝑅 → ((𝑒𝑅)‘𝑡) = (𝑒𝑡))
300299adantl 482 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((𝑒𝑅)‘𝑡) = (𝑒𝑡))
301298, 300eqtrd 2655 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((2nd ‘(𝐷𝑐))‘𝑡) = (𝑒𝑡))
302262, 275, 3013eqtrd 2659 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
303302adantlr 751 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
304 simpl 473 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
305 elunnel1 3752 . . . . . . . . . . . . . 14 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡𝑅) → 𝑡 ∈ {𝑍})
306 elsni 4192 . . . . . . . . . . . . . 14 (𝑡 ∈ {𝑍} → 𝑡 = 𝑍)
307305, 306syl 17 . . . . . . . . . . . . 13 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
308307adantll 750 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
309 simpr 477 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
310309fveq2d 6193 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑐𝑍))
3113nn0cnd 11350 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐽 ∈ ℂ)
312311adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
313312, 131nncand 10394 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝑐𝑍))
314313eqcomd 2627 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
315314adantrr 753 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
316315adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
317266fveq2d 6193 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘(𝐷𝑐)) = (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
318269, 236op1st 7173 . . . . . . . . . . . . . . . . . . . . 21 (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝐽 − (𝑐𝑍))
319318a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝐽 − (𝑐𝑍)))
320317, 319eqtr2d 2656 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) = (1st ‘(𝐷𝑐)))
321320oveq2d 6663 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
322321adantrr 753 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
323322adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
324 fveq2 6189 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷𝑐) = (𝐷𝑒) → (1st ‘(𝐷𝑐)) = (1st ‘(𝐷𝑒)))
325324adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑐)) = (1st ‘(𝐷𝑒)))
326286fveq2d 6193 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘(𝐷𝑒)) = (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
327326adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑒)) = (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
328292, 294op1st 7173 . . . . . . . . . . . . . . . . . . . . 21 (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝐽 − (𝑒𝑍))
329328a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝐽 − (𝑒𝑍)))
330325, 327, 3293eqtrd 2659 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑐)) = (𝐽 − (𝑒𝑍)))
331330oveq2d 6663 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝐽 − (𝐽 − (𝑒𝑍))))
332311adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
333 zsscn 11382 . . . . . . . . . . . . . . . . . . . . . . 23 ℤ ⊆ ℂ
3346, 333sstri 3610 . . . . . . . . . . . . . . . . . . . . . 22 (0...𝐽) ⊆ ℂ
335334a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℂ)
336 eleq1 2688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑒 → (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↔ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
337336anbi2d 740 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ↔ (𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))))
338 feq1 6024 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑒 → (𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽) ↔ 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽)))
339337, 338imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑒 → (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽)) ↔ ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))))
340339, 49chvarv 2262 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))
34154adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
342340, 341ffvelrnd 6358 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒𝑍) ∈ (0...𝐽))
343335, 342sseldd 3602 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒𝑍) ∈ ℂ)
344332, 343nncand 10394 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑒𝑍))) = (𝑒𝑍))
345344adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (𝐽 − (𝑒𝑍))) = (𝑒𝑍))
346 eqidd 2622 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑒𝑍) = (𝑒𝑍))
347331, 345, 3463eqtrd 2659 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝑒𝑍))
348347adantlrl 756 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝑒𝑍))
349316, 323, 3483eqtrd 2659 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐𝑍) = (𝑒𝑍))
350349adantr 481 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑍) = (𝑒𝑍))
351 fveq2 6189 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → (𝑒𝑡) = (𝑒𝑍))
352351eqcomd 2627 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (𝑒𝑍) = (𝑒𝑡))
353352adantl 482 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑒𝑍) = (𝑒𝑡))
354310, 350, 3533eqtrd 2659 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑒𝑡))
355354adantlr 751 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑒𝑡))
356304, 308, 355syl2anc 693 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
357303, 356pm2.61dan 832 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) = (𝑒𝑡))
358357ex 450 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → (𝑐𝑡) = (𝑒𝑡)))
359259, 358ralrimi 2956 . . . . . . . 8 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡))
36074adantrr 753 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑐 Fn (𝑅 ∪ {𝑍}))
361360adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
362 ffn 6043 . . . . . . . . . . . 12 (𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽) → 𝑒 Fn (𝑅 ∪ {𝑍}))
363340, 362syl 17 . . . . . . . . . . 11 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
364363adantrl 752 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑒 Fn (𝑅 ∪ {𝑍}))
365364adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
366 eqfnfv 6309 . . . . . . . . 9 ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑒 Fn (𝑅 ∪ {𝑍})) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡)))
367361, 365, 366syl2anc 693 . . . . . . . 8 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡)))
368359, 367mpbird 247 . . . . . . 7 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑐 = 𝑒)
369368ex 450 . . . . . 6 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒))
370369ralrimivva 2970 . . . . 5 (𝜑 → ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒))
371254, 370jca 554 . . . 4 (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒)))
372 dff13 6509 . . . 4 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒)))
373371, 372sylibr 224 . . 3 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
374 eliun 4522 . . . . . . . . . . 11 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
375374biimpi 206 . . . . . . . . . 10 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
376375adantl 482 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
377 nfv 1842 . . . . . . . . . . 11 𝑘𝜑
378 nfcv 2763 . . . . . . . . . . . 12 𝑘𝑝
379 nfiu1 4548 . . . . . . . . . . . 12 𝑘 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
380378, 379nfel 2776 . . . . . . . . . . 11 𝑘 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
381377, 380nfan 1827 . . . . . . . . . 10 𝑘(𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
382 nfv 1842 . . . . . . . . . 10 𝑘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽}
383 nfv 1842 . . . . . . . . . . . . . . . . 17 𝑡 𝑘 ∈ (0...𝐽)
384 nfcv 2763 . . . . . . . . . . . . . . . . . 18 𝑡𝑝
385 nfcv 2763 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑘}
386 nfcv 2763 . . . . . . . . . . . . . . . . . . . . 21 𝑡𝑅
38791, 386nffv 6196 . . . . . . . . . . . . . . . . . . . 20 𝑡(𝐶𝑅)
388 nfcv 2763 . . . . . . . . . . . . . . . . . . . 20 𝑡𝑘
389387, 388nffv 6196 . . . . . . . . . . . . . . . . . . 19 𝑡((𝐶𝑅)‘𝑘)
390385, 389nfxp 5140 . . . . . . . . . . . . . . . . . 18 𝑡({𝑘} × ((𝐶𝑅)‘𝑘))
391384, 390nfel 2776 . . . . . . . . . . . . . . . . 17 𝑡 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))
39279, 383, 391nf3an 1830 . . . . . . . . . . . . . . . 16 𝑡(𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
393 0zd 11386 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ∈ ℤ)
3944adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
3953943ad2antl1 1222 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
396 iftrue 4090 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡𝑅 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
397396adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
398 fzssz 12340 . . . . . . . . . . . . . . . . . . . . . . 23 (0...𝑘) ⊆ ℤ
399398a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → (0...𝑘) ⊆ ℤ)
400 simp1 1060 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝜑)
401 simp2 1061 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
402 xp2nd 7196 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
4034023ad2ant3 1083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
404198adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
405 oveq2 6655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
406405oveq1d 6662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 = 𝑘 → ((0...𝑛) ↑𝑚 𝑅) = ((0...𝑘) ↑𝑚 𝑅))
407 rabeq 3190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((0...𝑛) ↑𝑚 𝑅) = ((0...𝑘) ↑𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
408406, 407syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
409 eqeq2 2632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑛 = 𝑘 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑘))
410409rabbidv 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
411408, 410eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
412411adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
413 elfznn0 12429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ0)
414413adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ0)
415 ovex 6675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((0...𝑘) ↑𝑚 𝑅) ∈ V
416415rabex 4811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V
417416a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V)
418404, 412, 414, 417fvmptd 6286 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
4194183adant3 1080 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
420403, 419eleqtrd 2702 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
421 elrabi 3357 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} → (2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅))
4224213ad2ant3 1083 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑘 ∈ (0...𝐽) ∧ (2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}) → (2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅))
423400, 401, 420, 422syl3anc 1325 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅))
424 elmapi 7876 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅) → (2nd𝑝):𝑅⟶(0...𝑘))
425423, 424syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝑘))
426425adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (2nd𝑝):𝑅⟶(0...𝑘))
427426ffvelrnda 6357 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑘))
428399, 427sseldd 3602 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℤ)
429397, 428eqeltrd 2700 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
430 simpl 473 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})))
431307adantll 750 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
432 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑡 = 𝑍) → 𝑡 = 𝑍)
433136adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑡 = 𝑍) → ¬ 𝑍𝑅)
434432, 433eqneltrd 2719 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡 = 𝑍) → ¬ 𝑡𝑅)
435434iffalsed 4095 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
4364353ad2antl1 1222 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
4374adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡 = 𝑍) → 𝐽 ∈ ℤ)
4384373ad2antl1 1222 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
439 xp1st 7195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ {𝑘})
440 elsni 4192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((1st𝑝) ∈ {𝑘} → (1st𝑝) = 𝑘)
441439, 440syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) = 𝑘)
442441adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
4436sseli 3597 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
444443adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ ℤ)
445442, 444eqeltrd 2700 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
4464453adant1 1078 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
447446adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (1st𝑝) ∈ ℤ)
448438, 447zsubcld 11484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1st𝑝)) ∈ ℤ)
449436, 448eqeltrd 2700 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
450449adantlr 751 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
451430, 431, 450syl2anc 693 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
452429, 451pm2.61dan 832 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
453393, 395, 4523jca 1241 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ))
454425ffvelrnda 6357 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑘))
455 elfzle1 12341 . . . . . . . . . . . . . . . . . . . . . 22 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → 0 ≤ ((2nd𝑝)‘𝑡))
456454, 455syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 0 ≤ ((2nd𝑝)‘𝑡))
457396eqcomd 2627 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡𝑅 → ((2nd𝑝)‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
458457adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
459456, 458breqtrd 4677 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
460459adantlr 751 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
461 simpll 790 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))))
462 elfzle2 12342 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → 𝑘𝐽)
463 elfzel2 12337 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
464463zred 11479 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
465115sseli 3597 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
466464, 465subge0d 10614 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽𝑘) ↔ 𝑘𝐽))
467462, 466mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽𝑘))
468467adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ (0...𝐽) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽𝑘))
4694683ad2antl2 1223 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽𝑘))
470400, 434sylan 488 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → ¬ 𝑡𝑅)
471470iffalsed 4095 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
4724423adant1 1078 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
473472oveq2d 6663 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) = (𝐽𝑘))
474473adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1st𝑝)) = (𝐽𝑘))
475471, 474eqtr2d 2656 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽𝑘) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
476469, 475breqtrd 4677 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
477461, 431, 476syl2anc 693 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
478460, 477pm2.61dan 832 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
479 simpl2 1064 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑘 ∈ (0...𝐽))
480398sseli 3597 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ∈ ℤ)
481480zred 11479 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ∈ ℝ)
482481adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ∈ ℝ)
483465adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
484464adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
485 elfzle2 12342 . . . . . . . . . . . . . . . . . . . . . . . 24 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ≤ 𝑘)
486485adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ≤ 𝑘)
487462adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘𝐽)
488482, 483, 484, 486, 487letrd 10191 . . . . . . . . . . . . . . . . . . . . . 22 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
489454, 479, 488syl2anc 693 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
490489adantlr 751 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
491397, 490eqbrtrd 4673 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
492475eqcomd 2627 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽𝑘))
493414nn0ge0d 11351 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
494464adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
495465adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
496494, 495subge02d 10616 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑘 ∈ (0...𝐽)) → (0 ≤ 𝑘 ↔ (𝐽𝑘) ≤ 𝐽))
497493, 496mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽𝑘) ≤ 𝐽)
498497adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑡 = 𝑍) → (𝐽𝑘) ≤ 𝐽)
4994983adantl3 1218 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽𝑘) ≤ 𝐽)
500492, 499eqbrtrd 4673 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
501461, 431, 500syl2anc 693 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
502491, 501pm2.61dan 832 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
503453, 478, 502jca32 558 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ) ∧ (0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)))
504 elfz2 12330 . . . . . . . . . . . . . . . . 17 (if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ) ∧ (0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∧ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)))
505503, 504sylibr 224 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ (0...𝐽))
506 eqid 2621 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
507392, 505, 506fmptdf 6385 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽))
508 ovexd 6677 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (0...𝐽) ∈ V)
509400, 22syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑅 ∪ {𝑍}) ∈ V)
510508, 509elmapd 7868 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ↔ (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽)))
511507, 510mpbird 247 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
512 eqidd 2622 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
513 eleq1 2688 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = 𝑡 → (𝑟𝑅𝑡𝑅))
514 fveq2 6189 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = 𝑡 → ((2nd𝑝)‘𝑟) = ((2nd𝑝)‘𝑡))
515513, 514ifbieq1d 4107 . . . . . . . . . . . . . . . . . . . 20 (𝑟 = 𝑡 → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
516515adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑟 = 𝑡) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
517 simpr 477 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
518512, 516, 517, 452fvmptd 6286 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
519518ex 450 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
520392, 519ralrimi 2956 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
521520sumeq2d 14426 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
522 nfcv 2763 . . . . . . . . . . . . . . . 16 𝑡if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))
523400, 112syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
524400, 50syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑍𝑇)
525400, 136syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ¬ 𝑍𝑅)
526396adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
527454, 480syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℤ)
528527zcnd 11480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℂ)
529526, 528eqeltrd 2700 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℂ)
530 eleq1 2688 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑍 → (𝑡𝑅𝑍𝑅))
531 fveq2 6189 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑍 → ((2nd𝑝)‘𝑡) = ((2nd𝑝)‘𝑍))
532530, 531ifbieq1d 4107 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))))
533136adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ¬ 𝑍𝑅)
534533iffalsed 4095 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
5355343adant2 1079 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
53643ad2ant1 1081 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℤ)
537536, 446zsubcld 11484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ ℤ)
538537zcnd 11480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ ℂ)
539535, 538eqeltrd 2700 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) ∈ ℂ)
540392, 522, 523, 524, 525, 529, 532, 539fsumsplitsn 14468 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))))
541396a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡)))
542392, 541ralrimi 2956 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ∀𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
543542sumeq2d 14426 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = Σ𝑡𝑅 ((2nd𝑝)‘𝑡))
544 eqidd 2622 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (2nd𝑝) → 𝑅 = 𝑅)
545 simpl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑐 = (2nd𝑝) ∧ 𝑡𝑅) → 𝑐 = (2nd𝑝))
546545fveq1d 6191 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑐 = (2nd𝑝) ∧ 𝑡𝑅) → (𝑐𝑡) = ((2nd𝑝)‘𝑡))
547544, 546sumeq12rdv 14432 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = (2nd𝑝) → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑡𝑅 ((2nd𝑝)‘𝑡))
548547eqeq1d 2623 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = (2nd𝑝) → (Σ𝑡𝑅 (𝑐𝑡) = 𝑘 ↔ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
549548elrab 3361 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ↔ ((2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅) ∧ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
550420, 549sylib 208 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((2nd𝑝) ∈ ((0...𝑘) ↑𝑚 𝑅) ∧ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
551550simprd 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘)
552543, 551eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = 𝑘)
553525iffalsed 4095 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
554553, 473eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽𝑘))
555552, 554oveq12d 6665 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))) = (𝑘 + (𝐽𝑘)))
556334sseli 3597 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℂ)
5575563ad2ant2 1082 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ ℂ)
558400, 311syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℂ)
559557, 558pncan3d 10392 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 + (𝐽𝑘)) = 𝐽)
560555, 559eqtrd 2655 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))) = 𝐽)
561521, 540, 5603eqtrd 2659 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽)
562511, 561jca 554 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽))
563 eleq1 2688 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑟 → (𝑡𝑅𝑟𝑅))
564 fveq2 6189 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑟 → ((2nd𝑝)‘𝑡) = ((2nd𝑝)‘𝑟))
565563, 564ifbieq1d 4107 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑟 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))
566565cbvmptv 4748 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))
567566eqeq2i 2633 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↔ 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
568567biimpi 206 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
569 fveq1 6188 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) → (𝑐𝑡) = ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
570569sumeq2ad 14428 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
571568, 570syl 17 . . . . . . . . . . . . . . 15 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
572571eqeq1d 2623 . . . . . . . . . . . . . 14 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽))
573572elrab 3361 . . . . . . . . . . . . 13 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ↔ ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽))
574562, 573sylibr 224 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
5755743exp 1263 . . . . . . . . . . 11 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})))
576575adantr 481 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})))
577381, 382, 576rexlimd 3024 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽}))
578376, 577mpd 15 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
57941eqcomd 2627 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
580579adantr 481 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
581578, 580eleqtrd 2702 . . . . . . 7 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
582253a1i 11 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
583 simpr 477 . . . . . . . . . . . . . . 15 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
584566a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
585583, 584eqtrd 2655 . . . . . . . . . . . . . 14 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
586 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟 = 𝑍) → 𝑟 = 𝑍)
587136adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑟 = 𝑍) → ¬ 𝑍𝑅)
588586, 587eqneltrd 2719 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 = 𝑍) → ¬ 𝑟𝑅)
589588iffalsed 4095 . . . . . . . . . . . . . . 15 ((𝜑𝑟 = 𝑍) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
590589adantlr 751 . . . . . . . . . . . . . 14 (((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) ∧ 𝑟 = 𝑍) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
59154adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
592 ovexd 6677 . . . . . . . . . . . . . 14 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (1st𝑝)) ∈ V)
593585, 590, 591, 592fvmptd 6286 . . . . . . . . . . . . 13 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑍) = (𝐽 − (1st𝑝)))
594593oveq2d 6663 . . . . . . . . . . . 12 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝐽 − (1st𝑝))))
595594adantlr 751 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝐽 − (1st𝑝))))
596311ad2antrr 762 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝐽 ∈ ℂ)
597 nfv 1842 . . . . . . . . . . . . . . . . 17 𝑘(1st𝑝) ∈ (0...𝐽)
598 simpl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
599 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ (0...𝐽) ∧ (1st𝑝) = 𝑘) → (1st𝑝) = 𝑘)
600 simpl 473 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ (0...𝐽) ∧ (1st𝑝) = 𝑘) → 𝑘 ∈ (0...𝐽))
601599, 600eqeltrd 2700 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ (0...𝐽) ∧ (1st𝑝) = 𝑘) → (1st𝑝) ∈ (0...𝐽))
602598, 442, 601syl2anc 693 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
603602ex 450 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
604603a1i 11 . . . . . . . . . . . . . . . . 17 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))))
605380, 597, 604rexlimd 3024 . . . . . . . . . . . . . . . 16 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
606375, 605mpd 15 . . . . . . . . . . . . . . 15 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))
6076sseli 3597 . . . . . . . . . . . . . . 15 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℤ)
608606, 607syl 17 . . . . . . . . . . . . . 14 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ ℤ)
609608zcnd 11480 . . . . . . . . . . . . 13 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ ℂ)
610609ad2antlr 763 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (1st𝑝) ∈ ℂ)
611596, 610nncand 10394 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝐽 − (1st𝑝))) = (1st𝑝))
612595, 611eqtrd 2655 . . . . . . . . . 10 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (1st𝑝))
613 reseq1 5388 . . . . . . . . . . . 12 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (𝑐𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅))
614613adantl 482 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅))
61575a1i 11 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
616615resmptd 5450 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅) = (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
617 nfv 1842 . . . . . . . . . . . . . 14 𝑘(𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝)
618396mpteq2ia 4738 . . . . . . . . . . . . . . . . . 18 (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡))
619618a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡)))
620425feqmptd 6247 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡)))
621619, 620eqtr4d 2658 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
6226213exp 1263 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))))
623622adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))))
624381, 617, 623rexlimd 3024 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝)))
625376, 624mpd 15 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
626625adantr 481 . . . . . . . . . . 11 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
627614, 616, 6263eqtrd 2659 . . . . . . . . . 10 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑅) = (2nd𝑝))
628612, 627opeq12d 4408 . . . . . . . . 9 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(1st𝑝), (2nd𝑝)⟩)
629 opex 4930 . . . . . . . . . 10 ⟨(1st𝑝), (2nd𝑝)⟩ ∈ V
630629a1i 11 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ⟨(1st𝑝), (2nd𝑝)⟩ ∈ V)
631582, 628, 581, 630fvmptd 6286 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) = ⟨(1st𝑝), (2nd𝑝)⟩)
632 nfv 1842 . . . . . . . . . 10 𝑘⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝
633 1st2nd2 7202 . . . . . . . . . . . . 13 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
634633eqcomd 2627 . . . . . . . . . . . 12 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)
635634a1i 11 . . . . . . . . . . 11 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝))
636635a1i 11 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)))
637381, 632, 636rexlimd 3024 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝))
638376, 637mpd 15 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)
639631, 638eqtr2d 2656 . . . . . . 7 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))))
640 fveq2 6189 . . . . . . . . 9 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (𝐷𝑐) = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))))
641640eqeq2d 2631 . . . . . . . 8 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (𝑝 = (𝐷𝑐) ↔ 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))))
642641rspcev 3307 . . . . . . 7 (((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
643581, 639, 642syl2anc 693 . . . . . 6 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
644643ralrimiva 2965 . . . . 5 (𝜑 → ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
645254, 644jca 554 . . . 4 (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐)))
646 dffo3 6372 . . . 4 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐)))
647645, 646sylibr 224 . . 3 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
648373, 647jca 554 . 2 (𝜑 → (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))))
649 df-f1o 5893 . 2 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))))
650648, 649sylibr 224 1 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1037   = wceq 1482  wex 1703  wcel 1989  wral 2911  wrex 2912  {crab 2915  Vcvv 3198  cun 3570  wss 3572  ifcif 4084  𝒫 cpw 4156  {csn 4175  cop 4181   ciun 4518   class class class wbr 4651  cmpt 4727   × cxp 5110  cres 5114   Fn wfn 5881  wf 5882  1-1wf1 5883  ontowfo 5884  1-1-ontowf1o 5885  cfv 5886  (class class class)co 6647  1st c1st 7163  2nd c2nd 7164  𝑚 cmap 7854  Fincfn 7952  cc 9931  cr 9932  0cc0 9933   + caddc 9936  cle 10072  cmin 10263  0cn0 11289  cz 11374  ...cfz 12323  Σcsu 14410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-inf2 8535  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010  ax-pre-sup 10011
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-fal 1488  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-se 5072  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-isom 5895  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-om 7063  df-1st 7165  df-2nd 7166  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-1o 7557  df-oadd 7561  df-er 7739  df-map 7856  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-sup 8345  df-oi 8412  df-card 8762  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-div 10682  df-nn 11018  df-2 11076  df-3 11077  df-n0 11290  df-z 11375  df-uz 11685  df-rp 11830  df-ico 12178  df-fz 12324  df-fzo 12462  df-seq 12797  df-exp 12856  df-hash 13113  df-cj 13833  df-re 13834  df-im 13835  df-sqrt 13969  df-abs 13970  df-clim 14213  df-sum 14411
This theorem is referenced by:  dvnprodlem2  39931
  Copyright terms: Public domain W3C validator