Proof of Theorem fourierdlem19
Step | Hyp | Ref
| Expression |
1 | | fourierdlem19.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | fourierdlem19.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ ℝ) |
3 | 1, 2 | readdcld 10862 |
. . . . 5
⊢ (𝜑 → (𝐴 + 𝑋) ∈ ℝ) |
4 | 3 | rexrd 10883 |
. . . 4
⊢ (𝜑 → (𝐴 + 𝑋) ∈
ℝ*) |
5 | | fourierdlem19.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
6 | 5, 2 | readdcld 10862 |
. . . . 5
⊢ (𝜑 → (𝐵 + 𝑋) ∈ ℝ) |
7 | 6 | rexrd 10883 |
. . . 4
⊢ (𝜑 → (𝐵 + 𝑋) ∈
ℝ*) |
8 | | fourierdlem19.d |
. . . . . 6
⊢ 𝐷 = {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} |
9 | | ssrab2 3993 |
. . . . . 6
⊢ {𝑦 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ 𝐶} ⊆ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) |
10 | 8, 9 | eqsstri 3935 |
. . . . 5
⊢ 𝐷 ⊆ ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) |
11 | | fourierdlem19.z |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝐷) |
12 | 10, 11 | sseldi 3899 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋))) |
13 | | iocleub 42716 |
. . . 4
⊢ (((𝐴 + 𝑋) ∈ ℝ* ∧ (𝐵 + 𝑋) ∈ ℝ* ∧ 𝑍 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋))) → 𝑍 ≤ (𝐵 + 𝑋)) |
14 | 4, 7, 12, 13 | syl3anc 1373 |
. . 3
⊢ (𝜑 → 𝑍 ≤ (𝐵 + 𝑋)) |
15 | 14 | adantr 484 |
. 2
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → 𝑍 ≤ (𝐵 + 𝑋)) |
16 | 6 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (𝐵 + 𝑋) ∈ ℝ) |
17 | | iocssre 13015 |
. . . . . . . 8
⊢ (((𝐴 + 𝑋) ∈ ℝ* ∧ (𝐵 + 𝑋) ∈ ℝ) → ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ⊆ ℝ) |
18 | 4, 6, 17 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 + 𝑋)(,](𝐵 + 𝑋)) ⊆ ℝ) |
19 | | fourierdlem19.w |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ 𝐷) |
20 | 10, 19 | sseldi 3899 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋))) |
21 | 18, 20 | sseldd 3902 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ ℝ) |
22 | | fourierdlem19.t |
. . . . . . 7
⊢ 𝑇 = (𝐵 − 𝐴) |
23 | 5, 1 | resubcld 11260 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
24 | 22, 23 | eqeltrid 2842 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ ℝ) |
25 | 21, 24 | readdcld 10862 |
. . . . 5
⊢ (𝜑 → (𝑊 + 𝑇) ∈ ℝ) |
26 | 25 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (𝑊 + 𝑇) ∈ ℝ) |
27 | 18, 12 | sseldd 3902 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ ℝ) |
28 | 27 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → 𝑍 ∈ ℝ) |
29 | 22 | eqcomi 2746 |
. . . . . . . . . . 11
⊢ (𝐵 − 𝐴) = 𝑇 |
30 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) = 𝑇) |
31 | 5 | recnd 10861 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℂ) |
32 | 1 | recnd 10861 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
33 | 24 | recnd 10861 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ ℂ) |
34 | 31, 32, 33 | subaddd 11207 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 − 𝐴) = 𝑇 ↔ (𝐴 + 𝑇) = 𝐵)) |
35 | 30, 34 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + 𝑇) = 𝐵) |
36 | 35 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = (𝐴 + 𝑇)) |
37 | 36 | oveq1d 7228 |
. . . . . . 7
⊢ (𝜑 → (𝐵 + 𝑋) = ((𝐴 + 𝑇) + 𝑋)) |
38 | 2 | recnd 10861 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
39 | 32, 33, 38 | add32d 11059 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 + 𝑇) + 𝑋) = ((𝐴 + 𝑋) + 𝑇)) |
40 | 37, 39 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → (𝐵 + 𝑋) = ((𝐴 + 𝑋) + 𝑇)) |
41 | | iocgtlb 42715 |
. . . . . . . 8
⊢ (((𝐴 + 𝑋) ∈ ℝ* ∧ (𝐵 + 𝑋) ∈ ℝ* ∧ 𝑊 ∈ ((𝐴 + 𝑋)(,](𝐵 + 𝑋))) → (𝐴 + 𝑋) < 𝑊) |
42 | 4, 7, 20, 41 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝐴 + 𝑋) < 𝑊) |
43 | 3, 21, 24, 42 | ltadd1dd 11443 |
. . . . . 6
⊢ (𝜑 → ((𝐴 + 𝑋) + 𝑇) < (𝑊 + 𝑇)) |
44 | 40, 43 | eqbrtrd 5075 |
. . . . 5
⊢ (𝜑 → (𝐵 + 𝑋) < (𝑊 + 𝑇)) |
45 | 44 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (𝐵 + 𝑋) < (𝑊 + 𝑇)) |
46 | | fourierdlem19.e |
. . . . . . . . . . . . 13
⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
47 | 46 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))) |
48 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑊 → 𝑥 = 𝑊) |
49 | | oveq2 7221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑊 → (𝐵 − 𝑥) = (𝐵 − 𝑊)) |
50 | 49 | oveq1d 7228 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑊 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑊) / 𝑇)) |
51 | 50 | fveq2d 6721 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑊 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑊) / 𝑇))) |
52 | 51 | oveq1d 7228 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑊 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) |
53 | 48, 52 | oveq12d 7231 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑊 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑊 + ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇))) |
54 | 53 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 = 𝑊) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑊 + ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇))) |
55 | 5, 21 | resubcld 11260 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 − 𝑊) ∈ ℝ) |
56 | | fourierdlem19.altb |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐴 < 𝐵) |
57 | 1, 5 | posdifd 11419 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
58 | 56, 57 | mpbid 235 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
59 | 58, 22 | breqtrrdi 5095 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 < 𝑇) |
60 | 59 | gt0ne0d 11396 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑇 ≠ 0) |
61 | 55, 24, 60 | redivcld 11660 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐵 − 𝑊) / 𝑇) ∈ ℝ) |
62 | 61 | flcld 13373 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌊‘((𝐵 − 𝑊) / 𝑇)) ∈ ℤ) |
63 | 62 | zred 12282 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (⌊‘((𝐵 − 𝑊) / 𝑇)) ∈ ℝ) |
64 | 63, 24 | remulcld 10863 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇) ∈ ℝ) |
65 | 21, 64 | readdcld 10862 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑊 + ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) ∈ ℝ) |
66 | 47, 54, 21, 65 | fvmptd 6825 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸‘𝑊) = (𝑊 + ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇))) |
67 | 66, 65 | eqeltrd 2838 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸‘𝑊) ∈ ℝ) |
68 | 67 | recnd 10861 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸‘𝑊) ∈ ℂ) |
69 | 68 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (𝐸‘𝑊) ∈ ℂ) |
70 | 64 | recnd 10861 |
. . . . . . . . 9
⊢ (𝜑 → ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇) ∈ ℂ) |
71 | 70 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇) ∈ ℂ) |
72 | 33 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → 𝑇 ∈ ℂ) |
73 | 69, 71, 72 | subsubd 11217 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((𝐸‘𝑊) − (((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇) − 𝑇)) = (((𝐸‘𝑊) − ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) + 𝑇)) |
74 | 73 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (((𝐸‘𝑊) − ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) + 𝑇) = ((𝐸‘𝑊) − (((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇) − 𝑇))) |
75 | 5, 27 | resubcld 11260 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 − 𝑍) ∈ ℝ) |
76 | 75, 24, 60 | redivcld 11660 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 − 𝑍) / 𝑇) ∈ ℝ) |
77 | 76 | flcld 13373 |
. . . . . . . . . 10
⊢ (𝜑 → (⌊‘((𝐵 − 𝑍) / 𝑇)) ∈ ℤ) |
78 | 77 | zred 12282 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘((𝐵 − 𝑍) / 𝑇)) ∈ ℝ) |
79 | 78 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (⌊‘((𝐵 − 𝑍) / 𝑇)) ∈ ℝ) |
80 | 24 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → 𝑇 ∈ ℝ) |
81 | 79, 80 | remulcld 10863 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) ∈ ℝ) |
82 | 63 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (⌊‘((𝐵 − 𝑊) / 𝑇)) ∈ ℝ) |
83 | 82, 80 | remulcld 10863 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇) ∈ ℝ) |
84 | 83, 80 | resubcld 11260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇) − 𝑇) ∈ ℝ) |
85 | 67 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (𝐸‘𝑊) ∈ ℝ) |
86 | 78, 24 | remulcld 10863 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) ∈ ℝ) |
87 | 86 | recnd 10861 |
. . . . . . . . . . 11
⊢ (𝜑 → ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) ∈ ℂ) |
88 | 87, 33 | pncand 11190 |
. . . . . . . . . 10
⊢ (𝜑 → ((((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) + 𝑇) − 𝑇) = ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇)) |
89 | 88 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) = ((((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) + 𝑇) − 𝑇)) |
90 | 89 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) = ((((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) + 𝑇) − 𝑇)) |
91 | 81, 80 | readdcld 10862 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) + 𝑇) ∈ ℝ) |
92 | 78 | recnd 10861 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘((𝐵 − 𝑍) / 𝑇)) ∈ ℂ) |
93 | 92, 33 | adddirp1d 10859 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((⌊‘((𝐵 − 𝑍) / 𝑇)) + 1) · 𝑇) = (((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) + 𝑇)) |
94 | 93 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → (((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) + 𝑇) = (((⌊‘((𝐵 − 𝑍) / 𝑇)) + 1) · 𝑇)) |
95 | 94 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) + 𝑇) = (((⌊‘((𝐵 − 𝑍) / 𝑇)) + 1) · 𝑇)) |
96 | | 1red 10834 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → 1 ∈ ℝ) |
97 | 79, 96 | readdcld 10862 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((⌊‘((𝐵 − 𝑍) / 𝑇)) + 1) ∈ ℝ) |
98 | | 0red 10836 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) |
99 | 98, 24, 59 | ltled 10980 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ 𝑇) |
100 | 99 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → 0 ≤ 𝑇) |
101 | 85, 28 | resubcld 11260 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((𝐸‘𝑊) − 𝑍) ∈ ℝ) |
102 | 21 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → 𝑊 ∈ ℝ) |
103 | 85, 102 | resubcld 11260 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((𝐸‘𝑊) − 𝑊) ∈ ℝ) |
104 | 24, 59 | elrpd 12625 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
105 | 104 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → 𝑇 ∈
ℝ+) |
106 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → 𝑊 < 𝑍) |
107 | 102, 28, 85, 106 | ltsub2dd 11445 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((𝐸‘𝑊) − 𝑍) < ((𝐸‘𝑊) − 𝑊)) |
108 | 101, 103,
105, 107 | ltdiv1dd 12685 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (((𝐸‘𝑊) − 𝑍) / 𝑇) < (((𝐸‘𝑊) − 𝑊) / 𝑇)) |
109 | | fourierdlem19.ezew |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐸‘𝑍) = (𝐸‘𝑊)) |
110 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑍 → 𝑥 = 𝑍) |
111 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑍 → (𝐵 − 𝑥) = (𝐵 − 𝑍)) |
112 | 111 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑍 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑍) / 𝑇)) |
113 | 112 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑍 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑍) / 𝑇))) |
114 | 113 | oveq1d 7228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑍 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇)) |
115 | 110, 114 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑍 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑍 + ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇))) |
116 | 115 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 = 𝑍) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑍 + ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇))) |
117 | 27, 86 | readdcld 10862 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑍 + ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇)) ∈ ℝ) |
118 | 47, 116, 27, 117 | fvmptd 6825 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐸‘𝑍) = (𝑍 + ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇))) |
119 | 109, 118 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐸‘𝑊) = (𝑍 + ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇))) |
120 | 119 | oveq1d 7228 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐸‘𝑊) − 𝑍) = ((𝑍 + ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇)) − 𝑍)) |
121 | 27 | recnd 10861 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑍 ∈ ℂ) |
122 | 121, 87 | pncan2d 11191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑍 + ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇)) − 𝑍) = ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇)) |
123 | 120, 122 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐸‘𝑊) − 𝑍) = ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇)) |
124 | 123 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐸‘𝑊) − 𝑍) / 𝑇) = (((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) / 𝑇)) |
125 | 92, 33, 60 | divcan4d 11614 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − 𝑍) / 𝑇))) |
126 | 124, 125 | eqtr2d 2778 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (⌊‘((𝐵 − 𝑍) / 𝑇)) = (((𝐸‘𝑊) − 𝑍) / 𝑇)) |
127 | 126 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (⌊‘((𝐵 − 𝑍) / 𝑇)) = (((𝐸‘𝑊) − 𝑍) / 𝑇)) |
128 | 66 | oveq1d 7228 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐸‘𝑊) − 𝑊) = ((𝑊 + ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) − 𝑊)) |
129 | 128 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐸‘𝑊) − 𝑊) / 𝑇) = (((𝑊 + ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) − 𝑊) / 𝑇)) |
130 | 21 | recnd 10861 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑊 ∈ ℂ) |
131 | 130, 70 | pncan2d 11191 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑊 + ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) − 𝑊) = ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) |
132 | 131 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑊 + ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) − 𝑊) / 𝑇) = (((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇) / 𝑇)) |
133 | 63 | recnd 10861 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (⌊‘((𝐵 − 𝑊) / 𝑇)) ∈ ℂ) |
134 | 133, 33, 60 | divcan4d 11614 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − 𝑊) / 𝑇))) |
135 | 129, 132,
134 | 3eqtrrd 2782 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (⌊‘((𝐵 − 𝑊) / 𝑇)) = (((𝐸‘𝑊) − 𝑊) / 𝑇)) |
136 | 135 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (⌊‘((𝐵 − 𝑊) / 𝑇)) = (((𝐸‘𝑊) − 𝑊) / 𝑇)) |
137 | 108, 127,
136 | 3brtr4d 5085 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (⌊‘((𝐵 − 𝑍) / 𝑇)) < (⌊‘((𝐵 − 𝑊) / 𝑇))) |
138 | 77 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (⌊‘((𝐵 − 𝑍) / 𝑇)) ∈ ℤ) |
139 | 62 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (⌊‘((𝐵 − 𝑊) / 𝑇)) ∈ ℤ) |
140 | | zltp1le 12227 |
. . . . . . . . . . . . 13
⊢
(((⌊‘((𝐵
− 𝑍) / 𝑇)) ∈ ℤ ∧
(⌊‘((𝐵 −
𝑊) / 𝑇)) ∈ ℤ) →
((⌊‘((𝐵 −
𝑍) / 𝑇)) < (⌊‘((𝐵 − 𝑊) / 𝑇)) ↔ ((⌊‘((𝐵 − 𝑍) / 𝑇)) + 1) ≤ (⌊‘((𝐵 − 𝑊) / 𝑇)))) |
141 | 138, 139,
140 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((⌊‘((𝐵 − 𝑍) / 𝑇)) < (⌊‘((𝐵 − 𝑊) / 𝑇)) ↔ ((⌊‘((𝐵 − 𝑍) / 𝑇)) + 1) ≤ (⌊‘((𝐵 − 𝑊) / 𝑇)))) |
142 | 137, 141 | mpbid 235 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((⌊‘((𝐵 − 𝑍) / 𝑇)) + 1) ≤ (⌊‘((𝐵 − 𝑊) / 𝑇))) |
143 | 97, 82, 80, 100, 142 | lemul1ad 11771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (((⌊‘((𝐵 − 𝑍) / 𝑇)) + 1) · 𝑇) ≤ ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) |
144 | 95, 143 | eqbrtrd 5075 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) + 𝑇) ≤ ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) |
145 | 91, 83, 80, 144 | lesub1dd 11448 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) + 𝑇) − 𝑇) ≤ (((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇) − 𝑇)) |
146 | 90, 145 | eqbrtrd 5075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇) ≤ (((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇) − 𝑇)) |
147 | 81, 84, 85, 146 | lesub2dd 11449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((𝐸‘𝑊) − (((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇) − 𝑇)) ≤ ((𝐸‘𝑊) − ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇))) |
148 | 74, 147 | eqbrtrd 5075 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (((𝐸‘𝑊) − ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) + 𝑇) ≤ ((𝐸‘𝑊) − ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇))) |
149 | 66 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → (𝑊 + ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) = (𝐸‘𝑊)) |
150 | 68, 70, 130 | subadd2d 11208 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐸‘𝑊) − ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) = 𝑊 ↔ (𝑊 + ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) = (𝐸‘𝑊))) |
151 | 149, 150 | mpbird 260 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸‘𝑊) − ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) = 𝑊) |
152 | 151 | eqcomd 2743 |
. . . . . . 7
⊢ (𝜑 → 𝑊 = ((𝐸‘𝑊) − ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇))) |
153 | 152 | oveq1d 7228 |
. . . . . 6
⊢ (𝜑 → (𝑊 + 𝑇) = (((𝐸‘𝑊) − ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) + 𝑇)) |
154 | 153 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (𝑊 + 𝑇) = (((𝐸‘𝑊) − ((⌊‘((𝐵 − 𝑊) / 𝑇)) · 𝑇)) + 𝑇)) |
155 | 118 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝜑 → (𝑍 + ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇)) = (𝐸‘𝑍)) |
156 | 1 | rexrd 10883 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
157 | | iocssre 13015 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴(,]𝐵) ⊆
ℝ) |
158 | 156, 5, 157 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ) |
159 | 1, 5, 56, 22, 46 | fourierdlem4 43327 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵)) |
160 | 159, 27 | ffvelrnd 6905 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸‘𝑍) ∈ (𝐴(,]𝐵)) |
161 | 158, 160 | sseldd 3902 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸‘𝑍) ∈ ℝ) |
162 | 161 | recnd 10861 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸‘𝑍) ∈ ℂ) |
163 | 162, 87, 121 | subadd2d 11208 |
. . . . . . . 8
⊢ (𝜑 → (((𝐸‘𝑍) − ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇)) = 𝑍 ↔ (𝑍 + ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇)) = (𝐸‘𝑍))) |
164 | 155, 163 | mpbird 260 |
. . . . . . 7
⊢ (𝜑 → ((𝐸‘𝑍) − ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇)) = 𝑍) |
165 | 109 | oveq1d 7228 |
. . . . . . 7
⊢ (𝜑 → ((𝐸‘𝑍) − ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇)) = ((𝐸‘𝑊) − ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇))) |
166 | 164, 165 | eqtr3d 2779 |
. . . . . 6
⊢ (𝜑 → 𝑍 = ((𝐸‘𝑊) − ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇))) |
167 | 166 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → 𝑍 = ((𝐸‘𝑊) − ((⌊‘((𝐵 − 𝑍) / 𝑇)) · 𝑇))) |
168 | 148, 154,
167 | 3brtr4d 5085 |
. . . 4
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (𝑊 + 𝑇) ≤ 𝑍) |
169 | 16, 26, 28, 45, 168 | ltletrd 10992 |
. . 3
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → (𝐵 + 𝑋) < 𝑍) |
170 | 16, 28 | ltnled 10979 |
. . 3
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ((𝐵 + 𝑋) < 𝑍 ↔ ¬ 𝑍 ≤ (𝐵 + 𝑋))) |
171 | 169, 170 | mpbid 235 |
. 2
⊢ ((𝜑 ∧ 𝑊 < 𝑍) → ¬ 𝑍 ≤ (𝐵 + 𝑋)) |
172 | 15, 171 | pm2.65da 817 |
1
⊢ (𝜑 → ¬ 𝑊 < 𝑍) |