Theorem isumsplit 12010

Description: Split off the first 𝑁 terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 21-Oct-2022.)

Hypotheses

Ref	Expression
isumsplit.1	⊢ 𝑍 = (ℤ≥‘𝑀)
isumsplit.2	⊢ 𝑊 = (ℤ≥‘𝑁)
isumsplit.3	⊢ (𝜑 → 𝑁 ∈ 𝑍)
isumsplit.4	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
isumsplit.5	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)
isumsplit.6	⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )

Assertion

Ref	Expression
isumsplit	⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴))

Distinct variable groups:   𝑘,𝐹   𝑘,𝑀   𝜑,𝑘   𝑘,𝑍   𝑘,𝑁   𝑘,𝑊

Allowed substitution hint:   𝐴(𝑘)

Proof of Theorem isumsplit

Dummy variables 𝑗 𝑚 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isumsplit.1	. 2 ⊢ 𝑍 = (ℤ≥‘𝑀)
2		isumsplit.3	. . . 4 ⊢ (𝜑 → 𝑁 ∈ 𝑍)
3	2, 1	eleqtrdi 2322	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))
4		eluzel2 9735	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
5	3, 4	syl 14	. 2 ⊢ (𝜑 → 𝑀 ∈ ℤ)
6		isumsplit.4	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)
7		isumsplit.5	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ∈ ℂ)
8		isumsplit.2	. . 3 ⊢ 𝑊 = (ℤ≥‘𝑁)
9		eluzelz 9739	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
10	3, 9	syl 14	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℤ)
11		uzss 9751	. . . . . . . 8 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀))
12	3, 11	syl 14	. . . . . . 7 ⊢ (𝜑 → (ℤ≥‘𝑁) ⊆ (ℤ≥‘𝑀))
13	12, 8, 1	3sstr4g 3267	. . . . . 6 ⊢ (𝜑 → 𝑊 ⊆ 𝑍)
14	13	sselda 3224	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝑘 ∈ 𝑍)
15	14, 6	syldan 282	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) = 𝐴)
16	14, 7	syldan 282	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → 𝐴 ∈ ℂ)
17		isumsplit.6	. . . . 5 ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
18	6, 7	eqeltrd 2306	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ)
19	1, 2, 18	iserex 11858	. . . . 5 ⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
20	17, 19	mpbid 147	. . . 4 ⊢ (𝜑 → seq𝑁( + , 𝐹) ∈ dom ⇝ )
21	8, 10, 15, 16, 20	isumclim2 11941	. . 3 ⊢ (𝜑 → seq𝑁( + , 𝐹) ⇝ Σ𝑘 ∈ 𝑊 𝐴)
22		peano2zm 9492	. . . . . 6 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
23	10, 22	syl 14	. . . . 5 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
24	5, 23	fzfigd 10661	. . . 4 ⊢ (𝜑 → (𝑀...(𝑁 − 1)) ∈ Fin)
25		elfzuz 10225	. . . . . 6 ⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) → 𝑘 ∈ (ℤ≥‘𝑀))
26	25, 1	eleqtrrdi 2323	. . . . 5 ⊢ (𝑘 ∈ (𝑀...(𝑁 − 1)) → 𝑘 ∈ 𝑍)
27	26, 7	sylan2 286	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → 𝐴 ∈ ℂ)
28	24, 27	fsumcl 11919	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 ∈ ℂ)
29	14, 18	syldan 282	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑊) → (𝐹‘𝑘) ∈ ℂ)
30	8, 10, 29	serf 10713	. . . 4 ⊢ (𝜑 → seq𝑁( + , 𝐹):𝑊⟶ℂ)
31	30	ffvelcdmda 5772	. . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑁( + , 𝐹)‘𝑗) ∈ ℂ)
32	5	zred 9577	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℝ)
33	32	ltm1d 9087	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − 1) < 𝑀)
34		peano2zm 9492	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
35	5, 34	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 − 1) ∈ ℤ)
36		fzn 10246	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ) → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅))
37	5, 35, 36	syl2anc 411	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅))
38	33, 37	mpbid 147	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀...(𝑀 − 1)) = ∅)
39	38	sumeq1d 11885	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = Σ𝑘 ∈ ∅ 𝐴)
40	39	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = Σ𝑘 ∈ ∅ 𝐴)
41		sum0 11907	. . . . . . . 8 ⊢ Σ𝑘 ∈ ∅ 𝐴 = 0
42	40, 41	eqtrdi 2278	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 = 0)
43	42	oveq1d 6022	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗)) = (0 + (seq𝑀( + , 𝐹)‘𝑗)))
44	13	sselda 3224	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝑗 ∈ 𝑍)
45	1, 5, 18	serf 10713	. . . . . . . . 9 ⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℂ)
46	45	ffvelcdmda 5772	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℂ)
47	44, 46	syldan 282	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℂ)
48	47	addlidd 8304	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (0 + (seq𝑀( + , 𝐹)‘𝑗)) = (seq𝑀( + , 𝐹)‘𝑗))
49	43, 48	eqtr2d 2263	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗)))
50		oveq1 6014	. . . . . . . . 9 ⊢ (𝑁 = 𝑀 → (𝑁 − 1) = (𝑀 − 1))
51	50	oveq2d 6023	. . . . . . . 8 ⊢ (𝑁 = 𝑀 → (𝑀...(𝑁 − 1)) = (𝑀...(𝑀 − 1)))
52	51	sumeq1d 11885	. . . . . . 7 ⊢ (𝑁 = 𝑀 → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 = Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴)
53		seqeq1 10680	. . . . . . . 8 ⊢ (𝑁 = 𝑀 → seq𝑁( + , 𝐹) = seq𝑀( + , 𝐹))
54	53	fveq1d 5631	. . . . . . 7 ⊢ (𝑁 = 𝑀 → (seq𝑁( + , 𝐹)‘𝑗) = (seq𝑀( + , 𝐹)‘𝑗))
55	52, 54	oveq12d 6025	. . . . . 6 ⊢ (𝑁 = 𝑀 → (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗)))
56	55	eqeq2d 2241	. . . . 5 ⊢ (𝑁 = 𝑀 → ((seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) ↔ (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑀 − 1))𝐴 + (seq𝑀( + , 𝐹)‘𝑗))))
57	49, 56	syl5ibrcom 157	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 = 𝑀 → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗))))
58		addcl 8132	. . . . . . . 8 ⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝑘 + 𝑚) ∈ ℂ)
59	58	adantl 277	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝑘 + 𝑚) ∈ ℂ)
60		addass 8137	. . . . . . . 8 ⊢ ((𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝑘 + 𝑚) + 𝑥) = (𝑘 + (𝑚 + 𝑥)))
61	60	adantl 277	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ (𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑘 + 𝑚) + 𝑥) = (𝑘 + (𝑚 + 𝑥)))
62		simplr 528	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈ 𝑊)
63		simpll 527	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝜑)
64	10	zcnd 9578	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
65		ax-1cn 8100	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
66		npcan 8363	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
67	64, 65, 66	sylancl 413	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
68	67	eqcomd 2235	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 = ((𝑁 − 1) + 1))
69	63, 68	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑁 = ((𝑁 − 1) + 1))
70	69	fveq2d 5633	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (ℤ≥‘𝑁) = (ℤ≥‘((𝑁 − 1) + 1)))
71	8, 70	eqtrid 2274	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑊 = (ℤ≥‘((𝑁 − 1) + 1)))
72	62, 71	eleqtrd 2308	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑗 ∈ (ℤ≥‘((𝑁 − 1) + 1)))
73	5	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → 𝑀 ∈ ℤ)
74		eluzp1m1 9754	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈ (ℤ≥‘𝑀))
75	73, 74	sylan 283	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈ (ℤ≥‘𝑀))
76	1	eleq2i 2296	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝑍 ↔ 𝑘 ∈ (ℤ≥‘𝑀))
77	76, 6	sylan2br 288	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = 𝐴)
78	63, 77	sylan 283	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = 𝐴)
79	76, 7	sylan2br 288	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℂ)
80	63, 79	sylan 283	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℂ)
81	78, 80	eqeltrd 2306	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) ∈ ℂ)
82	59, 61, 72, 75, 81	seq3split 10718	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑗) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗)))
83	78, 75, 80	fsum3ser 11916	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 = (seq𝑀( + , 𝐹)‘(𝑁 − 1)))
84	69	seqeq1d 10683	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → seq𝑁( + , 𝐹) = seq((𝑁 − 1) + 1)( + , 𝐹))
85	84	fveq1d 5631	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑁( + , 𝐹)‘𝑗) = (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗))
86	83, 85	oveq12d 6025	. . . . . 6 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (seq((𝑁 − 1) + 1)( + , 𝐹)‘𝑗)))
87	82, 86	eqtr4d 2265	. . . . 5 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝑊) ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)))
88	87	ex 115	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗))))
89		uzp1 9764	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))))
90	3, 89	syl 14	. . . . 5 ⊢ (𝜑 → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))))
91	90	adantr 276	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (𝑁 = 𝑀 ∨ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))))
92	57, 88, 91	mpjaod 723	. . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑗) = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + (seq𝑁( + , 𝐹)‘𝑗)))
93	8, 10, 21, 28, 17, 31, 92	climaddc2 11849	. 2 ⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴))
94	1, 5, 6, 7, 93	isumclim 11940	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 𝐴 = (Σ𝑘 ∈ (𝑀...(𝑁 − 1))𝐴 + Σ𝑘 ∈ 𝑊 𝐴))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 713   ∧ w3a 1002   = wceq 1395   ∈ wcel 2200   ⊆ wss 3197  ∅c0 3491   class class class wbr 4083  dom cdm 4719  ‘cfv 5318  (class class class)co 6007  ℂcc 8005  0cc0 8007  1c1 8008   + caddc 8010   < clt 8189   − cmin 8325  ℤcz 9454  ℤ_≥cuz 9730  ...cfz 10212  seqcseq 10677   ⇝ cli 11797  Σcsu 11872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4199  ax-sep 4202  ax-nul 4210  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-iinf 4680  ax-cnex 8098  ax-resscn 8099  ax-1cn 8100  ax-1re 8101  ax-icn 8102  ax-addcl 8103  ax-addrcl 8104  ax-mulcl 8105  ax-mulrcl 8106  ax-addcom 8107  ax-mulcom 8108  ax-addass 8109  ax-mulass 8110  ax-distr 8111  ax-i2m1 8112  ax-0lt1 8113  ax-1rid 8114  ax-0id 8115  ax-rnegex 8116  ax-precex 8117  ax-cnre 8118  ax-pre-ltirr 8119  ax-pre-ltwlin 8120  ax-pre-lttrn 8121  ax-pre-apti 8122  ax-pre-ltadd 8123  ax-pre-mulgt0 8124  ax-pre-mulext 8125  ax-arch 8126  ax-caucvg 8127

