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 45901
Description: 𝐷 is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
dvnprodlem1.c 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
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 2735 . . . . . 6 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
2 0zd 12622 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ∈ ℤ)
3 dvnprodlem1.j . . . . . . . . . 10 (𝜑𝐽 ∈ ℕ0)
43nn0zd 12636 . . . . . . . . 9 (𝜑𝐽 ∈ ℤ)
54adantr 480 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℤ)
6 oveq2 7438 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
76oveq1d 7445 . . . . . . . . . . . . . . . 16 (𝑛 = 𝐽 → ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
8 eqeq2 2746 . . . . . . . . . . . . . . . 16 (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
97, 8rabeqbidv 3451 . . . . . . . . . . . . . . 15 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
10 dvnprodlem1.c . . . . . . . . . . . . . . . 16 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
11 oveq2 7438 . . . . . . . . . . . . . . . . . 18 (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m (𝑅 ∪ {𝑍})))
12 sumeq1 15721 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
1312eqeq1d 2736 . . . . . . . . . . . . . . . . . 18 (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛))
1411, 13rabeqbidv 3451 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
1514mpteq2dv 5249 . . . . . . . . . . . . . . . 16 (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
16 dvnprodlem1.t . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ∈ Fin)
17 dvnprodlem1.rzt . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
1816, 17sselpwd 5333 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
19 nn0ex 12529 . . . . . . . . . . . . . . . . . 18 0 ∈ V
2019mptex 7242 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V
2120a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V)
2210, 15, 18, 21fvmptd3 7038 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
23 ovex 7463 . . . . . . . . . . . . . . . . 17 ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ V
2423rabex 5344 . . . . . . . . . . . . . . . 16 {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V
2524a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V)
269, 22, 3, 25fvmptd4 7039 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
27 ssrab2 4089 . . . . . . . . . . . . . 14 {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍}))
2826, 27eqsstrdi 4049 . . . . . . . . . . . . 13 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
2928sselda 3994 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
30 elmapi 8887 . . . . . . . . . . . 12 (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
3129, 30syl 17 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
32 dvnprodlem1.z . . . . . . . . . . . . 13 (𝜑𝑍𝑇)
33 snidg 4664 . . . . . . . . . . . . 13 (𝑍𝑇𝑍 ∈ {𝑍})
34 elun2 4192 . . . . . . . . . . . . 13 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
3532, 33, 343syl 18 . . . . . . . . . . . 12 (𝜑𝑍 ∈ (𝑅 ∪ {𝑍}))
3635adantr 480 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
3731, 36ffvelcdmd 7104 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝐽))
3837elfzelzd 13561 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℤ)
395, 38zsubcld 12724 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
40 elfzle2 13564 . . . . . . . . . 10 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ≤ 𝐽)
4137, 40syl 17 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ≤ 𝐽)
425zred 12719 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℝ)
4338zred 12719 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℝ)
4442, 43subge0d 11850 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝐽 − (𝑐𝑍)) ↔ (𝑐𝑍) ≤ 𝐽))
4541, 44mpbird 257 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝐽 − (𝑐𝑍)))
46 elfzle1 13563 . . . . . . . . . 10 ((𝑐𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐𝑍))
4737, 46syl 17 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 0 ≤ (𝑐𝑍))
4842, 43subge02d 11852 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0 ≤ (𝑐𝑍) ↔ (𝐽 − (𝑐𝑍)) ≤ 𝐽))
4947, 48mpbid 232 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ≤ 𝐽)
502, 5, 39, 45, 49elfzd 13551 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
51 eqidd 2735 . . . . . . . . . . 11 (𝑒 = (𝑐𝑅) → 𝑅 = 𝑅)
52 simpl 482 . . . . . . . . . . . 12 ((𝑒 = (𝑐𝑅) ∧ 𝑡𝑅) → 𝑒 = (𝑐𝑅))
5352fveq1d 6908 . . . . . . . . . . 11 ((𝑒 = (𝑐𝑅) ∧ 𝑡𝑅) → (𝑒𝑡) = ((𝑐𝑅)‘𝑡))
5451, 53sumeq12rdv 15739 . . . . . . . . . 10 (𝑒 = (𝑐𝑅) → Σ𝑡𝑅 (𝑒𝑡) = Σ𝑡𝑅 ((𝑐𝑅)‘𝑡))
5554eqeq1d 2736 . . . . . . . . 9 (𝑒 = (𝑐𝑅) → (Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍)) ↔ Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍))))
56 ovexd 7465 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...(𝐽 − (𝑐𝑍))) ∈ V)
5717unssad 4202 . . . . . . . . . . . 12 (𝜑𝑅𝑇)
5816, 57ssfid 9298 . . . . . . . . . . 11 (𝜑𝑅 ∈ Fin)
5958adantr 480 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
60 elmapfn 8903 . . . . . . . . . . . . 13 (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → 𝑐 Fn (𝑅 ∪ {𝑍}))
6129, 60syl 17 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
62 ssun1 4187 . . . . . . . . . . . . 13 𝑅 ⊆ (𝑅 ∪ {𝑍})
6362a1i 11 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
6461, 63fnssresd 6692 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) Fn 𝑅)
65 nfv 1911 . . . . . . . . . . . . 13 𝑡𝜑
66 nfcv 2902 . . . . . . . . . . . . . . . . . 18 𝑡𝒫 𝑇
67 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑡0
68 nfcv 2902 . . . . . . . . . . . . . . . . . . . . . 22 𝑡𝑠
6968nfsum1 15722 . . . . . . . . . . . . . . . . . . . . 21 𝑡Σ𝑡𝑠 (𝑐𝑡)
7069nfeq1 2918 . . . . . . . . . . . . . . . . . . . 20 𝑡Σ𝑡𝑠 (𝑐𝑡) = 𝑛
71 nfcv 2902 . . . . . . . . . . . . . . . . . . . 20 𝑡((0...𝑛) ↑m 𝑠)
7270, 71nfrabw 3472 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}
7367, 72nfmpt 5254 . . . . . . . . . . . . . . . . . 18 𝑡(𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
7466, 73nfmpt 5254 . . . . . . . . . . . . . . . . 17 𝑡(𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
7510, 74nfcxfr 2900 . . . . . . . . . . . . . . . 16 𝑡𝐶
76 nfcv 2902 . . . . . . . . . . . . . . . 16 𝑡(𝑅 ∪ {𝑍})
7775, 76nffv 6916 . . . . . . . . . . . . . . 15 𝑡(𝐶‘(𝑅 ∪ {𝑍}))
78 nfcv 2902 . . . . . . . . . . . . . . 15 𝑡𝐽
7977, 78nffv 6916 . . . . . . . . . . . . . 14 𝑡((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
8079nfcri 2894 . . . . . . . . . . . . 13 𝑡 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
8165, 80nfan 1896 . . . . . . . . . . . 12 𝑡(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
82 fvres 6925 . . . . . . . . . . . . . 14 (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
8382adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
84 0zd 12622 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 0 ∈ ℤ)
8539adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
8631adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
8763sselda 3994 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
8886, 87ffvelcdmd 7104 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝐽))
8988elfzelzd 13561 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℤ)
90 elfzle1 13563 . . . . . . . . . . . . . . 15 ((𝑐𝑡) ∈ (0...𝐽) → 0 ≤ (𝑐𝑡))
9188, 90syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 0 ≤ (𝑐𝑡))
9258ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑅 ∈ Fin)
93 fzssre 45264 . . . . . . . . . . . . . . . . . 18 (0...𝐽) ⊆ ℝ
9431adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
9563sselda 3994 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 𝑟 ∈ (𝑅 ∪ {𝑍}))
9694, 95ffvelcdmd 7104 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ (0...𝐽))
9793, 96sselid 3992 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℝ)
9897adantlr 715 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℝ)
99 elfzle1 13563 . . . . . . . . . . . . . . . . . 18 ((𝑐𝑟) ∈ (0...𝐽) → 0 ≤ (𝑐𝑟))
10096, 99syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → 0 ≤ (𝑐𝑟))
101100adantlr 715 . . . . . . . . . . . . . . . 16 ((((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) ∧ 𝑟𝑅) → 0 ≤ (𝑐𝑟))
102 fveq2 6906 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑡 → (𝑐𝑟) = (𝑐𝑡))
103 simpr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡𝑅)
10492, 98, 101, 102, 103fsumge1 15829 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ≤ Σ𝑟𝑅 (𝑐𝑟))
10597recnd 11286 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑟𝑅) → (𝑐𝑟) ∈ ℂ)
10659, 105fsumcl 15765 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) ∈ ℂ)
10738zcnd 12720 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℂ)
108102cbvsumv 15728 . . . . . . . . . . . . . . . . . 18 Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡)
109 nfv 1911 . . . . . . . . . . . . . . . . . . 19 𝑟(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
110 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑟(𝑐𝑍)
11132adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
112 dvnprodlem1.zr . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ 𝑍𝑅)
113112adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
114 fveq2 6906 . . . . . . . . . . . . . . . . . . 19 (𝑟 = 𝑍 → (𝑐𝑟) = (𝑐𝑍))
115109, 110, 59, 111, 113, 105, 114, 107fsumsplitsn 15776 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟 ∈ (𝑅 ∪ {𝑍})(𝑐𝑟) = (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)))
116 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
11726adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
118116, 117eleqtrd 2840 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
119 rabid 3454 . . . . . . . . . . . . . . . . . . . 20 (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ↔ (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
120118, 119sylib 218 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∧ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
121120simprd 495 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽)
122108, 115, 1213eqtr3a 2798 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (Σ𝑟𝑅 (𝑐𝑟) + (𝑐𝑍)) = 𝐽)
123106, 107, 122mvlraddd 11670 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
124123adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → Σ𝑟𝑅 (𝑐𝑟) = (𝐽 − (𝑐𝑍)))
125104, 124breqtrd 5173 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ≤ (𝐽 − (𝑐𝑍)))
12684, 85, 89, 91, 125elfzd 13551 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
12783, 126eqeltrd 2838 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
12881, 127ralrimia 3255 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍))))
129 ffnfv 7138 . . . . . . . . . . 11 ((𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍))) ↔ ((𝑐𝑅) Fn 𝑅 ∧ ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) ∈ (0...(𝐽 − (𝑐𝑍)))))
13064, 128, 129sylanbrc 583 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅):𝑅⟶(0...(𝐽 − (𝑐𝑍))))
13156, 59, 130elmapdd 8879 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅))
13282a1i 11 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡)))
13381, 132ralrimi 3254 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∀𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
134133sumeq2d 15733 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = Σ𝑡𝑅 (𝑐𝑡))
135102cbvsumv 15728 . . . . . . . . . . . 12 Σ𝑟𝑅 (𝑐𝑟) = Σ𝑡𝑅 (𝑐𝑡)
136135eqcomi 2743 . . . . . . . . . . 11 Σ𝑡𝑅 (𝑐𝑡) = Σ𝑟𝑅 (𝑐𝑟)
137136a1i 11 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑟𝑅 (𝑐𝑟))
138134, 137, 1233eqtrd 2778 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → Σ𝑡𝑅 ((𝑐𝑅)‘𝑡) = (𝐽 − (𝑐𝑍)))
13955, 131, 138elrabd 3696 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
140 fveq1 6905 . . . . . . . . . . . . . 14 (𝑐 = 𝑒 → (𝑐𝑡) = (𝑒𝑡))
141140sumeq2sdv 15735 . . . . . . . . . . . . 13 (𝑐 = 𝑒 → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑡𝑅 (𝑒𝑡))
142141eqeq1d 2736 . . . . . . . . . . . 12 (𝑐 = 𝑒 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑚 ↔ Σ𝑡𝑅 (𝑒𝑡) = 𝑚))
143142cbvrabv 3443 . . . . . . . . . . 11 {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚}
144143a1i 11 . . . . . . . . . 10 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
145 oveq2 7438 . . . . . . . . . . . 12 (𝑚 = (𝐽 − (𝑐𝑍)) → (0...𝑚) = (0...(𝐽 − (𝑐𝑍))))
146145oveq1d 7445 . . . . . . . . . . 11 (𝑚 = (𝐽 − (𝑐𝑍)) → ((0...𝑚) ↑m 𝑅) = ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅))
147146rabeqdv 3448 . . . . . . . . . 10 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑒 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚})
148 eqeq2 2746 . . . . . . . . . . 11 (𝑚 = (𝐽 − (𝑐𝑍)) → (Σ𝑡𝑅 (𝑒𝑡) = 𝑚 ↔ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))))
149148rabbidv 3440 . . . . . . . . . 10 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
150144, 147, 1493eqtrd 2778 . . . . . . . . 9 (𝑚 = (𝐽 − (𝑐𝑍)) → {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚} = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
151 oveq2 7438 . . . . . . . . . . . . . 14 (𝑠 = 𝑅 → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑅))
152 sumeq1 15721 . . . . . . . . . . . . . . 15 (𝑠 = 𝑅 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑅 (𝑐𝑡))
153152eqeq1d 2736 . . . . . . . . . . . . . 14 (𝑠 = 𝑅 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑛))
154151, 153rabeqbidv 3451 . . . . . . . . . . . . 13 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
155154mpteq2dv 5249 . . . . . . . . . . . 12 (𝑠 = 𝑅 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
15616, 57sselpwd 5333 . . . . . . . . . . . 12 (𝜑𝑅 ∈ 𝒫 𝑇)
15719mptex 7242 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V
158157a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V)
15910, 155, 156, 158fvmptd3 7038 . . . . . . . . . . 11 (𝜑 → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
160159adantr 480 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
161 oveq2 7438 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → (0...𝑛) = (0...𝑚))
162161oveq1d 7445 . . . . . . . . . . . 12 (𝑛 = 𝑚 → ((0...𝑛) ↑m 𝑅) = ((0...𝑚) ↑m 𝑅))
163 eqeq2 2746 . . . . . . . . . . . 12 (𝑛 = 𝑚 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑚))
164162, 163rabeqbidv 3451 . . . . . . . . . . 11 (𝑛 = 𝑚 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
165164cbvmptv 5260 . . . . . . . . . 10 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚})
166160, 165eqtrdi 2790 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐶𝑅) = (𝑚 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑚) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑚}))
167 elnn0z 12623 . . . . . . . . . 10 ((𝐽 − (𝑐𝑍)) ∈ ℕ0 ↔ ((𝐽 − (𝑐𝑍)) ∈ ℤ ∧ 0 ≤ (𝐽 − (𝑐𝑍))))
16839, 45, 167sylanbrc 583 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
169 ovex 7463 . . . . . . . . . . 11 ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∈ V
170169rabex 5344 . . . . . . . . . 10 {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ∈ V
171170a1i 11 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))} ∈ V)
172150, 166, 168, 171fvmptd4 7039 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))) = {𝑒 ∈ ((0...(𝐽 − (𝑐𝑍))) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑒𝑡) = (𝐽 − (𝑐𝑍))})
173139, 172eleqtrrd 2841 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
17450, 173jca 511 . . . . . 6 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))
175 ovexd 7465 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ V)
176 vex 3481 . . . . . . . 8 𝑐 ∈ V
177176resex 6048 . . . . . . 7 (𝑐𝑅) ∈ V
178 opeq12 4879 . . . . . . . . . 10 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ⟨𝑘, 𝑑⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
179178eqeq2d 2745 . . . . . . . . 9 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ↔ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
180 eleq1 2826 . . . . . . . . . . 11 (𝑘 = (𝐽 − (𝑐𝑍)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐𝑍)) ∈ (0...𝐽)))
181180adantr 480 . . . . . . . . . 10 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (𝑘 ∈ (0...𝐽) ↔ (𝐽 − (𝑐𝑍)) ∈ (0...𝐽)))
182 simpr 484 . . . . . . . . . . 11 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → 𝑑 = (𝑐𝑅))
183 fveq2 6906 . . . . . . . . . . . 12 (𝑘 = (𝐽 − (𝑐𝑍)) → ((𝐶𝑅)‘𝑘) = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
184183adantr 480 . . . . . . . . . . 11 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((𝐶𝑅)‘𝑘) = ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))
185182, 184eleq12d 2832 . . . . . . . . . 10 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → (𝑑 ∈ ((𝐶𝑅)‘𝑘) ↔ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))
186181, 185anbi12d 632 . . . . . . . . 9 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)) ↔ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))))
187179, 186anbi12d 632 . . . . . . . 8 ((𝑘 = (𝐽 − (𝑐𝑍)) ∧ 𝑑 = (𝑐𝑅)) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))) ↔ (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍)))))))
188187spc2egv 3598 . . . . . . 7 (((𝐽 − (𝑐𝑍)) ∈ V ∧ (𝑐𝑅) ∈ V) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)))))
189175, 177, 188sylancl 586 . . . . . 6 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∧ ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ∧ (𝑐𝑅) ∈ ((𝐶𝑅)‘(𝐽 − (𝑐𝑍))))) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘)))))
1901, 174, 189mp2and 699 . . . . 5 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))))
191 eliunxp 5850 . . . . 5 (⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘𝑑(⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨𝑘, 𝑑⟩ ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑑 ∈ ((𝐶𝑅)‘𝑘))))
192190, 191sylibr 234 . . . 4 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
193 dvnprodlem1.d . . . 4 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
194192, 193fmptd 7133 . . 3 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
19579nfcri 2894 . . . . . . . . . 10 𝑡 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)
19680, 195nfan 1896 . . . . . . . . 9 𝑡(𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
19765, 196nfan 1896 . . . . . . . 8 𝑡(𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
198 nfv 1911 . . . . . . . 8 𝑡(𝐷𝑐) = (𝐷𝑒)
199197, 198nfan 1896 . . . . . . 7 𝑡((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒))
20083eqcomd 2740 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
201200adantlrr 721 . . . . . . . . . . 11 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
202201adantlr 715 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (𝑐𝑡) = ((𝑐𝑅)‘𝑡))
203193a1i 11 . . . . . . . . . . . . . . . 16 (𝜑𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
204 opex 5474 . . . . . . . . . . . . . . . . 17 ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V
205204a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V)
206203, 205fvmpt2d 7028 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
207206fveq2d 6910 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
208207fveq1d 6908 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((2nd ‘(𝐷𝑐))‘𝑡) = ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡))
209 ovex 7463 . . . . . . . . . . . . . . 15 (𝐽 − (𝑐𝑍)) ∈ V
210209, 177op2nd 8021 . . . . . . . . . . . . . 14 (2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝑐𝑅)
211210fveq1i 6907 . . . . . . . . . . . . 13 ((2nd ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)‘𝑡) = ((𝑐𝑅)‘𝑡)
212208, 211eqtr2di 2791 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
213212adantrr 717 . . . . . . . . . . 11 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
214213ad2antrr 726 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((𝑐𝑅)‘𝑡) = ((2nd ‘(𝐷𝑐))‘𝑡))
215 simpr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑐) = (𝐷𝑒))
216 fveq1 6905 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑒 → (𝑐𝑍) = (𝑒𝑍))
217216oveq2d 7446 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝑒𝑍)))
218 reseq1 5993 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (𝑐𝑅) = (𝑒𝑅))
219217, 218opeq12d 4885 . . . . . . . . . . . . . . . . . . 19 (𝑐 = 𝑒 → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
220 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
221 opex 5474 . . . . . . . . . . . . . . . . . . . 20 ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩ ∈ V
222221a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩ ∈ V)
223193, 219, 220, 222fvmptd3 7038 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑒) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
224223adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑒) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
225215, 224eqtrd 2774 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐷𝑐) = ⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩)
226225fveq2d 6910 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
227226adantlrl 720 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
228227adantr 480 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘(𝐷𝑐)) = (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
229 ovex 7463 . . . . . . . . . . . . . 14 (𝐽 − (𝑒𝑍)) ∈ V
230 vex 3481 . . . . . . . . . . . . . . 15 𝑒 ∈ V
231230resex 6048 . . . . . . . . . . . . . 14 (𝑒𝑅) ∈ V
232229, 231op2nd 8021 . . . . . . . . . . . . 13 (2nd ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝑒𝑅)
233228, 232eqtrdi 2790 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (2nd ‘(𝐷𝑐)) = (𝑒𝑅))
234233fveq1d 6908 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((2nd ‘(𝐷𝑐))‘𝑡) = ((𝑒𝑅)‘𝑡))
235 fvres 6925 . . . . . . . . . . . 12 (𝑡𝑅 → ((𝑒𝑅)‘𝑡) = (𝑒𝑡))
236235adantl 481 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((𝑒𝑅)‘𝑡) = (𝑒𝑡))
237234, 236eqtrd 2774 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → ((2nd ‘(𝐷𝑐))‘𝑡) = (𝑒𝑡))
238202, 214, 2373eqtrd 2778 . . . . . . . . 9 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
239238adantlr 715 . . . . . . . 8 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
240 elunnel1 4163 . . . . . . . . . . 11 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡𝑅) → 𝑡 ∈ {𝑍})
241 elsni 4647 . . . . . . . . . . 11 (𝑡 ∈ {𝑍} → 𝑡 = 𝑍)
242240, 241syl 17 . . . . . . . . . 10 ((𝑡 ∈ (𝑅 ∪ {𝑍}) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
243242adantll 714 . . . . . . . . 9 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
244 simpr 484 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → 𝑡 = 𝑍)
245244fveq2d 6910 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑐𝑍))
2463nn0cnd 12586 . . . . . . . . . . . . . . . . . 18 (𝜑𝐽 ∈ ℂ)
247246adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
248247, 107nncand 11622 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝑐𝑍))
249248eqcomd 2740 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
250249adantrr 717 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
251250adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐𝑍) = (𝐽 − (𝐽 − (𝑐𝑍))))
252206fveq2d 6910 . . . . . . . . . . . . . . . . 17 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘(𝐷𝑐)) = (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩))
253209, 177op1st 8020 . . . . . . . . . . . . . . . . 17 (1st ‘⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩) = (𝐽 − (𝑐𝑍))
254252, 253eqtr2di 2791 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) = (1st ‘(𝐷𝑐)))
255254oveq2d 7446 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
256255adantrr 717 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
257256adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝐽 − (1st ‘(𝐷𝑐))))
258 fveq2 6906 . . . . . . . . . . . . . . . . . 18 ((𝐷𝑐) = (𝐷𝑒) → (1st ‘(𝐷𝑐)) = (1st ‘(𝐷𝑒)))
259258adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑐)) = (1st ‘(𝐷𝑒)))
260223fveq2d 6910 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (1st ‘(𝐷𝑒)) = (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
261260adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑒)) = (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩))
262229, 231op1st 8020 . . . . . . . . . . . . . . . . . 18 (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝐽 − (𝑒𝑍))
263262a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘⟨(𝐽 − (𝑒𝑍)), (𝑒𝑅)⟩) = (𝐽 − (𝑒𝑍)))
264259, 261, 2633eqtrd 2778 . . . . . . . . . . . . . . . 16 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (1st ‘(𝐷𝑐)) = (𝐽 − (𝑒𝑍)))
265264oveq2d 7446 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝐽 − (𝐽 − (𝑒𝑍))))
266246adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
267 fzsscn 45261 . . . . . . . . . . . . . . . . . 18 (0...𝐽) ⊆ ℂ
268 eleq1w 2821 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = 𝑒 → (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↔ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)))
269268anbi2d 630 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑒 → ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ↔ (𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))))
270 feq1 6716 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑒 → (𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽) ↔ 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽)))
271269, 270imbi12d 344 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = 𝑒 → (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽)) ↔ ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))))
272271, 31chvarvv 1995 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒:(𝑅 ∪ {𝑍})⟶(0...𝐽))
27335adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
274272, 273ffvelcdmd 7104 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒𝑍) ∈ (0...𝐽))
275267, 274sselid 3992 . . . . . . . . . . . . . . . . 17 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑒𝑍) ∈ ℂ)
276266, 275nncand 11622 . . . . . . . . . . . . . . . 16 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑒𝑍))) = (𝑒𝑍))
277276adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (𝐽 − (𝑒𝑍))) = (𝑒𝑍))
278265, 277eqtrd 2774 . . . . . . . . . . . . . 14 (((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝑒𝑍))
279278adantlrl 720 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝐽 − (1st ‘(𝐷𝑐))) = (𝑒𝑍))
280251, 257, 2793eqtrd 2778 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐𝑍) = (𝑒𝑍))
281280adantr 480 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑍) = (𝑒𝑍))
282 fveq2 6906 . . . . . . . . . . . . 13 (𝑡 = 𝑍 → (𝑒𝑡) = (𝑒𝑍))
283282eqcomd 2740 . . . . . . . . . . . 12 (𝑡 = 𝑍 → (𝑒𝑍) = (𝑒𝑡))
284283adantl 481 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑒𝑍) = (𝑒𝑡))
285245, 281, 2843eqtrd 2778 . . . . . . . . . 10 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑒𝑡))
286285adantlr 715 . . . . . . . . 9 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → (𝑐𝑡) = (𝑒𝑡))
287243, 286syldan 591 . . . . . . . 8 (((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (𝑐𝑡) = (𝑒𝑡))
288239, 287pm2.61dan 813 . . . . . . 7 ((((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) = (𝑒𝑡))
289199, 288ralrimia 3255 . . . . . 6 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡))
29061adantrr 717 . . . . . . . 8 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑐 Fn (𝑅 ∪ {𝑍}))
291290adantr 480 . . . . . . 7 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑐 Fn (𝑅 ∪ {𝑍}))
292272ffnd 6737 . . . . . . . . 9 ((𝜑𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
293292adantrl 716 . . . . . . . 8 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → 𝑒 Fn (𝑅 ∪ {𝑍}))
294293adantr 480 . . . . . . 7 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑒 Fn (𝑅 ∪ {𝑍}))
295 eqfnfv 7050 . . . . . . 7 ((𝑐 Fn (𝑅 ∪ {𝑍}) ∧ 𝑒 Fn (𝑅 ∪ {𝑍})) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡)))
296291, 294, 295syl2anc 584 . . . . . 6 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → (𝑐 = 𝑒 ↔ ∀𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = (𝑒𝑡)))
297289, 296mpbird 257 . . . . 5 (((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) ∧ (𝐷𝑐) = (𝐷𝑒)) → 𝑐 = 𝑒)
298297ex 412 . . . 4 ((𝜑 ∧ (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))) → ((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒))
299298ralrimivva 3199 . . 3 (𝜑 → ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒))
300 dff13 7274 . . 3 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)∀𝑒 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐷𝑐) = (𝐷𝑒) → 𝑐 = 𝑒)))
301194, 299, 300sylanbrc 583 . 2 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
302 eliun 4999 . . . . . . . . 9 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
303302biimpi 216 . . . . . . . 8 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
304303adantl 481 . . . . . . 7 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
305 nfv 1911 . . . . . . . . 9 𝑘𝜑
306 nfiu1 5031 . . . . . . . . . 10 𝑘 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
307306nfcri 2894 . . . . . . . . 9 𝑘 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
308305, 307nfan 1896 . . . . . . . 8 𝑘(𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
309 nfv 1911 . . . . . . . 8 𝑘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽}
310 eleq1w 2821 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑟 → (𝑡𝑅𝑟𝑅))
311 fveq2 6906 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑟 → ((2nd𝑝)‘𝑡) = ((2nd𝑝)‘𝑟))
312310, 311ifbieq1d 4554 . . . . . . . . . . . . . . 15 (𝑡 = 𝑟 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))
313312cbvmptv 5260 . . . . . . . . . . . . . 14 (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))
314313eqeq2i 2747 . . . . . . . . . . . . 13 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↔ 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
315 fveq1 6905 . . . . . . . . . . . . . 14 (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) → (𝑐𝑡) = ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
316315sumeq2sdv 15735 . . . . . . . . . . . . 13 (𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
317314, 316sylbi 217 . . . . . . . . . . . 12 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡))
318317eqeq1d 2736 . . . . . . . . . . 11 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽))
319 ovexd 7465 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (0...𝐽) ∈ V)
32016, 17ssexd 5329 . . . . . . . . . . . . 13 (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
3213203ad2ant1 1132 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑅 ∪ {𝑍}) ∈ V)
322 nfv 1911 . . . . . . . . . . . . . 14 𝑡 𝑘 ∈ (0...𝐽)
323 nfcv 2902 . . . . . . . . . . . . . . . 16 𝑡{𝑘}
324 nfcv 2902 . . . . . . . . . . . . . . . . . 18 𝑡𝑅
32575, 324nffv 6916 . . . . . . . . . . . . . . . . 17 𝑡(𝐶𝑅)
326 nfcv 2902 . . . . . . . . . . . . . . . . 17 𝑡𝑘
327325, 326nffv 6916 . . . . . . . . . . . . . . . 16 𝑡((𝐶𝑅)‘𝑘)
328323, 327nfxp 5721 . . . . . . . . . . . . . . 15 𝑡({𝑘} × ((𝐶𝑅)‘𝑘))
329328nfcri 2894 . . . . . . . . . . . . . 14 𝑡 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))
33065, 322, 329nf3an 1898 . . . . . . . . . . . . 13 𝑡(𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
331 0zd 12622 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ∈ ℤ)
3324adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
3333323ad2antl1 1184 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝐽 ∈ ℤ)
334 iftrue 4536 . . . . . . . . . . . . . . . . 17 (𝑡𝑅 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
335334adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
336 xp2nd 8045 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
3373363ad2ant3 1134 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
338 oveq2 7438 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
339338oveq1d 7445 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑘 → ((0...𝑛) ↑m 𝑅) = ((0...𝑘) ↑m 𝑅))
340 eqeq2 2746 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑘 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑘))
341339, 340rabeqbidv 3451 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
342159adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
343 elfznn0 13656 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ0)
344343adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ0)
345 ovex 7463 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0...𝑘) ↑m 𝑅) ∈ V
346345rabex 5344 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V
347346a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V)
348341, 342, 344, 347fvmptd4 7039 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
3493483adant3 1131 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
350337, 349eleqtrd 2840 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
351 elrabi 3689 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} → (2nd𝑝) ∈ ((0...𝑘) ↑m 𝑅))
352 elmapi 8887 . . . . . . . . . . . . . . . . . . . 20 ((2nd𝑝) ∈ ((0...𝑘) ↑m 𝑅) → (2nd𝑝):𝑅⟶(0...𝑘))
353350, 351, 3523syl 18 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝑘))
354353adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (2nd𝑝):𝑅⟶(0...𝑘))
355354ffvelcdmda 7103 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑘))
356355elfzelzd 13561 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℤ)
357335, 356eqeltrd 2838 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
358242adantll 714 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 𝑡 = 𝑍)
359 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 = 𝑍) → 𝑡 = 𝑍)
360112adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡 = 𝑍) → ¬ 𝑍𝑅)
361359, 360eqneltrd 2858 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 = 𝑍) → ¬ 𝑡𝑅)
362361iffalsed 4541 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
3633623ad2antl1 1184 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
3644adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 = 𝑍) → 𝐽 ∈ ℤ)
3653643ad2antl1 1184 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 𝐽 ∈ ℤ)
366 xp1st 8044 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ {𝑘})
367 elsni 4647 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1st𝑝) ∈ {𝑘} → (1st𝑝) = 𝑘)
368366, 367syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) = 𝑘)
369368adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
370 elfzelz 13560 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
371370adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ ℤ)
372369, 371eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
3733723adant1 1129 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
374373adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (1st𝑝) ∈ ℤ)
375365, 374zsubcld 12724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1st𝑝)) ∈ ℤ)
376363, 375eqeltrd 2838 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
377376adantlr 715 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
378358, 377syldan 591 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
379357, 378pm2.61dan 813 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℤ)
380353ffvelcdmda 7103 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑘))
381 elfzle1 13563 . . . . . . . . . . . . . . . . . 18 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → 0 ≤ ((2nd𝑝)‘𝑡))
382380, 381syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 0 ≤ ((2nd𝑝)‘𝑡))
383334eqcomd 2740 . . . . . . . . . . . . . . . . . 18 (𝑡𝑅 → ((2nd𝑝)‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
384383adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
385382, 384breqtrd 5173 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
386385adantlr 715 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
387 simpll 767 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → (𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))))
388 elfzle2 13564 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (0...𝐽) → 𝑘𝐽)
389 elfzel2 13558 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
390389zred 12719 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
39193sseli 3990 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
392390, 391subge0d 11850 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽𝑘) ↔ 𝑘𝐽))
393388, 392mpbird 257 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽𝑘))
394393adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ (0...𝐽) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽𝑘))
3953943ad2antl2 1185 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ (𝐽𝑘))
3963613ad2antl1 1184 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → ¬ 𝑡𝑅)
397396iffalsed 4541 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
3983683ad2ant3 1134 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
399398oveq2d 7446 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) = (𝐽𝑘))
400399adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽 − (1st𝑝)) = (𝐽𝑘))
401397, 400eqtr2d 2775 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽𝑘) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
402395, 401breqtrd 5173 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
403387, 358, 402syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
404386, 403pm2.61dan 813 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 0 ≤ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
405 simpl2 1191 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑘 ∈ (0...𝐽))
406 elfzelz 13560 . . . . . . . . . . . . . . . . . . . . 21 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ∈ ℤ)
407406zred 12719 . . . . . . . . . . . . . . . . . . . 20 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ∈ ℝ)
408407adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ∈ ℝ)
409391adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
410390adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
411 elfzle2 13564 . . . . . . . . . . . . . . . . . . . 20 (((2nd𝑝)‘𝑡) ∈ (0...𝑘) → ((2nd𝑝)‘𝑡) ≤ 𝑘)
412411adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ≤ 𝑘)
413388adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → 𝑘𝐽)
414408, 409, 410, 412, 413letrd 11415 . . . . . . . . . . . . . . . . . 18 ((((2nd𝑝)‘𝑡) ∈ (0...𝑘) ∧ 𝑘 ∈ (0...𝐽)) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
415380, 405, 414syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
416415adantlr 715 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ≤ 𝐽)
417335, 416eqbrtrd 5169 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
418344nn0ge0d 12587 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
419390adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
420391adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
421419, 420subge02d 11852 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽)) → (0 ≤ 𝑘 ↔ (𝐽𝑘) ≤ 𝐽))
422418, 421mpbid 232 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽𝑘) ≤ 𝐽)
423422adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑡 = 𝑍) → (𝐽𝑘) ≤ 𝐽)
4244233adantl3 1167 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → (𝐽𝑘) ≤ 𝐽)
425401, 424eqbrtrrd 5171 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 = 𝑍) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
426387, 358, 425syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) ∧ ¬ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
427417, 426pm2.61dan 813 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ≤ 𝐽)
428331, 333, 379, 404, 427elfzd 13551 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ (0...𝐽))
429330, 428fmptd2f 45177 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))):(𝑅 ∪ {𝑍})⟶(0...𝐽))
430319, 321, 429elmapdd 8879 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
431 eleq1w 2821 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑡 → (𝑟𝑅𝑡𝑅))
432 fveq2 6906 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑡 → ((2nd𝑝)‘𝑟) = ((2nd𝑝)‘𝑡))
433431, 432ifbieq1d 4554 . . . . . . . . . . . . . . 15 (𝑟 = 𝑡 → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
434 eqidd 2735 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))) = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
435 simpr 484 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
436433, 434, 435, 379fvmptd4 7039 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
437330, 436ralrimia 3255 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ∀𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
438437sumeq2d 15733 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))
439 nfcv 2902 . . . . . . . . . . . . 13 𝑡if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))
440583ad2ant1 1132 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
441323ad2ant1 1132 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑍𝑇)
4421123ad2ant1 1132 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ¬ 𝑍𝑅)
443334adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
444380elfzelzd 13561 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℤ)
445444zcnd 12720 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ ℂ)
446443, 445eqeltrd 2838 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) ∈ ℂ)
447 eleq1 2826 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → (𝑡𝑅𝑍𝑅))
448 fveq2 6906 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → ((2nd𝑝)‘𝑡) = ((2nd𝑝)‘𝑍))
449447, 448ifbieq1d 4554 . . . . . . . . . . . . 13 (𝑡 = 𝑍 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))))
450112adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ¬ 𝑍𝑅)
451450iffalsed 4541 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
4524513adant2 1130 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
45343ad2ant1 1132 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℤ)
454453, 373zsubcld 12724 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ ℤ)
455454zcnd 12720 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ ℂ)
456452, 455eqeltrd 2838 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) ∈ ℂ)
457330, 439, 440, 441, 442, 446, 449, 456fsumsplitsn 15776 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))))
458334a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 → if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡)))
459330, 458ralrimi 3254 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ∀𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = ((2nd𝑝)‘𝑡))
460459sumeq2d 15733 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = Σ𝑡𝑅 ((2nd𝑝)‘𝑡))
461 eqidd 2735 . . . . . . . . . . . . . . . . . . . 20 (𝑐 = (2nd𝑝) → 𝑅 = 𝑅)
462 simpl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑐 = (2nd𝑝) ∧ 𝑡𝑅) → 𝑐 = (2nd𝑝))
463462fveq1d 6908 . . . . . . . . . . . . . . . . . . . 20 ((𝑐 = (2nd𝑝) ∧ 𝑡𝑅) → (𝑐𝑡) = ((2nd𝑝)‘𝑡))
464461, 463sumeq12rdv 15739 . . . . . . . . . . . . . . . . . . 19 (𝑐 = (2nd𝑝) → Σ𝑡𝑅 (𝑐𝑡) = Σ𝑡𝑅 ((2nd𝑝)‘𝑡))
465464eqeq1d 2736 . . . . . . . . . . . . . . . . . 18 (𝑐 = (2nd𝑝) → (Σ𝑡𝑅 (𝑐𝑡) = 𝑘 ↔ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
466465elrab 3694 . . . . . . . . . . . . . . . . 17 ((2nd𝑝) ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ↔ ((2nd𝑝) ∈ ((0...𝑘) ↑m 𝑅) ∧ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
467350, 466sylib 218 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((2nd𝑝) ∈ ((0...𝑘) ↑m 𝑅) ∧ Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘))
468467simprd 495 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 ((2nd𝑝)‘𝑡) = 𝑘)
469460, 468eqtrd 2774 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) = 𝑘)
470442iffalsed 4541 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
471470, 399eqtrd 2774 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝))) = (𝐽𝑘))
472469, 471oveq12d 7448 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))) = (𝑘 + (𝐽𝑘)))
473267sseli 3990 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℂ)
4744733ad2ant2 1133 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ ℂ)
4752463ad2ant1 1132 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℂ)
476474, 475pncan3d 11620 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 + (𝐽𝑘)) = 𝐽)
477472, 476eqtrd 2774 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (Σ𝑡𝑅 if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))) + if(𝑍𝑅, ((2nd𝑝)‘𝑍), (𝐽 − (1st𝑝)))) = 𝐽)
478438, 457, 4773eqtrd 2778 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → Σ𝑡 ∈ (𝑅 ∪ {𝑍})((𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))))‘𝑡) = 𝐽)
479318, 430, 478elrabd 3696 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
4804793exp 1118 . . . . . . . . 9 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})))
481480adantr 480 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})))
482308, 309, 481rexlimd 3263 . . . . . . 7 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽}))
483304, 482mpd 15 . . . . . 6 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
48426eqcomd 2740 . . . . . . 7 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
485484adantr 480 . . . . . 6 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} = ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
486483, 485eleqtrd 2840 . . . . 5 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
487 simpr 484 . . . . . . . . . . . . 13 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
488487, 313eqtrdi 2790 . . . . . . . . . . . 12 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑐 = (𝑟 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝)))))
489 simpr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑟 = 𝑍) → 𝑟 = 𝑍)
490112adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑟 = 𝑍) → ¬ 𝑍𝑅)
491489, 490eqneltrd 2858 . . . . . . . . . . . . . 14 ((𝜑𝑟 = 𝑍) → ¬ 𝑟𝑅)
492491iffalsed 4541 . . . . . . . . . . . . 13 ((𝜑𝑟 = 𝑍) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
493492adantlr 715 . . . . . . . . . . . 12 (((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) ∧ 𝑟 = 𝑍) → if(𝑟𝑅, ((2nd𝑝)‘𝑟), (𝐽 − (1st𝑝))) = (𝐽 − (1st𝑝)))
49435adantr 480 . . . . . . . . . . . 12 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
495 ovexd 7465 . . . . . . . . . . . 12 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (1st𝑝)) ∈ V)
496488, 493, 494, 495fvmptd 7022 . . . . . . . . . . 11 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑍) = (𝐽 − (1st𝑝)))
497496oveq2d 7446 . . . . . . . . . 10 ((𝜑𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝐽 − (1st𝑝))))
498497adantlr 715 . . . . . . . . 9 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (𝐽 − (𝐽 − (1st𝑝))))
499246ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝐽 ∈ ℂ)
500 nfv 1911 . . . . . . . . . . . . . . 15 𝑘(1st𝑝) ∈ (0...𝐽)
501 simpl 482 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
502369, 501eqeltrd 2838 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
503502ex 412 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
504503a1i 11 . . . . . . . . . . . . . . 15 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))))
505307, 500, 504rexlimd 3263 . . . . . . . . . . . . . 14 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
506303, 505mpd 15 . . . . . . . . . . . . 13 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))
507506elfzelzd 13561 . . . . . . . . . . . 12 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ ℤ)
508507zcnd 12720 . . . . . . . . . . 11 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ ℂ)
509508ad2antlr 727 . . . . . . . . . 10 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (1st𝑝) ∈ ℂ)
510499, 509nncand 11622 . . . . . . . . 9 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝐽 − (1st𝑝))) = (1st𝑝))
511498, 510eqtrd 2774 . . . . . . . 8 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝐽 − (𝑐𝑍)) = (1st𝑝))
512 reseq1 5993 . . . . . . . . . 10 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (𝑐𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅))
513512adantl 481 . . . . . . . . 9 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑅) = ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅))
51462a1i 11 . . . . . . . . . 10 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → 𝑅 ⊆ (𝑅 ∪ {𝑍}))
515514resmptd 6059 . . . . . . . . 9 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → ((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ↾ 𝑅) = (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))
516 nfv 1911 . . . . . . . . . . . 12 𝑘(𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝)
517334mpteq2ia 5250 . . . . . . . . . . . . . . 15 (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡))
518353feqmptd 6976 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) = (𝑡𝑅 ↦ ((2nd𝑝)‘𝑡)))
519517, 518eqtr4id 2793 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
5205193exp 1118 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))))
521520adantr 480 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))))
522308, 516, 521rexlimd 3263 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝)))
523304, 522mpd 15 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
524523adantr 480 . . . . . . . . 9 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑡𝑅 ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) = (2nd𝑝))
525513, 515, 5243eqtrd 2778 . . . . . . . 8 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → (𝑐𝑅) = (2nd𝑝))
526511, 525opeq12d 4885 . . . . . . 7 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ = ⟨(1st𝑝), (2nd𝑝)⟩)
527 opex 5474 . . . . . . . 8 ⟨(1st𝑝), (2nd𝑝)⟩ ∈ V
528527a1i 11 . . . . . . 7 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ⟨(1st𝑝), (2nd𝑝)⟩ ∈ V)
529193, 526, 486, 528fvmptd2 7023 . . . . . 6 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))) = ⟨(1st𝑝), (2nd𝑝)⟩)
530 nfv 1911 . . . . . . . 8 𝑘⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝
531 1st2nd2 8051 . . . . . . . . . 10 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
532531eqcomd 2740 . . . . . . . . 9 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)
5335322a1i 12 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)))
534308, 530, 533rexlimd 3263 . . . . . . 7 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝))
535304, 534mpd 15 . . . . . 6 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ⟨(1st𝑝), (2nd𝑝)⟩ = 𝑝)
536529, 535eqtr2d 2775 . . . . 5 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))))
537 fveq2 6906 . . . . . 6 (𝑐 = (𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) → (𝐷𝑐) = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝))))))
538537rspceeqv 3644 . . . . 5 (((𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))) ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ 𝑝 = (𝐷‘(𝑡 ∈ (𝑅 ∪ {𝑍}) ↦ if(𝑡𝑅, ((2nd𝑝)‘𝑡), (𝐽 − (1st𝑝)))))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
539486, 536, 538syl2anc 584 . . . 4 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
540539ralrimiva 3143 . . 3 (𝜑 → ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐))
541 dffo3 7121 . . 3 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)⟶ 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ ∀𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))∃𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)𝑝 = (𝐷𝑐)))
542194, 540, 541sylanbrc 583 . 2 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
543 df-f1o 6569 . 2 (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ (𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ∧ 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))))
544301, 542, 543sylanbrc 583 1 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wex 1775  wcel 2105  wral 3058  wrex 3067  {crab 3432  Vcvv 3477  cun 3960  wss 3962  ifcif 4530  𝒫 cpw 4604  {csn 4630  cop 4636   ciun 4995   class class class wbr 5147  cmpt 5230   × cxp 5686  cres 5690   Fn wfn 6557  wf 6558  1-1wf1 6559  ontowfo 6560  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  1st c1st 8010  2nd c2nd 8011  m cmap 8864  Fincfn 8983  cc 11150  cr 11151  0cc0 11152   + caddc 11155  cle 11293  cmin 11489  0cn0 12523  cz 12610  ...cfz 13543  Σcsu 15718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-ico 13389  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719
This theorem is referenced by:  dvnprodlem2  45902
  Copyright terms: Public domain W3C validator