Proof of Theorem fourierdlem4
Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
2 | | fourierdlem4.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | 2 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ) |
4 | 3, 1 | resubcld 11403 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℝ) |
5 | | fourierdlem4.t |
. . . . . . . . . 10
⊢ 𝑇 = (𝐵 − 𝐴) |
6 | | fourierdlem4.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
7 | 2, 6 | resubcld 11403 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
8 | 5, 7 | eqeltrid 2843 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ ℝ) |
9 | 8 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ) |
10 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 = (𝐵 − 𝐴)) |
11 | 2 | recnd 11003 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
12 | 6 | recnd 11003 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
13 | | fourierdlem4.altb |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 < 𝐵) |
14 | 6, 13 | gtned 11110 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ≠ 𝐴) |
15 | 11, 12, 14 | subne0d 11341 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0) |
16 | 10, 15 | eqnetrd 3011 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ≠ 0) |
17 | 16 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ≠ 0) |
18 | 4, 9, 17 | redivcld 11803 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ) |
19 | 18 | flcld 13518 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐵 −
𝑥) / 𝑇)) ∈ ℤ) |
20 | 19 | zred 12426 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐵 −
𝑥) / 𝑇)) ∈ ℝ) |
21 | 20, 9 | remulcld 11005 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐵 −
𝑥) / 𝑇)) · 𝑇) ∈ ℝ) |
22 | 1, 21 | readdcld 11004 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ) |
23 | 6 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ) |
24 | 23, 1 | resubcld 11403 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴 − 𝑥) ∈ ℝ) |
25 | 24, 9, 17 | redivcld 11803 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) ∈ ℝ) |
26 | 25, 9 | remulcld 11005 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) ∈ ℝ) |
27 | 11 | addid1d 11175 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 + 0) = 𝐵) |
28 | 27 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 = (𝐵 + 0)) |
29 | 11, 12 | subcld 11332 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) |
30 | 29 | subidd 11320 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐵 − 𝐴) − (𝐵 − 𝐴)) = 0) |
31 | 30 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 = ((𝐵 − 𝐴) − (𝐵 − 𝐴))) |
32 | 31 | oveq2d 7291 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 + 0) = (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴)))) |
33 | 11, 29, 29 | addsub12d 11355 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴))) = ((𝐵 − 𝐴) + (𝐵 − (𝐵 − 𝐴)))) |
34 | 11, 12 | nncand 11337 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 − (𝐵 − 𝐴)) = 𝐴) |
35 | 34 | oveq2d 7291 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 − 𝐴) + (𝐵 − (𝐵 − 𝐴))) = ((𝐵 − 𝐴) + 𝐴)) |
36 | 29, 12 | addcomd 11177 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝐴 + (𝐵 − 𝐴))) |
37 | 10 | eqcomd 2744 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇) |
38 | 37 | oveq2d 7291 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = (𝐴 + 𝑇)) |
39 | 36, 38 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝐴 + 𝑇)) |
40 | 33, 35, 39 | 3eqtrd 2782 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴))) = (𝐴 + 𝑇)) |
41 | 28, 32, 40 | 3eqtrd 2782 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 = (𝐴 + 𝑇)) |
42 | 41 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 = (𝐴 + 𝑇)) |
43 | 42 | oveq1d 7290 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) = ((𝐴 + 𝑇) − 𝑥)) |
44 | 12 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℂ) |
45 | 9 | recnd 11003 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ) |
46 | 1 | recnd 11003 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
47 | 44, 45, 46 | addsubd 11353 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 + 𝑇) − 𝑥) = ((𝐴 − 𝑥) + 𝑇)) |
48 | 43, 47 | eqtrd 2778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) = ((𝐴 − 𝑥) + 𝑇)) |
49 | 48 | oveq1d 7290 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) = (((𝐴 − 𝑥) + 𝑇) / 𝑇)) |
50 | 44, 46 | subcld 11332 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴 − 𝑥) ∈ ℂ) |
51 | 50, 45, 45, 17 | divdird 11789 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) + 𝑇) / 𝑇) = (((𝐴 − 𝑥) / 𝑇) + (𝑇 / 𝑇))) |
52 | 5, 29 | eqeltrid 2843 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ ℂ) |
53 | 52, 16 | dividd 11749 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 / 𝑇) = 1) |
54 | 53 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑇 / 𝑇) = 1) |
55 | 54 | oveq2d 7291 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) + (𝑇 / 𝑇)) = (((𝐴 − 𝑥) / 𝑇) + 1)) |
56 | 49, 51, 55 | 3eqtrd 2782 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) = (((𝐴 − 𝑥) / 𝑇) + 1)) |
57 | 56 | fveq2d 6778 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐵 −
𝑥) / 𝑇)) = (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1))) |
58 | 57 | oveq1d 7290 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐵 −
𝑥) / 𝑇)) · 𝑇) = ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)) |
59 | 58, 21 | eqeltrrd 2840 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘(((𝐴
− 𝑥) / 𝑇) + 1)) · 𝑇) ∈
ℝ) |
60 | | peano2re 11148 |
. . . . . . . 8
⊢ (((𝐴 − 𝑥) / 𝑇) ∈ ℝ → (((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ) |
61 | 25, 60 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ) |
62 | | reflcl 13516 |
. . . . . . 7
⊢ ((((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ →
(⌊‘(((𝐴 −
𝑥) / 𝑇) + 1)) ∈ ℝ) |
63 | 61, 62 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘(((𝐴 −
𝑥) / 𝑇) + 1)) ∈ ℝ) |
64 | 6, 2 | posdifd 11562 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
65 | 13, 64 | mpbid 231 |
. . . . . . . . 9
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
66 | 65, 10 | breqtrrd 5102 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝑇) |
67 | 8, 66 | elrpd 12769 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
68 | 67 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈
ℝ+) |
69 | | flltp1 13520 |
. . . . . . . 8
⊢ (((𝐴 − 𝑥) / 𝑇) ∈ ℝ → ((𝐴 − 𝑥) / 𝑇) < ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1)) |
70 | 25, 69 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) < ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1)) |
71 | | 1zzd 12351 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈
ℤ) |
72 | | fladdz 13545 |
. . . . . . . 8
⊢ ((((𝐴 − 𝑥) / 𝑇) ∈ ℝ ∧ 1 ∈ ℤ)
→ (⌊‘(((𝐴
− 𝑥) / 𝑇) + 1)) =
((⌊‘((𝐴 −
𝑥) / 𝑇)) + 1)) |
73 | 25, 71, 72 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘(((𝐴 −
𝑥) / 𝑇) + 1)) = ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1)) |
74 | 70, 73 | breqtrrd 5102 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) < (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1))) |
75 | 25, 63, 68, 74 | ltmul1dd 12827 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) < ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)) |
76 | 26, 59, 1, 75 | ltadd2dd 11134 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) < (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇))) |
77 | 50, 45, 17 | divcan1d 11752 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) = (𝐴 − 𝑥)) |
78 | 77 | oveq2d 7291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) = (𝑥 + (𝐴 − 𝑥))) |
79 | 46, 44 | pncan3d 11335 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝐴 − 𝑥)) = 𝐴) |
80 | 78, 79 | eqtrd 2778 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) = 𝐴) |
81 | 58 | oveq2d 7291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇))) |
82 | 81 | eqcomd 2744 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
83 | 76, 80, 82 | 3brtr3d 5105 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
84 | 18, 9 | remulcld 11005 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐵 − 𝑥) / 𝑇) · 𝑇) ∈ ℝ) |
85 | | flle 13519 |
. . . . . . 7
⊢ (((𝐵 − 𝑥) / 𝑇) ∈ ℝ →
(⌊‘((𝐵 −
𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇)) |
86 | 18, 85 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐵 −
𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇)) |
87 | 20, 18, 68 | lemul1d 12815 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐵 −
𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇) ↔ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ≤ (((𝐵 − 𝑥) / 𝑇) · 𝑇))) |
88 | 86, 87 | mpbid 231 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐵 −
𝑥) / 𝑇)) · 𝑇) ≤ (((𝐵 − 𝑥) / 𝑇) · 𝑇)) |
89 | 21, 84, 1, 88 | leadd2dd 11590 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇))) |
90 | 4 | recnd 11003 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℂ) |
91 | 90, 45, 17 | divcan1d 11752 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐵 − 𝑥) / 𝑇) · 𝑇) = (𝐵 − 𝑥)) |
92 | 91 | oveq2d 7291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇)) = (𝑥 + (𝐵 − 𝑥))) |
93 | 11 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℂ) |
94 | 46, 93 | pncan3d 11335 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝐵 − 𝑥)) = 𝐵) |
95 | 92, 94 | eqtrd 2778 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇)) = 𝐵) |
96 | 89, 95 | breqtrd 5100 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵) |
97 | 23 | rexrd 11025 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈
ℝ*) |
98 | | elioc2 13142 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ ((𝑥 +
((⌊‘((𝐵 −
𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ ∧ 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵))) |
99 | 97, 3, 98 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ ∧ 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵))) |
100 | 22, 83, 96, 99 | mpbir3and 1341 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵)) |
101 | | fourierdlem4.e |
. 2
⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
102 | 100, 101 | fmptd 6988 |
1
⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵)) |