Step | Hyp | Ref
| Expression |
1 | | fourierdlem93.4 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) |
2 | | fourierdlem93.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
3 | | fourierdlem93.1 |
. . . . . . . . . 10
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
4 | 3 | fourierdlem2 43325 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
5 | 2, 4 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
6 | 1, 5 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
7 | 6 | simprd 499 |
. . . . . 6
⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))) |
8 | 7 | simplld 768 |
. . . . 5
⊢ (𝜑 → (𝑄‘0) = -π) |
9 | 8 | eqcomd 2743 |
. . . 4
⊢ (𝜑 → -π = (𝑄‘0)) |
10 | 7 | simplrd 770 |
. . . . 5
⊢ (𝜑 → (𝑄‘𝑀) = π) |
11 | 10 | eqcomd 2743 |
. . . 4
⊢ (𝜑 → π = (𝑄‘𝑀)) |
12 | 9, 11 | oveq12d 7231 |
. . 3
⊢ (𝜑 → (-π[,]π) = ((𝑄‘0)[,](𝑄‘𝑀))) |
13 | 12 | itgeq1d 43173 |
. 2
⊢ (𝜑 → ∫(-π[,]π)(𝐹‘𝑡) d𝑡 = ∫((𝑄‘0)[,](𝑄‘𝑀))(𝐹‘𝑡) d𝑡) |
14 | | 0zd 12188 |
. . 3
⊢ (𝜑 → 0 ∈
ℤ) |
15 | | nnuz 12477 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
16 | 2, 15 | eleqtrdi 2848 |
. . . 4
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
17 | | 1e0p1 12335 |
. . . . . 6
⊢ 1 = (0 +
1) |
18 | 17 | a1i 11 |
. . . . 5
⊢ (𝜑 → 1 = (0 +
1)) |
19 | 18 | fveq2d 6721 |
. . . 4
⊢ (𝜑 →
(ℤ≥‘1) = (ℤ≥‘(0 +
1))) |
20 | 16, 19 | eleqtrd 2840 |
. . 3
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(0 +
1))) |
21 | 3, 2, 1 | fourierdlem15 43338 |
. . . 4
⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π)) |
22 | | pire 25348 |
. . . . . . 7
⊢ π
∈ ℝ |
23 | 22 | renegcli 11139 |
. . . . . 6
⊢ -π
∈ ℝ |
24 | | iccssre 13017 |
. . . . . 6
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆
ℝ) |
25 | 23, 22, 24 | mp2an 692 |
. . . . 5
⊢
(-π[,]π) ⊆ ℝ |
26 | 25 | a1i 11 |
. . . 4
⊢ (𝜑 → (-π[,]π) ⊆
ℝ) |
27 | 21, 26 | fssd 6563 |
. . 3
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
28 | 7 | simprd 499 |
. . . 4
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
29 | 28 | r19.21bi 3130 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))) |
30 | | fourierdlem93.6 |
. . . . 5
⊢ (𝜑 → 𝐹:(-π[,]π)⟶ℂ) |
31 | 30 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝐹:(-π[,]π)⟶ℂ) |
32 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) |
33 | 12 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → ((𝑄‘0)[,](𝑄‘𝑀)) = (-π[,]π)) |
34 | 33 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → ((𝑄‘0)[,](𝑄‘𝑀)) = (-π[,]π)) |
35 | 32, 34 | eleqtrd 2840 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝑡 ∈ (-π[,]π)) |
36 | 31, 35 | ffvelrnd 6905 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → (𝐹‘𝑡) ∈ ℂ) |
37 | 27 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
38 | | elfzofz 13258 |
. . . . . 6
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
39 | 38 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) |
40 | 37, 39 | ffvelrnd 6905 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ) |
41 | | fzofzp1 13339 |
. . . . . 6
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
42 | 41 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) |
43 | 37, 42 | ffvelrnd 6905 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
44 | 30 | feqmptd 6780 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡))) |
45 | 44 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹 = (𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡))) |
46 | 45 | reseq1d 5850 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
47 | | ioossicc 13021 |
. . . . . . . . . . 11
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) |
48 | 47 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) |
49 | 23 | rexri 10891 |
. . . . . . . . . . . . . 14
⊢ -π
∈ ℝ* |
50 | 49 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → -π ∈
ℝ*) |
51 | 22 | rexri 10891 |
. . . . . . . . . . . . . 14
⊢ π
∈ ℝ* |
52 | 51 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → π ∈
ℝ*) |
53 | 21 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(-π[,]π)) |
54 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀)) |
55 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) |
56 | 50, 52, 53, 54, 55 | fourierdlem1 43324 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑡 ∈ (-π[,]π)) |
57 | 56 | ralrimiva 3105 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))𝑡 ∈ (-π[,]π)) |
58 | | dfss3 3888 |
. . . . . . . . . . 11
⊢ (((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π) ↔
∀𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))𝑡 ∈ (-π[,]π)) |
59 | 57, 58 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆
(-π[,]π)) |
60 | 48, 59 | sstrd 3911 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆
(-π[,]π)) |
61 | 60 | resmptd 5908 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑡 ∈ (-π[,]π) ↦ (𝐹‘𝑡)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡))) |
62 | 46, 61 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡))) |
63 | 62 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
64 | | fourierdlem93.7 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) |
65 | 63, 64 | eqeltrd 2838 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) |
66 | | fourierdlem93.9 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) |
67 | 62 | oveq1d 7228 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) = ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) limℂ (𝑄‘(𝑖 + 1)))) |
68 | 66, 67 | eleqtrd 2840 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) limℂ (𝑄‘(𝑖 + 1)))) |
69 | | fourierdlem93.8 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
70 | 62 | oveq1d 7228 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) = ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) limℂ (𝑄‘𝑖))) |
71 | 69, 70 | eleqtrd 2840 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) limℂ (𝑄‘𝑖))) |
72 | 40, 43, 65, 68, 71 | iblcncfioo 43194 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
73 | 30 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝐹:(-π[,]π)⟶ℂ) |
74 | 73, 56 | ffvelrnd 6905 |
. . . 4
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹‘𝑡) ∈ ℂ) |
75 | 40, 43, 72, 74 | ibliooicc 43187 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑡)) ∈
𝐿1) |
76 | 14, 20, 27, 29, 36, 75 | itgspltprt 43195 |
. 2
⊢ (𝜑 → ∫((𝑄‘0)[,](𝑄‘𝑀))(𝐹‘𝑡) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡) |
77 | | fvres 6736 |
. . . . . . . 8
⊢ (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) = (𝐹‘𝑡)) |
78 | 77 | eqcomd 2743 |
. . . . . . 7
⊢ (𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → (𝐹‘𝑡) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡)) |
79 | 78 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹‘𝑡) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡)) |
80 | 79 | itgeq2dv 24679 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) d𝑡) |
81 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))) = (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))) |
82 | 30 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:(-π[,]π)⟶ℂ) |
83 | 82, 59 | fssresd 6586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))⟶ℂ) |
84 | 48 | resabs1d 5882 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
85 | 84, 64 | eqeltrd 2838 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) |
86 | 84 | oveq1d 7228 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) |
87 | 40, 43, 29, 83 | limcicciooub 42853 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) |
88 | 86, 87 | eqtr3d 2779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) |
89 | 66, 88 | eleqtrd 2840 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1)))) |
90 | 84 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
91 | 90 | oveq1d 7228 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) = (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
92 | 40, 43, 29, 83 | limciccioolb 42837 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
93 | 91, 92 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) = ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
94 | 69, 93 | eleqtrd 2840 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖))) |
95 | | fourierdlem93.5 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℝ) |
96 | 95 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ) |
97 | 81, 40, 43, 29, 83, 85, 89, 94, 96 | fourierdlem82 43404 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘𝑡) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) d𝑡) |
98 | 40 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘𝑖) ∈ ℝ) |
99 | 43 | adantr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
100 | 95 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑋 ∈ ℝ) |
101 | 98, 100 | resubcld 11260 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ) |
102 | 99, 100 | resubcld 11260 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ) |
103 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) |
104 | | eliccre 42718 |
. . . . . . . . . 10
⊢ ((((𝑄‘𝑖) − 𝑋) ∈ ℝ ∧ ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ ℝ) |
105 | 101, 102,
103, 104 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ∈ ℝ) |
106 | 100, 105 | readdcld 10862 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ∈ ℝ) |
107 | | elicc2 13000 |
. . . . . . . . . . . 12
⊢ ((((𝑄‘𝑖) − 𝑋) ∈ ℝ ∧ ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋)))) |
108 | 101, 102,
107 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋)) ↔ (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋)))) |
109 | 103, 108 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑡 ∈ ℝ ∧ ((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ∧ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))) |
110 | 109 | simp2d 1145 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑄‘𝑖) − 𝑋) ≤ 𝑡) |
111 | 98, 100, 105 | lesubadd2d 11431 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (((𝑄‘𝑖) − 𝑋) ≤ 𝑡 ↔ (𝑄‘𝑖) ≤ (𝑋 + 𝑡))) |
112 | 110, 111 | mpbid 235 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑄‘𝑖) ≤ (𝑋 + 𝑡)) |
113 | 109 | simp3d 1146 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋)) |
114 | 100, 105,
99 | leaddsub2d 11434 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝑋 + 𝑡) ≤ (𝑄‘(𝑖 + 1)) ↔ 𝑡 ≤ ((𝑄‘(𝑖 + 1)) − 𝑋))) |
115 | 113, 114 | mpbird 260 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ≤ (𝑄‘(𝑖 + 1))) |
116 | 98, 99, 106, 112, 115 | eliccd 42717 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) |
117 | | fvres 6736 |
. . . . . . 7
⊢ ((𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡))) |
118 | 116, 117 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) → ((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡))) |
119 | 118 | itgeq2dv 24679 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))((𝐹 ↾ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡) |
120 | 80, 97, 119 | 3eqtrd 2781 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡) |
121 | 120 | sumeq2dv 15267 |
. . 3
⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡) |
122 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑠 = 𝑡 → (𝑋 + 𝑠) = (𝑋 + 𝑡)) |
123 | 122 | fveq2d 6721 |
. . . . . 6
⊢ (𝑠 = 𝑡 → (𝐹‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑡))) |
124 | 123 | cbvitgv 24674 |
. . . . 5
⊢
∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡 |
125 | 124 | a1i 11 |
. . . 4
⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡) |
126 | | fourierdlem93.2 |
. . . . . . . . 9
⊢ 𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋)) |
127 | 126 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋))) |
128 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0)) |
129 | 128 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝑖 = 0 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋)) |
130 | 129 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋)) |
131 | 2 | nnzd 12281 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
132 | | 0le0 11931 |
. . . . . . . . . 10
⊢ 0 ≤
0 |
133 | 132 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 0) |
134 | | 0red 10836 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) |
135 | 2 | nnred 11845 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
136 | 2 | nngt0d 11879 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 𝑀) |
137 | 134, 135,
136 | ltled 10980 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝑀) |
138 | 14, 131, 14, 133, 137 | elfzd 13103 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
139 | 8, 23 | eqeltrdi 2846 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘0) ∈ ℝ) |
140 | 139, 95 | resubcld 11260 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄‘0) − 𝑋) ∈ ℝ) |
141 | 127, 130,
138, 140 | fvmptd 6825 |
. . . . . . 7
⊢ (𝜑 → (𝐻‘0) = ((𝑄‘0) − 𝑋)) |
142 | 8 | oveq1d 7228 |
. . . . . . 7
⊢ (𝜑 → ((𝑄‘0) − 𝑋) = (-π − 𝑋)) |
143 | 141, 142 | eqtr2d 2778 |
. . . . . 6
⊢ (𝜑 → (-π − 𝑋) = (𝐻‘0)) |
144 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀)) |
145 | 144 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝑖 = 𝑀 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑀) − 𝑋)) |
146 | 145 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 = 𝑀) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑀) − 𝑋)) |
147 | 135 | leidd 11398 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ≤ 𝑀) |
148 | 14, 131, 131, 137, 147 | elfzd 13103 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
149 | 10, 22 | eqeltrdi 2846 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ) |
150 | 149, 95 | resubcld 11260 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄‘𝑀) − 𝑋) ∈ ℝ) |
151 | 127, 146,
148, 150 | fvmptd 6825 |
. . . . . . 7
⊢ (𝜑 → (𝐻‘𝑀) = ((𝑄‘𝑀) − 𝑋)) |
152 | 10 | oveq1d 7228 |
. . . . . . 7
⊢ (𝜑 → ((𝑄‘𝑀) − 𝑋) = (π − 𝑋)) |
153 | 151, 152 | eqtr2d 2778 |
. . . . . 6
⊢ (𝜑 → (π − 𝑋) = (𝐻‘𝑀)) |
154 | 143, 153 | oveq12d 7231 |
. . . . 5
⊢ (𝜑 → ((-π − 𝑋)[,](π − 𝑋)) = ((𝐻‘0)[,](𝐻‘𝑀))) |
155 | 154 | itgeq1d 43173 |
. . . 4
⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡) |
156 | 27 | ffvelrnda 6904 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ) |
157 | 95 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ) |
158 | 156, 157 | resubcld 11260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ) |
159 | 158, 126 | fmptd 6931 |
. . . . . 6
⊢ (𝜑 → 𝐻:(0...𝑀)⟶ℝ) |
160 | 40, 43, 96, 29 | ltsub1dd 11444 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − 𝑋) < ((𝑄‘(𝑖 + 1)) − 𝑋)) |
161 | 39, 158 | syldan 594 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) − 𝑋) ∈ ℝ) |
162 | 126 | fvmpt2 6829 |
. . . . . . . 8
⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑄‘𝑖) − 𝑋) ∈ ℝ) → (𝐻‘𝑖) = ((𝑄‘𝑖) − 𝑋)) |
163 | 39, 161, 162 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) = ((𝑄‘𝑖) − 𝑋)) |
164 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗)) |
165 | 164 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘𝑗) − 𝑋)) |
166 | 165 | cbvmptv 5158 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋)) |
167 | 126, 166 | eqtri 2765 |
. . . . . . . . 9
⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋)) |
168 | 167 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐻 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) − 𝑋))) |
169 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑖 + 1) → (𝑄‘𝑗) = (𝑄‘(𝑖 + 1))) |
170 | 169 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝑗 = (𝑖 + 1) → ((𝑄‘𝑗) − 𝑋) = ((𝑄‘(𝑖 + 1)) − 𝑋)) |
171 | 170 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑄‘𝑗) − 𝑋) = ((𝑄‘(𝑖 + 1)) − 𝑋)) |
172 | 43, 96 | resubcld 11260 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) − 𝑋) ∈ ℝ) |
173 | 168, 171,
42, 172 | fvmptd 6825 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) − 𝑋)) |
174 | 160, 163,
173 | 3brtr4d 5085 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) |
175 | | frn 6552 |
. . . . . . . . 9
⊢ (𝐹:(-π[,]π)⟶ℂ
→ ran 𝐹 ⊆
ℂ) |
176 | 30, 175 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 ⊆ ℂ) |
177 | 176 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → ran 𝐹 ⊆ ℂ) |
178 | | ffun 6548 |
. . . . . . . . . 10
⊢ (𝐹:(-π[,]π)⟶ℂ
→ Fun 𝐹) |
179 | 30, 178 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → Fun 𝐹) |
180 | 179 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → Fun 𝐹) |
181 | 23 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π ∈
ℝ) |
182 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → π ∈
ℝ) |
183 | 95 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑋 ∈ ℝ) |
184 | 141, 140 | eqeltrd 2838 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐻‘0) ∈ ℝ) |
185 | 184 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘0) ∈ ℝ) |
186 | 151, 150 | eqeltrd 2838 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐻‘𝑀) ∈ ℝ) |
187 | 186 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘𝑀) ∈ ℝ) |
188 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) |
189 | | eliccre 42718 |
. . . . . . . . . . . 12
⊢ (((𝐻‘0) ∈ ℝ ∧
(𝐻‘𝑀) ∈ ℝ ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ℝ) |
190 | 185, 187,
188, 189 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ∈ ℝ) |
191 | 183, 190 | readdcld 10862 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ ℝ) |
192 | 128 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 = 0) → (𝑄‘𝑖) = (𝑄‘0)) |
193 | 192 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑄‘𝑖) − 𝑋) = ((𝑄‘0) − 𝑋)) |
194 | 127, 193,
138, 140 | fvmptd 6825 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐻‘0) = ((𝑄‘0) − 𝑋)) |
195 | 194 | oveq2d 7229 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 + (𝐻‘0)) = (𝑋 + ((𝑄‘0) − 𝑋))) |
196 | 95 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ∈ ℂ) |
197 | 139 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑄‘0) ∈ ℂ) |
198 | 196, 197 | pncan3d 11192 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 + ((𝑄‘0) − 𝑋)) = (𝑄‘0)) |
199 | 195, 198,
8 | 3eqtrrd 2782 |
. . . . . . . . . . . 12
⊢ (𝜑 → -π = (𝑋 + (𝐻‘0))) |
200 | 199 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π = (𝑋 + (𝐻‘0))) |
201 | | elicc2 13000 |
. . . . . . . . . . . . . . 15
⊢ (((𝐻‘0) ∈ ℝ ∧
(𝐻‘𝑀) ∈ ℝ) → (𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀)))) |
202 | 185, 187,
201 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀)) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀)))) |
203 | 188, 202 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑡 ∈ ℝ ∧ (𝐻‘0) ≤ 𝑡 ∧ 𝑡 ≤ (𝐻‘𝑀))) |
204 | 203 | simp2d 1145 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐻‘0) ≤ 𝑡) |
205 | 185, 190,
183, 204 | leadd2dd 11447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + (𝐻‘0)) ≤ (𝑋 + 𝑡)) |
206 | 200, 205 | eqbrtrd 5075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → -π ≤ (𝑋 + 𝑡)) |
207 | 203 | simp3d 1146 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → 𝑡 ≤ (𝐻‘𝑀)) |
208 | 190, 187,
183, 207 | leadd2dd 11447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ≤ (𝑋 + (𝐻‘𝑀))) |
209 | 151 | oveq2d 7229 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 + (𝐻‘𝑀)) = (𝑋 + ((𝑄‘𝑀) − 𝑋))) |
210 | 149 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑄‘𝑀) ∈ ℂ) |
211 | 196, 210 | pncan3d 11192 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 + ((𝑄‘𝑀) − 𝑋)) = (𝑄‘𝑀)) |
212 | 209, 211,
10 | 3eqtrrd 2782 |
. . . . . . . . . . . 12
⊢ (𝜑 → π = (𝑋 + (𝐻‘𝑀))) |
213 | 212 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → π = (𝑋 + (𝐻‘𝑀))) |
214 | 208, 213 | breqtrrd 5081 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ≤ π) |
215 | 181, 182,
191, 206, 214 | eliccd 42717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ (-π[,]π)) |
216 | | fdm 6554 |
. . . . . . . . . . . 12
⊢ (𝐹:(-π[,]π)⟶ℂ
→ dom 𝐹 =
(-π[,]π)) |
217 | 30, 216 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = (-π[,]π)) |
218 | 217 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝜑 → (-π[,]π) = dom 𝐹) |
219 | 218 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (-π[,]π) = dom 𝐹) |
220 | 215, 219 | eleqtrd 2840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝑋 + 𝑡) ∈ dom 𝐹) |
221 | | fvelrn 6897 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ (𝑋 + 𝑡) ∈ dom 𝐹) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹) |
222 | 180, 220,
221 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐹‘(𝑋 + 𝑡)) ∈ ran 𝐹) |
223 | 177, 222 | sseldd 3902 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘0)[,](𝐻‘𝑀))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ) |
224 | 163, 161 | eqeltrd 2838 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℝ) |
225 | 173, 172 | eqeltrd 2838 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℝ) |
226 | 82, 60 | fssresd 6586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ) |
227 | 40 | rexrd 10883 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈
ℝ*) |
228 | 227 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈
ℝ*) |
229 | 43 | rexrd 10883 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈
ℝ*) |
230 | 229 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈
ℝ*) |
231 | 95 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℝ) |
232 | | elioore 12965 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → 𝑡 ∈ ℝ) |
233 | 232 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ℝ) |
234 | 231, 233 | readdcld 10862 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ℝ) |
235 | 163 | oveq2d 7229 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + ((𝑄‘𝑖) − 𝑋))) |
236 | 196 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ) |
237 | 40 | recnd 10861 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ) |
238 | 236, 237 | pncan3d 11192 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑄‘𝑖) − 𝑋)) = (𝑄‘𝑖)) |
239 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (𝑄‘𝑖)) |
240 | 235, 238,
239 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖))) |
241 | 240 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖))) |
242 | 224 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) ∈ ℝ) |
243 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) |
244 | 242 | rexrd 10883 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) ∈
ℝ*) |
245 | 225 | rexrd 10883 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈
ℝ*) |
246 | 245 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘(𝑖 + 1)) ∈
ℝ*) |
247 | | elioo2 12976 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐻‘𝑖) ∈ ℝ* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ*) →
(𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1))))) |
248 | 244, 246,
247 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↔ (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1))))) |
249 | 243, 248 | mpbid 235 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑡 ∈ ℝ ∧ (𝐻‘𝑖) < 𝑡 ∧ 𝑡 < (𝐻‘(𝑖 + 1)))) |
250 | 249 | simp2d 1145 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘𝑖) < 𝑡) |
251 | 242, 233,
231, 250 | ltadd2dd 10991 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + (𝐻‘𝑖)) < (𝑋 + 𝑡)) |
252 | 241, 251 | eqbrtrd 5075 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑋 + 𝑡)) |
253 | 225 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝐻‘(𝑖 + 1)) ∈ ℝ) |
254 | 249 | simp3d 1146 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑡 < (𝐻‘(𝑖 + 1))) |
255 | 233, 253,
231, 254 | ltadd2dd 10991 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) < (𝑋 + (𝐻‘(𝑖 + 1)))) |
256 | 173 | oveq2d 7229 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑋 + ((𝑄‘(𝑖 + 1)) − 𝑋))) |
257 | 43 | recnd 10861 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ) |
258 | 236, 257 | pncan3d 11192 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑄‘(𝑖 + 1)) − 𝑋)) = (𝑄‘(𝑖 + 1))) |
259 | 256, 258 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑄‘(𝑖 + 1))) |
260 | 259 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + (𝐻‘(𝑖 + 1))) = (𝑄‘(𝑖 + 1))) |
261 | 255, 260 | breqtrd 5079 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) < (𝑄‘(𝑖 + 1))) |
262 | 228, 230,
234, 252, 261 | eliood 42711 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
263 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) |
264 | 262, 263 | fmptd 6931 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
265 | | fcompt 6948 |
. . . . . . . . . . 11
⊢ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ ∧ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)))) |
266 | 226, 264,
265 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)))) |
267 | | oveq2 7221 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑟 → (𝑋 + 𝑡) = (𝑋 + 𝑟)) |
268 | 267 | cbvmptv 5158 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟)) |
269 | 268 | fveq1i 6718 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠) |
270 | 269 | fveq2i 6720 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)) |
271 | 270 | mpteq2i 5147 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))) |
272 | 271 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)))) |
273 | | fveq2 6717 |
. . . . . . . . . . . . . 14
⊢ (𝑠 = 𝑡 → ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠) = ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)) |
274 | 273 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑡 → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))) |
275 | 274 | cbvmptv 5158 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))) |
276 | 275 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)))) |
277 | | eqidd 2738 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟)) = (𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))) |
278 | | oveq2 7221 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑡 → (𝑋 + 𝑟) = (𝑋 + 𝑡)) |
279 | 278 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) ∧ 𝑟 = 𝑡) → (𝑋 + 𝑟) = (𝑋 + 𝑡)) |
280 | 277, 279,
243, 234 | fvmptd 6825 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡) = (𝑋 + 𝑡)) |
281 | 280 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡))) |
282 | | fvres 6736 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 + 𝑡) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡))) |
283 | 262, 282 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑋 + 𝑡)) = (𝐹‘(𝑋 + 𝑡))) |
284 | 281, 283 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡)) = (𝐹‘(𝑋 + 𝑡))) |
285 | 284 | mpteq2dva 5150 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑟 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑟))‘𝑡))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡)))) |
286 | 272, 276,
285 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡)))) |
287 | 266, 286 | eqtr2d 2778 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)))) |
288 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) |
289 | | ssid 3923 |
. . . . . . . . . . . . . . 15
⊢ ℂ
⊆ ℂ |
290 | 289 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → ℂ
⊆ ℂ) |
291 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → 𝑋 ∈
ℂ) |
292 | 290, 291,
290 | constcncfg 43088 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑋) ∈ (ℂ–cn→ℂ)) |
293 | | cncfmptid 23810 |
. . . . . . . . . . . . . . 15
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)) |
294 | 289, 289,
293 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ) |
295 | 294 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ 𝑡) ∈ (ℂ–cn→ℂ)) |
296 | 292, 295 | addcncf 24341 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) ∈ (ℂ–cn→ℂ)) |
297 | 236, 296 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ℂ ↦ (𝑋 + 𝑡)) ∈ (ℂ–cn→ℂ)) |
298 | | ioosscn 12997 |
. . . . . . . . . . . 12
⊢ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ⊆ ℂ |
299 | 298 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ⊆ ℂ) |
300 | | ioosscn 12997 |
. . . . . . . . . . . 12
⊢ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ |
301 | 300 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ) |
302 | 288, 297,
299, 301, 262 | cncfmptssg 43087 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
303 | 302, 64 | cncfco 23804 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→ℂ)) |
304 | 287, 303 | eqeltrd 2838 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))–cn→ℂ)) |
305 | 227 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) ∈
ℝ*) |
306 | 229 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘(𝑖 + 1)) ∈
ℝ*) |
307 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) |
308 | | vex 3412 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑟 ∈ V |
309 | 263 | elrnmpt 5825 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ V → (𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ↔ ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡))) |
310 | 308, 309 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ↔ ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡)) |
311 | 307, 310 | sylib 221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡)) |
312 | | nfv 1922 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0..^𝑀)) |
313 | | nfmpt1 5153 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑡(𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) |
314 | 313 | nfrn 5821 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡ran
(𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) |
315 | 314 | nfcri 2891 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) |
316 | 312, 315 | nfan 1907 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) |
317 | | nfv 1922 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡 𝑟 ∈ ℝ |
318 | | simp3 1140 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 = (𝑋 + 𝑡)) |
319 | 95 | 3ad2ant1 1135 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑋 ∈ ℝ) |
320 | 232 | 3ad2ant2 1136 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑡 ∈ ℝ) |
321 | 319, 320 | readdcld 10862 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑋 + 𝑡) ∈ ℝ) |
322 | 318, 321 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 ∈ ℝ) |
323 | 322 | 3exp 1121 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ))) |
324 | 323 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ))) |
325 | 316, 317,
324 | rexlimd 3236 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → 𝑟 ∈ ℝ)) |
326 | 311, 325 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ℝ) |
327 | | nfv 1922 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡(𝑄‘𝑖) < 𝑟 |
328 | 252 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑄‘𝑖) < (𝑋 + 𝑡)) |
329 | | simp3 1140 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 = (𝑋 + 𝑡)) |
330 | 328, 329 | breqtrrd 5081 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑄‘𝑖) < 𝑟) |
331 | 330 | 3exp 1121 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟))) |
332 | 331 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟))) |
333 | 316, 327,
332 | rexlimd 3236 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → (𝑄‘𝑖) < 𝑟)) |
334 | 311, 333 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) < 𝑟) |
335 | | nfv 1922 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡 𝑟 < (𝑄‘(𝑖 + 1)) |
336 | 261 | 3adant3 1134 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → (𝑋 + 𝑡) < (𝑄‘(𝑖 + 1))) |
337 | 329, 336 | eqbrtrd 5075 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∧ 𝑟 = (𝑋 + 𝑡)) → 𝑟 < (𝑄‘(𝑖 + 1))) |
338 | 337 | 3exp 1121 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1))))) |
339 | 338 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → (𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1))))) |
340 | 316, 335,
339 | rexlimd 3236 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (∃𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))𝑟 = (𝑋 + 𝑡) → 𝑟 < (𝑄‘(𝑖 + 1)))) |
341 | 311, 340 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 < (𝑄‘(𝑖 + 1))) |
342 | 305, 306,
326, 334, 341 | eliood 42711 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
343 | 217 | ineq2d 4127 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩
(-π[,]π))) |
344 | 343 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩
(-π[,]π))) |
345 | | dmres 5873 |
. . . . . . . . . . . . . . . . 17
⊢ dom
(𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹) |
346 | 345 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩ dom 𝐹)) |
347 | | dfss 3884 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π) ↔ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩
(-π[,]π))) |
348 | 60, 347 | sylib 221 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∩
(-π[,]π))) |
349 | 344, 346,
348 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
350 | 349 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
351 | 342, 350 | eleqtrrd 2841 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))) |
352 | 326, 341 | ltned 10968 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ≠ (𝑄‘(𝑖 + 1))) |
353 | 352 | neneqd 2945 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 = (𝑄‘(𝑖 + 1))) |
354 | | velsn 4557 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ {(𝑄‘(𝑖 + 1))} ↔ 𝑟 = (𝑄‘(𝑖 + 1))) |
355 | 353, 354 | sylnibr 332 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 ∈ {(𝑄‘(𝑖 + 1))}) |
356 | 351, 355 | eldifd 3877 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))})) |
357 | 356 | ralrimiva 3105 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))})) |
358 | | dfss3 3888 |
. . . . . . . . . . 11
⊢ (ran
(𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))}) ↔ ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))})) |
359 | 357, 358 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘(𝑖 + 1))})) |
360 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) |
361 | 196 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑋 ∈ ℂ) |
362 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → 𝑠 ∈ ℂ) |
363 | 361, 362 | addcomd 11034 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑠 ∈ ℂ) → (𝑋 + 𝑠) = (𝑠 + 𝑋)) |
364 | 363 | mpteq2dva 5150 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋))) |
365 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) = (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) |
366 | 365 | addccncf 23814 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑋 ∈ ℂ → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ)) |
367 | 196, 366 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑠 + 𝑋)) ∈ (ℂ–cn→ℂ)) |
368 | 364, 367 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ)) |
369 | 368 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ℂ ↦ (𝑋 + 𝑠)) ∈ (ℂ–cn→ℂ)) |
370 | 224 | rexrd 10883 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈
ℝ*) |
371 | | iocssre 13015 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐻‘𝑖) ∈ ℝ* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℝ) |
372 | 370, 225,
371 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℝ) |
373 | | ax-resscn 10786 |
. . . . . . . . . . . . . . . . . 18
⊢ ℝ
⊆ ℂ |
374 | 372, 373 | sstrdi 3913 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ) |
375 | 289 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ℂ ⊆
ℂ) |
376 | 196 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℂ) |
377 | 374 | sselda 3901 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℂ) |
378 | 376, 377 | addcld 10852 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℂ) |
379 | 360, 369,
374, 375, 378 | cncfmptssg 43087 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ)) |
380 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
381 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) =
((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) |
382 | 380 | cnfldtop 23681 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(TopOpen‘ℂfld) ∈ Top |
383 | | unicntop 23683 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
384 | 383 | restid 16938 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
385 | 382, 384 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
386 | 385 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
387 | 380, 381,
386 | cncfcn 23807 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn
(TopOpen‘ℂfld))) |
388 | 374, 375,
387 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn
(TopOpen‘ℂfld))) |
389 | 379, 388 | eleqtrd 2840 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
(((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn
(TopOpen‘ℂfld))) |
390 | 380 | cnfldtopon 23680 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
391 | 390 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
392 | | resttopon 22058 |
. . . . . . . . . . . . . . . . 17
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))) |
393 | 391, 374,
392 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) →
((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))) |
394 | | cncnp 22177 |
. . . . . . . . . . . . . . . 16
⊢
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
(((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn
(TopOpen‘ℂfld)) ↔ ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡)))) |
395 | 393, 391,
394 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
(((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) Cn
(TopOpen‘ℂfld)) ↔ ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡)))) |
396 | 389, 395 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡))) |
397 | 396 | simprd 499 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡)) |
398 | | ubioc1 12988 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑖) ∈ ℝ* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ* ∧
(𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (𝐻‘(𝑖 + 1)) ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) |
399 | 370, 245,
174, 398 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) |
400 | | fveq2 6717 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (𝐻‘(𝑖 + 1)) →
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡) = ((((TopOpen‘ℂfld)
↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1)))) |
401 | 400 | eleq2d 2823 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (𝐻‘(𝑖 + 1)) → ((𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1))))) |
402 | 401 | rspccva 3536 |
. . . . . . . . . . . . 13
⊢
((∀𝑡 ∈
((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡) ∧ (𝐻‘(𝑖 + 1)) ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1)))) |
403 | 397, 399,
402 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1)))) |
404 | | ioounsn 13065 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑖) ∈ ℝ* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ* ∧
(𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) = ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) |
405 | 370, 245,
174, 404 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) = ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) |
406 | 259 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = (𝑋 + (𝐻‘(𝑖 + 1)))) |
407 | 406 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) = (𝑋 + (𝐻‘(𝑖 + 1)))) |
408 | | iftrue 4445 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝐻‘(𝑖 + 1)) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘(𝑖 + 1))) |
409 | 408 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘(𝑖 + 1))) |
410 | | oveq2 7221 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝐻‘(𝑖 + 1)) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘(𝑖 + 1)))) |
411 | 410 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘(𝑖 + 1)))) |
412 | 407, 409,
411 | 3eqtr4d 2787 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠)) |
413 | | iffalse 4448 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑠 = (𝐻‘(𝑖 + 1)) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) |
414 | 413 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) |
415 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) |
416 | | oveq2 7221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑠 → (𝑋 + 𝑡) = (𝑋 + 𝑠)) |
417 | 416 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) ∧ 𝑡 = 𝑠) → (𝑋 + 𝑡) = (𝑋 + 𝑠)) |
418 | | velsn 4557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ {(𝐻‘(𝑖 + 1))} ↔ 𝑠 = (𝐻‘(𝑖 + 1))) |
419 | 418 | notbii 323 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑠 ∈ {(𝐻‘(𝑖 + 1))} ↔ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) |
420 | | elun 4063 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))})) |
421 | 420 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))})) |
422 | 421 | orcomd 871 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (𝑠 ∈ {(𝐻‘(𝑖 + 1))} ∨ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))) |
423 | 422 | ord 864 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (¬ 𝑠 ∈ {(𝐻‘(𝑖 + 1))} → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))) |
424 | 419, 423 | syl5bir 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) → (¬ 𝑠 = (𝐻‘(𝑖 + 1)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))) |
425 | 424 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) |
426 | 425 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) |
427 | 95 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → 𝑋 ∈ ℝ) |
428 | | elioore 12965 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) → 𝑠 ∈ ℝ) |
429 | 428 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℝ) |
430 | | elsni 4558 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 ∈ {(𝐻‘(𝑖 + 1))} → 𝑠 = (𝐻‘(𝑖 + 1))) |
431 | 430 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → 𝑠 = (𝐻‘(𝑖 + 1))) |
432 | 225 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → (𝐻‘(𝑖 + 1)) ∈ ℝ) |
433 | 431, 432 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘(𝑖 + 1))}) → 𝑠 ∈ ℝ) |
434 | 429, 433 | jaodan 958 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘(𝑖 + 1))})) → 𝑠 ∈ ℝ) |
435 | 420, 434 | sylan2b 597 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → 𝑠 ∈ ℝ) |
436 | 427, 435 | readdcld 10862 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → (𝑋 + 𝑠) ∈ ℝ) |
437 | 436 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → (𝑋 + 𝑠) ∈ ℝ) |
438 | 415, 417,
426, 437 | fvmptd 6825 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = (𝑋 + 𝑠)) |
439 | 414, 438 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) ∧ ¬ 𝑠 = (𝐻‘(𝑖 + 1))) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠)) |
440 | 412, 439 | pm2.61dan 813 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) → if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠)) |
441 | 405, 440 | mpteq12dva 5139 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠))) |
442 | 405 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) →
((TopOpen‘ℂfld) ↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) =
((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1))))) |
443 | 442 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) →
(((TopOpen‘ℂfld) ↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP
(TopOpen‘ℂfld)) =
(((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))) |
444 | 443 | fveq1d 6719 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) →
((((TopOpen‘ℂfld) ↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP
(TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1))) =
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)(,](𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1)))) |
445 | 403, 441,
444 | 3eltr4d 2853 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP
(TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1)))) |
446 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) =
((TopOpen‘ℂfld) ↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) |
447 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) |
448 | 264, 301 | fssd 6563 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)):((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))⟶ℂ) |
449 | 225 | recnd 10861 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘(𝑖 + 1)) ∈ ℂ) |
450 | 446, 380,
447, 448, 299, 449 | ellimc 24770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) limℂ (𝐻‘(𝑖 + 1))) ↔ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))}) ↦ if(𝑠 = (𝐻‘(𝑖 + 1)), (𝑄‘(𝑖 + 1)), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘(𝑖 + 1))})) CnP
(TopOpen‘ℂfld))‘(𝐻‘(𝑖 + 1))))) |
451 | 445, 450 | mpbird 260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) limℂ (𝐻‘(𝑖 + 1)))) |
452 | 359, 451,
66 | limccog 42836 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) limℂ (𝐻‘(𝑖 + 1)))) |
453 | 266, 286 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡)))) |
454 | 453 | oveq1d 7228 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) limℂ (𝐻‘(𝑖 + 1))) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) limℂ (𝐻‘(𝑖 + 1)))) |
455 | 452, 454 | eleqtrd 2840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) limℂ (𝐻‘(𝑖 + 1)))) |
456 | 40 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → (𝑄‘𝑖) ∈ ℝ) |
457 | 456, 334 | gtned 10967 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ≠ (𝑄‘𝑖)) |
458 | 457 | neneqd 2945 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 = (𝑄‘𝑖)) |
459 | | velsn 4557 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ {(𝑄‘𝑖)} ↔ 𝑟 = (𝑄‘𝑖)) |
460 | 458, 459 | sylnibr 332 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → ¬ 𝑟 ∈ {(𝑄‘𝑖)}) |
461 | 351, 460 | eldifd 3877 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) → 𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)})) |
462 | 461 | ralrimiva 3105 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)})) |
463 | | dfss3 3888 |
. . . . . . . . . . 11
⊢ (ran
(𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)}) ↔ ∀𝑟 ∈ ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))𝑟 ∈ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)})) |
464 | 462, 463 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) ⊆ (dom (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∖ {(𝑄‘𝑖)})) |
465 | | icossre 13016 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐻‘𝑖) ∈ ℝ ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ*) →
((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℝ) |
466 | 224, 245,
465 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℝ) |
467 | 466, 373 | sstrdi 3913 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ) |
468 | 196 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → 𝑋 ∈ ℂ) |
469 | 467 | sselda 3901 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → 𝑠 ∈ ℂ) |
470 | 468, 469 | addcld 10852 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℂ) |
471 | 360, 369,
467, 375, 470 | cncfmptssg 43087 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈ (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ)) |
472 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) =
((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) |
473 | 380, 472,
386 | cncfcn 23807 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ ∧ ℂ ⊆
ℂ) → (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn
(TopOpen‘ℂfld))) |
474 | 467, 375,
473 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn
(TopOpen‘ℂfld))) |
475 | 471, 474 | eleqtrd 2840 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
(((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn
(TopOpen‘ℂfld))) |
476 | | resttopon 22058 |
. . . . . . . . . . . . . . . . 17
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))) |
477 | 391, 467,
476 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) →
((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))) |
478 | | cncnp 22177 |
. . . . . . . . . . . . . . . 16
⊢
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∈ (TopOn‘((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
(((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn
(TopOpen‘ℂfld)) ↔ ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡)))) |
479 | 477, 391,
478 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
(((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) Cn
(TopOpen‘ℂfld)) ↔ ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡)))) |
480 | 475, 479 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)):((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))⟶ℂ ∧ ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡))) |
481 | 480 | simprd 499 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑡 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡)) |
482 | | lbico1 12989 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑖) ∈ ℝ* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ* ∧
(𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) |
483 | 370, 245,
174, 482 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) |
484 | | fveq2 6717 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (𝐻‘𝑖) →
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡) = ((((TopOpen‘ℂfld)
↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘(𝐻‘𝑖))) |
485 | 484 | eleq2d 2823 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = (𝐻‘𝑖) → ((𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡) ↔ (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘(𝐻‘𝑖)))) |
486 | 485 | rspccva 3536 |
. . . . . . . . . . . . 13
⊢
((∀𝑡 ∈
((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))(𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘𝑡) ∧ (𝐻‘𝑖) ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘(𝐻‘𝑖))) |
487 | 481, 483,
486 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠)) ∈
((((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘(𝐻‘𝑖))) |
488 | | uncom 4067 |
. . . . . . . . . . . . . 14
⊢ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) = ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) |
489 | | snunioo 13066 |
. . . . . . . . . . . . . . 15
⊢ (((𝐻‘𝑖) ∈ ℝ* ∧ (𝐻‘(𝑖 + 1)) ∈ ℝ* ∧
(𝐻‘𝑖) < (𝐻‘(𝑖 + 1))) → ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) |
490 | 370, 245,
174, 489 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ({(𝐻‘𝑖)} ∪ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) |
491 | 488, 490 | syl5eq 2790 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) = ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) |
492 | | iftrue 4445 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝐻‘𝑖) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘𝑖)) |
493 | 492 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑄‘𝑖)) |
494 | 240 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → (𝑄‘𝑖) = (𝑋 + (𝐻‘𝑖))) |
495 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = (𝐻‘𝑖) → (𝑋 + 𝑠) = (𝑋 + (𝐻‘𝑖))) |
496 | 495 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝐻‘𝑖) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + 𝑠)) |
497 | 496 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → (𝑋 + (𝐻‘𝑖)) = (𝑋 + 𝑠)) |
498 | 493, 494,
497 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠)) |
499 | 498 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠)) |
500 | | iffalse 4448 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑠 = (𝐻‘𝑖) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) |
501 | 500 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) |
502 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) = (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) |
503 | 416 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) ∧ 𝑡 = 𝑠) → (𝑋 + 𝑡) = (𝑋 + 𝑠)) |
504 | | velsn 4557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ {(𝐻‘𝑖)} ↔ 𝑠 = (𝐻‘𝑖)) |
505 | 504 | notbii 323 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑠 ∈ {(𝐻‘𝑖)} ↔ ¬ 𝑠 = (𝐻‘𝑖)) |
506 | | elun 4063 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↔ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)})) |
507 | 506 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)})) |
508 | 507 | orcomd 871 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (𝑠 ∈ {(𝐻‘𝑖)} ∨ 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))) |
509 | 508 | ord 864 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (¬ 𝑠 ∈ {(𝐻‘𝑖)} → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))) |
510 | 505, 509 | syl5bir 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) → (¬ 𝑠 = (𝐻‘𝑖) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))))) |
511 | 510 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) |
512 | 511 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → 𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1)))) |
513 | 95 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → 𝑋 ∈ ℝ) |
514 | | elsni 4558 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 ∈ {(𝐻‘𝑖)} → 𝑠 = (𝐻‘𝑖)) |
515 | 514 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → 𝑠 = (𝐻‘𝑖)) |
516 | 224 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → (𝐻‘𝑖) ∈ ℝ) |
517 | 515, 516 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ {(𝐻‘𝑖)}) → 𝑠 ∈ ℝ) |
518 | 429, 517 | jaodan 958 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑠 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∨ 𝑠 ∈ {(𝐻‘𝑖)})) → 𝑠 ∈ ℝ) |
519 | 506, 518 | sylan2b 597 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → 𝑠 ∈ ℝ) |
520 | 513, 519 | readdcld 10862 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → (𝑋 + 𝑠) ∈ ℝ) |
521 | 520 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → (𝑋 + 𝑠) ∈ ℝ) |
522 | 502, 503,
512, 521 | fvmptd 6825 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠) = (𝑋 + 𝑠)) |
523 | 501, 522 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) ∧ ¬ 𝑠 = (𝐻‘𝑖)) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠)) |
524 | 499, 523 | pm2.61dan 813 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) → if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠)) = (𝑋 + 𝑠)) |
525 | 491, 524 | mpteq12dva 5139 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑠))) |
526 | 491 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) →
((TopOpen‘ℂfld) ↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) = ((TopOpen‘ℂfld)
↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1))))) |
527 | 526 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) →
(((TopOpen‘ℂfld) ↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP
(TopOpen‘ℂfld)) =
(((TopOpen‘ℂfld) ↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))) |
528 | 527 | fveq1d 6719 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) →
((((TopOpen‘ℂfld) ↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP
(TopOpen‘ℂfld))‘(𝐻‘𝑖)) = ((((TopOpen‘ℂfld)
↾t ((𝐻‘𝑖)[,)(𝐻‘(𝑖 + 1)))) CnP
(TopOpen‘ℂfld))‘(𝐻‘𝑖))) |
529 | 487, 525,
528 | 3eltr4d 2853 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP
(TopOpen‘ℂfld))‘(𝐻‘𝑖))) |
530 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) = ((TopOpen‘ℂfld)
↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) |
531 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) = (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) |
532 | 224 | recnd 10861 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐻‘𝑖) ∈ ℂ) |
533 | 530, 380,
531, 448, 299, 532 | ellimc 24770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) limℂ (𝐻‘𝑖)) ↔ (𝑠 ∈ (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)}) ↦ if(𝑠 = (𝐻‘𝑖), (𝑄‘𝑖), ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))‘𝑠))) ∈
((((TopOpen‘ℂfld) ↾t (((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ∪ {(𝐻‘𝑖)})) CnP
(TopOpen‘ℂfld))‘(𝐻‘𝑖)))) |
534 | 529, 533 | mpbird 260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡)) limℂ (𝐻‘𝑖))) |
535 | 464, 534,
69 | limccog 42836 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) limℂ (𝐻‘𝑖))) |
536 | 453 | oveq1d 7228 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∘ (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝑋 + 𝑡))) limℂ (𝐻‘𝑖)) = ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) limℂ (𝐻‘𝑖))) |
537 | 535, 536 | eleqtrd 2840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) limℂ (𝐻‘𝑖))) |
538 | 224, 225,
304, 455, 537 | iblcncfioo 43194 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)(,)(𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈
𝐿1) |
539 | 30 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝐹:(-π[,]π)⟶ℂ) |
540 | 49 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → -π ∈
ℝ*) |
541 | 51 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → π ∈
ℝ*) |
542 | 21 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(-π[,]π)) |
543 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀)) |
544 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) |
545 | 163, 173 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) = (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) |
546 | 545 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) = (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) |
547 | 544, 546 | eleqtrd 2840 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → 𝑡 ∈ (((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))) |
548 | 547, 116 | syldan 594 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) |
549 | 540, 541,
542, 543, 548 | fourierdlem1 43324 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝑋 + 𝑡) ∈ (-π[,]π)) |
550 | 539, 549 | ffvelrnd 6905 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑡)) ∈ ℂ) |
551 | 224, 225,
538, 550 | ibliooicc 43187 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑡 ∈ ((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑡))) ∈
𝐿1) |
552 | 14, 20, 159, 174, 223, 551 | itgspltprt 43195 |
. . . . 5
⊢ (𝜑 → ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡) |
553 | 545 | itgeq1d 43173 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡 = ∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡) |
554 | 553 | sumeq2dv 15267 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝐻‘𝑖)[,](𝐻‘(𝑖 + 1)))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡) |
555 | 552, 554 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → ∫((𝐻‘0)[,](𝐻‘𝑀))(𝐹‘(𝑋 + 𝑡)) d𝑡 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡) |
556 | 125, 155,
555 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠 = Σ𝑖 ∈ (0..^𝑀)∫(((𝑄‘𝑖) − 𝑋)[,]((𝑄‘(𝑖 + 1)) − 𝑋))(𝐹‘(𝑋 + 𝑡)) d𝑡) |
557 | 121, 556 | eqtr4d 2780 |
. 2
⊢ (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠) |
558 | 13, 76, 557 | 3eqtrd 2781 |
1
⊢ (𝜑 → ∫(-π[,]π)(𝐹‘𝑡) d𝑡 = ∫((-π − 𝑋)[,](π − 𝑋))(𝐹‘(𝑋 + 𝑠)) d𝑠) |