Theorem fourierdlem4

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

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

Proof

Step	Hyp	Ref	Expression
1		fourierdlem4.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		fourierdlem4.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		fourierdlem4.altb	⊢ ( 𝜑 → 𝐴 < 𝐵 )
4		fourierdlem4.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
5		fourierdlem4.e	⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
7	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℝ )
8	7 6	resubcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐵 − 𝑥 ) ∈ ℝ )
9	2 1	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
10	4 9	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℝ )
12	4	a1i	⊢ ( 𝜑 → 𝑇 = ( 𝐵 − 𝐴 ) )
13	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
14	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
15	1 3	gtned	⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
16	13 14 15	subne0d	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≠ 0 )
17	12 16	eqnetrd	⊢ ( 𝜑 → 𝑇 ≠ 0 )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ≠ 0 )
19	8 11 18	redivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) ∈ ℝ )
20	19	flcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℤ )
21	20	zred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ∈ ℝ )
22	21 11	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
23	6 22	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
24	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ )
25	24 6	resubcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐴 − 𝑥 ) ∈ ℝ )
26	25 11 18	redivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 − 𝑥 ) / 𝑇 ) ∈ ℝ )
27	26 11	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) · 𝑇 ) ∈ ℝ )
28	13	addridd	⊢ ( 𝜑 → ( 𝐵 + 0 ) = 𝐵 )
29	28	eqcomd	⊢ ( 𝜑 → 𝐵 = ( 𝐵 + 0 ) )
30	13 14	subcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℂ )
31	30	subidd	⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) − ( 𝐵 − 𝐴 ) ) = 0 )
32	31	eqcomd	⊢ ( 𝜑 → 0 = ( ( 𝐵 − 𝐴 ) − ( 𝐵 − 𝐴 ) ) )
33	32	oveq2d	⊢ ( 𝜑 → ( 𝐵 + 0 ) = ( 𝐵 + ( ( 𝐵 − 𝐴 ) − ( 𝐵 − 𝐴 ) ) ) )
34	13 30 30	addsub12d	⊢ ( 𝜑 → ( 𝐵 + ( ( 𝐵 − 𝐴 ) − ( 𝐵 − 𝐴 ) ) ) = ( ( 𝐵 − 𝐴 ) + ( 𝐵 − ( 𝐵 − 𝐴 ) ) ) )
35	13 14	nncand	⊢ ( 𝜑 → ( 𝐵 − ( 𝐵 − 𝐴 ) ) = 𝐴 )
36	35	oveq2d	⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) + ( 𝐵 − ( 𝐵 − 𝐴 ) ) ) = ( ( 𝐵 − 𝐴 ) + 𝐴 ) )
37	30 14	addcomd	⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) + 𝐴 ) = ( 𝐴 + ( 𝐵 − 𝐴 ) ) )
38	12	eqcomd	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = 𝑇 )
39	38	oveq2d	⊢ ( 𝜑 → ( 𝐴 + ( 𝐵 − 𝐴 ) ) = ( 𝐴 + 𝑇 ) )
40	37 39	eqtrd	⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) + 𝐴 ) = ( 𝐴 + 𝑇 ) )
41	34 36 40	3eqtrd	⊢ ( 𝜑 → ( 𝐵 + ( ( 𝐵 − 𝐴 ) − ( 𝐵 − 𝐴 ) ) ) = ( 𝐴 + 𝑇 ) )
42	29 33 41	3eqtrd	⊢ ( 𝜑 → 𝐵 = ( 𝐴 + 𝑇 ) )
43	42	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐵 = ( 𝐴 + 𝑇 ) )
44	43	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐵 − 𝑥 ) = ( ( 𝐴 + 𝑇 ) − 𝑥 ) )
45	14	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℂ )
46	11	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℂ )
47	6	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
48	45 46 47	addsubd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 + 𝑇 ) − 𝑥 ) = ( ( 𝐴 − 𝑥 ) + 𝑇 ) )
49	44 48	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐵 − 𝑥 ) = ( ( 𝐴 − 𝑥 ) + 𝑇 ) )
50	49	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( ( 𝐴 − 𝑥 ) + 𝑇 ) / 𝑇 ) )
51	45 47	subcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐴 − 𝑥 ) ∈ ℂ )
52	51 46 46 18	divdird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 − 𝑥 ) + 𝑇 ) / 𝑇 ) = ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + ( 𝑇 / 𝑇 ) ) )
53	4 30	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
54	53 17	dividd	⊢ ( 𝜑 → ( 𝑇 / 𝑇 ) = 1 )
55	54	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑇 / 𝑇 ) = 1 )
56	55	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + ( 𝑇 / 𝑇 ) ) = ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) )
57	50 52 56	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) )
58	57	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ) )
59	58	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ) · 𝑇 ) )
60	59 22	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ) · 𝑇 ) ∈ ℝ )
61		peano2re	⊢ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) ∈ ℝ → ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ∈ ℝ )
62	26 61	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ∈ ℝ )
63		reflcl	⊢ ( ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ∈ ℝ → ( ⌊ ‘ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ) ∈ ℝ )
64	62 63	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ) ∈ ℝ )
65	1 2	posdifd	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
66	3 65	mpbid	⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
67	66 12	breqtrrd	⊢ ( 𝜑 → 0 < 𝑇 )
68	10 67	elrpd	⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
69	68	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℝ+ )
70		flltp1	⊢ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) ∈ ℝ → ( ( 𝐴 − 𝑥 ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐴 − 𝑥 ) / 𝑇 ) ) + 1 ) )
71	26 70	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 − 𝑥 ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐴 − 𝑥 ) / 𝑇 ) ) + 1 ) )
72		1zzd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℤ )
73		fladdz	⊢ ( ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ⌊ ‘ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ) = ( ( ⌊ ‘ ( ( 𝐴 − 𝑥 ) / 𝑇 ) ) + 1 ) )
74	26 72 73	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ) = ( ( ⌊ ‘ ( ( 𝐴 − 𝑥 ) / 𝑇 ) ) + 1 ) )
75	71 74	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 − 𝑥 ) / 𝑇 ) < ( ⌊ ‘ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ) )
76	26 64 69 75	ltmul1dd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) · 𝑇 ) < ( ( ⌊ ‘ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ) · 𝑇 ) )
77	27 60 6 76	ltadd2dd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) · 𝑇 ) ) < ( 𝑥 + ( ( ⌊ ‘ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ) · 𝑇 ) ) )
78	51 46 18	divcan1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) · 𝑇 ) = ( 𝐴 − 𝑥 ) )
79	78	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) · 𝑇 ) ) = ( 𝑥 + ( 𝐴 − 𝑥 ) ) )
80	47 45	pncan3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( 𝐴 − 𝑥 ) ) = 𝐴 )
81	79 80	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) · 𝑇 ) ) = 𝐴 )
82	59	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ) · 𝑇 ) ) )
83	82	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( ( 𝐴 − 𝑥 ) / 𝑇 ) + 1 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
84	77 81 83	3brtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 < ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
85	19 11	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐵 − 𝑥 ) / 𝑇 ) · 𝑇 ) ∈ ℝ )
86		flle	⊢ ( ( ( 𝐵 − 𝑥 ) / 𝑇 ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ≤ ( ( 𝐵 − 𝑥 ) / 𝑇 ) )
87	19 86	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ≤ ( ( 𝐵 − 𝑥 ) / 𝑇 ) )
88	21 19 69	lemul1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) ≤ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ↔ ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ≤ ( ( ( 𝐵 − 𝑥 ) / 𝑇 ) · 𝑇 ) ) )
89	87 88	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ≤ ( ( ( 𝐵 − 𝑥 ) / 𝑇 ) · 𝑇 ) )
90	22 85 6 89	leadd2dd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ≤ ( 𝑥 + ( ( ( 𝐵 − 𝑥 ) / 𝑇 ) · 𝑇 ) ) )
91	8	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐵 − 𝑥 ) ∈ ℂ )
92	91 46 18	divcan1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐵 − 𝑥 ) / 𝑇 ) · 𝑇 ) = ( 𝐵 − 𝑥 ) )
93	92	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ( 𝐵 − 𝑥 ) / 𝑇 ) · 𝑇 ) ) = ( 𝑥 + ( 𝐵 − 𝑥 ) ) )
94	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℂ )
95	47 94	pncan3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( 𝐵 − 𝑥 ) ) = 𝐵 )
96	93 95	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ( 𝐵 − 𝑥 ) / 𝑇 ) · 𝑇 ) ) = 𝐵 )
97	90 96	breqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ≤ 𝐵 )
98	24	rexrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ* )
99		elioc2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ ∧ 𝐴 < ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ≤ 𝐵 ) ) )
100	98 7 99	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ ∧ 𝐴 < ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ≤ 𝐵 ) ) )
101	23 84 97 100	mpbir3and	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
102	101 5	fmptd	⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )