Theorem gsumval2 18112

Description: Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014.)

Hypotheses

Ref	Expression
gsumval2.b	⊢ 𝐵 = (Base‘𝐺)
gsumval2.p	⊢ + = (+g‘𝐺)
gsumval2.g	⊢ (𝜑 → 𝐺 ∈ 𝑉)
gsumval2.n	⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
gsumval2.f	⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)

Assertion

Ref	Expression
gsumval2	⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq𝑀( + , 𝐹)‘𝑁))

Proof of Theorem gsumval2

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gsumval2.b	. . . 4 ⊢ 𝐵 = (Base‘𝐺)
2		eqid 2736	. . . 4 ⊢ (0g‘𝐺) = (0g‘𝐺)
3		gsumval2.p	. . . 4 ⊢ + = (+g‘𝐺)
4		eqid 2736	. . . 4 ⊢ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}
5		gsumval2.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ 𝑉)
6	5	adantr 484	. . . 4 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → 𝐺 ∈ 𝑉)
7		ovexd 7226	. . . 4 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → (𝑀...𝑁) ∈ V)
8		gsumval2.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)
9	8	ffnd 6524	. . . . . 6 ⊢ (𝜑 → 𝐹 Fn (𝑀...𝑁))
10	9	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → 𝐹 Fn (𝑀...𝑁))
11		simpr 488	. . . . 5 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)})
12		df-f 6362	. . . . 5 ⊢ (𝐹:(𝑀...𝑁)⟶{𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} ↔ (𝐹 Fn (𝑀...𝑁) ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}))
13	10, 11, 12	sylanbrc 586	. . . 4 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → 𝐹:(𝑀...𝑁)⟶{𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)})
14	1, 2, 3, 4, 6, 7, 13	gsumval1 18109	. . 3 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → (𝐺 Σg 𝐹) = (0g‘𝐺))
15		simpl 486	. . . . . . . . 9 ⊢ (((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦) → (𝑥 + 𝑦) = 𝑦)
16	15	ralimi 3073	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦) → ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = 𝑦)
17	16	a1i 11	. . . . . . 7 ⊢ (𝑥 ∈ 𝐵 → (∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦) → ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = 𝑦))
18	17	ss2rabi 3976	. . . . . 6 ⊢ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = 𝑦}
19		fvex 6708	. . . . . . . 8 ⊢ (0g‘𝐺) ∈ V
20	19	snid 4563	. . . . . . 7 ⊢ (0g‘𝐺) ∈ {(0g‘𝐺)}
21	8	fdmd 6534	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom 𝐹 = (𝑀...𝑁))
22		gsumval2.n	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
23		eluzfz1 13084	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))
24		ne0i 4235	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (𝑀...𝑁) → (𝑀...𝑁) ≠ ∅)
25	22, 23, 24	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀...𝑁) ≠ ∅)
26	21, 25	eqnetrd 2999	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐹 ≠ ∅)
27		dm0rn0 5779	. . . . . . . . . . . . 13 ⊢ (dom 𝐹 = ∅ ↔ ran 𝐹 = ∅)
28	27	necon3bii 2984	. . . . . . . . . . . 12 ⊢ (dom 𝐹 ≠ ∅ ↔ ran 𝐹 ≠ ∅)
29	26, 28	sylib 221	. . . . . . . . . . 11 ⊢ (𝜑 → ran 𝐹 ≠ ∅)
30	29	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → ran 𝐹 ≠ ∅)
31		ssn0 4301	. . . . . . . . . 10 ⊢ ((ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} ∧ ran 𝐹 ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} ≠ ∅)
32	11, 30, 31	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} ≠ ∅)
33	32	neneqd 2937	. . . . . . . 8 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → ¬ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} = ∅)
34	1, 2, 3, 4	mgmidsssn0 18098	. . . . . . . . . . 11 ⊢ (𝐺 ∈ 𝑉 → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} ⊆ {(0g‘𝐺)})
35	5, 34	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} ⊆ {(0g‘𝐺)})
36		sssn 4725	. . . . . . . . . 10 ⊢ ({𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} ⊆ {(0g‘𝐺)} ↔ ({𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} = ∅ ∨ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} = {(0g‘𝐺)}))
37	35, 36	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → ({𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} = ∅ ∨ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} = {(0g‘𝐺)}))
38	37	orcanai 1003	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} = ∅) → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} = {(0g‘𝐺)})
39	33, 38	syldan 594	. . . . . . 7 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} = {(0g‘𝐺)})
40	20, 39	eleqtrrid 2838	. . . . . 6 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → (0g‘𝐺) ∈ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)})
41	18, 40	sseldi 3885	. . . . 5 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → (0g‘𝐺) ∈ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = 𝑦})
42		oveq1 7198	. . . . . . . . 9 ⊢ (𝑥 = (0g‘𝐺) → (𝑥 + 𝑦) = ((0g‘𝐺) + 𝑦))
43	42	eqeq1d 2738	. . . . . . . 8 ⊢ (𝑥 = (0g‘𝐺) → ((𝑥 + 𝑦) = 𝑦 ↔ ((0g‘𝐺) + 𝑦) = 𝑦))
44	43	ralbidv 3108	. . . . . . 7 ⊢ (𝑥 = (0g‘𝐺) → (∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = 𝑦 ↔ ∀𝑦 ∈ 𝐵 ((0g‘𝐺) + 𝑦) = 𝑦))
45	44	elrab 3591	. . . . . 6 ⊢ ((0g‘𝐺) ∈ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = 𝑦} ↔ ((0g‘𝐺) ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ((0g‘𝐺) + 𝑦) = 𝑦))
46		oveq2 7199	. . . . . . . 8 ⊢ (𝑦 = (0g‘𝐺) → ((0g‘𝐺) + 𝑦) = ((0g‘𝐺) + (0g‘𝐺)))
47		id 22	. . . . . . . 8 ⊢ (𝑦 = (0g‘𝐺) → 𝑦 = (0g‘𝐺))
48	46, 47	eqeq12d 2752	. . . . . . 7 ⊢ (𝑦 = (0g‘𝐺) → (((0g‘𝐺) + 𝑦) = 𝑦 ↔ ((0g‘𝐺) + (0g‘𝐺)) = (0g‘𝐺)))
49	48	rspcva 3525	. . . . . 6 ⊢ (((0g‘𝐺) ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ((0g‘𝐺) + 𝑦) = 𝑦) → ((0g‘𝐺) + (0g‘𝐺)) = (0g‘𝐺))
50	45, 49	sylbi 220	. . . . 5 ⊢ ((0g‘𝐺) ∈ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = 𝑦} → ((0g‘𝐺) + (0g‘𝐺)) = (0g‘𝐺))
51	41, 50	syl 17	. . . 4 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → ((0g‘𝐺) + (0g‘𝐺)) = (0g‘𝐺))
52	22	adantr 484	. . . 4 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → 𝑁 ∈ (ℤ≥‘𝑀))
53	35	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) ∧ 𝑧 ∈ (𝑀...𝑁)) → {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} ⊆ {(0g‘𝐺)})
54	13	ffvelrnda 6882	. . . . . 6 ⊢ (((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) ∧ 𝑧 ∈ (𝑀...𝑁)) → (𝐹‘𝑧) ∈ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)})
55	53, 54	sseldd 3888	. . . . 5 ⊢ (((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) ∧ 𝑧 ∈ (𝑀...𝑁)) → (𝐹‘𝑧) ∈ {(0g‘𝐺)})
56		elsni 4544	. . . . 5 ⊢ ((𝐹‘𝑧) ∈ {(0g‘𝐺)} → (𝐹‘𝑧) = (0g‘𝐺))
57	55, 56	syl 17	. . . 4 ⊢ (((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) ∧ 𝑧 ∈ (𝑀...𝑁)) → (𝐹‘𝑧) = (0g‘𝐺))
58	51, 52, 57	seqid3 13585	. . 3 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → (seq𝑀( + , 𝐹)‘𝑁) = (0g‘𝐺))
59	14, 58	eqtr4d 2774	. 2 ⊢ ((𝜑 ∧ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → (𝐺 Σg 𝐹) = (seq𝑀( + , 𝐹)‘𝑁))
60	5	adantr 484	. . 3 ⊢ ((𝜑 ∧ ¬ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → 𝐺 ∈ 𝑉)
61	22	adantr 484	. . 3 ⊢ ((𝜑 ∧ ¬ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → 𝑁 ∈ (ℤ≥‘𝑀))
62	8	adantr 484	. . 3 ⊢ ((𝜑 ∧ ¬ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → 𝐹:(𝑀...𝑁)⟶𝐵)
63		simpr 488	. . 3 ⊢ ((𝜑 ∧ ¬ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → ¬ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)})
64	1, 3, 60, 61, 62, 4, 63	gsumval2a 18111	. 2 ⊢ ((𝜑 ∧ ¬ ran 𝐹 ⊆ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}) → (𝐺 Σg 𝐹) = (seq𝑀( + , 𝐹)‘𝑁))
65	59, 64	pm2.61dan 813	1 ⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq𝑀( + , 𝐹)‘𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 847   = wceq 1543   ∈ wcel 2112   ≠ wne 2932  ∀wral 3051  {crab 3055  Vcvv 3398   ⊆ wss 3853  ∅c0 4223  {csn 4527  dom cdm 5536  ran crn 5537   Fn wfn 6353  ⟶wf 6354  ‘cfv 6358  (class class class)co 7191  ℤ_≥cuz 12403  ...cfz 13060  seqcseq 13539  Basecbs 16666  +_gcplusg 16749  0_gc0g 16898   Σ_g cgsu 16899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-cnex 10750  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-mulcom 10758  ax-addass 10759  ax-mulass 10760  ax-distr 10761  ax-i2m1 10762  ax-1ne0 10763  ax-1rid 10764  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767  ax-pre-lttri 10768  ax-pre-lttrn 10769  ax-pre-ltadd 10770  ax-pre-mulgt0 10771

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7148  df-ov 7194  df-oprab 7195  df-mpo 7196  df-om 7623  df-1st 7739  df-2nd 7740  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-pnf 10834  df-mnf 10835  df-xr 10836  df-ltxr 10837  df-le 10838  df-sub 11029  df-neg 11030  df-nn 11796  df-n0 12056  df-z 12142  df-uz 12404  df-fz 13061  df-seq 13540  df-0g 16900  df-gsum 16901

This theorem is referenced by:  gsumsplit1r  18113  gsumprval  18114  gsumwsubmcl  18217  gsumws1  18218  gsumsgrpccat  18220  gsumccatOLD  18221  gsumwmhm  18226  mulgnngsum  18451  gsumval3  19246  gsummptfzcl  19308  gsumncl  32185  gsumnunsn  32186