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 45800

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 2741	. . . . . . 7 ⊢ (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇)))
2	1	rexbidv 3161	. . . . . 6 ⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)))
3	2	elrab 3647	. . . . 5 ⊢ (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ↔ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)))
4		simprr 773	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))
5		nfv 1916	. . . . . . . 8 ⊢ Ⅎ𝑧𝜑
6		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑧 𝑥 ∈ ℂ
7		nfre1 3262	. . . . . . . . 9 ⊢ Ⅎ𝑧∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)
8	6, 7	nfan 1901	. . . . . . . 8 ⊢ Ⅎ𝑧(𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))
9	5, 8	nfan 1901	. . . . . . 7 ⊢ Ⅎ𝑧(𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)))
10		nfv 1916	. . . . . . 7 ⊢ Ⅎ𝑧 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))
11		simp3 1139	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 = (𝑧 + 𝑇))
12		iccshift.1	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ ℝ)
13		iccshift.2	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ∈ ℝ)
14	12, 13	iccssred 13354	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
15	14	sselda 3934	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ∈ ℝ)
16		iccshift.3	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇 ∈ ℝ)
17	16	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ)
18	15, 17	readdcld 11165	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 + 𝑇) ∈ ℝ)
19	12	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
20		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ∈ (𝐴[,]𝐵))
21	13	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
22		elicc2 13331	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵)))
23	19, 21, 22	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵)))
24	20, 23	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵))
25	24	simp2d 1144	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑧)
26	19, 15, 17, 25	leadd1dd 11755	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ≤ (𝑧 + 𝑇))
27	24	simp3d 1145	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → 𝑧 ≤ 𝐵)
28	15, 21, 17, 27	leadd1dd 11755	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑧 + 𝑇) ≤ (𝐵 + 𝑇))
29	18, 26, 28	3jca 1129	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇)))
30	29	3adant3 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇)))
31	12, 16	readdcld 11165	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 + 𝑇) ∈ ℝ)
32	31	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝐴 + 𝑇) ∈ ℝ)
33	13, 16	readdcld 11165	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 + 𝑇) ∈ ℝ)
34	33	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝐵 + 𝑇) ∈ ℝ)
35		elicc2 13331	. . . . . . . . . . . 12 ⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ) → ((𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇))))
36	32, 34, 35	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → ((𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ ((𝑧 + 𝑇) ∈ ℝ ∧ (𝐴 + 𝑇) ≤ (𝑧 + 𝑇) ∧ (𝑧 + 𝑇) ≤ (𝐵 + 𝑇))))
37	30, 36	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝑧 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
38	11, 37	eqeltrd 2837	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
39	38	3exp 1120	. . . . . . . 8 ⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) → (𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))))
40	39	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → (𝑧 ∈ (𝐴[,]𝐵) → (𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))))
41	9, 10, 40	rexlimd 3244	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → (∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))))
42	4, 41	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
43	3, 42	sylan2b 595	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
44	31	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ)
45	33	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ)
46		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
47		eliccre 45787	. . . . . . 7 ⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
48	44, 45, 46, 47	syl3anc 1374	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
49	48	recnd 11164	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℂ)
50	12	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ∈ ℝ)
51	13	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐵 ∈ ℝ)
52	16	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℝ)
53	48, 52	resubcld 11569	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ ℝ)
54	12	recnd 11164	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
55	16	recnd 11164	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℂ)
56	54, 55	pncand 11497	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
57	56	eqcomd 2743	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 = ((𝐴 + 𝑇) − 𝑇))
58	57	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇))
59		elicc2 13331	. . . . . . . . . . . 12 ⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇))))
60	44, 45, 59	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇))))
61	46, 60	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇)))
62	61	simp2d 1144	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥)
63	44, 48, 52, 62	lesub1dd 11757	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) ≤ (𝑥 − 𝑇))
64	58, 63	eqbrtrd 5121	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 − 𝑇))
65	61	simp3d 1145	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇))
66	48, 45, 52, 65	lesub1dd 11757	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ ((𝐵 + 𝑇) − 𝑇))
67	13	recnd 11164	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℂ)
68	67, 55	pncand 11497	. . . . . . . . 9 ⊢ (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
69	68	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
70	66, 69	breqtrd 5125	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ 𝐵)
71	50, 51, 53, 64, 70	eliccd 45786	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ (𝐴[,]𝐵))
72	55	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℂ)
73	49, 72	npcand 11500	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 − 𝑇) + 𝑇) = 𝑥)
74	73	eqcomd 2743	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 = ((𝑥 − 𝑇) + 𝑇))
75		oveq1 7367	. . . . . . 7 ⊢ (𝑧 = (𝑥 − 𝑇) → (𝑧 + 𝑇) = ((𝑥 − 𝑇) + 𝑇))
76	75	rspceeqv 3600	. . . . . 6 ⊢ (((𝑥 − 𝑇) ∈ (𝐴[,]𝐵) ∧ 𝑥 = ((𝑥 − 𝑇) + 𝑇)) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))
77	71, 74, 76	syl2anc 585	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇))
78	49, 77, 3	sylanbrc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)})
79	43, 78	impbida 801	. . 3 ⊢ (𝜑 → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} ↔ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))))
80	79	eqrdv 2735	. 2 ⊢ (𝜑 → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} = ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
81	80	eqcomd 2743	1 ⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∃wrex 3061 {crab 3400 class class class wbr 5099 (class class class)co 7360 ℂcc 11028 ℝcr 11029 + caddc 11033 ≤ cle 11171 − cmin 11368 [,]cicc 13268

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7682 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-br 5100 df-opab 5162 df-mpt 5181 df-id 5520 df-po 5533 df-so 5534 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-icc 13272

This theorem is referenced by: itgiccshift 46260 itgperiod 46261

W3C validator