Step | Hyp | Ref
| Expression |
1 | | fourierdlem79.q |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) |
2 | | fourierdlem79.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
3 | | fourierdlem79.p |
. . . . . . . . . 10
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
4 | 3 | fourierdlem2 41253 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
5 | 2, 4 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
6 | 1, 5 | mpbid 224 |
. . . . . . 7
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
7 | 6 | simpld 490 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑𝑚
(0...𝑀))) |
8 | | elmapi 8162 |
. . . . . 6
⊢ (𝑄 ∈ (ℝ
↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
9 | 7, 8 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
10 | 9 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑄:(0...𝑀)⟶ℝ) |
11 | | fourierdlem79.t |
. . . . . . . . 9
⊢ 𝑇 = (𝐵 − 𝐴) |
12 | | fourierdlem79.e |
. . . . . . . . 9
⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
13 | | fourierdlem79.l |
. . . . . . . . 9
⊢ 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦)) |
14 | | fourierdlem79.i |
. . . . . . . . 9
⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < )) |
15 | 3, 2, 1, 11, 12, 13, 14 | fourierdlem37 41288 |
. . . . . . . 8
⊢ (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}))) |
16 | 15 | simpld 490 |
. . . . . . 7
⊢ (𝜑 → 𝐼:ℝ⟶(0..^𝑀)) |
17 | | fzossfz 12807 |
. . . . . . . 8
⊢
(0..^𝑀) ⊆
(0...𝑀) |
18 | 17 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (0..^𝑀) ⊆ (0...𝑀)) |
19 | 16, 18 | fssd 6305 |
. . . . . 6
⊢ (𝜑 → 𝐼:ℝ⟶(0...𝑀)) |
20 | 19 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐼:ℝ⟶(0...𝑀)) |
21 | | fourierdlem79.c |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ℝ) |
22 | | fourierdlem79.d |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ∈ ℝ) |
23 | | fourierdlem79.cltd |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 < 𝐷) |
24 | | fourierdlem79.o |
. . . . . . . . . . . . 13
⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚
(0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
25 | | fourierdlem79.h |
. . . . . . . . . . . . 13
⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) |
26 | | fourierdlem79.n |
. . . . . . . . . . . . 13
⊢ 𝑁 = ((♯‘𝐻) − 1) |
27 | | fourierdlem79.s |
. . . . . . . . . . . . 13
⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) |
28 | 11, 3, 2, 1, 21, 22, 23, 24, 25, 26, 27 | fourierdlem54 41304 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻))) |
29 | 28 | simpld 490 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁))) |
30 | 29 | simprd 491 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁)) |
31 | 30 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (𝑂‘𝑁)) |
32 | 29 | simpld 490 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
33 | 32 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑁 ∈ ℕ) |
34 | 24 | fourierdlem2 41253 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) |
36 | 31, 35 | mpbid 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆 ∈ (ℝ ↑𝑚
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))) |
37 | 36 | simpld 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 ∈ (ℝ ↑𝑚
(0...𝑁))) |
38 | | elmapi 8162 |
. . . . . . 7
⊢ (𝑆 ∈ (ℝ
↑𝑚 (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ) |
39 | 37, 38 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆:(0...𝑁)⟶ℝ) |
40 | | elfzofz 12804 |
. . . . . . 7
⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ (0...𝑁)) |
41 | 40 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0...𝑁)) |
42 | 39, 41 | ffvelrnd 6624 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℝ) |
43 | 20, 42 | ffvelrnd 6624 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ (0...𝑀)) |
44 | 10, 43 | ffvelrnd 6624 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) ∈ ℝ) |
45 | 44 | rexrd 10426 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) ∈
ℝ*) |
46 | 16 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐼:ℝ⟶(0..^𝑀)) |
47 | 46, 42 | ffvelrnd 6624 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀)) |
48 | | fzofzp1 12884 |
. . . . 5
⊢ ((𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0...𝑀)) |
49 | 47, 48 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0...𝑀)) |
50 | 10, 49 | ffvelrnd 6624 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ) |
51 | 50 | rexrd 10426 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈
ℝ*) |
52 | 14 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ))) |
53 | | fveq2 6446 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑆‘𝑗) → (𝐸‘𝑥) = (𝐸‘(𝑆‘𝑗))) |
54 | 53 | fveq2d 6450 |
. . . . . . . . 9
⊢ (𝑥 = (𝑆‘𝑗) → (𝐿‘(𝐸‘𝑥)) = (𝐿‘(𝐸‘(𝑆‘𝑗)))) |
55 | 54 | breq2d 4898 |
. . . . . . . 8
⊢ (𝑥 = (𝑆‘𝑗) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥)) ↔ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))) |
56 | 55 | rabbidv 3386 |
. . . . . . 7
⊢ (𝑥 = (𝑆‘𝑗) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}) |
57 | 56 | supeq1d 8640 |
. . . . . 6
⊢ (𝑥 = (𝑆‘𝑗) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) |
58 | 57 | adantl 475 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑥 = (𝑆‘𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) |
59 | | ltso 10457 |
. . . . . . 7
⊢ < Or
ℝ |
60 | 59 | supex 8657 |
. . . . . 6
⊢
sup({𝑖 ∈
(0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈
V |
61 | 60 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈
V) |
62 | 52, 58, 42, 61 | fvmptd 6548 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) |
63 | 62 | fveq2d 6450 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))) |
64 | | simpl 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝜑) |
65 | 64, 42 | jca 507 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝜑 ∧ (𝑆‘𝑗) ∈ ℝ)) |
66 | | eleq1 2847 |
. . . . . . . . 9
⊢ (𝑥 = (𝑆‘𝑗) → (𝑥 ∈ ℝ ↔ (𝑆‘𝑗) ∈ ℝ)) |
67 | 66 | anbi2d 622 |
. . . . . . . 8
⊢ (𝑥 = (𝑆‘𝑗) → ((𝜑 ∧ 𝑥 ∈ ℝ) ↔ (𝜑 ∧ (𝑆‘𝑗) ∈ ℝ))) |
68 | 57, 56 | eleq12d 2853 |
. . . . . . . 8
⊢ (𝑥 = (𝑆‘𝑗) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ↔ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})) |
69 | 67, 68 | imbi12d 336 |
. . . . . . 7
⊢ (𝑥 = (𝑆‘𝑗) → (((𝜑 ∧ 𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}) ↔ ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}))) |
70 | 15 | simprd 491 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))})) |
71 | 70 | imp 397 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}) |
72 | 69, 71 | vtoclg 3467 |
. . . . . 6
⊢ ((𝑆‘𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))})) |
73 | 42, 65, 72 | sylc 65 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}) |
74 | | nfrab1 3309 |
. . . . . . 7
⊢
Ⅎ𝑖{𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} |
75 | | nfcv 2934 |
. . . . . . 7
⊢
Ⅎ𝑖ℝ |
76 | | nfcv 2934 |
. . . . . . 7
⊢
Ⅎ𝑖
< |
77 | 74, 75, 76 | nfsup 8645 |
. . . . . 6
⊢
Ⅎ𝑖sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) |
78 | | nfcv 2934 |
. . . . . 6
⊢
Ⅎ𝑖(0..^𝑀) |
79 | | nfcv 2934 |
. . . . . . . 8
⊢
Ⅎ𝑖𝑄 |
80 | 79, 77 | nffv 6456 |
. . . . . . 7
⊢
Ⅎ𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) |
81 | | nfcv 2934 |
. . . . . . 7
⊢
Ⅎ𝑖
≤ |
82 | | nfcv 2934 |
. . . . . . 7
⊢
Ⅎ𝑖(𝐿‘(𝐸‘(𝑆‘𝑗))) |
83 | 80, 81, 82 | nfbr 4933 |
. . . . . 6
⊢
Ⅎ𝑖(𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) |
84 | | fveq2 6446 |
. . . . . . 7
⊢ (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) → (𝑄‘𝑖) = (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ))) |
85 | 84 | breq1d 4896 |
. . . . . 6
⊢ (𝑖 = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ↔ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))) |
86 | 77, 78, 83, 85 | elrabf 3568 |
. . . . 5
⊢
(sup({𝑖 ∈
(0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ↔ (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))) |
87 | 73, 86 | sylib 210 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈ (0..^𝑀) ∧ (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))) |
88 | 87 | simprd 491 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) |
89 | 63, 88 | eqbrtrd 4908 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑄‘(𝐼‘(𝑆‘𝑗))) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) |
90 | 2 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑀 ∈ ℕ) |
91 | 1 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑄 ∈ (𝑃‘𝑀)) |
92 | 21 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐶 ∈ ℝ) |
93 | 22 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐷 ∈ ℝ) |
94 | 23 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐶 < 𝐷) |
95 | | 0le1 10898 |
. . . . . . . 8
⊢ 0 ≤
1 |
96 | 95 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 1) |
97 | 2 | nnge1d 11423 |
. . . . . . 7
⊢ (𝜑 → 1 ≤ 𝑀) |
98 | | 1zzd 11760 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℤ) |
99 | | 0zd 11740 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℤ) |
100 | 2 | nnzd 11833 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
101 | | elfz 12649 |
. . . . . . . 8
⊢ ((1
∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤
𝑀))) |
102 | 98, 99, 100, 101 | syl3anc 1439 |
. . . . . . 7
⊢ (𝜑 → (1 ∈ (0...𝑀) ↔ (0 ≤ 1 ∧ 1 ≤
𝑀))) |
103 | 96, 97, 102 | mpbir2and 703 |
. . . . . 6
⊢ (𝜑 → 1 ∈ (0...𝑀)) |
104 | 103 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 1 ∈ (0...𝑀)) |
105 | | simplr 759 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁)) |
106 | | fourierdlem79.z |
. . . . . . . 8
⊢ 𝑍 = ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) |
107 | | fzofzp1 12884 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (0..^𝑁) → (𝑗 + 1) ∈ (0...𝑁)) |
108 | 107 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 + 1) ∈ (0...𝑁)) |
109 | 39, 108 | ffvelrnd 6624 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℝ) |
110 | 109, 42 | resubcld 10803 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℝ) |
111 | 110 | rehalfcld 11629 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℝ) |
112 | 9, 103 | ffvelrnd 6624 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄‘1) ∈ ℝ) |
113 | 3, 2, 1 | fourierdlem11 41262 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)) |
114 | 113 | simp1d 1133 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℝ) |
115 | 112, 114 | resubcld 10803 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑄‘1) − 𝐴) ∈ ℝ) |
116 | 115 | rehalfcld 11629 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ) |
117 | 116 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ) |
118 | 111, 117 | ifcld 4352 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ) |
119 | 42, 118 | readdcld 10406 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ∈ ℝ) |
120 | 106, 119 | syl5eqel 2863 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ℝ) |
121 | | 2re 11449 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
122 | 121 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 2 ∈ ℝ) |
123 | | elfzoelz 12789 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℤ) |
124 | 123 | zred 11834 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 ∈ ℝ) |
125 | 124 | ltp1d 11308 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0..^𝑁) → 𝑗 < (𝑗 + 1)) |
126 | 125 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 < (𝑗 + 1)) |
127 | 28 | simprd 491 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻)) |
128 | 127 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝐻)) |
129 | | isorel 6848 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝑗 + 1) ∈ (0...𝑁))) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))) |
130 | 128, 41, 108, 129 | syl12anc 827 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑗 < (𝑗 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1)))) |
131 | 126, 130 | mpbid 224 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))) |
132 | 42, 109 | posdifd 10962 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ↔ 0 < ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))) |
133 | 131, 132 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))) |
134 | | 2pos 11485 |
. . . . . . . . . . . . . 14
⊢ 0 <
2 |
135 | 134 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < 2) |
136 | 110, 122,
133, 135 | divgt0d 11313 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) |
137 | 111, 136 | elrpd 12178 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈
ℝ+) |
138 | 121 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℝ) |
139 | 2 | nngt0d 11424 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 < 𝑀) |
140 | | fzolb 12795 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
(0..^𝑀) ↔ (0 ∈
ℤ ∧ 𝑀 ∈
ℤ ∧ 0 < 𝑀)) |
141 | 99, 100, 139, 140 | syl3anbrc 1400 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ∈ (0..^𝑀)) |
142 | | 0re 10378 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
143 | | eleq1 2847 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 0 → (𝑖 ∈ (0..^𝑀) ↔ 0 ∈ (0..^𝑀))) |
144 | 143 | anbi2d 622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 0 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 0 ∈ (0..^𝑀)))) |
145 | | fveq2 6446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0)) |
146 | | oveq1 6929 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1)) |
147 | 146 | fveq2d 6450 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 0 → (𝑄‘(𝑖 + 1)) = (𝑄‘(0 + 1))) |
148 | 145, 147 | breq12d 4899 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 0 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘0) < (𝑄‘(0 + 1)))) |
149 | 144, 148 | imbi12d 336 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 0 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))))) |
150 | 6 | simprd 491 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
151 | 150 | simprd 491 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
152 | 151 | r19.21bi 3114 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
153 | 149, 152 | vtoclg 3467 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ℝ → ((𝜑 ∧ 0
∈ (0..^𝑀)) →
(𝑄‘0) < (𝑄‘(0 +
1)))) |
154 | 142, 153 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 0 ∈ (0..^𝑀)) → (𝑄‘0) < (𝑄‘(0 + 1))) |
155 | 141, 154 | mpdan 677 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄‘0) < (𝑄‘(0 + 1))) |
156 | 150 | simpld 490 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵)) |
157 | 156 | simpld 490 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄‘0) = 𝐴) |
158 | | 0p1e1 11504 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 1) =
1 |
159 | 158 | fveq2i 6449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄‘(0 + 1)) = (𝑄‘1) |
160 | 159 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄‘(0 + 1)) = (𝑄‘1)) |
161 | 155, 157,
160 | 3brtr3d 4917 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 < (𝑄‘1)) |
162 | 114, 112 | posdifd 10962 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 < (𝑄‘1) ↔ 0 < ((𝑄‘1) − 𝐴))) |
163 | 161, 162 | mpbid 224 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < ((𝑄‘1) − 𝐴)) |
164 | 134 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 2) |
165 | 115, 138,
163, 164 | divgt0d 11313 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < (((𝑄‘1) − 𝐴) / 2)) |
166 | 116, 165 | elrpd 12178 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈
ℝ+) |
167 | 166 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ∈
ℝ+) |
168 | 137, 167 | ifcld 4352 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈
ℝ+) |
169 | 42, 168 | ltaddrpd 12214 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))) |
170 | 42, 119, 169 | ltled 10524 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))) |
171 | 170, 106 | syl6breqr 4928 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ 𝑍) |
172 | 42, 111 | readdcld 10406 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) ∈ ℝ) |
173 | | iftrue 4313 |
. . . . . . . . . . . . 13
⊢ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) |
174 | 173 | adantl 475 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) |
175 | 111 | leidd 10941 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) |
176 | 175 | adantr 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) |
177 | 174, 176 | eqbrtrd 4908 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) |
178 | | iffalse 4316 |
. . . . . . . . . . . . 13
⊢ (¬
((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2)) |
179 | 178 | adantl 475 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2)) |
180 | 115 | ad2antrr 716 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ) |
181 | 110 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℝ) |
182 | | 2rp 12142 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ+ |
183 | 182 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈
ℝ+) |
184 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) |
185 | 180, 181,
184 | nltled 10526 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ≤ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))) |
186 | 180, 181,
183, 185 | lediv1dd 12239 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) |
187 | 179, 186 | eqbrtrd 4908 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) |
188 | 177, 187 | pm2.61dan 803 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) |
189 | 118, 111,
42, 188 | leadd2dd 10990 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))) |
190 | 42 | recnd 10405 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ℂ) |
191 | 109 | recnd 10405 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈ ℂ) |
192 | 190, 191 | addcomd 10578 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) = ((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗))) |
193 | 192 | oveq1d 6937 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) = (((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2)) |
194 | 193 | oveq1d 6937 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))) |
195 | | halfaddsub 11615 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆‘(𝑗 + 1)) ∈ ℂ ∧ (𝑆‘𝑗) ∈ ℂ) → (((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗))) |
196 | 191, 190,
195 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘(𝑗 + 1)) ∧ ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗))) |
197 | 196 | simprd 491 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘(𝑗 + 1)) + (𝑆‘𝑗)) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗)) |
198 | 194, 197 | eqtrd 2814 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗)) |
199 | 190, 191 | addcld 10396 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) ∈ ℂ) |
200 | 199 | halfcld 11627 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) ∈ ℂ) |
201 | 111 | recnd 10405 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℂ) |
202 | 200, 201,
190 | subsub23d 40409 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (𝑆‘𝑗) ↔ ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆‘𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))) |
203 | 198, 202 | mpbid 224 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆‘𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) |
204 | 200, 190,
201 | subaddd 10752 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) − (𝑆‘𝑗)) = (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ↔ ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2))) |
205 | 203, 204 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) = (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2)) |
206 | | avglt2 11621 |
. . . . . . . . . . . 12
⊢ (((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ) → ((𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1)))) |
207 | 42, 109, 206 | syl2anc 579 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) < (𝑆‘(𝑗 + 1)) ↔ (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1)))) |
208 | 131, 207 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + (𝑆‘(𝑗 + 1))) / 2) < (𝑆‘(𝑗 + 1))) |
209 | 205, 208 | eqbrtrd 4908 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) < (𝑆‘(𝑗 + 1))) |
210 | 119, 172,
109, 189, 209 | lelttrd 10534 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑆‘(𝑗 + 1))) |
211 | 106, 210 | syl5eqbr 4921 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 < (𝑆‘(𝑗 + 1))) |
212 | 109 | rexrd 10426 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘(𝑗 + 1)) ∈
ℝ*) |
213 | | elico2 12549 |
. . . . . . . 8
⊢ (((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) →
(𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) ≤ 𝑍 ∧ 𝑍 < (𝑆‘(𝑗 + 1))))) |
214 | 42, 212, 213 | syl2anc 579 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) ≤ 𝑍 ∧ 𝑍 < (𝑆‘(𝑗 + 1))))) |
215 | 120, 171,
211, 214 | mpbir3and 1399 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1)))) |
216 | 215 | adantr 474 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1)))) |
217 | 114 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 ∈ ℝ) |
218 | 113 | simp2d 1134 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℝ) |
219 | 218 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ℝ) |
220 | 113 | simp3d 1135 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 < 𝐵) |
221 | 220 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐴 < 𝐵) |
222 | 42 | adantr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑆‘𝑗) ∈ ℝ) |
223 | | simpr 479 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) = 𝐵) |
224 | 169, 106 | syl6breqr 4928 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) < 𝑍) |
225 | 218, 114 | resubcld 10803 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
226 | 11, 225 | syl5eqel 2863 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ∈ ℝ) |
227 | 226 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑇 ∈ ℝ) |
228 | 111 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ∈ ℝ) |
229 | 116 | ad2antrr 716 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ∈ ℝ) |
230 | 110 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ∈ ℝ) |
231 | 115 | ad2antrr 716 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑄‘1) − 𝐴) ∈ ℝ) |
232 | 182 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → 2 ∈
ℝ+) |
233 | | simpr 479 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) |
234 | 230, 231,
232, 233 | ltdiv1dd 12238 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) < (((𝑄‘1) − 𝐴) / 2)) |
235 | 228, 229,
234 | ltled 10524 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2) ≤ (((𝑄‘1) − 𝐴) / 2)) |
236 | 174, 235 | eqbrtrd 4908 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2)) |
237 | 178 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) − 𝐴) / 2)) |
238 | 116 | leidd 10941 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2)) |
239 | 238 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (((𝑄‘1) − 𝐴) / 2) ≤ (((𝑄‘1) − 𝐴) / 2)) |
240 | 237, 239 | eqbrtrd 4908 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2)) |
241 | 240 | adantlr 705 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2)) |
242 | 236, 241 | pm2.61dan 803 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ (((𝑄‘1) − 𝐴) / 2)) |
243 | 225 | rehalfcld 11629 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐵 − 𝐴) / 2) ∈ ℝ) |
244 | 182 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ∈
ℝ+) |
245 | 114 | rexrd 10426 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
246 | 218 | rexrd 10426 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
247 | 3, 2, 1 | fourierdlem15 41266 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵)) |
248 | 247, 103 | ffvelrnd 6624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑄‘1) ∈ (𝐴[,]𝐵)) |
249 | | iccleub 12541 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ (𝑄‘1) ∈ (𝐴[,]𝐵)) → (𝑄‘1) ≤ 𝐵) |
250 | 245, 246,
248, 249 | syl3anc 1439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑄‘1) ≤ 𝐵) |
251 | 112, 218,
114, 250 | lesub1dd 10991 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑄‘1) − 𝐴) ≤ (𝐵 − 𝐴)) |
252 | 115, 225,
244, 251 | lediv1dd 12239 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ ((𝐵 − 𝐴) / 2)) |
253 | 11 | eqcomi 2787 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 − 𝐴) = 𝑇 |
254 | 253 | oveq1i 6932 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 − 𝐴) / 2) = (𝑇 / 2) |
255 | 114, 218 | posdifd 10962 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
256 | 220, 255 | mpbid 224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
257 | 256, 11 | syl6breqr 4928 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < 𝑇) |
258 | 226, 257 | elrpd 12178 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
259 | | rphalflt 12168 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ ℝ+
→ (𝑇 / 2) < 𝑇) |
260 | 258, 259 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑇 / 2) < 𝑇) |
261 | 254, 260 | syl5eqbr 4921 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐵 − 𝐴) / 2) < 𝑇) |
262 | 116, 243,
226, 252, 261 | lelttrd 10534 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑄‘1) − 𝐴) / 2) < 𝑇) |
263 | 116, 226,
262 | ltled 10524 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇) |
264 | 263 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑄‘1) − 𝐴) / 2) ≤ 𝑇) |
265 | 118, 117,
227, 242, 264 | letrd 10533 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ≤ 𝑇) |
266 | 118, 227,
42, 265 | leadd2dd 10990 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) ≤ ((𝑆‘𝑗) + 𝑇)) |
267 | 106, 266 | syl5eqbr 4921 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ≤ ((𝑆‘𝑗) + 𝑇)) |
268 | 42 | rexrd 10426 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈
ℝ*) |
269 | 42, 227 | readdcld 10406 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) + 𝑇) ∈ ℝ) |
270 | | elioc2 12548 |
. . . . . . . . . . 11
⊢ (((𝑆‘𝑗) ∈ ℝ* ∧ ((𝑆‘𝑗) + 𝑇) ∈ ℝ) → (𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) < 𝑍 ∧ 𝑍 ≤ ((𝑆‘𝑗) + 𝑇)))) |
271 | 268, 269,
270 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇)) ↔ (𝑍 ∈ ℝ ∧ (𝑆‘𝑗) < 𝑍 ∧ 𝑍 ≤ ((𝑆‘𝑗) + 𝑇)))) |
272 | 120, 224,
267, 271 | mpbir3and 1399 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇))) |
273 | 272 | adantr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑍 ∈ ((𝑆‘𝑗)(,]((𝑆‘𝑗) + 𝑇))) |
274 | 217, 219,
221, 11, 12, 222, 223, 273 | fourierdlem26 41277 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘𝑍) = (𝐴 + (𝑍 − (𝑆‘𝑗)))) |
275 | 106 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑍 = ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))) |
276 | 275 | oveq1d 6937 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑍 − (𝑆‘𝑗)) = (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))) |
277 | 276 | oveq2d 6938 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (𝑍 − (𝑆‘𝑗))) = (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗)))) |
278 | 277 | adantr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐴 + (𝑍 − (𝑆‘𝑗))) = (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗)))) |
279 | 118 | recnd 10405 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)) ∈ ℂ) |
280 | 190, 279 | pncan2d 10736 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗)) = if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) |
281 | 280 | oveq2d 6938 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))) |
282 | 281 | adantr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐴 + (((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) − (𝑆‘𝑗))) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))) |
283 | 274, 278,
282 | 3eqtrd 2818 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘𝑍) = (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))) |
284 | 173 | oveq2d 6938 |
. . . . . . . . . 10
⊢ (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))) |
285 | 284 | adantl 475 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2))) |
286 | 114 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ) |
287 | 286, 111 | readdcld 10406 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) ∈ ℝ) |
288 | 287 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) ∈ ℝ) |
289 | 286, 117 | readdcld 10406 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ) |
290 | 289 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) ∈ ℝ) |
291 | 112 | ad2antrr 716 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝑄‘1) ∈ ℝ) |
292 | 114 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → 𝐴 ∈ ℝ) |
293 | 228, 229,
292, 234 | ltadd2dd 10535 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) < (𝐴 + (((𝑄‘1) − 𝐴) / 2))) |
294 | 112 | recnd 10405 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑄‘1) ∈ ℂ) |
295 | 114 | recnd 10405 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℂ) |
296 | | halfaddsub 11615 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑄‘1) ∈ ℂ ∧
𝐴 ∈ ℂ) →
(((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴)) |
297 | 294, 295,
296 | syl2anc 579 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((((𝑄‘1) + 𝐴) / 2) + (((𝑄‘1) − 𝐴) / 2)) = (𝑄‘1) ∧ ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴)) |
298 | 297 | simprd 491 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) = 𝐴) |
299 | 298 | oveq1d 6937 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (𝐴 + (((𝑄‘1) − 𝐴) / 2))) |
300 | 112, 114 | readdcld 10406 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑄‘1) + 𝐴) ∈ ℝ) |
301 | 300 | rehalfcld 11629 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℝ) |
302 | 301 | recnd 10405 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑄‘1) + 𝐴) / 2) ∈ ℂ) |
303 | 116 | recnd 10405 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑄‘1) − 𝐴) / 2) ∈ ℂ) |
304 | 302, 303 | npcand 10738 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((((𝑄‘1) + 𝐴) / 2) − (((𝑄‘1) − 𝐴) / 2)) + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2)) |
305 | 299, 304 | eqtr3d 2816 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) = (((𝑄‘1) + 𝐴) / 2)) |
306 | 112, 112 | readdcld 10406 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑄‘1) + (𝑄‘1)) ∈ ℝ) |
307 | 114, 112,
112, 161 | ltadd2dd 10535 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑄‘1) + 𝐴) < ((𝑄‘1) + (𝑄‘1))) |
308 | 300, 306,
244, 307 | ltdiv1dd 12238 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (((𝑄‘1) + (𝑄‘1)) / 2)) |
309 | 294 | 2timesd 11625 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 · (𝑄‘1)) = ((𝑄‘1) + (𝑄‘1))) |
310 | 309 | eqcomd 2784 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑄‘1) + (𝑄‘1)) = (2 · (𝑄‘1))) |
311 | 310 | oveq1d 6937 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = ((2 · (𝑄‘1)) /
2)) |
312 | | 2cnd 11453 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℂ) |
313 | | 2ne0 11486 |
. . . . . . . . . . . . . . . 16
⊢ 2 ≠
0 |
314 | 313 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ≠ 0) |
315 | 294, 312,
314 | divcan3d 11156 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · (𝑄‘1)) / 2) = (𝑄‘1)) |
316 | 311, 315 | eqtrd 2814 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑄‘1) + (𝑄‘1)) / 2) = (𝑄‘1)) |
317 | 308, 316 | breqtrd 4912 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑄‘1) + 𝐴) / 2) < (𝑄‘1)) |
318 | 305, 317 | eqbrtrd 4908 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1)) |
319 | 318 | ad2antrr 716 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1)) |
320 | 288, 290,
291, 293, 319 | lttrd 10537 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2)) < (𝑄‘1)) |
321 | 285, 320 | eqbrtrd 4908 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1)) |
322 | 178 | oveq2d 6938 |
. . . . . . . . . 10
⊢ (¬
((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2))) |
323 | 322 | adantl 475 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = (𝐴 + (((𝑄‘1) − 𝐴) / 2))) |
324 | 318 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + (((𝑄‘1) − 𝐴) / 2)) < (𝑄‘1)) |
325 | 323, 324 | eqbrtrd 4908 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1)) |
326 | 321, 325 | pm2.61dan 803 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1)) |
327 | 326 | adantr 474 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐴 + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) < (𝑄‘1)) |
328 | 283, 327 | eqbrtrd 4908 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘𝑍) < (𝑄‘1)) |
329 | | eqid 2778 |
. . . . 5
⊢ ((𝑄‘1) − ((𝐸‘𝑍) − 𝑍)) = ((𝑄‘1) − ((𝐸‘𝑍) − 𝑍)) |
330 | 11, 3, 90, 91, 92, 93, 94, 24, 25, 26, 27, 12, 104, 105, 216, 328, 329 | fourierdlem63 41313 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘1)) |
331 | 14 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ))) |
332 | 57 | adantl 475 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ 𝑥 = (𝑆‘𝑗)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) |
333 | 60 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) ∈
V) |
334 | 331, 332,
222, 333 | fvmptd 6548 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐼‘(𝑆‘𝑗)) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) |
335 | | fveq2 6446 |
. . . . . . . . . . . . 13
⊢ ((𝐸‘(𝑆‘𝑗)) = 𝐵 → (𝐿‘(𝐸‘(𝑆‘𝑗))) = (𝐿‘𝐵)) |
336 | 13 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))) |
337 | | iftrue 4313 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝐵 → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴) |
338 | 337 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝐴) |
339 | | ubioc1 12539 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
< 𝐵) → 𝐵 ∈ (𝐴(,]𝐵)) |
340 | 245, 246,
220, 339 | syl3anc 1439 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ (𝐴(,]𝐵)) |
341 | 336, 338,
340, 114 | fvmptd 6548 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿‘𝐵) = 𝐴) |
342 | 335, 341 | sylan9eqr 2836 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) = 𝐴) |
343 | 342 | breq2d 4898 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ↔ (𝑄‘𝑖) ≤ 𝐴)) |
344 | 343 | rabbidv 3386 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} = {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) |
345 | 344 | supeq1d 8640 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < )) |
346 | 345 | adantlr 705 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < )) |
347 | | simpl 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝜑) |
348 | | elrabi 3567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} → 𝑗 ∈ (0..^𝑀)) |
349 | 348 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝑗 ∈ (0..^𝑀)) |
350 | | fveq2 6446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗)) |
351 | 350 | breq1d 4896 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) ≤ 𝐴 ↔ (𝑄‘𝑗) ≤ 𝐴)) |
352 | 351 | elrab 3572 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ↔ (𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴)) |
353 | 352 | simprbi 492 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} → (𝑄‘𝑗) ≤ 𝐴) |
354 | 353 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → (𝑄‘𝑗) ≤ 𝐴) |
355 | | simp3 1129 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → (𝑄‘𝑗) ≤ 𝐴) |
356 | 114 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 ∈ ℝ) |
357 | 112 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ∈ ℝ) |
358 | 9 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
359 | 18 | sselda 3821 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀)) |
360 | 358, 359 | ffvelrnd 6624 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (𝑄‘𝑗) ∈ ℝ) |
361 | 360 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘𝑗) ∈ ℝ) |
362 | 161 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄‘1)) |
363 | | 1zzd 11760 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ∈
ℤ) |
364 | | elfzoelz 12789 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ) |
365 | 364 | ad2antlr 717 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℤ) |
366 | | 1e0p1 11888 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 = (0 +
1) |
367 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ 𝑗 ≤ 0) |
368 | | 0red 10380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈
ℝ) |
369 | 365 | zred 11834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈ ℝ) |
370 | 368, 369 | ltnled 10523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ ¬ 𝑗 ≤ 0)) |
371 | 367, 370 | mpbird 249 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 < 𝑗) |
372 | | 0zd 11740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 0 ∈
ℤ) |
373 | | zltp1le 11779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((0
∈ ℤ ∧ 𝑗
∈ ℤ) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗)) |
374 | 372, 365,
373 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 < 𝑗 ↔ (0 + 1) ≤ 𝑗)) |
375 | 371, 374 | mpbid 224 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (0 + 1) ≤ 𝑗) |
376 | 366, 375 | syl5eqbr 4921 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 1 ≤ 𝑗) |
377 | | eluz2 11998 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤
𝑗)) |
378 | 363, 365,
376, 377 | syl3anbrc 1400 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝑗 ∈
(ℤ≥‘1)) |
379 | 9 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑄:(0...𝑀)⟶ℝ) |
380 | | 0red 10380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑙 ∈ (1...𝑗) → 0 ∈ ℝ) |
381 | | elfzelz 12659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℤ) |
382 | 381 | zred 11834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑙 ∈ (1...𝑗) → 𝑙 ∈ ℝ) |
383 | | 1red 10377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑙 ∈ (1...𝑗) → 1 ∈ ℝ) |
384 | | 0lt1 10897 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 0 <
1 |
385 | 384 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑙 ∈ (1...𝑗) → 0 < 1) |
386 | | elfzle1 12661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑙 ∈ (1...𝑗) → 1 ≤ 𝑙) |
387 | 380, 383,
382, 385, 386 | ltletrd 10536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑙 ∈ (1...𝑗) → 0 < 𝑙) |
388 | 380, 382,
387 | ltled 10524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑙 ∈ (1...𝑗) → 0 ≤ 𝑙) |
389 | 388 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ≤ 𝑙) |
390 | 382 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℝ) |
391 | 100 | zred 11834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑀 ∈ ℝ) |
392 | 391 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℝ) |
393 | 364 | zred 11834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ) |
394 | 393 | ad2antlr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 ∈ ℝ) |
395 | | elfzle2 12662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑙 ∈ (1...𝑗) → 𝑙 ≤ 𝑗) |
396 | 395 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ≤ 𝑗) |
397 | | elfzolt2 12798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 < 𝑀) |
398 | 397 | ad2antlr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑗 < 𝑀) |
399 | 390, 394,
392, 396, 398 | lelttrd 10534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 < 𝑀) |
400 | 390, 392,
399 | ltled 10524 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ≤ 𝑀) |
401 | 381 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ ℤ) |
402 | | 0zd 11740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 0 ∈ ℤ) |
403 | 100 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑀 ∈ ℤ) |
404 | | elfz 12649 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑙 ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑀 ∈
ℤ) → (𝑙 ∈
(0...𝑀) ↔ (0 ≤
𝑙 ∧ 𝑙 ≤ 𝑀))) |
405 | 401, 402,
403, 404 | syl3anc 1439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑙 ∈ (0...𝑀) ↔ (0 ≤ 𝑙 ∧ 𝑙 ≤ 𝑀))) |
406 | 389, 400,
405 | mpbir2and 703 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑙 ∈ (0...𝑀)) |
407 | 379, 406 | ffvelrnd 6624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄‘𝑙) ∈ ℝ) |
408 | 407 | adantlr 705 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...𝑗)) → (𝑄‘𝑙) ∈ ℝ) |
409 | 9 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑄:(0...𝑀)⟶ℝ) |
410 | | 0zd 11740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈
ℤ) |
411 | 100 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ) |
412 | | elfzelz 12659 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℤ) |
413 | 412 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ) |
414 | 410, 411,
413 | 3jca 1119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (0 ∈ ℤ ∧
𝑀 ∈ ℤ ∧
𝑙 ∈
ℤ)) |
415 | | 0red 10380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → 0 ∈
ℝ) |
416 | 412 | zred 11834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ∈ ℝ) |
417 | | 1red 10377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈
ℝ) |
418 | 384 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → 0 <
1) |
419 | | elfzle1 12661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → 1 ≤ 𝑙) |
420 | 415, 417,
416, 418, 419 | ltletrd 10536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → 0 < 𝑙) |
421 | 415, 416,
420 | ltled 10524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ 𝑙) |
422 | 421 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙) |
423 | 413 | zred 11834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ) |
424 | 391 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ) |
425 | 393 | ad2antlr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ) |
426 | 416 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℝ) |
427 | | peano2rem 10690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑗 ∈ ℝ → (𝑗 − 1) ∈
ℝ) |
428 | 393, 427 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℝ) |
429 | 428 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) ∈ ℝ) |
430 | 393 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 ∈ ℝ) |
431 | | elfzle2 12662 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → 𝑙 ≤ (𝑗 − 1)) |
432 | 431 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ≤ (𝑗 − 1)) |
433 | 430 | ltm1d 11310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑗 − 1) < 𝑗) |
434 | 426, 429,
430, 432, 433 | lelttrd 10534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗) |
435 | 434 | adantll 704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑗) |
436 | 397 | ad2antlr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀) |
437 | 423, 425,
424, 435, 436 | lttrd 10537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀) |
438 | 423, 424,
437 | ltled 10524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ≤ 𝑀) |
439 | 414, 422,
438 | jca32 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((0 ∈ ℤ ∧
𝑀 ∈ ℤ ∧
𝑙 ∈ ℤ) ∧ (0
≤ 𝑙 ∧ 𝑙 ≤ 𝑀))) |
440 | | elfz2 12650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑙 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑙 ∈ ℤ) ∧ (0 ≤
𝑙 ∧ 𝑙 ≤ 𝑀))) |
441 | 439, 440 | sylibr 226 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0...𝑀)) |
442 | 409, 441 | ffvelrnd 6624 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) ∈ ℝ) |
443 | 413 | peano2zd 11837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℤ) |
444 | 410, 411,
443 | 3jca 1119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (0 ∈ ℤ ∧
𝑀 ∈ ℤ ∧
(𝑙 + 1) ∈
ℤ)) |
445 | 416, 417 | readdcld 10406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℝ) |
446 | 416, 417,
420, 418 | addgt0d 10950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → 0 < (𝑙 + 1)) |
447 | 415, 445,
446 | ltled 10524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → 0 ≤ (𝑙 + 1)) |
448 | 447 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ (𝑙 + 1)) |
449 | 445 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ ℝ) |
450 | 445 | recnd 10405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ∈ ℂ) |
451 | | 1cnd 10371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → 1 ∈
ℂ) |
452 | 450, 451 | npcand 10738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → (((𝑙 + 1) − 1) + 1) = (𝑙 + 1)) |
453 | 452 | eqcomd 2784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1)) |
454 | 453 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) = (((𝑙 + 1) − 1) + 1)) |
455 | | peano2re 10549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑙 ∈ ℝ → (𝑙 + 1) ∈
ℝ) |
456 | | peano2rem 10690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑙 + 1) ∈ ℝ →
((𝑙 + 1) − 1) ∈
ℝ) |
457 | 426, 455,
456 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ∈
ℝ) |
458 | | peano2re 10549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑗 − 1) ∈ ℝ
→ ((𝑗 − 1) + 1)
∈ ℝ) |
459 | | peano2rem 10690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑗 − 1) + 1) ∈ ℝ
→ (((𝑗 − 1) + 1)
− 1) ∈ ℝ) |
460 | 429, 458,
459 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑗 − 1) + 1) − 1) ∈
ℝ) |
461 | | 1red 10377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 1 ∈
ℝ) |
462 | | elfzel2 12657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℤ) |
463 | 462 | zred 11834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → (𝑗 − 1) ∈ ℝ) |
464 | 463, 417 | readdcld 10406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑗 − 1) + 1) ∈
ℝ) |
465 | 416, 463,
417, 431 | leadd1dd 10989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → (𝑙 + 1) ≤ ((𝑗 − 1) + 1)) |
466 | 445, 464,
417, 465 | lesub1dd 10991 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑙 ∈ (1...(𝑗 − 1)) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1)) |
467 | 466 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((𝑙 + 1) − 1) ≤ (((𝑗 − 1) + 1) − 1)) |
468 | 457, 460,
461, 467 | leadd1dd 10989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ ((((𝑗 − 1) + 1) − 1) +
1)) |
469 | | peano2zm 11772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑗 ∈ ℤ → (𝑗 − 1) ∈
ℤ) |
470 | 364, 469 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑗 ∈ (0..^𝑀) → (𝑗 − 1) ∈ ℤ) |
471 | 470 | peano2zd 11837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈
ℤ) |
472 | 471 | zcnd 11835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) ∈
ℂ) |
473 | | 1cnd 10371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ (0..^𝑀) → 1 ∈ ℂ) |
474 | 472, 473 | npcand 10738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = ((𝑗 − 1) +
1)) |
475 | 393 | recnd 10405 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℂ) |
476 | 475, 473 | npcand 10738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑗 ∈ (0..^𝑀) → ((𝑗 − 1) + 1) = 𝑗) |
477 | 474, 476 | eqtrd 2814 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑗 ∈ (0..^𝑀) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗) |
478 | 477 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((((𝑗 − 1) + 1) − 1) + 1) = 𝑗) |
479 | 468, 478 | breqtrd 4912 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (((𝑙 + 1) − 1) + 1) ≤ 𝑗) |
480 | 454, 479 | eqbrtrd 4908 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗) |
481 | 480 | adantll 704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑗) |
482 | 449, 425,
424, 481, 436 | lelttrd 10534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) < 𝑀) |
483 | 449, 424,
482 | ltled 10524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ≤ 𝑀) |
484 | 444, 448,
483 | jca32 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → ((0 ∈ ℤ ∧
𝑀 ∈ ℤ ∧
(𝑙 + 1) ∈ ℤ)
∧ (0 ≤ (𝑙 + 1) ∧
(𝑙 + 1) ≤ 𝑀))) |
485 | | elfz2 12650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑙 + 1) ∈ (0...𝑀) ↔ ((0 ∈ ℤ
∧ 𝑀 ∈ ℤ
∧ (𝑙 + 1) ∈
ℤ) ∧ (0 ≤ (𝑙 +
1) ∧ (𝑙 + 1) ≤ 𝑀))) |
486 | 484, 485 | sylibr 226 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑙 + 1) ∈ (0...𝑀)) |
487 | 409, 486 | ffvelrnd 6624 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘(𝑙 + 1)) ∈ ℝ) |
488 | | simpll 757 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝜑) |
489 | | 0zd 11740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ∈
ℤ) |
490 | 412 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ ℤ) |
491 | 421 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 0 ≤ 𝑙) |
492 | | eluz2 11998 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑙 ∈
(ℤ≥‘0) ↔ (0 ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ 0 ≤
𝑙)) |
493 | 489, 490,
491, 492 | syl3anbrc 1400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈
(ℤ≥‘0)) |
494 | | elfzoel2 12788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ (0..^𝑀) → 𝑀 ∈ ℤ) |
495 | 494 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℤ) |
496 | 495 | zred 11834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑀 ∈ ℝ) |
497 | 397 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑗 < 𝑀) |
498 | 426, 430,
496, 434, 497 | lttrd 10537 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 < 𝑀) |
499 | | elfzo2 12792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑙 ∈ (0..^𝑀) ↔ (𝑙 ∈ (ℤ≥‘0)
∧ 𝑀 ∈ ℤ
∧ 𝑙 < 𝑀)) |
500 | 493, 495,
498, 499 | syl3anbrc 1400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ (0..^𝑀) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀)) |
501 | 500 | adantll 704 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → 𝑙 ∈ (0..^𝑀)) |
502 | | eleq1 2847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 = 𝑙 → (𝑖 ∈ (0..^𝑀) ↔ 𝑙 ∈ (0..^𝑀))) |
503 | 502 | anbi2d 622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 = 𝑙 → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑙 ∈ (0..^𝑀)))) |
504 | | fveq2 6446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 = 𝑙 → (𝑄‘𝑖) = (𝑄‘𝑙)) |
505 | | oveq1 6929 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑖 = 𝑙 → (𝑖 + 1) = (𝑙 + 1)) |
506 | 505 | fveq2d 6450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 = 𝑙 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑙 + 1))) |
507 | 504, 506 | breq12d 4899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑖 = 𝑙 → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘𝑙) < (𝑄‘(𝑙 + 1)))) |
508 | 503, 507 | imbi12d 336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 = 𝑙 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) ↔ ((𝜑 ∧ 𝑙 ∈ (0..^𝑀)) → (𝑄‘𝑙) < (𝑄‘(𝑙 + 1))))) |
509 | 508, 152 | chvarv 2361 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑙 ∈ (0..^𝑀)) → (𝑄‘𝑙) < (𝑄‘(𝑙 + 1))) |
510 | 488, 501,
509 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) < (𝑄‘(𝑙 + 1))) |
511 | 442, 487,
510 | ltled 10524 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) ≤ (𝑄‘(𝑙 + 1))) |
512 | 511 | adantlr 705 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) ∧ 𝑙 ∈ (1...(𝑗 − 1))) → (𝑄‘𝑙) ≤ (𝑄‘(𝑙 + 1))) |
513 | 378, 408,
512 | monoord 13149 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝑄‘1) ≤ (𝑄‘𝑗)) |
514 | 356, 357,
361, 362, 513 | ltletrd 10536 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → 𝐴 < (𝑄‘𝑗)) |
515 | 356, 361 | ltnled 10523 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → (𝐴 < (𝑄‘𝑗) ↔ ¬ (𝑄‘𝑗) ≤ 𝐴)) |
516 | 514, 515 | mpbid 224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) ∧ ¬ 𝑗 ≤ 0) → ¬ (𝑄‘𝑗) ≤ 𝐴) |
517 | 516 | ex 403 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀)) → (¬ 𝑗 ≤ 0 → ¬ (𝑄‘𝑗) ≤ 𝐴)) |
518 | 517 | 3adant3 1123 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → (¬ 𝑗 ≤ 0 → ¬ (𝑄‘𝑗) ≤ 𝐴)) |
519 | 355, 518 | mt4d 154 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 𝑗 ≤ 0) |
520 | | elfzole1 12797 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (0..^𝑀) → 0 ≤ 𝑗) |
521 | 520 | 3ad2ant2 1125 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 0 ≤ 𝑗) |
522 | 393 | 3ad2ant2 1125 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 𝑗 ∈ ℝ) |
523 | | 0red 10380 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 0 ∈ ℝ) |
524 | 522, 523 | letri3d 10518 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → (𝑗 = 0 ↔ (𝑗 ≤ 0 ∧ 0 ≤ 𝑗))) |
525 | 519, 521,
524 | mpbir2and 703 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑀) ∧ (𝑄‘𝑗) ≤ 𝐴) → 𝑗 = 0) |
526 | 347, 349,
354, 525 | syl3anc 1439 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝑗 = 0) |
527 | | velsn 4414 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ {0} ↔ 𝑗 = 0) |
528 | 526, 527 | sylibr 226 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) → 𝑗 ∈ {0}) |
529 | 528 | ralrimiva 3148 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}𝑗 ∈ {0}) |
530 | | dfss3 3810 |
. . . . . . . . . . . . 13
⊢ ({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ⊆ {0} ↔ ∀𝑗 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}𝑗 ∈ {0}) |
531 | 529, 530 | sylibr 226 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ⊆ {0}) |
532 | 157, 114 | eqeltrd 2859 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄‘0) ∈ ℝ) |
533 | 532, 157 | eqled 10479 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑄‘0) ≤ 𝐴) |
534 | 145 | breq1d 4896 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 0 → ((𝑄‘𝑖) ≤ 𝐴 ↔ (𝑄‘0) ≤ 𝐴)) |
535 | 534 | elrab 3572 |
. . . . . . . . . . . . . 14
⊢ (0 ∈
{𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ 𝐴)) |
536 | 141, 533,
535 | sylanbrc 578 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) |
537 | 536 | snssd 4571 |
. . . . . . . . . . . 12
⊢ (𝜑 → {0} ⊆ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}) |
538 | 531, 537 | eqssd 3838 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴} = {0}) |
539 | 538 | supeq1d 8640 |
. . . . . . . . . 10
⊢ (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ) = sup({0}, ℝ, <
)) |
540 | | supsn 8666 |
. . . . . . . . . . . 12
⊢ (( <
Or ℝ ∧ 0 ∈ ℝ) → sup({0}, ℝ, < ) =
0) |
541 | 59, 142, 540 | mp2an 682 |
. . . . . . . . . . 11
⊢ sup({0},
ℝ, < ) = 0 |
542 | 541 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → sup({0}, ℝ, < ) =
0) |
543 | 539, 542 | eqtrd 2814 |
. . . . . . . . 9
⊢ (𝜑 → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ) = 0) |
544 | 543 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ 𝐴}, ℝ, < ) = 0) |
545 | 334, 346,
544 | 3eqtrd 2818 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐼‘(𝑆‘𝑗)) = 0) |
546 | 545 | oveq1d 6937 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → ((𝐼‘(𝑆‘𝑗)) + 1) = (0 + 1)) |
547 | 546 | fveq2d 6450 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) = (𝑄‘(0 + 1))) |
548 | 547, 159 | syl6req 2831 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝑄‘1) = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
549 | 330, 548 | breqtrd 4912 |
. . 3
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
550 | 65 | adantr 474 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝜑 ∧ (𝑆‘𝑗) ∈ ℝ)) |
551 | | simplr 759 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝑗 ∈ (0..^𝑁)) |
552 | 13 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))) |
553 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
(𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 = (𝐸‘(𝑆‘𝑗))) |
554 | | neqne 2977 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(𝐸‘(𝑆‘𝑗)) = 𝐵 → (𝐸‘(𝑆‘𝑗)) ≠ 𝐵) |
555 | 554 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
(𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → (𝐸‘(𝑆‘𝑗)) ≠ 𝐵) |
556 | 553, 555 | eqnetrd 3036 |
. . . . . . . . . . . . . . 15
⊢ ((¬
(𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → 𝑦 ≠ 𝐵) |
557 | 556 | neneqd 2974 |
. . . . . . . . . . . . . 14
⊢ ((¬
(𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → ¬ 𝑦 = 𝐵) |
558 | 557 | iffalsed 4318 |
. . . . . . . . . . . . 13
⊢ ((¬
(𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = 𝑦) |
559 | 558, 553 | eqtrd 2814 |
. . . . . . . . . . . 12
⊢ ((¬
(𝐸‘(𝑆‘𝑗)) = 𝐵 ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆‘𝑗))) |
560 | 559 | adantll 704 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ 𝑦 = (𝐸‘(𝑆‘𝑗))) → if(𝑦 = 𝐵, 𝐴, 𝑦) = (𝐸‘(𝑆‘𝑗))) |
561 | 114, 218,
220, 11, 12 | fourierdlem4 41255 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵)) |
562 | 561 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐸:ℝ⟶(𝐴(,]𝐵)) |
563 | 562, 42 | ffvelrnd 6624 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵)) |
564 | 563 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵)) |
565 | 552, 560,
564, 564 | fvmptd 6548 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) = (𝐸‘(𝑆‘𝑗))) |
566 | 565 | eqcomd 2784 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) = (𝐿‘(𝐸‘(𝑆‘𝑗)))) |
567 | 114, 218,
220, 13 | fourierdlem17 41268 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵)) |
568 | 567 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶(𝐴[,]𝐵)) |
569 | 114, 218 | iccssred 40639 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
570 | 569 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ ℝ) |
571 | 568, 570 | fssd 6305 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐿:(𝐴(,]𝐵)⟶ℝ) |
572 | 571, 563 | ffvelrnd 6624 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) ∈ ℝ) |
573 | 572 | adantr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐿‘(𝐸‘(𝑆‘𝑗))) ∈ ℝ) |
574 | 566, 573 | eqeltrd 2859 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ∈ ℝ) |
575 | 218 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ∈ ℝ) |
576 | 245 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈
ℝ*) |
577 | 218 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℝ) |
578 | | elioc2 12548 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ ((𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵))) |
579 | 576, 577,
578 | syl2anc 579 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵))) |
580 | 563, 579 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘𝑗)) ∈ ℝ ∧ 𝐴 < (𝐸‘(𝑆‘𝑗)) ∧ (𝐸‘(𝑆‘𝑗)) ≤ 𝐵)) |
581 | 580 | simp3d 1135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘𝑗)) ≤ 𝐵) |
582 | 581 | adantr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) ≤ 𝐵) |
583 | 554 | necomd 3024 |
. . . . . . . . 9
⊢ (¬
(𝐸‘(𝑆‘𝑗)) = 𝐵 → 𝐵 ≠ (𝐸‘(𝑆‘𝑗))) |
584 | 583 | adantl 475 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → 𝐵 ≠ (𝐸‘(𝑆‘𝑗))) |
585 | 574, 575,
582, 584 | leneltd 10530 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) < 𝐵) |
586 | 585 | adantr 474 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) < 𝐵) |
587 | | oveq1 6929 |
. . . . . . . . . . 11
⊢ ((𝐼‘(𝑆‘𝑗)) = (𝑀 − 1) → ((𝐼‘(𝑆‘𝑗)) + 1) = ((𝑀 − 1) + 1)) |
588 | 2 | nncnd 11392 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℂ) |
589 | | 1cnd 10371 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
590 | 588, 589 | npcand 10738 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀) |
591 | 587, 590 | sylan9eqr 2836 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) = 𝑀) |
592 | 591 | fveq2d 6450 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) = (𝑄‘𝑀)) |
593 | 156 | simprd 491 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄‘𝑀) = 𝐵) |
594 | 593 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑄‘𝑀) = 𝐵) |
595 | 592, 594 | eqtr2d 2815 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
596 | 595 | adantlr 705 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
597 | 596 | adantlr 705 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝐵 = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
598 | 586, 597 | breqtrd 4912 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
599 | 566 | adantr 474 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) = (𝐿‘(𝐸‘(𝑆‘𝑗)))) |
600 | | ssrab2 3908 |
. . . . . . . . . . . . 13
⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ (0..^𝑀) |
601 | | fzssz 12660 |
. . . . . . . . . . . . . . 15
⊢
(0...𝑀) ⊆
ℤ |
602 | 17, 601 | sstri 3830 |
. . . . . . . . . . . . . 14
⊢
(0..^𝑀) ⊆
ℤ |
603 | | zssre 11735 |
. . . . . . . . . . . . . 14
⊢ ℤ
⊆ ℝ |
604 | 602, 603 | sstri 3830 |
. . . . . . . . . . . . 13
⊢
(0..^𝑀) ⊆
ℝ |
605 | 600, 604 | sstri 3830 |
. . . . . . . . . . . 12
⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ |
606 | 605 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ) |
607 | 56 | neeq1d 3028 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑆‘𝑗) → ({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅ ↔ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅)) |
608 | 67, 607 | imbi12d 336 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑆‘𝑗) → (((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅) ↔ ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅))) |
609 | 141 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ (0..^𝑀)) |
610 | 533 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ 𝐴) |
611 | | iftrue 4313 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐸‘𝑥) = 𝐵 → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) = 𝐴) |
612 | 611 | eqcomd 2784 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸‘𝑥) = 𝐵 → 𝐴 = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
613 | 612 | adantl 475 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → 𝐴 = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
614 | 610, 613 | breqtrd 4912 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
615 | 532 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ∈ ℝ) |
616 | 114 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ) |
617 | 616 | rexrd 10426 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈
ℝ*) |
618 | 218 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐵 ∈ ℝ) |
619 | | iocssre 12565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴(,]𝐵) ⊆
ℝ) |
620 | 617, 618,
619 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ) |
621 | 561 | ffvelrnda 6623 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ (𝐴(,]𝐵)) |
622 | 620, 621 | sseldd 3822 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐸‘𝑥) ∈ ℝ) |
623 | 157 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) = 𝐴) |
624 | | elioc2 12548 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ ((𝐸‘𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵))) |
625 | 617, 618,
624 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐸‘𝑥) ∈ (𝐴(,]𝐵) ↔ ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵))) |
626 | 621, 625 | mpbid 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐸‘𝑥) ∈ ℝ ∧ 𝐴 < (𝐸‘𝑥) ∧ (𝐸‘𝑥) ≤ 𝐵)) |
627 | 626 | simp2d 1134 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 < (𝐸‘𝑥)) |
628 | 623, 627 | eqbrtrd 4908 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) < (𝐸‘𝑥)) |
629 | 615, 622,
628 | ltled 10524 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐸‘𝑥)) |
630 | 629 | adantr 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ (𝐸‘𝑥)) |
631 | | iffalse 4316 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
(𝐸‘𝑥) = 𝐵 → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) = (𝐸‘𝑥)) |
632 | 631 | eqcomd 2784 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
(𝐸‘𝑥) = 𝐵 → (𝐸‘𝑥) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
633 | 632 | adantl 475 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝐸‘𝑥) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
634 | 630, 633 | breqtrd 4912 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ¬ (𝐸‘𝑥) = 𝐵) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
635 | 614, 634 | pm2.61dan 803 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
636 | 13 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))) |
637 | | eqeq1 2782 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝐸‘𝑥) → (𝑦 = 𝐵 ↔ (𝐸‘𝑥) = 𝐵)) |
638 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝐸‘𝑥) → 𝑦 = (𝐸‘𝑥)) |
639 | 637, 638 | ifbieq2d 4332 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝐸‘𝑥) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
640 | 639 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 = (𝐸‘𝑥)) → if(𝑦 = 𝐵, 𝐴, 𝑦) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
641 | 616, 622 | ifcld 4352 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥)) ∈ ℝ) |
642 | 636, 640,
621, 641 | fvmptd 6548 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐿‘(𝐸‘𝑥)) = if((𝐸‘𝑥) = 𝐵, 𝐴, (𝐸‘𝑥))) |
643 | 635, 642 | breqtrrd 4914 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥))) |
644 | 145 | breq1d 4896 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 0 → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥)) ↔ (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥)))) |
645 | 644 | elrab 3572 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
{𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝐿‘(𝐸‘𝑥)))) |
646 | 609, 643,
645 | sylanbrc 578 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))}) |
647 | | ne0i 4149 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
{𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅) |
648 | 646, 647 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘𝑥))} ≠ ∅) |
649 | 608, 648 | vtoclg 3467 |
. . . . . . . . . . . . 13
⊢ ((𝑆‘𝑗) ∈ ℝ → ((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅)) |
650 | 42, 65, 649 | sylc 65 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅) |
651 | 650 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅) |
652 | 605 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ) |
653 | | fzofi 13092 |
. . . . . . . . . . . . . . 15
⊢
(0..^𝑀) ∈
Fin |
654 | | ssfi 8468 |
. . . . . . . . . . . . . . 15
⊢
(((0..^𝑀) ∈ Fin
∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ (0..^𝑀)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin) |
655 | 653, 600,
654 | mp2an 682 |
. . . . . . . . . . . . . 14
⊢ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin |
656 | 655 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin) |
657 | | fimaxre2 11323 |
. . . . . . . . . . . . 13
⊢ (({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥) |
658 | 652, 656,
657 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥) |
659 | 658 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥) |
660 | | 0red 10380 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ∈ ℝ) |
661 | 604, 47 | sseldi 3819 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ ℝ) |
662 | | 1red 10377 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 1 ∈ ℝ) |
663 | 661, 662 | readdcld 10406 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℝ) |
664 | | elfzouz 12793 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆‘𝑗)) ∈
(ℤ≥‘0)) |
665 | | eluzle 12005 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼‘(𝑆‘𝑗)) ∈ (ℤ≥‘0)
→ 0 ≤ (𝐼‘(𝑆‘𝑗))) |
666 | 47, 664, 665 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ≤ (𝐼‘(𝑆‘𝑗))) |
667 | 384 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < 1) |
668 | 661, 662,
666, 667 | addgegt0d 10948 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 < ((𝐼‘(𝑆‘𝑗)) + 1)) |
669 | 660, 663,
668 | ltled 10524 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1)) |
670 | 669 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1)) |
671 | 661 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆‘𝑗)) ∈ ℝ) |
672 | | 1red 10377 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈
ℝ) |
673 | 391, 672 | resubcld 10803 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑀 − 1) ∈ ℝ) |
674 | 673 | ad2antrr 716 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ) |
675 | | 1red 10377 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 1 ∈
ℝ) |
676 | | elfzolt2 12798 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐼‘(𝑆‘𝑗)) ∈ (0..^𝑀) → (𝐼‘(𝑆‘𝑗)) < 𝑀) |
677 | 47, 676 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) < 𝑀) |
678 | 601, 43 | sseldi 3819 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ∈ ℤ) |
679 | 100 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℤ) |
680 | | zltlem1 11782 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼‘(𝑆‘𝑗)) ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝐼‘(𝑆‘𝑗)) < 𝑀 ↔ (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1))) |
681 | 678, 679,
680 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) < 𝑀 ↔ (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1))) |
682 | 677, 681 | mpbid 224 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1)) |
683 | 682 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆‘𝑗)) ≤ (𝑀 − 1)) |
684 | | neqne 2977 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
(𝐼‘(𝑆‘𝑗)) = (𝑀 − 1) → (𝐼‘(𝑆‘𝑗)) ≠ (𝑀 − 1)) |
685 | 684 | necomd 3024 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝐼‘(𝑆‘𝑗)) = (𝑀 − 1) → (𝑀 − 1) ≠ (𝐼‘(𝑆‘𝑗))) |
686 | 685 | adantl 475 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑀 − 1) ≠ (𝐼‘(𝑆‘𝑗))) |
687 | 671, 674,
683, 686 | leneltd 10530 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐼‘(𝑆‘𝑗)) < (𝑀 − 1)) |
688 | 671, 674,
675, 687 | ltadd1dd 10986 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) < ((𝑀 − 1) + 1)) |
689 | 590 | ad2antrr 716 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝑀 − 1) + 1) = 𝑀) |
690 | 688, 689 | breqtrd 4912 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) < 𝑀) |
691 | 601, 49 | sseldi 3819 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℤ) |
692 | 691 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℤ) |
693 | | 0zd 11740 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 0 ∈
ℤ) |
694 | 100 | ad2antrr 716 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → 𝑀 ∈ ℤ) |
695 | | elfzo 12791 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐼‘(𝑆‘𝑗)) + 1) ∈ ℤ ∧ 0 ∈ ℤ
∧ 𝑀 ∈ ℤ)
→ (((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1) ∧ ((𝐼‘(𝑆‘𝑗)) + 1) < 𝑀))) |
696 | 692, 693,
694, 695 | syl3anc 1439 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀) ↔ (0 ≤ ((𝐼‘(𝑆‘𝑗)) + 1) ∧ ((𝐼‘(𝑆‘𝑗)) + 1) < 𝑀))) |
697 | 670, 690,
696 | mpbir2and 703 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀)) |
698 | 697 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀)) |
699 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) |
700 | | fveq2 6446 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = ((𝐼‘(𝑆‘𝑗)) + 1) → (𝑄‘𝑖) = (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
701 | 700 | breq1d 4896 |
. . . . . . . . . . . . 13
⊢ (𝑖 = ((𝐼‘(𝑆‘𝑗)) + 1) → ((𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ↔ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))) |
702 | 701 | elrab 3572 |
. . . . . . . . . . . 12
⊢ (((𝐼‘(𝑆‘𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ↔ (((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0..^𝑀) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))) |
703 | 698, 699,
702 | sylanbrc 578 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}) |
704 | | suprub 11338 |
. . . . . . . . . . 11
⊢ ((({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ⊆ ℝ ∧ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑙 ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}𝑙 ≤ 𝑥) ∧ ((𝐼‘(𝑆‘𝑗)) + 1) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}) → ((𝐼‘(𝑆‘𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) |
705 | 606, 651,
659, 703, 704 | syl31anc 1441 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ≤ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < )) |
706 | 62 | eqcomd 2784 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = (𝐼‘(𝑆‘𝑗))) |
707 | 706 | ad2antrr 716 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))}, ℝ, < ) = (𝐼‘(𝑆‘𝑗))) |
708 | 705, 707 | breqtrd 4912 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗))) |
709 | 661 | ltp1d 11308 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐼‘(𝑆‘𝑗)) < ((𝐼‘(𝑆‘𝑗)) + 1)) |
710 | 661, 663 | ltnled 10523 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐼‘(𝑆‘𝑗)) < ((𝐼‘(𝑆‘𝑗)) + 1) ↔ ¬ ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗)))) |
711 | 709, 710 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ¬ ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗))) |
712 | 711 | ad2antrr 716 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) → ¬ ((𝐼‘(𝑆‘𝑗)) + 1) ≤ (𝐼‘(𝑆‘𝑗))) |
713 | 708, 712 | pm2.65da 807 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ¬ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗)))) |
714 | 572 | adantr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) ∈ ℝ) |
715 | 50 | adantr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ) |
716 | 714, 715 | ltnled 10523 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → ((𝐿‘(𝐸‘(𝑆‘𝑗))) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ↔ ¬ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))))) |
717 | 713, 716 | mpbird 249 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
718 | 717 | adantlr 705 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐿‘(𝐸‘(𝑆‘𝑗))) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
719 | 599, 718 | eqbrtrd 4908 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) ∧ ¬ (𝐼‘(𝑆‘𝑗)) = (𝑀 − 1)) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
720 | 598, 719 | pm2.61dan 803 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
721 | 2 | 3ad2ant1 1124 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝑀 ∈ ℕ) |
722 | 1 | 3ad2ant1 1124 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝑄 ∈ (𝑃‘𝑀)) |
723 | 21 | 3ad2ant1 1124 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝐶 ∈ ℝ) |
724 | 22 | 3ad2ant1 1124 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝐷 ∈ ℝ) |
725 | 23 | 3ad2ant1 1124 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝐶 < 𝐷) |
726 | 49 | 3adant3 1123 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → ((𝐼‘(𝑆‘𝑗)) + 1) ∈ (0...𝑀)) |
727 | | simp2 1128 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → 𝑗 ∈ (0..^𝑁)) |
728 | 42 | leidd 10941 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ≤ (𝑆‘𝑗)) |
729 | | elico2 12549 |
. . . . . . . . 9
⊢ (((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘(𝑗 + 1)) ∈ ℝ*) →
((𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘𝑗) ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))) |
730 | 42, 212, 729 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1))) ↔ ((𝑆‘𝑗) ∈ ℝ ∧ (𝑆‘𝑗) ≤ (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝑗 + 1))))) |
731 | 42, 728, 131, 730 | mpbir3and 1399 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1)))) |
732 | 731 | 3adant3 1123 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝑆‘𝑗) ∈ ((𝑆‘𝑗)[,)(𝑆‘(𝑗 + 1)))) |
733 | | simp3 1129 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
734 | | eqid 2778 |
. . . . . 6
⊢ ((𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))) = ((𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) − ((𝐸‘(𝑆‘𝑗)) − (𝑆‘𝑗))) |
735 | 11, 3, 721, 722, 723, 724, 725, 24, 25, 26, 27, 12, 726, 727, 732, 733, 734 | fourierdlem63 41313 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
736 | 735 | 3adant1r 1180 |
. . . 4
⊢ (((𝜑 ∧ (𝑆‘𝑗) ∈ ℝ) ∧ 𝑗 ∈ (0..^𝑁) ∧ (𝐸‘(𝑆‘𝑗)) < (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
737 | 550, 551,
720, 736 | syl3anc 1439 |
. . 3
⊢ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ ¬ (𝐸‘(𝑆‘𝑗)) = 𝐵) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
738 | 549, 737 | pm2.61dan 803 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) |
739 | | ioossioo 12578 |
. 2
⊢ ((((𝑄‘(𝐼‘(𝑆‘𝑗))) ∈ ℝ* ∧ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) ∈ ℝ*) ∧
((𝑄‘(𝐼‘(𝑆‘𝑗))) ≤ (𝐿‘(𝐸‘(𝑆‘𝑗))) ∧ (𝐸‘(𝑆‘(𝑗 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))) → ((𝐿‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))) |
740 | 45, 51, 89, 738, 739 | syl22anc 829 |
1
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐿‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))) |