iccshift - Mathbox for Glauco Siliprandi

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

Theorem iccshift 46452

Description: A closed interval shifted by a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
iccshift.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
iccshift.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
iccshift.3	⊢ (𝜑 → 𝑇 ∈ ℝ)

**Assertion**
Ref	Expression
iccshift	⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)})

Distinct variable groups: 𝑤,𝐴,𝑧 𝑤,𝐵,𝑧 𝑤,𝑇,𝑧 𝜑,𝑧 Allowed substitution hint: 𝜑(𝑤)

Proof of Theorem iccshift Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2764	. . . . . . 7 ⊢ (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇)))
2	1	rexbidv 3186	. . . . . 6 ⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)))
3	2	elrab 3644	. . . . 5 ⊢ (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ↔ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)))
4		simprr 785	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))
5		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑧𝜑
6		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑧 𝑥 ∈ ℂ
7		nfre1 3287	. . . . . . . . 9 ⊢ Ⅎ𝑧∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)
8	6, 7	nfan 1932	. . . . . . . 8 ⊢ Ⅎ𝑧(𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))
9	5, 8	nfan 1932	. . . . . . 7 ⊢ Ⅎ𝑧(𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)))
10		nfv 1947	. . . . . . 7 ⊢ Ⅎ𝑧 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))
11		simp3 1156	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 = (𝑧 + 𝑇))
12		iccshift.1	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ ℝ)
13		iccshift.2	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ∈ ℝ)
14	12, 13	iccssred 13535	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
15	14	sselda 3930	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ∈ ℝ)
16		iccshift.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇 ∈ ℝ)
17	16	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ)
18	15, 17	readdcld 11310	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 + 𝑇) ∈ ℝ)
19	12	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
20		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ∈ (𝐴[,]𝐵))
21	13	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
22		elicc2 13512	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵)))
23	19, 21, 22	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵)))
24	20, 23	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))
25	24	simp2d 1161	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑧)
26	19, 15, 17, 25	leadd1dd 11900	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ≤ (𝑧 + 𝑇))
27	24	simp3d 1162	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ≤ 𝐵)
28	15, 21, 17, 27	leadd1dd 11900	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 + 𝑇) ≤ (𝐵 + 𝑇))
29	18, 26, 28	3jca 1146	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇)))
30	29	3adant3 1150	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇)))
31	12, 16	readdcld 11310	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 + 𝑇) ∈ ℝ)
32	31	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝐴 + 𝑇) ∈ ℝ)
33	13, 16	readdcld 11310	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 + 𝑇) ∈ ℝ)
34	33	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝐵 + 𝑇) ∈ ℝ)
35		elicc2 13512	. . . . . . . . . . . 12 ⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ) → ((𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇))))
36	32, 34, 35	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → ((𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇))))
37	30, 36	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
38	11, 37	eqeltrd 2860	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
39	38	3exp 1137	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) → (𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))))
40	39	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → (𝑧 ∈ (𝐴[,]𝐵) → (𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))))
41	9, 10, 40	rexlimd 3269	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → (∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))))
42	4, 41	mpd 16	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
43	3, 42	sylan2b 606	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
44	31	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ)
45	33	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ)
46		simpr 490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
47		eliccre 46439	. . . . . . 7 ⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
48	44, 45, 46, 47	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
49	48	recnd 11309	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℂ)
50	12	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ∈ ℝ)
51	13	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐵 ∈ ℝ)
52	16	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℝ)
53	48, 52	resubcld 11714	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ ℝ)
54	12	recnd 11309	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
55	16	recnd 11309	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℂ)
56	54, 55	pncand 11642	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
57	56	eqcomd 2766	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 = ((𝐴 + 𝑇) − 𝑇))
58	57	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇))
59		elicc2 13512	. . . . . . . . . . . 12 ⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇))))
60	44, 45, 59	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇))))
61	46, 60	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇)))
62	61	simp2d 1161	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥)
63	44, 48, 52, 62	lesub1dd 11902	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) ≤ (𝑥 − 𝑇))
64	58, 63	eqbrtrd 5126	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 − 𝑇))
65	61	simp3d 1162	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇))
66	48, 45, 52, 65	lesub1dd 11902	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ ((𝐵 + 𝑇) − 𝑇))
67	13	recnd 11309	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℂ)
68	67, 55	pncand 11642	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
69	68	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
70	66, 69	breqtrd 5130	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ 𝐵)
71	50, 51, 53, 64, 70	eliccd 46438	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ (𝐴[,]𝐵))
72	55	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℂ)
73	49, 72	npcand 11645	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 − 𝑇) + 𝑇) = 𝑥)
74	73	eqcomd 2766	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 = ((𝑥 − 𝑇) + 𝑇))
75		oveq1 7415	. . . . . . 7 ⊢ (𝑧 = (𝑥 − 𝑇) → (𝑧 + 𝑇) = ((𝑥 − 𝑇) + 𝑇))
76	75	rspceeqv 3598	. . . . . 6 ⊢ (((𝑥 − 𝑇) ∈ (𝐴[,]𝐵) ∧ 𝑥 = ((𝑥 − 𝑇) + 𝑇)) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))
77	71, 74, 76	syl2anc 596	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))
78	49, 77, 3	sylanbrc 595	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)})
79	43, 78	impbida 813	. . 3 ⊢ (𝜑 → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ↔ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))))
80	79	eqrdv 2758	. 2 ⊢ (𝜑 → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} = ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
81	80	eqcomd 2766	1 ⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)})

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∃wrex 3086 {crab 3412 class class class wbr 5102 (class class class)co 7408 ℂcc 11170 ℝcr 11171 + caddc 11175 ≤ cle 11316 − cmin 11513 [,]cicc 13449

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734 ax-cnex 11228 ax-resscn 11229 ax-1cn 11230 ax-icn 11231 ax-addcl 11232 ax-addrcl 11233 ax-mulcl 11234 ax-mulrcl 11235 ax-mulcom 11236 ax-addass 11237 ax-mulass 11238 ax-distr 11239 ax-i2m1 11240 ax-1ne0 11241 ax-1rid 11242 ax-rnegex 11243 ax-rrecex 11244 ax-cnre 11245 ax-pre-lttri 11246 ax-pre-lttrn 11247 ax-pre-ltadd 11248

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5542 df-po 5555 df-so 5556 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-er 8695 df-en 8952 df-dom 8953 df-sdom 8954 df-pnf 11317 df-mnf 11318 df-xr 11319 df-ltxr 11320 df-le 11321 df-sub 11515 df-neg 11516 df-icc 13453

This theorem is used by: itgiccshift 46912 itgperiod 46913

W3C validator