Metamath Proof Explorer

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 ⊢ φ → A ∈ ℝ
fourierdlem4.b ⊢ φ → B ∈ ℝ
fourierdlem4.altb ⊢ φ → A < B
fourierdlem4.t ⊢ T = B − A
fourierdlem4.e ⊢ E = x ∈ ℝ ⟼ x + B − x T ⁢ T
Assertion fourierdlem4 ⊢ φ → E : ℝ ⟶ A B

Proof

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