Proof of Theorem fourierdlem4
Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
2 | | fourierdlem4.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | 2 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ) |
4 | 3, 1 | resubcld 11287 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℝ) |
5 | | fourierdlem4.t |
. . . . . . . . . 10
⊢ 𝑇 = (𝐵 − 𝐴) |
6 | | fourierdlem4.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
7 | 2, 6 | resubcld 11287 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
8 | 5, 7 | eqeltrid 2844 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ ℝ) |
9 | 8 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ) |
10 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 = (𝐵 − 𝐴)) |
11 | 2 | recnd 10888 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
12 | 6 | recnd 10888 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
13 | | fourierdlem4.altb |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 < 𝐵) |
14 | 6, 13 | gtned 10994 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ≠ 𝐴) |
15 | 11, 12, 14 | subne0d 11225 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0) |
16 | 10, 15 | eqnetrd 3010 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ≠ 0) |
17 | 16 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ≠ 0) |
18 | 4, 9, 17 | redivcld 11687 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ) |
19 | 18 | flcld 13400 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐵 −
𝑥) / 𝑇)) ∈ ℤ) |
20 | 19 | zred 12309 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐵 −
𝑥) / 𝑇)) ∈ ℝ) |
21 | 20, 9 | remulcld 10890 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐵 −
𝑥) / 𝑇)) · 𝑇) ∈ ℝ) |
22 | 1, 21 | readdcld 10889 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ) |
23 | 6 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ) |
24 | 23, 1 | resubcld 11287 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴 − 𝑥) ∈ ℝ) |
25 | 24, 9, 17 | redivcld 11687 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) ∈ ℝ) |
26 | 25, 9 | remulcld 10890 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) ∈ ℝ) |
27 | 11 | addid1d 11059 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 + 0) = 𝐵) |
28 | 27 | eqcomd 2745 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 = (𝐵 + 0)) |
29 | 11, 12 | subcld 11216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) |
30 | 29 | subidd 11204 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐵 − 𝐴) − (𝐵 − 𝐴)) = 0) |
31 | 30 | eqcomd 2745 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 = ((𝐵 − 𝐴) − (𝐵 − 𝐴))) |
32 | 31 | oveq2d 7250 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 + 0) = (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴)))) |
33 | 11, 29, 29 | addsub12d 11239 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴))) = ((𝐵 − 𝐴) + (𝐵 − (𝐵 − 𝐴)))) |
34 | 11, 12 | nncand 11221 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 − (𝐵 − 𝐴)) = 𝐴) |
35 | 34 | oveq2d 7250 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 − 𝐴) + (𝐵 − (𝐵 − 𝐴))) = ((𝐵 − 𝐴) + 𝐴)) |
36 | 29, 12 | addcomd 11061 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝐴 + (𝐵 − 𝐴))) |
37 | 10 | eqcomd 2745 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇) |
38 | 37 | oveq2d 7250 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = (𝐴 + 𝑇)) |
39 | 36, 38 | eqtrd 2779 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝐴 + 𝑇)) |
40 | 33, 35, 39 | 3eqtrd 2783 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴))) = (𝐴 + 𝑇)) |
41 | 28, 32, 40 | 3eqtrd 2783 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 = (𝐴 + 𝑇)) |
42 | 41 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 = (𝐴 + 𝑇)) |
43 | 42 | oveq1d 7249 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) = ((𝐴 + 𝑇) − 𝑥)) |
44 | 12 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℂ) |
45 | 9 | recnd 10888 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ) |
46 | 1 | recnd 10888 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
47 | 44, 45, 46 | addsubd 11237 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 + 𝑇) − 𝑥) = ((𝐴 − 𝑥) + 𝑇)) |
48 | 43, 47 | eqtrd 2779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) = ((𝐴 − 𝑥) + 𝑇)) |
49 | 48 | oveq1d 7249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) = (((𝐴 − 𝑥) + 𝑇) / 𝑇)) |
50 | 44, 46 | subcld 11216 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴 − 𝑥) ∈ ℂ) |
51 | 50, 45, 45, 17 | divdird 11673 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) + 𝑇) / 𝑇) = (((𝐴 − 𝑥) / 𝑇) + (𝑇 / 𝑇))) |
52 | 5, 29 | eqeltrid 2844 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ ℂ) |
53 | 52, 16 | dividd 11633 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 / 𝑇) = 1) |
54 | 53 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑇 / 𝑇) = 1) |
55 | 54 | oveq2d 7250 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) + (𝑇 / 𝑇)) = (((𝐴 − 𝑥) / 𝑇) + 1)) |
56 | 49, 51, 55 | 3eqtrd 2783 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) = (((𝐴 − 𝑥) / 𝑇) + 1)) |
57 | 56 | fveq2d 6742 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐵 −
𝑥) / 𝑇)) = (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1))) |
58 | 57 | oveq1d 7249 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐵 −
𝑥) / 𝑇)) · 𝑇) = ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)) |
59 | 58, 21 | eqeltrrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘(((𝐴
− 𝑥) / 𝑇) + 1)) · 𝑇) ∈
ℝ) |
60 | | peano2re 11032 |
. . . . . . . 8
⊢ (((𝐴 − 𝑥) / 𝑇) ∈ ℝ → (((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ) |
61 | 25, 60 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ) |
62 | | reflcl 13398 |
. . . . . . 7
⊢ ((((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ →
(⌊‘(((𝐴 −
𝑥) / 𝑇) + 1)) ∈ ℝ) |
63 | 61, 62 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘(((𝐴 −
𝑥) / 𝑇) + 1)) ∈ ℝ) |
64 | 6, 2 | posdifd 11446 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
65 | 13, 64 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
66 | 65, 10 | breqtrrd 5097 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝑇) |
67 | 8, 66 | elrpd 12652 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
68 | 67 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈
ℝ+) |
69 | | flltp1 13402 |
. . . . . . . 8
⊢ (((𝐴 − 𝑥) / 𝑇) ∈ ℝ → ((𝐴 − 𝑥) / 𝑇) < ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1)) |
70 | 25, 69 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) < ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1)) |
71 | | 1zzd 12235 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈
ℤ) |
72 | | fladdz 13427 |
. . . . . . . 8
⊢ ((((𝐴 − 𝑥) / 𝑇) ∈ ℝ ∧ 1 ∈ ℤ)
→ (⌊‘(((𝐴
− 𝑥) / 𝑇) + 1)) =
((⌊‘((𝐴 −
𝑥) / 𝑇)) + 1)) |
73 | 25, 71, 72 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘(((𝐴 −
𝑥) / 𝑇) + 1)) = ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1)) |
74 | 70, 73 | breqtrrd 5097 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) < (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1))) |
75 | 25, 63, 68, 74 | ltmul1dd 12710 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) < ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)) |
76 | 26, 59, 1, 75 | ltadd2dd 11018 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) < (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇))) |
77 | 50, 45, 17 | divcan1d 11636 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) = (𝐴 − 𝑥)) |
78 | 77 | oveq2d 7250 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) = (𝑥 + (𝐴 − 𝑥))) |
79 | 46, 44 | pncan3d 11219 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝐴 − 𝑥)) = 𝐴) |
80 | 78, 79 | eqtrd 2779 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) = 𝐴) |
81 | 58 | oveq2d 7250 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇))) |
82 | 81 | eqcomd 2745 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
83 | 76, 80, 82 | 3brtr3d 5100 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
84 | 18, 9 | remulcld 10890 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐵 − 𝑥) / 𝑇) · 𝑇) ∈ ℝ) |
85 | | flle 13401 |
. . . . . . 7
⊢ (((𝐵 − 𝑥) / 𝑇) ∈ ℝ →
(⌊‘((𝐵 −
𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇)) |
86 | 18, 85 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐵 −
𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇)) |
87 | 20, 18, 68 | lemul1d 12698 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐵 −
𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇) ↔ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ≤ (((𝐵 − 𝑥) / 𝑇) · 𝑇))) |
88 | 86, 87 | mpbid 235 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐵 −
𝑥) / 𝑇)) · 𝑇) ≤ (((𝐵 − 𝑥) / 𝑇) · 𝑇)) |
89 | 21, 84, 1, 88 | leadd2dd 11474 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇))) |
90 | 4 | recnd 10888 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℂ) |
91 | 90, 45, 17 | divcan1d 11636 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐵 − 𝑥) / 𝑇) · 𝑇) = (𝐵 − 𝑥)) |
92 | 91 | oveq2d 7250 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇)) = (𝑥 + (𝐵 − 𝑥))) |
93 | 11 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℂ) |
94 | 46, 93 | pncan3d 11219 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝐵 − 𝑥)) = 𝐵) |
95 | 92, 94 | eqtrd 2779 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇)) = 𝐵) |
96 | 89, 95 | breqtrd 5095 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵) |
97 | 23 | rexrd 10910 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈
ℝ*) |
98 | | elioc2 13025 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ ((𝑥 +
((⌊‘((𝐵 −
𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ ∧ 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵))) |
99 | 97, 3, 98 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ ∧ 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵))) |
100 | 22, 83, 96, 99 | mpbir3and 1344 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵)) |
101 | | fourierdlem4.e |
. 2
⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
102 | 100, 101 | fmptd 6952 |
1
⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵)) |