Proof of Theorem fourierdlem4
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) | 
| 2 |  | fourierdlem4.b | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 3 | 2 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ) | 
| 4 | 3, 1 | resubcld 11691 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℝ) | 
| 5 |  | fourierdlem4.t | . . . . . . . . . 10
⊢ 𝑇 = (𝐵 − 𝐴) | 
| 6 |  | fourierdlem4.a | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 7 | 2, 6 | resubcld 11691 | . . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) | 
| 8 | 5, 7 | eqeltrid 2845 | . . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ ℝ) | 
| 9 | 8 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℝ) | 
| 10 | 5 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 𝑇 = (𝐵 − 𝐴)) | 
| 11 | 2 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 12 | 6 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 13 |  | fourierdlem4.altb | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 < 𝐵) | 
| 14 | 6, 13 | gtned 11396 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ≠ 𝐴) | 
| 15 | 11, 12, 14 | subne0d 11629 | . . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ≠ 0) | 
| 16 | 10, 15 | eqnetrd 3008 | . . . . . . . . 9
⊢ (𝜑 → 𝑇 ≠ 0) | 
| 17 | 16 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ≠ 0) | 
| 18 | 4, 9, 17 | redivcld 12095 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) ∈ ℝ) | 
| 19 | 18 | flcld 13838 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐵 −
𝑥) / 𝑇)) ∈ ℤ) | 
| 20 | 19 | zred 12722 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐵 −
𝑥) / 𝑇)) ∈ ℝ) | 
| 21 | 20, 9 | remulcld 11291 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐵 −
𝑥) / 𝑇)) · 𝑇) ∈ ℝ) | 
| 22 | 1, 21 | readdcld 11290 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ) | 
| 23 | 6 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ) | 
| 24 | 23, 1 | resubcld 11691 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴 − 𝑥) ∈ ℝ) | 
| 25 | 24, 9, 17 | redivcld 12095 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) ∈ ℝ) | 
| 26 | 25, 9 | remulcld 11291 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) ∈ ℝ) | 
| 27 | 11 | addridd 11461 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 + 0) = 𝐵) | 
| 28 | 27 | eqcomd 2743 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 = (𝐵 + 0)) | 
| 29 | 11, 12 | subcld 11620 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) | 
| 30 | 29 | subidd 11608 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐵 − 𝐴) − (𝐵 − 𝐴)) = 0) | 
| 31 | 30 | eqcomd 2743 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 = ((𝐵 − 𝐴) − (𝐵 − 𝐴))) | 
| 32 | 31 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 + 0) = (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴)))) | 
| 33 | 11, 29, 29 | addsub12d 11643 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴))) = ((𝐵 − 𝐴) + (𝐵 − (𝐵 − 𝐴)))) | 
| 34 | 11, 12 | nncand 11625 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 − (𝐵 − 𝐴)) = 𝐴) | 
| 35 | 34 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 − 𝐴) + (𝐵 − (𝐵 − 𝐴))) = ((𝐵 − 𝐴) + 𝐴)) | 
| 36 | 29, 12 | addcomd 11463 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝐴 + (𝐵 − 𝐴))) | 
| 37 | 10 | eqcomd 2743 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇) | 
| 38 | 37 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 + (𝐵 − 𝐴)) = (𝐴 + 𝑇)) | 
| 39 | 36, 38 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 − 𝐴) + 𝐴) = (𝐴 + 𝑇)) | 
| 40 | 33, 35, 39 | 3eqtrd 2781 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 + ((𝐵 − 𝐴) − (𝐵 − 𝐴))) = (𝐴 + 𝑇)) | 
| 41 | 28, 32, 40 | 3eqtrd 2781 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 = (𝐴 + 𝑇)) | 
| 42 | 41 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 = (𝐴 + 𝑇)) | 
| 43 | 42 | oveq1d 7446 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) = ((𝐴 + 𝑇) − 𝑥)) | 
| 44 | 12 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℂ) | 
| 45 | 9 | recnd 11289 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈ ℂ) | 
| 46 | 1 | recnd 11289 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) | 
| 47 | 44, 45, 46 | addsubd 11641 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 + 𝑇) − 𝑥) = ((𝐴 − 𝑥) + 𝑇)) | 
| 48 | 43, 47 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) = ((𝐴 − 𝑥) + 𝑇)) | 
| 49 | 48 | oveq1d 7446 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) = (((𝐴 − 𝑥) + 𝑇) / 𝑇)) | 
| 50 | 44, 46 | subcld 11620 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴 − 𝑥) ∈ ℂ) | 
| 51 | 50, 45, 45, 17 | divdird 12081 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) + 𝑇) / 𝑇) = (((𝐴 − 𝑥) / 𝑇) + (𝑇 / 𝑇))) | 
| 52 | 5, 29 | eqeltrid 2845 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ ℂ) | 
| 53 | 52, 16 | dividd 12041 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑇 / 𝑇) = 1) | 
| 54 | 53 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑇 / 𝑇) = 1) | 
| 55 | 54 | oveq2d 7447 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) + (𝑇 / 𝑇)) = (((𝐴 − 𝑥) / 𝑇) + 1)) | 
| 56 | 49, 51, 55 | 3eqtrd 2781 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐵 − 𝑥) / 𝑇) = (((𝐴 − 𝑥) / 𝑇) + 1)) | 
| 57 | 56 | fveq2d 6910 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐵 −
𝑥) / 𝑇)) = (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1))) | 
| 58 | 57 | oveq1d 7446 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐵 −
𝑥) / 𝑇)) · 𝑇) = ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)) | 
| 59 | 58, 21 | eqeltrrd 2842 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘(((𝐴
− 𝑥) / 𝑇) + 1)) · 𝑇) ∈
ℝ) | 
| 60 |  | peano2re 11434 | . . . . . . . 8
⊢ (((𝐴 − 𝑥) / 𝑇) ∈ ℝ → (((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ) | 
| 61 | 25, 60 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ) | 
| 62 |  | reflcl 13836 | . . . . . . 7
⊢ ((((𝐴 − 𝑥) / 𝑇) + 1) ∈ ℝ →
(⌊‘(((𝐴 −
𝑥) / 𝑇) + 1)) ∈ ℝ) | 
| 63 | 61, 62 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘(((𝐴 −
𝑥) / 𝑇) + 1)) ∈ ℝ) | 
| 64 | 6, 2 | posdifd 11850 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) | 
| 65 | 13, 64 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) | 
| 66 | 65, 10 | breqtrrd 5171 | . . . . . . . 8
⊢ (𝜑 → 0 < 𝑇) | 
| 67 | 8, 66 | elrpd 13074 | . . . . . . 7
⊢ (𝜑 → 𝑇 ∈
ℝ+) | 
| 68 | 67 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑇 ∈
ℝ+) | 
| 69 |  | flltp1 13840 | . . . . . . . 8
⊢ (((𝐴 − 𝑥) / 𝑇) ∈ ℝ → ((𝐴 − 𝑥) / 𝑇) < ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1)) | 
| 70 | 25, 69 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) < ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1)) | 
| 71 |  | 1zzd 12648 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈
ℤ) | 
| 72 |  | fladdz 13865 | . . . . . . . 8
⊢ ((((𝐴 − 𝑥) / 𝑇) ∈ ℝ ∧ 1 ∈ ℤ)
→ (⌊‘(((𝐴
− 𝑥) / 𝑇) + 1)) =
((⌊‘((𝐴 −
𝑥) / 𝑇)) + 1)) | 
| 73 | 25, 71, 72 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘(((𝐴 −
𝑥) / 𝑇) + 1)) = ((⌊‘((𝐴 − 𝑥) / 𝑇)) + 1)) | 
| 74 | 70, 73 | breqtrrd 5171 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐴 − 𝑥) / 𝑇) < (⌊‘(((𝐴 − 𝑥) / 𝑇) + 1))) | 
| 75 | 25, 63, 68, 74 | ltmul1dd 13132 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) < ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)) | 
| 76 | 26, 59, 1, 75 | ltadd2dd 11420 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) < (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇))) | 
| 77 | 50, 45, 17 | divcan1d 12044 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐴 − 𝑥) / 𝑇) · 𝑇) = (𝐴 − 𝑥)) | 
| 78 | 77 | oveq2d 7447 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) = (𝑥 + (𝐴 − 𝑥))) | 
| 79 | 46, 44 | pncan3d 11623 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝐴 − 𝑥)) = 𝐴) | 
| 80 | 78, 79 | eqtrd 2777 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐴 − 𝑥) / 𝑇) · 𝑇)) = 𝐴) | 
| 81 | 58 | oveq2d 7447 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇))) | 
| 82 | 81 | eqcomd 2743 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘(((𝐴 − 𝑥) / 𝑇) + 1)) · 𝑇)) = (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) | 
| 83 | 76, 80, 82 | 3brtr3d 5174 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) | 
| 84 | 18, 9 | remulcld 11291 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐵 − 𝑥) / 𝑇) · 𝑇) ∈ ℝ) | 
| 85 |  | flle 13839 | . . . . . . 7
⊢ (((𝐵 − 𝑥) / 𝑇) ∈ ℝ →
(⌊‘((𝐵 −
𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇)) | 
| 86 | 18, 85 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(⌊‘((𝐵 −
𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇)) | 
| 87 | 20, 18, 68 | lemul1d 13120 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐵 −
𝑥) / 𝑇)) ≤ ((𝐵 − 𝑥) / 𝑇) ↔ ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) ≤ (((𝐵 − 𝑥) / 𝑇) · 𝑇))) | 
| 88 | 86, 87 | mpbid 232 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
((⌊‘((𝐵 −
𝑥) / 𝑇)) · 𝑇) ≤ (((𝐵 − 𝑥) / 𝑇) · 𝑇)) | 
| 89 | 21, 84, 1, 88 | leadd2dd 11878 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇))) | 
| 90 | 4 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐵 − 𝑥) ∈ ℂ) | 
| 91 | 90, 45, 17 | divcan1d 12044 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((𝐵 − 𝑥) / 𝑇) · 𝑇) = (𝐵 − 𝑥)) | 
| 92 | 91 | oveq2d 7447 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇)) = (𝑥 + (𝐵 − 𝑥))) | 
| 93 | 11 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℂ) | 
| 94 | 46, 93 | pncan3d 11623 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (𝐵 − 𝑥)) = 𝐵) | 
| 95 | 92, 94 | eqtrd 2777 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + (((𝐵 − 𝑥) / 𝑇) · 𝑇)) = 𝐵) | 
| 96 | 89, 95 | breqtrd 5169 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵) | 
| 97 | 23 | rexrd 11311 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈
ℝ*) | 
| 98 |  | elioc2 13450 | . . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ ((𝑥 +
((⌊‘((𝐵 −
𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ ∧ 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵))) | 
| 99 | 97, 3, 98 | syl2anc 584 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵) ↔ ((𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ ℝ ∧ 𝐴 < (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∧ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ≤ 𝐵))) | 
| 100 | 22, 83, 96, 99 | mpbir3and 1343 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) ∈ (𝐴(,]𝐵)) | 
| 101 |  | fourierdlem4.e | . 2
⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) | 
| 102 | 100, 101 | fmptd 7134 | 1
⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵)) |