This theorem depends on definitions:  df-bi 117  df-dc 840  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rmo 2516  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-nul 3492  df-if 3603  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-iun 3967  df-br 4084  df-opab 4146  df-mpt 4147  df-tr 4183  df-id 4384  df-po 4387  df-iso 4388  df-iord 4457  df-on 4459  df-ilim 4460  df-suc 4462  df-iom 4683  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-res 4731  df-ima 4732  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-f1 5323  df-fo 5324  df-f1o 5325  df-fv 5326  df-isom 5327  df-riota 5960  df-ov 6010  df-oprab 6011  df-mpo 6012  df-1st 6292  df-2nd 6293  df-recs 6457  df-irdg 6522  df-frec 6543  df-1o 6568  df-oadd 6572  df-er 6688  df-en 6896  df-dom 6897  df-fin 6898  df-pnf 8191  df-mnf 8192  df-xr 8193  df-ltxr 8194  df-le 8195  df-sub 8327  df-neg 8328  df-reap 8730  df-ap 8737  df-div 8828  df-inn 9119  df-2 9177  df-3 9178  df-4 9179  df-n0 9378  df-z 9455  df-uz 9731  df-q 9823  df-rp 9858  df-fz 10213  df-fzo 10347  df-seqfrec 10678  df-exp 10769  df-ihash 11006  df-cj 11361  df-re 11362  df-im 11363  df-rsqrt 11517  df-abs 11518  df-clim 11798  df-sumdc 11873

This theorem is referenced by:  isum1p  12011  geolim2  12031  mertenslem2  12055  mertensabs  12056  effsumlt  12211  eirraplem  12296  trilpolemeq1  16438  trilpolemlt1  16439  nconstwlpolemgt0  16462