fourierdlem4 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem4 46112

Description: 𝐸 is a function that maps any point to a periodic corresponding point in (𝐴, 𝐵]. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem4.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
fourierdlem4.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
fourierdlem4.altb	⊢ (𝜑 → 𝐴 < 𝐵)
fourierdlem4.t	⊢ 𝑇 = (𝐵 − 𝐴)
fourierdlem4.e	⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))

**Assertion**
Ref	Expression
fourierdlem4	⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 𝑥,𝑇 𝜑,𝑥 Allowed substitution hint: 𝐸(𝑥)

**Proof of Theorem fourierdlem4**
Step	Hyp	Ref	Expression
1		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
2		fourierdlem4.b	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3	2	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
4	3, 1	resubcld 11567	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℝ)
5		fourierdlem4.t	. . . . . . . . . 10 ⊢ 𝑇 = (𝐵 − 𝐴)
6		fourierdlem4.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
7	2, 6	resubcld 11567	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
8	5, 7	eqeltrid 2832	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ℝ)
9	8	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
10	5	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 = (𝐵 − 𝐴))
11	2	recnd 11162	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
12	6	recnd 11162	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
13		fourierdlem4.altb	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
14	6, 13	gtned 11270	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
15	11, 12, 14	subne0d 11503	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0)
16	10, 15	eqnetrd 2992	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ≠ 0)
17	16	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ≠ 0)
18	4, 9, 17	redivcld 11971	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ)
19	18	flcld 13721	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
20	19	zred 12599	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
21	20, 9	remulcld 11164	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
22	1, 21	readdcld 11163	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ)
23	6	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
24	23, 1	resubcld 11567	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴 − 𝑥) ∈ ℝ)
25	24, 9, 17	redivcld 11971	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) ∈ ℝ)
26	25, 9	remulcld 11164	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) ∈ ℝ)
27	11	addridd 11335	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 + 0) = 𝐵)
28	27	eqcomd 2735	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 = (𝐵 + 0))
29	11, 12	subcld 11494	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ)
30	29	subidd 11482	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 − 𝐴) − (𝐵 − 𝐴)) = 0)
31	30	eqcomd 2735	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 = ((𝐵 − 𝐴) − (𝐵 − 𝐴)))
32	31	oveq2d 7369	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 + 0) = (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴))))
33	11, 29, 29	addsub12d 11517	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴))) = ((𝐵 − 𝐴) + (𝐵 − (𝐵 − 𝐴))))
34	11, 12	nncand 11499	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − (𝐵 − 𝐴)) = 𝐴)
35	34	oveq2d 7369	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 − 𝐴) + (𝐵 − (𝐵 − 𝐴))) = ((𝐵 − 𝐴) + 𝐴))
36	29, 12	addcomd 11337	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝐴 + (𝐵 − 𝐴)))
37	10	eqcomd 2735	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
38	37	oveq2d 7369	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = (𝐴 + 𝑇))
39	36, 38	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝐴 + 𝑇))
40	33, 35, 39	3eqtrd 2768	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴))) = (𝐴 + 𝑇))
41	28, 32, 40	3eqtrd 2768	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 = (𝐴 + 𝑇))
42	41	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 = (𝐴 + 𝑇))
43	42	oveq1d 7368	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) = ((𝐴 + 𝑇) − 𝑥))
44	12	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℂ)
45	9	recnd 11162	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
46	1	recnd 11162	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
47	44, 45, 46	addsubd 11515	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 + 𝑇) − 𝑥) = ((𝐴 − 𝑥) + 𝑇))
48	43, 47	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) = ((𝐴 − 𝑥) + 𝑇))
49	48	oveq1d 7368	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) = (((𝐴 − 𝑥) + 𝑇) / 𝑇))
50	44, 46	subcld 11494	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴 − 𝑥) ∈ ℂ)
51	50, 45, 45, 17	divdird 11957	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) + 𝑇) / 𝑇) = (((𝐴 − 𝑥) / 𝑇) + (𝑇 / 𝑇)))
52	5, 29	eqeltrid 2832	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℂ)
53	52, 16	dividd 11917	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 / 𝑇) = 1)
54	53	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑇 / 𝑇) = 1)
55	54	oveq2d 7369	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) + (𝑇 / 𝑇)) = (((𝐴 − 𝑥) / 𝑇) + 1))
56	49, 51, 55	3eqtrd 2768	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) = (((𝐴 − 𝑥) / 𝑇) + 1))
57	56	fveq2d 6830	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)))
58	57	oveq1d 7368	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇))
59	58, 21	eqeltrrd 2829	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇) ∈ ℝ)
60		peano2re 11308	. . . . . . . 8 ⊢ (((𝐴 − 𝑥) / 𝑇) ∈ ℝ → (((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ)
61	25, 60	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ)
62		reflcl 13719	. . . . . . 7 ⊢ ((((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ → (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) ∈ ℝ)
63	61, 62	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) ∈ ℝ)
64	6, 2	posdifd 11726	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
65	13, 64	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
66	65, 10	breqtrrd 5123	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑇)
67	8, 66	elrpd 12953	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
68	67	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ⁺)
69		flltp1 13723	. . . . . . . 8 ⊢ (((𝐴 − 𝑥) / 𝑇) ∈ ℝ → ((𝐴 − 𝑥) / 𝑇) < ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1))
70	25, 69	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) < ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1))
71		1zzd 12525	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℤ)
72		fladdz 13748	. . . . . . . 8 ⊢ ((((𝐴 − 𝑥) / 𝑇) ∈ ℝ ∧ 1 ∈ ℤ) → (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) = ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1))
73	25, 71, 72	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) = ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1))
74	70, 73	breqtrrd 5123	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) < (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)))
75	25, 63, 68, 74	ltmul1dd 13011	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) < ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇))
76	26, 59, 1, 75	ltadd2dd 11294	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) < (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)))
77	50, 45, 17	divcan1d 11920	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) = (𝐴 − 𝑥))
78	77	oveq2d 7369	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) = (𝑥 + (𝐴 − 𝑥)))
79	46, 44	pncan3d 11497	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝐴 − 𝑥)) = 𝐴)
80	78, 79	eqtrd 2764	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) = 𝐴)
81	58	oveq2d 7369	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)))
82	81	eqcomd 2735	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
83	76, 80, 82	3brtr3d 5126	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
84	18, 9	remulcld 11164	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐵 − 𝑥) / 𝑇) · 𝑇) ∈ ℝ)
85		flle 13722	. . . . . . 7 ⊢ (((𝐵 − 𝑥) / 𝑇) ∈ ℝ → (⌊‘((𝐵 − 𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇))
86	18, 85	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇))
87	20, 18, 68	lemul1d 12999	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇) ↔ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ≤ (((𝐵 − 𝑥) / 𝑇) · 𝑇)))
88	86, 87	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ≤ (((𝐵 − 𝑥) / 𝑇) · 𝑇))
89	21, 84, 1, 88	leadd2dd 11754	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇)))
90	4	recnd 11162	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℂ)
91	90, 45, 17	divcan1d 11920	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐵 − 𝑥) / 𝑇) · 𝑇) = (𝐵 − 𝑥))
92	91	oveq2d 7369	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇)) = (𝑥 + (𝐵 − 𝑥)))
93	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℂ)
94	46, 93	pncan3d 11497	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝐵 − 𝑥)) = 𝐵)
95	92, 94	eqtrd 2764	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇)) = 𝐵)
96	89, 95	breqtrd 5121	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵)
97	23	rexrd 11184	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ^*)
98		elioc2 13331	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ ∧ 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵)))
99	97, 3, 98	syl2anc 584	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ ∧ 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵)))
100	22, 83, 96, 99	mpbir3and 1343	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵))
101		fourierdlem4.e	. 2 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
102	100, 101	fmptd 7052	1 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 class class class wbr 5095 ↦ cmpt 5176 ⟶wf 6482 ‘cfv 6486 (class class class)co 7353 ℂcc 11026 ℝcr 11027 0cc0 11028 1c1 11029 + caddc 11031 · cmul 11033 ℝ^*cxr 11167 < clt 11168 ≤ cle 11169 − cmin 11366 / cdiv 11796 ℤcz 12490 ℝ⁺crp 12912 (,]cioc 13268 ⌊cfl 13713

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-om 7807 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-er 8632 df-en 8880 df-dom 8881 df-sdom 8882 df-sup 9351 df-inf 9352 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12148 df-n0 12404 df-z 12491 df-uz 12755 df-rp 12913 df-ioc 13272 df-fl 13715

This theorem is referenced by: fourierdlem19 46127 fourierdlem37 46145 fourierdlem41 46149 fourierdlem48 46155 fourierdlem49 46156 fourierdlem51 46158 fourierdlem63 46170 fourierdlem65 46172 fourierdlem71 46178 fourierdlem79 46186 fourierdlem89 46196 fourierdlem90 46197 fourierdlem91 46198 fourierdlem102 46209 fourierdlem114 46221

W3C validator