itgiccshift - Mathbox for Glauco Siliprandi

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

Theorem itgiccshift 46912

Description: The integral of a function, 𝐹 stays the same if its closed interval domain is shifted by 𝑇. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
itgiccshift.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
itgiccshift.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
itgiccshift.aleb	⊢ (𝜑 → 𝐴 ≤ 𝐵)
itgiccshift.f	⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
itgiccshift.t	⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
itgiccshift.g	⊢ 𝐺 = (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑥 − 𝑇)))

**Assertion**
Ref	Expression
itgiccshift	⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐺‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 𝑥,𝐹 𝑥,𝐺 𝑥,𝑇 𝜑,𝑥

Proof of Theorem itgiccshift Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		itgiccshift.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		itgiccshift.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		itgiccshift.t	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
4	3	rpred 13133	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ℝ)
5		itgiccshift.aleb	. . . . 5 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
6	1, 2, 4, 5	leadd1dd 11899	. . . 4 ⊢ (𝜑 → (𝐴 + 𝑇) ≤ (𝐵 + 𝑇))
7	6	ditgpos 26137	. . 3 ⊢ (𝜑 → ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐺‘𝑥) d𝑥 = ∫((𝐴 + 𝑇)(,)(𝐵 + 𝑇))(𝐺‘𝑥) d𝑥)
8	1, 4	readdcld 11309	. . . 4 ⊢ (𝜑 → (𝐴 + 𝑇) ∈ ℝ)
9	2, 4	readdcld 11309	. . . 4 ⊢ (𝜑 → (𝐵 + 𝑇) ∈ ℝ)
10		itgiccshift.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
11		cncff 25175	. . . . . . . . 9 ⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
12	10, 11	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ)
13	12	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
14	1	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ∈ ℝ)
15	2	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐵 ∈ ℝ)
16	8	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ)
17	9	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ)
18		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
19		eliccre 46439	. . . . . . . . . 10 ⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
20	16, 17, 18, 19	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
21	4	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℝ)
22	20, 21	resubcld 11713	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ ℝ)
23	1	recnd 11308	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℂ)
24	4	recnd 11308	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℂ)
25	23, 24	pncand 11641	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
26	25	eqcomd 2766	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 = ((𝐴 + 𝑇) − 𝑇))
27	26	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇))
28		elicc2 13511	. . . . . . . . . . . . 13 ⊢ (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇))))
29	16, 17, 28	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇))))
30	18, 29	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 ∈ ℝ ∧ (𝐴 + 𝑇) ≤ 𝑥 ∧ 𝑥 ≤ (𝐵 + 𝑇)))
31	30	simp2d 1161	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥)
32	16, 20, 21, 31	lesub1dd 11901	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) ≤ (𝑥 − 𝑇))
33	27, 32	eqbrtrd 5126	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 − 𝑇))
34	30	simp3d 1162	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇))
35	20, 17, 21, 34	lesub1dd 11901	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ ((𝐵 + 𝑇) − 𝑇))
36	2	recnd 11308	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
37	36, 24	pncand 11641	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
38	37	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
39	35, 38	breqtrd 5130	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ≤ 𝐵)
40	14, 15, 22, 33, 39	eliccd 46438	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 − 𝑇) ∈ (𝐴[,]𝐵))
41	13, 40	ffvelcdmd 7073	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 − 𝑇)) ∈ ℂ)
42		itgiccshift.g	. . . . . 6 ⊢ 𝐺 = (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑥 − 𝑇)))
43	41, 42	fmptd 7102	. . . . 5 ⊢ (𝜑 → 𝐺:((𝐴 + 𝑇)[,](𝐵 + 𝑇))⟶ℂ)
44	43	ffvelcdmda 7072	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐺‘𝑥) ∈ ℂ)
45	8, 9, 44	itgioo 26097	. . 3 ⊢ (𝜑 → ∫((𝐴 + 𝑇)(,)(𝐵 + 𝑇))(𝐺‘𝑥) d𝑥 = ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐺‘𝑥) d𝑥)
46	7, 45	eqtr2d 2796	. 2 ⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐺‘𝑥) d𝑥 = ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐺‘𝑥) d𝑥)
47		eqid 2760	. . . 4 ⊢ (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) = (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇))
48	47	addccncf 25199	. . . . 5 ⊢ (𝑇 ∈ ℂ → (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) ∈ (ℂ–cn→ℂ))
49	24, 48	syl 18	. . . 4 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦 + 𝑇)) ∈ (ℂ–cn→ℂ))
50	1, 2	iccssred 13534	. . . . 5 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
51		ax-resscn 11228	. . . . 5 ⊢ ℝ ⊆ ℂ
52	50, 51	sstrdi 3942	. . . 4 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
53	8, 9	iccssred 13534	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ⊆ ℝ)
54	53, 51	sstrdi 3942	. . . 4 ⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ⊆ ℂ)
55	8	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ∈ ℝ)
56	9	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐵 + 𝑇) ∈ ℝ)
57	50	sselda 3930	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ)
58	4	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ)
59	57, 58	readdcld 11309	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ∈ ℝ)
60	1	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
61		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ (𝐴[,]𝐵))
62	2	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
63		elicc2 13511	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)))
64	60, 62, 63	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵)))
65	61, 64	mpbid 235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵))
66	65	simp2d 1161	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑦)
67	60, 57, 58, 66	leadd1dd 11899	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ≤ (𝑦 + 𝑇))
68	65	simp3d 1162	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑦 ≤ 𝐵)
69	57, 62, 58, 68	leadd1dd 11899	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ≤ (𝐵 + 𝑇))
70	55, 56, 59, 67, 69	eliccd 46438	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑦 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
71	47, 49, 52, 54, 70	cncfmptssg 46803	. . 3 ⊢ (𝜑 → (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇)) ∈ ((𝐴[,]𝐵)–cn→((𝐴 + 𝑇)[,](𝐵 + 𝑇))))
72		fvoveq1 7431	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝐹‘(𝑥 − 𝑇)) = (𝐹‘(𝑤 − 𝑇)))
73	72	cbvmptv 5208	. . . . . . 7 ⊢ (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑥 − 𝑇))) = (𝑤 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑤 − 𝑇)))
74	1, 2, 4	iccshift 46452	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)})
75	74	mpteq1d 5194	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑤 − 𝑇))) = (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇))))
76	73, 75	eqtrid 2807	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑥 − 𝑇))) = (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇))))
77	42, 76	eqtrid 2807	. . . . 5 ⊢ (𝜑 → 𝐺 = (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇))))
78		eqeq1 2764	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇)))
79	78	rexbidv 3186	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇)))
80		oveq1 7415	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → (𝑧 + 𝑇) = (𝑦 + 𝑇))
81	80	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑦 + 𝑇)))
82	81	cbvrexvw 3241	. . . . . . . . 9 ⊢ (∃𝑧 ∈ (𝐴[,]𝐵)𝑥 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇))
83	79, 82	bitrdi 290	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)))
84	83	cbvrabv 3422	. . . . . . 7 ⊢ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)}
85	84	eqcomi 2769	. . . . . 6 ⊢ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ (𝐴[,]𝐵)𝑤 = (𝑧 + 𝑇)}
86		eqid 2760	. . . . . 6 ⊢ (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇))) = (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇)))
87	52, 24, 85, 10, 86	cncfshift 46806	. . . . 5 ⊢ (𝜑 → (𝑤 ∈ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} ↦ (𝐹‘(𝑤 − 𝑇))) ∈ ({𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)}–cn→ℂ))
88	77, 87	eqeltrd 2860	. . . 4 ⊢ (𝜑 → 𝐺 ∈ ({𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)}–cn→ℂ))
89	43	feqmptd 6941	. . . 4 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐺‘𝑥)))
90	74	eqcomd 2766	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)} = ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
91	90	oveq1d 7423	. . . 4 ⊢ (𝜑 → ({𝑥 ∈ ℂ ∣ ∃𝑦 ∈ (𝐴[,]𝐵)𝑥 = (𝑦 + 𝑇)}–cn→ℂ) = (((𝐴 + 𝑇)[,](𝐵 + 𝑇))–cn→ℂ))
92	88, 89, 91	3eltr3d 2874	. . 3 ⊢ (𝜑 → (𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐺‘𝑥)) ∈ (((𝐴 + 𝑇)[,](𝐵 + 𝑇))–cn→ℂ))
93		ioosscn 13508	. . . . . 6 ⊢ (𝐴(,)𝐵) ⊆ ℂ
94	93	a1i 11	. . . . 5 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℂ)
95		1cnd 11273	. . . . 5 ⊢ (𝜑 → 1 ∈ ℂ)
96		ssid 3952	. . . . . 6 ⊢ ℂ ⊆ ℂ
97	96	a1i 11	. . . . 5 ⊢ (𝜑 → ℂ ⊆ ℂ)
98	94, 95, 97	constcncfg 46804	. . . 4 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈ ((𝐴(,)𝐵)–cn→ℂ))
99		fconstmpt 5709	. . . . 5 ⊢ ((𝐴(,)𝐵) × {1}) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)
100		ioombl 25847	. . . . . . 7 ⊢ (𝐴(,)𝐵) ∈ dom vol
101	100	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol)
102		ioovolcl 25852	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
103	1, 2, 102	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
104		iblconst 26099	. . . . . 6 ⊢ (((𝐴(,)𝐵) ∈ dom vol ∧ (vol‘(𝐴(,)𝐵)) ∈ ℝ ∧ 1 ∈ ℂ) → ((𝐴(,)𝐵) × {1}) ∈ 𝐿¹)
105	101, 103, 95, 104	syl3anc 1398	. . . . 5 ⊢ (𝜑 → ((𝐴(,)𝐵) × {1}) ∈ 𝐿¹)
106	99, 105	eqeltrrid 2865	. . . 4 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈ 𝐿¹)
107	98, 106	elind 4145	. . 3 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ 1) ∈ (((𝐴(,)𝐵)–cn→ℂ) ∩ 𝐿¹))
108	50	resmptd 6030	. . . . . . 7 ⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵)) = (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇)))
109	108	eqcomd 2766	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇)) = ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵)))
110	109	oveq2d 7424	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = (ℝ D ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))))
111	51	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℂ)
112	111	sselda 3930	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
113	24	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑇 ∈ ℂ)
114	112, 113	addcld 11299	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + 𝑇) ∈ ℂ)
115	114	fmpttd 7103	. . . . . 6 ⊢ (𝜑 → (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)):ℝ⟶ℂ)
116		ssid 3952	. . . . . . 7 ⊢ ℝ ⊆ ℝ
117	116	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℝ)
118		eqid 2760	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
119		tgioo4 25085	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
120	118, 119	dvres 26192	. . . . . 6 ⊢ (((ℝ ⊆ ℂ ∧ (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)):ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ (𝐴[,]𝐵) ⊆ ℝ)) → (ℝ D ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
121	111, 115, 117, 50, 120	syl22anc 852	. . . . 5 ⊢ (𝜑 → (ℝ D ((𝑦 ∈ ℝ ↦ (𝑦 + 𝑇)) ↾ (𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
122	110, 121	eqtrd 2795	. . . 4 ⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
123		iccntr 25102	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
124	1, 2, 123	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
125	124	reseq2d 5966	. . . 4 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) = ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵)))
126		reelprrecn 11263	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
127	126	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
128		1cnd 11273	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 1 ∈ ℂ)
129	127	dvmptid 26238	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
130		0cnd 11270	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 0 ∈ ℂ)
131	127, 24	dvmptc 26239	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ 𝑇)) = (𝑦 ∈ ℝ ↦ 0))
132	127, 112, 128, 129, 113, 130, 131	dvmptadd 26241	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) = (𝑦 ∈ ℝ ↦ (1 + 0)))
133	132	reseq1d 5965	. . . . 5 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵)) = ((𝑦 ∈ ℝ ↦ (1 + 0)) ↾ (𝐴(,)𝐵)))
134		ioossre 13507	. . . . . . 7 ⊢ (𝐴(,)𝐵) ⊆ ℝ
135	134	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
136	135	resmptd 6030	. . . . 5 ⊢ (𝜑 → ((𝑦 ∈ ℝ ↦ (1 + 0)) ↾ (𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0)))
137		1p0e1 12434	. . . . . . 7 ⊢ (1 + 0) = 1
138	137	mpteq2i 5200	. . . . . 6 ⊢ (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1)
139	138	a1i 11	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ (𝐴(,)𝐵) ↦ (1 + 0)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1))
140	133, 136, 139	3eqtrd 2799	. . . 4 ⊢ (𝜑 → ((ℝ D (𝑦 ∈ ℝ ↦ (𝑦 + 𝑇))) ↾ (𝐴(,)𝐵)) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1))
141	122, 125, 140	3eqtrd 2799	. . 3 ⊢ (𝜑 → (ℝ D (𝑦 ∈ (𝐴[,]𝐵) ↦ (𝑦 + 𝑇))) = (𝑦 ∈ (𝐴(,)𝐵) ↦ 1))
142		fveq2 6873	. . 3 ⊢ (𝑥 = (𝑦 + 𝑇) → (𝐺‘𝑥) = (𝐺‘(𝑦 + 𝑇)))
143		oveq1 7415	. . 3 ⊢ (𝑦 = 𝐴 → (𝑦 + 𝑇) = (𝐴 + 𝑇))
144		oveq1 7415	. . 3 ⊢ (𝑦 = 𝐵 → (𝑦 + 𝑇) = (𝐵 + 𝑇))
145	1, 2, 5, 71, 92, 107, 141, 142, 143, 144, 8, 9	itgsubsticc 46908	. 2 ⊢ (𝜑 → ⨜[(𝐴 + 𝑇) → (𝐵 + 𝑇)](𝐺‘𝑥) d𝑥 = ⨜[𝐴 → 𝐵]((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦)
146	5	ditgpos 26137	. . 3 ⊢ (𝜑 → ⨜[𝐴 → 𝐵]((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴(,)𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦)
147	43	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐺:((𝐴 + 𝑇)[,](𝐵 + 𝑇))⟶ℂ)
148	147, 70	ffvelcdmd 7073	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐺‘(𝑦 + 𝑇)) ∈ ℂ)
149		1cnd 11273	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 1 ∈ ℂ)
150	148, 149	mulcld 11300	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐺‘(𝑦 + 𝑇)) · 1) ∈ ℂ)
151	1, 2, 150	itgioo 26097	. . 3 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦)
152		fvoveq1 7431	. . . . . 6 ⊢ (𝑦 = 𝑥 → (𝐺‘(𝑦 + 𝑇)) = (𝐺‘(𝑥 + 𝑇)))
153	152	oveq1d 7423	. . . . 5 ⊢ (𝑦 = 𝑥 → ((𝐺‘(𝑦 + 𝑇)) · 1) = ((𝐺‘(𝑥 + 𝑇)) · 1))
154	153	cbvitgv 26058	. . . 4 ⊢ ∫(𝐴[,]𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)((𝐺‘(𝑥 + 𝑇)) · 1) d𝑥
155	43	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐺:((𝐴 + 𝑇)[,](𝐵 + 𝑇))⟶ℂ)
156	8	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ∈ ℝ)
157	9	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐵 + 𝑇) ∈ ℝ)
158	50	sselda 3930	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
159	4	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℝ)
160	158, 159	readdcld 11309	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 + 𝑇) ∈ ℝ)
161	1	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
162	1	rexrd 11330	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
163	162	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ^*)
164	2	rexrd 11330	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
165	164	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ^*)
166		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ (𝐴[,]𝐵))
167		iccgelb 13502	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥)
168	163, 165, 166, 167	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥)
169	161, 158, 159, 168	leadd1dd 11899	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴 + 𝑇) ≤ (𝑥 + 𝑇))
170	2	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ)
171		iccleub 13501	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
172	163, 165, 166, 171	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
173	158, 170, 159, 172	leadd1dd 11899	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 + 𝑇) ≤ (𝐵 + 𝑇))
174	156, 157, 160, 169, 173	eliccd 46438	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 + 𝑇) ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
175	155, 174	ffvelcdmd 7073	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐺‘(𝑥 + 𝑇)) ∈ ℂ)
176	175	mulridd 11297	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝐺‘(𝑥 + 𝑇)) · 1) = (𝐺‘(𝑥 + 𝑇)))
177	42, 73	eqtri 2783	. . . . . . . 8 ⊢ 𝐺 = (𝑤 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑤 − 𝑇)))
178	177	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐺 = (𝑤 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) ↦ (𝐹‘(𝑤 − 𝑇))))
179		fvoveq1 7431	. . . . . . . 8 ⊢ (𝑤 = (𝑥 + 𝑇) → (𝐹‘(𝑤 − 𝑇)) = (𝐹‘((𝑥 + 𝑇) − 𝑇)))
180	158	recnd 11308	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℂ)
181	24	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑇 ∈ ℂ)
182	180, 181	pncand 11641	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥 + 𝑇) − 𝑇) = 𝑥)
183	182	fveq2d 6877	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + 𝑇) − 𝑇)) = (𝐹‘𝑥))
184	179, 183	sylan9eqr 2817	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑤 = (𝑥 + 𝑇)) → (𝐹‘(𝑤 − 𝑇)) = (𝐹‘𝑥))
185	12	ffvelcdmda 7072	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ)
186	178, 184, 174, 185	fvmptd 6989	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐺‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
187	176, 186	eqtrd 2795	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝐺‘(𝑥 + 𝑇)) · 1) = (𝐹‘𝑥))
188	187	itgeq2dv 26063	. . . 4 ⊢ (𝜑 → ∫(𝐴[,]𝐵)((𝐺‘(𝑥 + 𝑇)) · 1) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
189	154, 188	eqtrid 2807	. . 3 ⊢ (𝜑 → ∫(𝐴[,]𝐵)((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
190	146, 151, 189	3eqtrd 2799	. 2 ⊢ (𝜑 → ⨜[𝐴 → 𝐵]((𝐺‘(𝑦 + 𝑇)) · 1) d𝑦 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
191	46, 145, 190	3eqtrd 2799	1 ⊢ (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐺‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)

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 ⊆ wss 3898 {csn 4583 {cpr 4585 class class class wbr 5102 ↦ cmpt 5185 × cxp 5645 dom cdm 5647 ran crn 5648 ↾ cres 5649 ⟶wf 6523 ‘cfv 6527 (class class class)co 7408 ℂcc 11169 ℝcr 11170 0cc0 11171 1c1 11172 + caddc 11174 · cmul 11176 ℝ^*cxr 11313 ≤ cle 11315 − cmin 11512 ℝ⁺crp 13089 (,)cioo 13445 [,]cicc 13448 TopOpenctopn 17553 topGenctg 17569 ℂ_fldccnfld 21639 intcnt 23296 –cn→ccncf 25158 volcvol 25745 𝐿¹cibl 25899 ∫citg 25900 ⨜cdit 26127 D cdv 26144

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-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734 ax-inf2 9620 ax-cc 10484 ax-cnex 11227 ax-resscn 11228 ax-1cn 11229 ax-icn 11230 ax-addcl 11231 ax-addrcl 11232 ax-mulcl 11233 ax-mulrcl 11234 ax-mulcom 11235 ax-addass 11236 ax-mulass 11237 ax-distr 11238 ax-i2m1 11239 ax-1ne0 11240 ax-1rid 11241 ax-rnegex 11242 ax-rrecex 11243 ax-cnre 11244 ax-pre-lttri 11245 ax-pre-lttrn 11246 ax-pre-ltadd 11247 ax-pre-mulgt0 11248 ax-pre-sup 11249 ax-addf 11250

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-rmo 3365 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-pss 3918 df-symdif 4198 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-disj 5070 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 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-pred 6293 df-ord 6354 df-on 6355 df-lim 6356 df-suc 6357 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-isom 6536 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-of 7676 df-ofr 7677 df-om 7861 df-1st 7984 df-2nd 7985 df-supp 8156 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8454 df-2o 8455 df-oadd 8458 df-omul 8459 df-er 8695 df-map 8827 df-pm 8828 df-ixp 8904 df-en 8952 df-dom 8953 df-sdom 8954 df-fin 8955 df-fsupp 9332 df-fi 9381 df-sup 9412 df-inf 9413 df-oi 9482 df-dju 9953 df-card 9991 df-acn 9994 df-pnf 11316 df-mnf 11317 df-xr 11318 df-ltxr 11319 df-le 11320 df-sub 11514 df-neg 11515 df-div 11943 df-nn 12305 df-2 12374 df-3 12375 df-4 12376 df-5 12377 df-6 12378 df-7 12379 df-8 12380 df-9 12381 df-n0 12576 df-z 12663 df-dec 12784 df-uz 12935 df-q 13045 df-rp 13090 df-xneg 13210 df-xadd 13211 df-xmul 13212 df-ioo 13449 df-ioc 13450 df-ico 13451 df-icc 13452 df-fz 13609 df-fzo 13757 df-fl 13900 df-mod 13978 df-seq 14113 df-exp 14173 df-hash 14442 df-cj 15233 df-re 15234 df-im 15235 df-sqrt 15369 df-abs 15370 df-limsup 15605 df-clim 15622 df-rlim 15623 df-sum 15821 df-struct 17286 df-sets 17303 df-slot 17321 df-ndx 17333 df-base 17349 df-ress 17370 df-plusg 17402 df-mulr 17403 df-starv 17404 df-sca 17405 df-vsca 17406 df-ip 17407 df-tset 17408 df-ple 17409 df-ds 17411 df-unif 17412 df-hom 17413 df-cco 17414 df-rest 17554 df-topn 17555 df-0g 17573 df-gsum 17574 df-topgen 17575 df-pt 17576 df-prds 17579 df-xrs 17635 df-qtop 17640 df-imas 17641 df-xps 17643 df-mre 17717 df-mrc 17718 df-acs 17720 df-mgm 18777 df-sgrp 18869 df-mnd 18885 df-submnd 18940 df-mulg 19239 df-cntz 19492 df-cmn 19957 df-psmet 21631 df-xmet 21632 df-met 21633 df-bl 21634 df-mopn 21635 df-fbas 21636 df-fg 21637 df-cnfld 21640 df-top 23173 df-topon 23190 df-topsp 23212 df-bases 23225 df-cld 23298 df-ntr 23299 df-cls 23300 df-nei 23377 df-lp 23415 df-perf 23416 df-cn 23506 df-cnp 23507 df-haus 23594 df-cmp 23666 df-tx 23842 df-hmeo 24035 df-fil 24126 df-fm 24218 df-flim 24219 df-flf 24220 df-xms 24600 df-ms 24601 df-tms 24602 df-cncf 25160 df-ovol 25746 df-vol 25747 df-mbf 25901 df-itg1 25902 df-itg2 25903 df-ibl 25904 df-itg 25905 df-0p 25952 df-ditg 26128 df-limc 26147 df-dv 26148

This theorem is used by: fourierdlem81 47119

W3C validator