Step | Hyp | Ref
| Expression |
1 | | fourierdlem46.h |
. . . . . . . . 9
⊢ 𝐻 = ({-π, π, 𝐶} ∪ ((-π[,]π) ∖
dom 𝐹)) |
2 | | pire 24014 |
. . . . . . . . . . . . 13
⊢ π
∈ ℝ |
3 | 2 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → π ∈
ℝ) |
4 | 3 | renegcld 10336 |
. . . . . . . . . . 11
⊢ (𝜑 → -π ∈
ℝ) |
5 | | fourierdlem46.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℝ) |
6 | | tpssi 4309 |
. . . . . . . . . . 11
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ ∧ 𝐶 ∈ ℝ) → {-π, π, 𝐶} ⊆
ℝ) |
7 | 4, 3, 5, 6 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → {-π, π, 𝐶} ⊆
ℝ) |
8 | 4, 3 | iccssred 38574 |
. . . . . . . . . . 11
⊢ (𝜑 → (-π[,]π) ⊆
ℝ) |
9 | 8 | ssdifssd 3710 |
. . . . . . . . . 10
⊢ (𝜑 → ((-π[,]π) ∖
dom 𝐹) ⊆
ℝ) |
10 | 7, 9 | unssd 3751 |
. . . . . . . . 9
⊢ (𝜑 → ({-π, π, 𝐶} ∪ ((-π[,]π) ∖
dom 𝐹)) ⊆
ℝ) |
11 | 1, 10 | syl5eqss 3612 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ⊆ ℝ) |
12 | | fourierdlem46.qf |
. . . . . . . . 9
⊢ (𝜑 → 𝑄:(0...𝑀)⟶𝐻) |
13 | | fourierdlem46.i |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ (0..^𝑀)) |
14 | | elfzofz 12354 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ∈ (0...𝑀)) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (0...𝑀)) |
16 | 12, 15 | ffvelrnd 6268 |
. . . . . . . 8
⊢ (𝜑 → (𝑄‘𝐼) ∈ 𝐻) |
17 | 11, 16 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ) |
18 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝑄‘𝐼) ∈ ℝ) |
19 | | fzofzp1 12431 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀)) |
20 | 13, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀)) |
21 | 12, 20 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ 𝐻) |
22 | 11, 21 | sseldd 3569 |
. . . . . . . 8
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ) |
23 | 22 | rexrd 9968 |
. . . . . . 7
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈
ℝ*) |
24 | 23 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) |
25 | | fourierdlem46.10 |
. . . . . . 7
⊢ (𝜑 → (𝑄‘𝐼) < (𝑄‘(𝐼 + 1))) |
26 | 25 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝑄‘𝐼) < (𝑄‘(𝐼 + 1))) |
27 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝑄‘𝐼) ∈ dom 𝐹 ∧ 𝑥 = (𝑄‘𝐼)) → 𝑥 = (𝑄‘𝐼)) |
28 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ (((𝑄‘𝐼) ∈ dom 𝐹 ∧ 𝑥 = (𝑄‘𝐼)) → (𝑄‘𝐼) ∈ dom 𝐹) |
29 | 27, 28 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ (((𝑄‘𝐼) ∈ dom 𝐹 ∧ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ dom 𝐹) |
30 | 29 | adantll 746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) ∧ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ dom 𝐹) |
31 | 30 | adantlr 747 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ dom 𝐹) |
32 | | ssun2 3739 |
. . . . . . . . . . . . . . . . . . 19
⊢
((-π[,]π) ∖ dom 𝐹) ⊆ ({-π, π, 𝐶} ∪ ((-π[,]π) ∖ dom 𝐹)) |
33 | 32, 1 | sseqtr4i 3601 |
. . . . . . . . . . . . . . . . . 18
⊢
((-π[,]π) ∖ dom 𝐹) ⊆ 𝐻 |
34 | | fourierdlem46.qiss |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆
(-π(,)π)) |
35 | | ioossicc 12130 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(-π(,)π) ⊆ (-π[,]π) |
36 | 34, 35 | syl6ss 3580 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆
(-π[,]π)) |
37 | 36 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ (-π[,]π)) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ (-π[,]π)) |
39 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → ¬ 𝑥 ∈ dom 𝐹) |
40 | 38, 39 | eldifd 3551 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ ((-π[,]π) ∖ dom 𝐹)) |
41 | 33, 40 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ 𝐻) |
42 | | fourierdlem46.ranq |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ran 𝑄 = 𝐻) |
43 | 42 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐻 = ran 𝑄) |
44 | 43 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝐻 = ran 𝑄) |
45 | 41, 44 | eleqtrd 2690 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → 𝑥 ∈ ran 𝑄) |
46 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝑄) → 𝑥 ∈ ran 𝑄) |
47 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑄:(0...𝑀)⟶𝐻 → 𝑄 Fn (0...𝑀)) |
48 | 12, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑄 Fn (0...𝑀)) |
49 | 48 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝑄) → 𝑄 Fn (0...𝑀)) |
50 | | fvelrnb 6153 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑄 Fn (0...𝑀) → (𝑥 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑥)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝑄) → (𝑥 ∈ ran 𝑄 ↔ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑥)) |
52 | 46, 51 | mpbid 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑥) |
53 | 52 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) → ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑥) |
54 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ) |
55 | 54 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = 𝑥) → 𝑗 ∈ ℤ) |
56 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = 𝑥) → 𝜑) |
57 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = 𝑥) → 𝑗 ∈ (0...𝑀)) |
58 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ (𝑄‘𝑗) = 𝑥) → (𝑄‘𝑗) = 𝑥) |
59 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ (𝑄‘𝑗) = 𝑥) → 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) |
60 | 58, 59 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ (𝑄‘𝑗) = 𝑥) → (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) |
61 | 60 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = 𝑥) → (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) |
62 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ∈ ℤ) |
63 | 13, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐼 ∈ ℤ) |
64 | 63 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝐼 ∈ ℤ) |
65 | 17 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑄‘𝐼) ∈
ℝ*) |
66 | 65 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) ∈
ℝ*) |
67 | 23 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) |
68 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) |
69 | | ioogtlb 38564 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧
(𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) < (𝑄‘𝑗)) |
70 | 66, 67, 68, 69 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) < (𝑄‘𝑗)) |
71 | | fourierdlem46.qiso |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑄 Isom < , < ((0...𝑀), 𝐻)) |
72 | 71 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑄 Isom < , < ((0...𝑀), 𝐻)) |
73 | 15 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝐼 ∈ (0...𝑀)) |
74 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑗 ∈ (0...𝑀)) |
75 | | isorel 6476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝐼 ∈ (0...𝑀) ∧ 𝑗 ∈ (0...𝑀))) → (𝐼 < 𝑗 ↔ (𝑄‘𝐼) < (𝑄‘𝑗))) |
76 | 72, 73, 74, 75 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝐼 < 𝑗 ↔ (𝑄‘𝐼) < (𝑄‘𝑗))) |
77 | 70, 76 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝐼 < 𝑗) |
78 | | iooltub 38582 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧
(𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝑗) < (𝑄‘(𝐼 + 1))) |
79 | 66, 67, 68, 78 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝑗) < (𝑄‘(𝐼 + 1))) |
80 | 20 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝐼 + 1) ∈ (0...𝑀)) |
81 | | isorel 6476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑗 ∈ (0...𝑀) ∧ (𝐼 + 1) ∈ (0...𝑀))) → (𝑗 < (𝐼 + 1) ↔ (𝑄‘𝑗) < (𝑄‘(𝐼 + 1)))) |
82 | 72, 74, 80, 81 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → (𝑗 < (𝐼 + 1) ↔ (𝑄‘𝑗) < (𝑄‘(𝐼 + 1)))) |
83 | 79, 82 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑗 < (𝐼 + 1)) |
84 | | btwnnz 11329 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐼 ∈ ℤ ∧ 𝐼 < 𝑗 ∧ 𝑗 < (𝐼 + 1)) → ¬ 𝑗 ∈ ℤ) |
85 | 64, 77, 83, 84 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → ¬ 𝑗 ∈ ℤ) |
86 | 56, 57, 61, 85 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = 𝑥) → ¬ 𝑗 ∈ ℤ) |
87 | 86 | adantllr 751 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) ∧ (𝑄‘𝑗) = 𝑥) → ¬ 𝑗 ∈ ℤ) |
88 | 55, 87 | pm2.65da 598 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) ∧ 𝑗 ∈ (0...𝑀)) → ¬ (𝑄‘𝑗) = 𝑥) |
89 | 88 | nrexdv 2984 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ 𝑥 ∈ ran 𝑄) → ¬ ∃𝑗 ∈ (0...𝑀)(𝑄‘𝑗) = 𝑥) |
90 | 53, 89 | pm2.65da 598 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → ¬ 𝑥 ∈ ran 𝑄) |
91 | 90 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 ∈ dom 𝐹) → ¬ 𝑥 ∈ ran 𝑄) |
92 | 45, 91 | condan 831 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ dom 𝐹) |
93 | 92 | ralrimiva 2949 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹) |
94 | | dfss3 3558 |
. . . . . . . . . . . . . 14
⊢ (((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 ↔ ∀𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹) |
95 | 93, 94 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹) |
96 | 95 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹) |
97 | 65 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → (𝑄‘𝐼) ∈
ℝ*) |
98 | 23 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) |
99 | | icossre 12125 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑄‘𝐼) ∈ ℝ ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ*) →
((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ ℝ) |
100 | 17, 23, 99 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ ℝ) |
101 | 100 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ ℝ) |
102 | 101 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ ℝ) |
103 | 17 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → (𝑄‘𝐼) ∈ ℝ) |
104 | 65 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) ∈
ℝ*) |
105 | 23 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) |
106 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) |
107 | | icogelb 12096 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧
𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) ≤ 𝑥) |
108 | 104, 105,
106, 107 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) ≤ 𝑥) |
109 | 108 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → (𝑄‘𝐼) ≤ 𝑥) |
110 | | neqne 2790 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑥 = (𝑄‘𝐼) → 𝑥 ≠ (𝑄‘𝐼)) |
111 | 110 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → 𝑥 ≠ (𝑄‘𝐼)) |
112 | 103, 102,
109, 111 | leneltd 10070 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → (𝑄‘𝐼) < 𝑥) |
113 | | icoltub 38579 |
. . . . . . . . . . . . . . 15
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧
𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 < (𝑄‘(𝐼 + 1))) |
114 | 104, 105,
106, 113 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 < (𝑄‘(𝐼 + 1))) |
115 | 114 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → 𝑥 < (𝑄‘(𝐼 + 1))) |
116 | 97, 98, 102, 112, 115 | eliood 38567 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) |
117 | 96, 116 | sseldd 3569 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ dom 𝐹) |
118 | 117 | adantllr 751 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝐼)) → 𝑥 ∈ dom 𝐹) |
119 | 31, 118 | pm2.61dan 828 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) → 𝑥 ∈ dom 𝐹) |
120 | 119 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ∀𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹) |
121 | | dfss3 3558 |
. . . . . . . 8
⊢ (((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 ↔ ∀𝑥 ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹) |
122 | 120, 121 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹) |
123 | | fourierdlem46.cn |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (dom 𝐹–cn→ℂ)) |
124 | 123 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → 𝐹 ∈ (dom 𝐹–cn→ℂ)) |
125 | | rescncf 22508 |
. . . . . . 7
⊢ (((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 → (𝐹 ∈ (dom 𝐹–cn→ℂ) → (𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∈ (((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))–cn→ℂ))) |
126 | 122, 124,
125 | sylc 63 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ∈ (((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))–cn→ℂ)) |
127 | 18, 24, 26, 126 | icocncflimc 38775 |
. . . . 5
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄‘𝐼)) ∈ (((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼))) |
128 | 17 | leidd 10473 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘𝐼) ≤ (𝑄‘𝐼)) |
129 | 65, 23, 65, 128, 25 | elicod 12095 |
. . . . . . . 8
⊢ (𝜑 → (𝑄‘𝐼) ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) |
130 | | fvres 6117 |
. . . . . . . 8
⊢ ((𝑄‘𝐼) ∈ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) → ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄‘𝐼)) = (𝐹‘(𝑄‘𝐼))) |
131 | 129, 130 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄‘𝐼)) = (𝐹‘(𝑄‘𝐼))) |
132 | 131 | eqcomd 2616 |
. . . . . 6
⊢ (𝜑 → (𝐹‘(𝑄‘𝐼)) = ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄‘𝐼))) |
133 | 132 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝐹‘(𝑄‘𝐼)) = ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))))‘(𝑄‘𝐼))) |
134 | | ioossico 12133 |
. . . . . . . . 9
⊢ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1))) |
135 | 134 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) |
136 | 135 | resabs1d 5348 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) |
137 | 136 | eqcomd 2616 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = ((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) |
138 | 137 | oveq1d 6564 |
. . . . 5
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) = (((𝐹 ↾ ((𝑄‘𝐼)[,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼))) |
139 | 127, 133,
138 | 3eltr4d 2703 |
. . . 4
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → (𝐹‘(𝑄‘𝐼)) ∈ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼))) |
140 | | ne0i 3880 |
. . . 4
⊢ ((𝐹‘(𝑄‘𝐼)) ∈ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅) |
141 | 139, 140 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅) |
142 | | pnfxr 9971 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
143 | 142 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → +∞ ∈
ℝ*) |
144 | 22 | ltpnfd 11831 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) < +∞) |
145 | 23, 143, 144 | xrltled 38427 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ≤ +∞) |
146 | | iooss2 12082 |
. . . . . . . . 9
⊢
((+∞ ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ≤ +∞) → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄‘𝐼)(,)+∞)) |
147 | 142, 145,
146 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄‘𝐼)(,)+∞)) |
148 | 147 | resabs1d 5348 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) |
149 | 148 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) = ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼))) |
150 | 149 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) = (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼))) |
151 | 150 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) = (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼))) |
152 | | limcresi 23455 |
. . . . 5
⊢ ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ⊆ (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) |
153 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → (𝑄‘𝐼) ∈ ℝ) |
154 | | simpl 472 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → 𝜑) |
155 | 2 | renegcli 10221 |
. . . . . . . . . . . 12
⊢ -π
∈ ℝ |
156 | 155 | rexri 9976 |
. . . . . . . . . . 11
⊢ -π
∈ ℝ* |
157 | 156 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → -π ∈
ℝ*) |
158 | 2 | rexri 9976 |
. . . . . . . . . . 11
⊢ π
∈ ℝ* |
159 | 158 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → π ∈
ℝ*) |
160 | 4, 3, 17, 22, 25, 34 | fourierdlem10 39010 |
. . . . . . . . . . 11
⊢ (𝜑 → (-π ≤ (𝑄‘𝐼) ∧ (𝑄‘(𝐼 + 1)) ≤ π)) |
161 | 160 | simpld 474 |
. . . . . . . . . 10
⊢ (𝜑 → -π ≤ (𝑄‘𝐼)) |
162 | 160 | simprd 478 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ≤ π) |
163 | 17, 22, 3, 25, 162 | ltletrd 10076 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄‘𝐼) < π) |
164 | 157, 159,
65, 161, 163 | elicod 12095 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘𝐼) ∈ (-π[,)π)) |
165 | 164 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → (𝑄‘𝐼) ∈ (-π[,)π)) |
166 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → ¬ (𝑄‘𝐼) ∈ dom 𝐹) |
167 | 165, 166 | eldifd 3551 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → (𝑄‘𝐼) ∈ ((-π[,)π) ∖ dom 𝐹)) |
168 | 154, 167 | jca 553 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → (𝜑 ∧ (𝑄‘𝐼) ∈ ((-π[,)π) ∖ dom 𝐹))) |
169 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑥 = (𝑄‘𝐼) → (𝑥 ∈ ((-π[,)π) ∖ dom 𝐹) ↔ (𝑄‘𝐼) ∈ ((-π[,)π) ∖ dom 𝐹))) |
170 | 169 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑥 = (𝑄‘𝐼) → ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐹)) ↔ (𝜑 ∧ (𝑄‘𝐼) ∈ ((-π[,)π) ∖ dom 𝐹)))) |
171 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑄‘𝐼) → (𝑥(,)+∞) = ((𝑄‘𝐼)(,)+∞)) |
172 | 171 | reseq2d 5317 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑄‘𝐼) → (𝐹 ↾ (𝑥(,)+∞)) = (𝐹 ↾ ((𝑄‘𝐼)(,)+∞))) |
173 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑄‘𝐼) → 𝑥 = (𝑄‘𝐼)) |
174 | 172, 173 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑥 = (𝑄‘𝐼) → ((𝐹 ↾ (𝑥(,)+∞)) limℂ 𝑥) = ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼))) |
175 | 174 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑥 = (𝑄‘𝐼) → (((𝐹 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅ ↔ ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ≠ ∅)) |
176 | 170, 175 | imbi12d 333 |
. . . . . . 7
⊢ (𝑥 = (𝑄‘𝐼) → (((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) ↔ ((𝜑 ∧ (𝑄‘𝐼) ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ≠ ∅))) |
177 | | fourierdlem46.rlim |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅) |
178 | 176, 177 | vtoclg 3239 |
. . . . . 6
⊢ ((𝑄‘𝐼) ∈ ℝ → ((𝜑 ∧ (𝑄‘𝐼) ∈ ((-π[,)π) ∖ dom 𝐹)) → ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ≠ ∅)) |
179 | 153, 168,
178 | sylc 63 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ≠ ∅) |
180 | | ssn0 3928 |
. . . . 5
⊢ ((((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ⊆ (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ∧ ((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) limℂ (𝑄‘𝐼)) ≠ ∅) → (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅) |
181 | 152, 179,
180 | sylancr 694 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → (((𝐹 ↾ ((𝑄‘𝐼)(,)+∞)) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅) |
182 | 151, 181 | eqnetrd 2849 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝑄‘𝐼) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅) |
183 | 141, 182 | pm2.61dan 828 |
. 2
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅) |
184 | 65 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘𝐼) ∈
ℝ*) |
185 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈ ℝ) |
186 | 25 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘𝐼) < (𝑄‘(𝐼 + 1))) |
187 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝑄‘(𝐼 + 1)) ∈ dom 𝐹 ∧ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 = (𝑄‘(𝐼 + 1))) |
188 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ (((𝑄‘(𝐼 + 1)) ∈ dom 𝐹 ∧ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) |
189 | 187, 188 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ (((𝑄‘(𝐼 + 1)) ∈ dom 𝐹 ∧ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹) |
190 | 189 | adantll 746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) ∧ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹) |
191 | 190 | adantlr 747 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹) |
192 | 95 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ dom 𝐹) |
193 | 65 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘𝐼) ∈
ℝ*) |
194 | 23 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) |
195 | 65 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) ∈
ℝ*) |
196 | 22 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄‘(𝐼 + 1)) ∈ ℝ) |
197 | | iocssre 12124 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) → ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ ℝ) |
198 | 195, 196,
197 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ ℝ) |
199 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) |
200 | 198, 199 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ∈ ℝ) |
201 | 200 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ ℝ) |
202 | 23 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) |
203 | | iocgtlb 38571 |
. . . . . . . . . . . . . . 15
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧
𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) < 𝑥) |
204 | 195, 202,
199, 203 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → (𝑄‘𝐼) < 𝑥) |
205 | 204 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘𝐼) < 𝑥) |
206 | 22 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ) |
207 | | iocleub 38572 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑄‘𝐼) ∈ ℝ* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ* ∧
𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ≤ (𝑄‘(𝐼 + 1))) |
208 | 195, 202,
199, 207 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ≤ (𝑄‘(𝐼 + 1))) |
209 | 208 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ≤ (𝑄‘(𝐼 + 1))) |
210 | | neqne 2790 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑥 = (𝑄‘(𝐼 + 1)) → 𝑥 ≠ (𝑄‘(𝐼 + 1))) |
211 | 210 | necomd 2837 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑥 = (𝑄‘(𝐼 + 1)) → (𝑄‘(𝐼 + 1)) ≠ 𝑥) |
212 | 211 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ≠ 𝑥) |
213 | 201, 206,
209, 212 | leneltd 10070 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 < (𝑄‘(𝐼 + 1))) |
214 | 193, 194,
201, 205, 213 | eliood 38567 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) |
215 | 192, 214 | sseldd 3569 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹) |
216 | 215 | adantllr 751 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∧ ¬ 𝑥 = (𝑄‘(𝐼 + 1))) → 𝑥 ∈ dom 𝐹) |
217 | 191, 216 | pm2.61dan 828 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) ∧ 𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) → 𝑥 ∈ dom 𝐹) |
218 | 217 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ∀𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹) |
219 | | dfss3 3558 |
. . . . . . . 8
⊢ (((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 ↔ ∀𝑥 ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))𝑥 ∈ dom 𝐹) |
220 | 218, 219 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ dom 𝐹) |
221 | 123 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → 𝐹 ∈ (dom 𝐹–cn→ℂ)) |
222 | | rescncf 22508 |
. . . . . . 7
⊢ (((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) ⊆ dom 𝐹 → (𝐹 ∈ (dom 𝐹–cn→ℂ) → (𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∈ (((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))–cn→ℂ))) |
223 | 220, 221,
222 | sylc 63 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ∈ (((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))–cn→ℂ)) |
224 | 184, 185,
186, 223 | ioccncflimc 38771 |
. . . . 5
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) ∈ (((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1)))) |
225 | 22 | leidd 10473 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ≤ (𝑄‘(𝐼 + 1))) |
226 | 65, 23, 23, 25, 225 | eliocd 38577 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) |
227 | | fvres 6117 |
. . . . . . . . 9
⊢ ((𝑄‘(𝐼 + 1)) ∈ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) → ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) = (𝐹‘(𝑄‘(𝐼 + 1)))) |
228 | 226, 227 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) = (𝐹‘(𝑄‘(𝐼 + 1)))) |
229 | 228 | eqcomd 2616 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘(𝑄‘(𝐼 + 1))) = ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1)))) |
230 | | ioossioc 38560 |
. . . . . . . . . . 11
⊢ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) |
231 | | resabs1 5347 |
. . . . . . . . . . 11
⊢ (((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))) → ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) |
232 | 230, 231 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) |
233 | 232 | eqcomi 2619 |
. . . . . . . . 9
⊢ (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) |
234 | 233 | oveq1i 6559 |
. . . . . . . 8
⊢ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) = (((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) |
235 | 234 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) = (((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1)))) |
236 | 229, 235 | eleq12d 2682 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘(𝑄‘(𝐼 + 1))) ∈ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ↔ ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) ∈ (((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))))) |
237 | 236 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹‘(𝑄‘(𝐼 + 1))) ∈ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ↔ ((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1))))‘(𝑄‘(𝐼 + 1))) ∈ (((𝐹 ↾ ((𝑄‘𝐼)(,](𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))))) |
238 | 224, 237 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝐹‘(𝑄‘(𝐼 + 1))) ∈ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1)))) |
239 | | ne0i 3880 |
. . . 4
⊢ ((𝐹‘(𝑄‘(𝐼 + 1))) ∈ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) |
240 | 238, 239 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) |
241 | | mnfxr 9975 |
. . . . . . . . 9
⊢ -∞
∈ ℝ* |
242 | 241 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → -∞ ∈
ℝ*) |
243 | 17 | mnfltd 11834 |
. . . . . . . . . 10
⊢ (𝜑 → -∞ < (𝑄‘𝐼)) |
244 | 242, 65, 243 | xrltled 38427 |
. . . . . . . . 9
⊢ (𝜑 → -∞ ≤ (𝑄‘𝐼)) |
245 | | iooss1 12081 |
. . . . . . . . 9
⊢
((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑄‘𝐼)) → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ (-∞(,)(𝑄‘(𝐼 + 1)))) |
246 | 241, 244,
245 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))) ⊆ (-∞(,)(𝑄‘(𝐼 + 1)))) |
247 | 246 | resabs1d 5348 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) |
248 | 247 | eqcomd 2616 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) |
249 | 248 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) = ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))) |
250 | 249 | oveq1d 6564 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) = (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1)))) |
251 | | limcresi 23455 |
. . . . 5
⊢ ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ⊆ (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) |
252 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈ ℝ) |
253 | | simpl 472 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → 𝜑) |
254 | 156 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → -π ∈
ℝ*) |
255 | 158 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → π ∈
ℝ*) |
256 | 23 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈
ℝ*) |
257 | 4, 17, 22, 161, 25 | lelttrd 10074 |
. . . . . . . . . 10
⊢ (𝜑 → -π < (𝑄‘(𝐼 + 1))) |
258 | 257 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → -π < (𝑄‘(𝐼 + 1))) |
259 | 162 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ≤ π) |
260 | 254, 255,
256, 258, 259 | eliocd 38577 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈
(-π(,]π)) |
261 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) |
262 | 260, 261 | eldifd 3551 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom
𝐹)) |
263 | 253, 262 | jca 553 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom
𝐹))) |
264 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → (𝑥 ∈ ((-π(,]π) ∖ dom 𝐹) ↔ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom
𝐹))) |
265 | 264 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐹)) ↔ (𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom
𝐹)))) |
266 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → (-∞(,)𝑥) = (-∞(,)(𝑄‘(𝐼 + 1)))) |
267 | 266 | reseq2d 5317 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → (𝐹 ↾ (-∞(,)𝑥)) = (𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1))))) |
268 | | id 22 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → 𝑥 = (𝑄‘(𝐼 + 1))) |
269 | 267, 268 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → ((𝐹 ↾ (-∞(,)𝑥)) limℂ 𝑥) = ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1)))) |
270 | 269 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → (((𝐹 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅ ↔ ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅)) |
271 | 265, 270 | imbi12d 333 |
. . . . . . 7
⊢ (𝑥 = (𝑄‘(𝐼 + 1)) → (((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐹)) → ((𝐹 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) ↔ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom
𝐹)) → ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅))) |
272 | | fourierdlem46.llim |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐹)) → ((𝐹 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅) |
273 | 271, 272 | vtoclg 3239 |
. . . . . 6
⊢ ((𝑄‘(𝐼 + 1)) ∈ ℝ → ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ((-π(,]π) ∖ dom
𝐹)) → ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅)) |
274 | 252, 263,
273 | sylc 63 |
. . . . 5
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) |
275 | | ssn0 3928 |
. . . . 5
⊢ ((((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ⊆ (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ∧ ((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) → (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) |
276 | 251, 274,
275 | sylancr 694 |
. . . 4
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → (((𝐹 ↾ (-∞(,)(𝑄‘(𝐼 + 1)))) ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) |
277 | 250, 276 | eqnetrd 2849 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝑄‘(𝐼 + 1)) ∈ dom 𝐹) → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) |
278 | 240, 277 | pm2.61dan 828 |
. 2
⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅) |
279 | 183, 278 | jca 553 |
1
⊢ (𝜑 → (((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘𝐼)) ≠ ∅ ∧ ((𝐹 ↾ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) limℂ (𝑄‘(𝐼 + 1))) ≠ ∅)) |