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 47228

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 490	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
2		fourierdlem4.b	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3	2	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ)
4	3, 1	resubcld 11749	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℝ)
5		fourierdlem4.t	. . . . . . . . . 10 ⊢ 𝑇 = (𝐵 − 𝐴)
6		fourierdlem4.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
7	2, 6	resubcld 11749	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
8	5, 7	eqeltrid 2864	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ℝ)
9	8	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ)
10	5	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 = (𝐵 − 𝐴))
11	2	recnd 11342	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
12	6	recnd 11342	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
13		fourierdlem4.altb	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 < 𝐵)
14	6, 13	gtned 11450	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
15	11, 12, 14	subne0d 11684	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0)
16	10, 15	eqnetrd 3022	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ≠ 0)
17	16	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ≠ 0)
18	4, 9, 17	redivcld 12150	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ)
19	18	flcld 13943	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℤ)
20	19	zred 12808	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ∈ ℝ)
21	20, 9	remulcld 11344	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ∈ ℝ)
22	1, 21	readdcld 11343	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ)
23	6	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
24	23, 1	resubcld 11749	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴 − 𝑥) ∈ ℝ)
25	24, 9, 17	redivcld 12150	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) ∈ ℝ)
26	25, 9	remulcld 11344	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) ∈ ℝ)
27	11	addridd 11515	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 + 0) = 𝐵)
28	27	eqcomd 2766	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 = (𝐵 + 0))
29	11, 12	subcld 11674	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ)
30	29	subidd 11662	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 − 𝐴) − (𝐵 − 𝐴)) = 0)
31	30	eqcomd 2766	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 = ((𝐵 − 𝐴) − (𝐵 − 𝐴)))
32	31	oveq2d 7438	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 + 0) = (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴))))
33	11, 29, 29	addsub12d 11697	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴))) = ((𝐵 − 𝐴) + (𝐵 − (𝐵 − 𝐴))))
34	11, 12	nncand 11679	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 − (𝐵 − 𝐴)) = 𝐴)
35	34	oveq2d 7438	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 − 𝐴) + (𝐵 − (𝐵 − 𝐴))) = ((𝐵 − 𝐴) + 𝐴))
36	29, 12	addcomd 11517	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝐴 + (𝐵 − 𝐴)))
37	10	eqcomd 2766	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇)
38	37	oveq2d 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = (𝐴 + 𝑇))
39	36, 38	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝐴 + 𝑇))
40	33, 35, 39	3eqtrd 2799	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴))) = (𝐴 + 𝑇))
41	28, 32, 40	3eqtrd 2799	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 = (𝐴 + 𝑇))
42	41	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 = (𝐴 + 𝑇))
43	42	oveq1d 7437	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) = ((𝐴 + 𝑇) − 𝑥))
44	12	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℂ)
45	9	recnd 11342	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
46	1	recnd 11342	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
47	44, 45, 46	addsubd 11695	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 + 𝑇) − 𝑥) = ((𝐴 − 𝑥) + 𝑇))
48	43, 47	eqtrd 2795	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) = ((𝐴 − 𝑥) + 𝑇))
49	48	oveq1d 7437	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) = (((𝐴 − 𝑥) + 𝑇) / 𝑇))
50	44, 46	subcld 11674	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴 − 𝑥) ∈ ℂ)
51	50, 45, 45, 17	divdird 12136	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) + 𝑇) / 𝑇) = (((𝐴 − 𝑥) / 𝑇) + (𝑇 / 𝑇)))
52	5, 29	eqeltrid 2864	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℂ)
53	52, 16	dividd 12096	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 / 𝑇) = 1)
54	53	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑇 / 𝑇) = 1)
55	54	oveq2d 7438	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) + (𝑇 / 𝑇)) = (((𝐴 − 𝑥) / 𝑇) + 1))
56	49, 51, 55	3eqtrd 2799	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) = (((𝐴 − 𝑥) / 𝑇) + 1))
57	56	fveq2d 6892	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)))
58	57	oveq1d 7437	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇))
59	58, 21	eqeltrrd 2861	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇) ∈ ℝ)
60		peano2re 11488	. . . . . . . 8 ⊢ (((𝐴 − 𝑥) / 𝑇) ∈ ℝ → (((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ)
61	25, 60	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ)
62		reflcl 13941	. . . . . . 7 ⊢ ((((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ → (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) ∈ ℝ)
63	61, 62	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) ∈ ℝ)
64	6, 2	posdifd 11908	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
65	13, 64	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
66	65, 10	breqtrrd 5132	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑇)
67	8, 66	elrpd 13166	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ ℝ⁺)
68	67	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ⁺)
69		flltp1 13945	. . . . . . . 8 ⊢ (((𝐴 − 𝑥) / 𝑇) ∈ ℝ → ((𝐴 − 𝑥) / 𝑇) < ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1))
70	25, 69	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) < ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1))
71		1zzd 12732	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈ ℤ)
72		fladdz 13970	. . . . . . . 8 ⊢ ((((𝐴 − 𝑥) / 𝑇) ∈ ℝ ∧ 1 ∈ ℤ) → (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) = ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1))
73	25, 71, 72	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) = ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1))
74	70, 73	breqtrrd 5132	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) < (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)))
75	25, 63, 68, 74	ltmul1dd 13224	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) < ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇))
76	26, 59, 1, 75	ltadd2dd 11474	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) < (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)))
77	50, 45, 17	divcan1d 12099	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) = (𝐴 − 𝑥))
78	77	oveq2d 7438	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) = (𝑥 + (𝐴 − 𝑥)))
79	46, 44	pncan3d 11677	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝐴 − 𝑥)) = 𝐴)
80	78, 79	eqtrd 2795	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) = 𝐴)
81	58	oveq2d 7438	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)))
82	81	eqcomd 2766	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
83	76, 80, 82	3brtr3d 5135	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
84	18, 9	remulcld 11344	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐵 − 𝑥) / 𝑇) · 𝑇) ∈ ℝ)
85		flle 13944	. . . . . . 7 ⊢ (((𝐵 − 𝑥) / 𝑇) ∈ ℝ → (⌊‘((𝐵 − 𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇))
86	18, 85	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐵 − 𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇))
87	20, 18, 68	lemul1d 13212	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇) ↔ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ≤ (((𝐵 − 𝑥) / 𝑇) · 𝑇)))
88	86, 87	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ≤ (((𝐵 − 𝑥) / 𝑇) · 𝑇))
89	21, 84, 1, 88	leadd2dd 11936	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇)))
90	4	recnd 11342	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℂ)
91	90, 45, 17	divcan1d 12099	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐵 − 𝑥) / 𝑇) · 𝑇) = (𝐵 − 𝑥))
92	91	oveq2d 7438	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇)) = (𝑥 + (𝐵 − 𝑥)))
93	11	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℂ)
94	46, 93	pncan3d 11677	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝐵 − 𝑥)) = 𝐵)
95	92, 94	eqtrd 2795	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇)) = 𝐵)
96	89, 95	breqtrd 5130	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵)
97	23	rexrd 11364	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ^*)
98		elioc2 13545	. . . 4 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ ∧ 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵)))
99	97, 3, 98	syl2anc 596	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ ∧ 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵)))
100	22, 83, 96, 99	mpbir3and 1361	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵))
101		fourierdlem4.e	. 2 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
102	100, 101	fmptd 7117	1 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 class class class wbr 5102 ↦ cmpt 5185 ⟶wf 6537 ‘cfv 6541 (class class class)co 7422 ℂcc 11203 ℝcr 11204 0cc0 11205 1c1 11206 + caddc 11208 · cmul 11210 ℝ^*cxr 11347 < clt 11348 ≤ cle 11349 − cmin 11546 / cdiv 11978 ℤcz 12698 ℝ⁺crp 13125 (,]cioc 13482 ⌊cfl 13935

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7753 ax-cnex 11261 ax-resscn 11262 ax-1cn 11263 ax-icn 11264 ax-addcl 11265 ax-addrcl 11266 ax-mulcl 11267 ax-mulrcl 11268 ax-mulcom 11269 ax-addass 11270 ax-mulass 11271 ax-distr 11272 ax-i2m1 11273 ax-1ne0 11274 ax-1rid 11275 ax-rnegex 11276 ax-rrecex 11277 ax-cnre 11278 ax-pre-lttri 11279 ax-pre-lttrn 11280 ax-pre-ltadd 11281 ax-pre-mulgt0 11282 ax-pre-sup 11283

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 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 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7379 df-ov 7425 df-oprab 7426 df-mpo 7427 df-om 7880 df-2nd 8004 df-frecs 8304 df-wrecs 8335 df-recs 8384 df-rdg 8423 df-er 8722 df-en 8979 df-dom 8980 df-sdom 8981 df-sup 9439 df-inf 9440 df-pnf 11350 df-mnf 11351 df-xr 11352 df-ltxr 11353 df-le 11354 df-sub 11548 df-neg 11549 df-div 11979 df-nn 12341 df-n0 12612 df-z 12699 df-uz 12971 df-rp 13126 df-ioc 13486 df-fl 13937

This theorem is used by: fourierdlem19 47243 fourierdlem37 47261 fourierdlem41 47265 fourierdlem48 47271 fourierdlem49 47272 fourierdlem51 47274 fourierdlem63 47286 fourierdlem65 47288 fourierdlem71 47294 fourierdlem79 47302 fourierdlem89 47312 fourierdlem90 47313 fourierdlem91 47314 fourierdlem102 47325 fourierdlem114 47337

W3C validator