Step | Hyp | Ref
| Expression |
1 | | arch 11490 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
∃𝑧 ∈ ℕ
𝑥 < 𝑧) |
2 | 1 | ad2antlr 698 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → ∃𝑧 ∈ ℕ 𝑥 < 𝑧) |
3 | | df-ima 5262 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∘ 𝐾) “ (1...𝑀)) = ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) |
4 | | ovolicc2.8 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐺:𝑈⟶ℕ) |
5 | | nnuz 11924 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℕ =
(ℤ≥‘1) |
6 | | ovolicc2.15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ ×
{𝐶})) |
7 | | 1zzd 11609 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ∈
ℤ) |
8 | | ovolicc2.14 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐶 ∈ 𝑇) |
9 | | ovolicc2.11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐻:𝑇⟶𝑇) |
10 | 5, 6, 7, 8, 9 | algrf 15493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾:ℕ⟶𝑇) |
11 | | ovolicc2.10 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} |
12 | | ssrab2 3834 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⊆ 𝑈 |
13 | 11, 12 | eqsstri 3782 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑇 ⊆ 𝑈 |
14 | | fss 6196 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑇 ⊆ 𝑈) → 𝐾:ℕ⟶𝑈) |
15 | 10, 13, 14 | sylancl 566 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾:ℕ⟶𝑈) |
16 | | fco 6198 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺:𝑈⟶ℕ ∧ 𝐾:ℕ⟶𝑈) → (𝐺 ∘ 𝐾):ℕ⟶ℕ) |
17 | 4, 15, 16 | syl2anc 565 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺 ∘ 𝐾):ℕ⟶ℕ) |
18 | | elfznn 12576 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ) |
19 | 18 | ssriv 3754 |
. . . . . . . . . . . . . . . . . 18
⊢
(1...𝑀) ⊆
ℕ |
20 | | fssres 6210 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∘ 𝐾):ℕ⟶ℕ ∧ (1...𝑀) ⊆ ℕ) →
((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ) |
21 | 17, 19, 20 | sylancl 566 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ) |
22 | | frn 6193 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ → ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) ⊆ ℕ) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) ⊆ ℕ) |
24 | 3, 23 | syl5eqss 3796 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℕ) |
25 | | nnssre 11225 |
. . . . . . . . . . . . . . 15
⊢ ℕ
⊆ ℝ |
26 | 24, 25 | syl6ss 3762 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ) |
27 | 26 | ad3antrrr 701 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ) |
28 | | simpr 471 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) |
29 | 27, 28 | sseldd 3751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ) |
30 | | simpllr 752 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑥 ∈ ℝ) |
31 | | nnre 11228 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) |
32 | 31 | ad2antlr 698 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ) |
33 | | lelttr 10329 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧) → 𝑦 < 𝑧)) |
34 | 29, 30, 32, 33 | syl3anc 1475 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧) → 𝑦 < 𝑧)) |
35 | 34 | ancomsd 456 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝑥 < 𝑧 ∧ 𝑦 ≤ 𝑥) → 𝑦 < 𝑧)) |
36 | 35 | expdimp 440 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) ∧ 𝑥 < 𝑧) → (𝑦 ≤ 𝑥 → 𝑦 < 𝑧)) |
37 | 36 | an32s 623 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 ≤ 𝑥 → 𝑦 < 𝑧)) |
38 | 37 | ralimdva 3110 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) → (∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) |
39 | 38 | impancom 439 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) |
40 | 39 | an32s 623 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) ∧ 𝑧 ∈ ℕ) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) |
41 | 40 | reximdva 3164 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → (∃𝑧 ∈ ℕ 𝑥 < 𝑧 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) |
42 | 2, 41 | mpd 15 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧) |
43 | | fzfid 12979 |
. . . . 5
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
44 | | fvres 6348 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑀) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺 ∘ 𝐾)‘𝑖)) |
45 | 44 | adantl 467 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺 ∘ 𝐾)‘𝑖)) |
46 | | fvco3 6417 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑖 ∈ ℕ) → ((𝐺 ∘ 𝐾)‘𝑖) = (𝐺‘(𝐾‘𝑖))) |
47 | 10, 18, 46 | syl2an 575 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝐾)‘𝑖) = (𝐺‘(𝐾‘𝑖))) |
48 | 45, 47 | eqtrd 2804 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾‘𝑖))) |
49 | 48 | adantrr 688 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾‘𝑖))) |
50 | | fvres 6348 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺 ∘ 𝐾)‘𝑗)) |
51 | 50 | ad2antll 700 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺 ∘ 𝐾)‘𝑗)) |
52 | | elfznn 12576 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ) |
53 | 52 | adantl 467 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ) |
54 | | fvco3 6417 |
. . . . . . . . . . . . . 14
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑗 ∈ ℕ) → ((𝐺 ∘ 𝐾)‘𝑗) = (𝐺‘(𝐾‘𝑗))) |
55 | 10, 53, 54 | syl2an 575 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺 ∘ 𝐾)‘𝑗) = (𝐺‘(𝐾‘𝑗))) |
56 | 51, 55 | eqtrd 2804 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = (𝐺‘(𝐾‘𝑗))) |
57 | 49, 56 | eqeq12d 2785 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) ↔ (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)))) |
58 | | fveq2 6332 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑗)))) |
59 | 58 | fveq2d 6336 |
. . . . . . . . . . . 12
⊢ ((𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))) |
60 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...𝑀) ⊆ ℕ) |
61 | | elfznn 12576 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ) |
62 | 61 | ad2antlr 698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ∈ ℕ) |
63 | 62 | nnred 11236 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ∈ ℝ) |
64 | | ovolicc2.16 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} |
65 | | ssrab2 3834 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} ⊆ ℕ |
66 | 64, 65 | eqsstri 3782 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑊 ⊆
ℕ |
67 | 66, 25 | sstri 3759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑊 ⊆
ℝ |
68 | | ovolicc2.17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑀 = inf(𝑊, ℝ, < ) |
69 | 66, 5 | sseqtri 3784 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑊 ⊆
(ℤ≥‘1) |
70 | | 1z 11608 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℤ |
71 | 5 | uzinf 12971 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 ∈
ℤ → ¬ ℕ ∈ Fin) |
72 | 70, 71 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ¬
ℕ ∈ Fin |
73 | | ovolicc2.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) |
74 | | elin 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑈 ∈ (𝒫 ran ((,)
∘ 𝐹) ∩ Fin)
↔ (𝑈 ∈ 𝒫
ran ((,) ∘ 𝐹) ∧
𝑈 ∈
Fin)) |
75 | 73, 74 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin)) |
76 | 75 | simprd 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑈 ∈ Fin) |
77 | | ssfi 8335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑈 ∈ Fin ∧ 𝑇 ⊆ 𝑈) → 𝑇 ∈ Fin) |
78 | 76, 13, 77 | sylancl 566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑇 ∈ Fin) |
79 | 78 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑇 ∈ Fin) |
80 | 10 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐾:ℕ⟶𝑇) |
81 | | fveq2 6332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗))) |
82 | 81 | fveq2d 6336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑗)))) |
83 | 82 | fveq2d 6336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))) |
84 | | simpll 742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝜑) |
85 | | simprl 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℕ) |
86 | | ral0 4215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
∀𝑚 ∈
∅ 𝑛 ≤ 𝑚 |
87 | | simplr 744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑊 = ∅) |
88 | 87 | raleqdv 3292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 ↔ ∀𝑚 ∈ ∅ 𝑛 ≤ 𝑚)) |
89 | 86, 88 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚) |
90 | 89 | ralrimivw 3115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚) |
91 | | rabid2 3266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (ℕ
= {𝑛 ∈ ℕ ∣
∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ↔ ∀𝑛 ∈ ℕ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚) |
92 | 90, 91 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ℕ = {𝑛 ∈ ℕ ∣
∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
93 | 85, 92 | eleqtrd 2851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
94 | | simprr 748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℕ) |
95 | 94, 92 | eleqtrd 2851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
96 | | ovolicc.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐴 ∈ ℝ) |
97 | | ovolicc.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐵 ∈ ℝ) |
98 | | ovolicc.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
99 | | ovolicc2.4 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
100 | | ovolicc2.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
101 | | ovolicc2.7 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) |
102 | | ovolicc2.9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) |
103 | | ovolicc2.12 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) |
104 | | ovolicc2.13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐴 ∈ 𝐶) |
105 | 96, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64 | ovolicc2lem3 23506 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))) |
106 | 84, 93, 95, 105 | syl12anc 1473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))) |
107 | 83, 106 | syl5ibr 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗)) |
108 | 107 | ralrimivva 3119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑊 = ∅) → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗)) |
109 | | dff13 6654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐾:ℕ–1-1→𝑇 ↔ (𝐾:ℕ⟶𝑇 ∧ ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗))) |
110 | 80, 108, 109 | sylanbrc 564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐾:ℕ–1-1→𝑇) |
111 | | f1domg 8128 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑇 ∈ Fin → (𝐾:ℕ–1-1→𝑇 → ℕ ≼ 𝑇)) |
112 | 79, 110, 111 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑊 = ∅) → ℕ ≼ 𝑇) |
113 | | domfi 8336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑇 ∈ Fin ∧ ℕ
≼ 𝑇) → ℕ
∈ Fin) |
114 | 79, 112, 113 | syl2anc 565 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑊 = ∅) → ℕ ∈
Fin) |
115 | 114 | ex 397 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑊 = ∅ → ℕ ∈
Fin)) |
116 | 115 | necon3bd 2956 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (¬ ℕ ∈ Fin
→ 𝑊 ≠
∅)) |
117 | 72, 116 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑊 ≠ ∅) |
118 | | infssuzcl 11974 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑊 ⊆
(ℤ≥‘1) ∧ 𝑊 ≠ ∅) → inf(𝑊, ℝ, < ) ∈ 𝑊) |
119 | 69, 117, 118 | sylancr 567 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → inf(𝑊, ℝ, < ) ∈ 𝑊) |
120 | 68, 119 | syl5eqel 2853 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ∈ 𝑊) |
121 | 67, 120 | sseldi 3748 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℝ) |
122 | 121 | ad2antrr 697 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑀 ∈ ℝ) |
123 | 67 | sseli 3746 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ 𝑊 → 𝑚 ∈ ℝ) |
124 | 123 | adantl 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑚 ∈ ℝ) |
125 | | elfzle2 12551 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ≤ 𝑀) |
126 | 125 | ad2antlr 698 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ≤ 𝑀) |
127 | | infssuzle 11973 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ⊆
(ℤ≥‘1) ∧ 𝑚 ∈ 𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑚) |
128 | 69, 127 | mpan 662 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ 𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑚) |
129 | 68, 128 | syl5eqbr 4819 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ 𝑊 → 𝑀 ≤ 𝑚) |
130 | 129 | adantl 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑀 ≤ 𝑚) |
131 | 63, 122, 124, 126, 130 | letrd 10395 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ≤ 𝑚) |
132 | 131 | ralrimiva 3114 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚) |
133 | 60, 132 | ssrabdv 3828 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
134 | 133 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
135 | | simprl 746 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ (1...𝑀)) |
136 | 134, 135 | sseldd 3751 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
137 | | simprr 748 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ (1...𝑀)) |
138 | 134, 137 | sseldd 3751 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
139 | 136, 138 | jca 495 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) |
140 | 139, 105 | syldan 571 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))) |
141 | 59, 140 | syl5ibr 236 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)) → 𝑖 = 𝑗)) |
142 | 57, 141 | sylbid 230 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗)) |
143 | 142 | ralrimivva 3119 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗)) |
144 | | dff13 6654 |
. . . . . . . . 9
⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ ↔ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ ∧ ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))) |
145 | 21, 143, 144 | sylanbrc 564 |
. . . . . . . 8
⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ) |
146 | | f1f1orn 6289 |
. . . . . . . 8
⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran
((𝐺 ∘ 𝐾) ↾ (1...𝑀))) |
147 | 145, 146 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran
((𝐺 ∘ 𝐾) ↾ (1...𝑀))) |
148 | | f1oeq3 6270 |
. . . . . . . 8
⊢ (((𝐺 ∘ 𝐾) “ (1...𝑀)) = ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀)) ↔ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran
((𝐺 ∘ 𝐾) ↾ (1...𝑀)))) |
149 | 3, 148 | ax-mp 5 |
. . . . . . 7
⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀)) ↔ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran
((𝐺 ∘ 𝐾) ↾ (1...𝑀))) |
150 | 147, 149 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀))) |
151 | | f1ofo 6285 |
. . . . . 6
⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀)) → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀))) |
152 | 150, 151 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀))) |
153 | | fofi 8407 |
. . . . 5
⊢
(((1...𝑀) ∈ Fin
∧ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin) |
154 | 43, 152, 153 | syl2anc 565 |
. . . 4
⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin) |
155 | | fimaxre2 11170 |
. . . 4
⊢ ((((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ ∧ ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) |
156 | 26, 154, 155 | syl2anc 565 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) |
157 | 42, 156 | r19.29a 3225 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧) |
158 | 97, 96 | resubcld 10659 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
159 | 158 | rexrd 10290 |
. . . 4
⊢ (𝜑 → (𝐵 − 𝐴) ∈
ℝ*) |
160 | 159 | adantr 466 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ∈
ℝ*) |
161 | | fzfid 12979 |
. . . . . 6
⊢ (𝜑 → (1...𝑧) ∈ Fin) |
162 | | elfznn 12576 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...𝑧) → 𝑗 ∈ ℕ) |
163 | | eqid 2770 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) |
164 | 163 | ovolfsf 23458 |
. . . . . . . . . . 11
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞)) |
165 | 100, 164 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐹):ℕ⟶(0[,)+∞)) |
166 | 165 | ffvelrnda 6502 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞)) |
167 | 162, 166 | sylan2 572 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ (0[,)+∞)) |
168 | | elrege0 12484 |
. . . . . . . 8
⊢ ((((abs
∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs
∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐹)‘𝑗))) |
169 | 167, 168 | sylib 208 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → ((((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐹)‘𝑗))) |
170 | 169 | simpld 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℝ) |
171 | 161, 170 | fsumrecl 14672 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
172 | 171 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
173 | 172 | rexrd 10290 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈
ℝ*) |
174 | 163, 99 | ovolsf 23459 |
. . . . . . . . 9
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
175 | 100, 174 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞)) |
176 | | frn 6193 |
. . . . . . . 8
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ ran 𝑆 ⊆
(0[,)+∞)) |
177 | 175, 176 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞)) |
178 | | rge0ssre 12486 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
179 | 177, 178 | syl6ss 3762 |
. . . . . 6
⊢ (𝜑 → ran 𝑆 ⊆ ℝ) |
180 | | ressxr 10284 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
181 | 179, 180 | syl6ss 3762 |
. . . . 5
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
182 | | supxrcl 12349 |
. . . . 5
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
183 | 181, 182 | syl 17 |
. . . 4
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
184 | 183 | adantr 466 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
185 | 158 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ∈ ℝ) |
186 | 24 | sselda 3750 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑗 ∈ ℕ) |
187 | 178, 166 | sseldi 3748 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
188 | 186, 187 | syldan 571 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℝ) |
189 | 154, 188 | fsumrecl 14672 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
190 | 189 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
191 | | inss2 3980 |
. . . . . . . . . . 11
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
192 | | fss 6196 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
193 | 100, 191,
192 | sylancl 566 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
194 | 66, 120 | sseldi 3748 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℕ) |
195 | 15, 194 | ffvelrnd 6503 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘𝑀) ∈ 𝑈) |
196 | 4, 195 | ffvelrnd 6503 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘(𝐾‘𝑀)) ∈ ℕ) |
197 | 193, 196 | ffvelrnd 6503 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝐺‘(𝐾‘𝑀))) ∈ (ℝ ×
ℝ)) |
198 | | xp2nd 7347 |
. . . . . . . . 9
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑀))) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℝ) |
199 | 197, 198 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℝ) |
200 | 13, 8 | sseldi 3748 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ 𝑈) |
201 | 4, 200 | ffvelrnd 6503 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝐶) ∈ ℕ) |
202 | 193, 201 | ffvelrnd 6503 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝐺‘𝐶)) ∈ (ℝ ×
ℝ)) |
203 | | xp1st 7346 |
. . . . . . . . 9
⊢ ((𝐹‘(𝐺‘𝐶)) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘(𝐺‘𝐶))) ∈ ℝ) |
204 | 202, 203 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘(𝐹‘(𝐺‘𝐶))) ∈ ℝ) |
205 | 199, 204 | resubcld 10659 |
. . . . . . 7
⊢ (𝜑 → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) ∈ ℝ) |
206 | | fveq2 6332 |
. . . . . . . . . 10
⊢ (𝑗 = (𝐺‘(𝐾‘𝑖)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖)))) |
207 | 187 | recnd 10269 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑗) ∈ ℂ) |
208 | 186, 207 | syldan 571 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℂ) |
209 | 206, 43, 150, 48, 208 | fsumf1o 14661 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖)))) |
210 | 100 | adantr 466 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
211 | 4 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐺:𝑈⟶ℕ) |
212 | | ffvelrn 6500 |
. . . . . . . . . . . . 13
⊢ ((𝐾:ℕ⟶𝑈 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑈) |
213 | 15, 18, 212 | syl2an 575 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝑈) |
214 | 211, 213 | ffvelrnd 6503 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐾‘𝑖)) ∈ ℕ) |
215 | 163 | ovolfsval 23457 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝐺‘(𝐾‘𝑖)) ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
216 | 210, 214,
215 | syl2anc 565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((abs ∘ − ) ∘
𝐹)‘(𝐺‘(𝐾‘𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
217 | 216 | sumeq2dv 14640 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
218 | 193 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
219 | 4 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐺:𝑈⟶ℕ) |
220 | 15 | ffvelrnda 6502 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑈) |
221 | 219, 220 | ffvelrnd 6503 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐺‘(𝐾‘𝑖)) ∈ ℕ) |
222 | 218, 221 | ffvelrnd 6503 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ ×
ℝ)) |
223 | | xp2nd 7347 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
224 | 222, 223 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
225 | 18, 224 | sylan2 572 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
226 | 225 | recnd 10269 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ) |
227 | 193 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
228 | 227, 214 | ffvelrnd 6503 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ ×
ℝ)) |
229 | | xp1st 7346 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
230 | 228, 229 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
231 | 230 | recnd 10269 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ) |
232 | 43, 226, 231 | fsumsub 14726 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
233 | 69, 120 | sseldi 3748 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
234 | | fveq2 6332 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑀 → (𝐾‘𝑖) = (𝐾‘𝑀)) |
235 | 234 | fveq2d 6336 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑀 → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑀))) |
236 | 235 | fveq2d 6336 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑀 → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑀)))) |
237 | 236 | fveq2d 6336 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑀 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))) |
238 | 233, 226,
237 | fsumm1 14687 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))) |
239 | | fzfid 12979 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...(𝑀 − 1)) ∈ Fin) |
240 | | elfznn 12576 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℕ) |
241 | 240, 224 | sylan2 572 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
242 | 239, 241 | fsumrecl 14672 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
243 | 242 | recnd 10269 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ) |
244 | 199 | recnd 10269 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℂ) |
245 | 243, 244 | addcomd 10439 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
246 | 238, 245 | eqtrd 2804 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
247 | | fveq2 6332 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 1 → (𝐾‘𝑖) = (𝐾‘1)) |
248 | 247 | fveq2d 6336 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 1 → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘1))) |
249 | 248 | fveq2d 6336 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 1 → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘1)))) |
250 | 249 | fveq2d 6336 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 1 → (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘1))))) |
251 | 233, 231,
250 | fsum1p 14689 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
252 | 5, 6, 7, 8 | algr0 15492 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐾‘1) = 𝐶) |
253 | 252 | fveq2d 6336 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺‘(𝐾‘1)) = (𝐺‘𝐶)) |
254 | 253 | fveq2d 6336 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘(𝐺‘(𝐾‘1))) = (𝐹‘(𝐺‘𝐶))) |
255 | 254 | fveq2d 6336 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1st
‘(𝐹‘(𝐺‘(𝐾‘1)))) = (1st ‘(𝐹‘(𝐺‘𝐶)))) |
256 | 7 | peano2zd 11686 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 + 1) ∈
ℤ) |
257 | 194 | nnzd 11682 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℤ) |
258 | | fzp1ss 12598 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℤ → ((1 + 1)...𝑀) ⊆ (1...𝑀)) |
259 | 70, 258 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 + 1)...𝑀) ⊆ (1...𝑀)) |
260 | 259 | sselda 3750 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((1 + 1)...𝑀)) → 𝑖 ∈ (1...𝑀)) |
261 | 260, 231 | syldan 571 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((1 + 1)...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ) |
262 | | fveq2 6332 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = (𝑗 + 1) → (𝐾‘𝑖) = (𝐾‘(𝑗 + 1))) |
263 | 262 | fveq2d 6336 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑗 + 1) → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘(𝑗 + 1)))) |
264 | 263 | fveq2d 6336 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑗 + 1) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) |
265 | 264 | fveq2d 6336 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑗 + 1) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))) |
266 | 7, 256, 257, 261, 265 | fsumshftm 14719 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))) |
267 | | ax-1cn 10195 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
268 | 267, 267 | pncan3oi 10498 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 + 1)
− 1) = 1 |
269 | 268 | oveq1i 6802 |
. . . . . . . . . . . . . . . 16
⊢ (((1 + 1)
− 1)...(𝑀 − 1))
= (1...(𝑀 −
1)) |
270 | 269 | sumeq1i 14635 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑗 ∈ (((1
+ 1) − 1)...(𝑀
− 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) |
271 | | fvoveq1 6815 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑖 → (𝐾‘(𝑗 + 1)) = (𝐾‘(𝑖 + 1))) |
272 | 271 | fveq2d 6336 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑖 → (𝐺‘(𝐾‘(𝑗 + 1))) = (𝐺‘(𝐾‘(𝑖 + 1)))) |
273 | 272 | fveq2d 6336 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑖 → (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))) = (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) |
274 | 273 | fveq2d 6336 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑖 → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) |
275 | 274 | cbvsumv 14633 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑗 ∈
(1...(𝑀 −
1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) |
276 | 270, 275 | eqtri 2792 |
. . . . . . . . . . . . . 14
⊢
Σ𝑗 ∈ (((1
+ 1) − 1)...(𝑀
− 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) |
277 | 266, 276 | syl6eq 2820 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) |
278 | 255, 277 | oveq12d 6810 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1st
‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) |
279 | 251, 278 | eqtrd 2804 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) |
280 | 246, 279 | oveq12d 6810 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) − ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
281 | 204 | recnd 10269 |
. . . . . . . . . . 11
⊢ (𝜑 → (1st
‘(𝐹‘(𝐺‘𝐶))) ∈ ℂ) |
282 | | peano2nn 11233 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℕ → (𝑖 + 1) ∈
ℕ) |
283 | | ffvelrn 6500 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾:ℕ⟶𝑈 ∧ (𝑖 + 1) ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈) |
284 | 15, 282, 283 | syl2an 575 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈) |
285 | 219, 284 | ffvelrnd 6503 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐺‘(𝐾‘(𝑖 + 1))) ∈ ℕ) |
286 | 218, 285 | ffvelrnd 6503 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ ×
ℝ)) |
287 | | xp1st 7346 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ)
→ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ) |
288 | 286, 287 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ) |
289 | 240, 288 | sylan2 572 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ) |
290 | 239, 289 | fsumrecl 14672 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ) |
291 | 290 | recnd 10269 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℂ) |
292 | 244, 243,
281, 291 | addsub4d 10640 |
. . . . . . . . . 10
⊢ (𝜑 → (((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) − ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
293 | 232, 280,
292 | 3eqtrd 2808 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
294 | 209, 217,
293 | 3eqtrd 2808 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
295 | 294, 189 | eqeltrrd 2850 |
. . . . . . 7
⊢ (𝜑 → (((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) ∈ ℝ) |
296 | | fveq2 6332 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑀 → (𝐾‘𝑛) = (𝐾‘𝑀)) |
297 | 296 | eleq2d 2835 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑀 → (𝐵 ∈ (𝐾‘𝑛) ↔ 𝐵 ∈ (𝐾‘𝑀))) |
298 | 297, 64 | elrab2 3516 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ 𝑊 ↔ (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾‘𝑀))) |
299 | 120, 298 | sylib 208 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾‘𝑀))) |
300 | 299 | simprd 477 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ (𝐾‘𝑀)) |
301 | 96, 97, 98, 99, 100, 73, 101, 4, 102 | ovolicc2lem1 23504 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐾‘𝑀) ∈ 𝑈) → (𝐵 ∈ (𝐾‘𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))))) |
302 | 195, 301 | mpdan 659 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 ∈ (𝐾‘𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))))) |
303 | 300, 302 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))) |
304 | 303 | simp3d 1137 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))) |
305 | 96, 97, 98, 99, 100, 73, 101, 4, 102 | ovolicc2lem1 23504 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 ∈ 𝑈) → (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2nd ‘(𝐹‘(𝐺‘𝐶)))))) |
306 | 200, 305 | mpdan 659 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2nd ‘(𝐹‘(𝐺‘𝐶)))))) |
307 | 104, 306 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2nd ‘(𝐹‘(𝐺‘𝐶))))) |
308 | 307 | simp2d 1136 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘(𝐹‘(𝐺‘𝐶))) < 𝐴) |
309 | 97, 204, 199, 96, 304, 308 | lt2subd 10852 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐴) < ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶))))) |
310 | 158, 205,
309 | ltled 10386 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ≤ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶))))) |
311 | 240 | adantl 467 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℕ) |
312 | | simpr 471 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (1...(𝑀 − 1))) |
313 | 257 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ) |
314 | | elfzm11 12617 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℤ ∧ 𝑀
∈ ℤ) → (𝑖
∈ (1...(𝑀 − 1))
↔ (𝑖 ∈ ℤ
∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀))) |
315 | 70, 313, 314 | sylancr 567 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀))) |
316 | 312, 315 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀)) |
317 | 316 | simp3d 1137 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀) |
318 | 311 | nnred 11236 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ) |
319 | 121 | adantr 466 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ) |
320 | 318, 319 | ltnled 10385 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 < 𝑀 ↔ ¬ 𝑀 ≤ 𝑖)) |
321 | 317, 320 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑀 ≤ 𝑖) |
322 | | infssuzle 11973 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ⊆
(ℤ≥‘1) ∧ 𝑖 ∈ 𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑖) |
323 | 69, 322 | mpan 662 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ 𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑖) |
324 | 68, 323 | syl5eqbr 4819 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ 𝑊 → 𝑀 ≤ 𝑖) |
325 | 321, 324 | nsyl 137 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑖 ∈ 𝑊) |
326 | 311, 325 | jca 495 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℕ ∧ ¬ 𝑖 ∈ 𝑊)) |
327 | 96, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64 | ovolicc2lem2 23505 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑖 ∈ ℕ ∧ ¬ 𝑖 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵) |
328 | 326, 327 | syldan 571 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵) |
329 | 328 | iftrued 4231 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → if((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
330 | | fveq2 6332 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = (𝐾‘𝑖) → (𝐺‘𝑡) = (𝐺‘(𝐾‘𝑖))) |
331 | 330 | fveq2d 6336 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = (𝐾‘𝑖) → (𝐹‘(𝐺‘𝑡)) = (𝐹‘(𝐺‘(𝐾‘𝑖)))) |
332 | 331 | fveq2d 6336 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = (𝐾‘𝑖) → (2nd ‘(𝐹‘(𝐺‘𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
333 | 332 | breq1d 4794 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (𝐾‘𝑖) → ((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵)) |
334 | 333, 332 | ifbieq1d 4246 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (𝐾‘𝑖) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵)) |
335 | | fveq2 6332 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (𝐾‘𝑖) → (𝐻‘𝑡) = (𝐻‘(𝐾‘𝑖))) |
336 | 334, 335 | eleq12d 2843 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝐾‘𝑖) → (if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑖)))) |
337 | 103 | ralrimiva 3114 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) |
338 | 337 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) |
339 | | ffvelrn 6500 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑇) |
340 | 10, 240, 339 | syl2an 575 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘𝑖) ∈ 𝑇) |
341 | 336, 338,
340 | rspcdva 3464 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → if((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑖))) |
342 | 329, 341 | eqeltrrd 2850 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐻‘(𝐾‘𝑖))) |
343 | 5, 6, 7, 8, 9 | algrp1 15494 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾‘𝑖))) |
344 | 240, 343 | sylan2 572 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾‘𝑖))) |
345 | 342, 344 | eleqtrrd 2852 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1))) |
346 | 240, 284 | sylan2 572 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) ∈ 𝑈) |
347 | 96, 97, 98, 99, 100, 73, 101, 4, 102 | ovolicc2lem1 23504 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐾‘(𝑖 + 1)) ∈ 𝑈) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
348 | 346, 347 | syldan 571 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
349 | 345, 348 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) |
350 | 349 | simp2d 1136 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
351 | 289, 241,
350 | ltled 10386 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
352 | 239, 289,
241, 351 | fsumle 14737 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
353 | 242, 290 | subge0d 10818 |
. . . . . . . . 9
⊢ (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
354 | 352, 353 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) |
355 | 242, 290 | resubcld 10659 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ∈ ℝ) |
356 | 205, 355 | addge01d 10816 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))) |
357 | 354, 356 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
358 | 158, 205,
295, 310, 357 | letrd 10395 |
. . . . . 6
⊢ (𝜑 → (𝐵 − 𝐴) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
359 | 358, 294 | breqtrrd 4812 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
360 | 359 | adantr 466 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
361 | | fzfid 12979 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (1...𝑧) ∈ Fin) |
362 | 170 | adantlr 686 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℝ) |
363 | 169 | simprd 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − )
∘ 𝐹)‘𝑗)) |
364 | 363 | adantlr 686 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − )
∘ 𝐹)‘𝑗)) |
365 | 24 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℕ) |
366 | 365 | sselda 3750 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℕ) |
367 | 366 | nnred 11236 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ) |
368 | 31 | ad2antlr 698 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ) |
369 | | ltle 10327 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧)) |
370 | 367, 368,
369 | syl2anc 565 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧)) |
371 | 366, 5 | syl6eleq 2859 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈
(ℤ≥‘1)) |
372 | | nnz 11600 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℤ) |
373 | 372 | ad2antlr 698 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℤ) |
374 | | elfz5 12540 |
. . . . . . . . . 10
⊢ ((𝑦 ∈
(ℤ≥‘1) ∧ 𝑧 ∈ ℤ) → (𝑦 ∈ (1...𝑧) ↔ 𝑦 ≤ 𝑧)) |
375 | 371, 373,
374 | syl2anc 565 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 ∈ (1...𝑧) ↔ 𝑦 ≤ 𝑧)) |
376 | 370, 375 | sylibrd 249 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 < 𝑧 → 𝑦 ∈ (1...𝑧))) |
377 | 376 | ralimdva 3110 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))) |
378 | 377 | impr 442 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)) |
379 | | dfss3 3739 |
. . . . . 6
⊢ (((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ (1...𝑧) ↔ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)) |
380 | 378, 379 | sylibr 224 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ (1...𝑧)) |
381 | 361, 362,
364, 380 | fsumless 14734 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
382 | 185, 190,
172, 360, 381 | letrd 10395 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
383 | | eqidd 2771 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
384 | | simprl 746 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ ℕ) |
385 | 384, 5 | syl6eleq 2859 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈
(ℤ≥‘1)) |
386 | 362 | recnd 10269 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℂ) |
387 | 383, 385,
386 | fsumser 14668 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑧)) |
388 | 99 | fveq1i 6333 |
. . . . 5
⊢ (𝑆‘𝑧) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑧) |
389 | 387, 388 | syl6eqr 2822 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (𝑆‘𝑧)) |
390 | 181 | adantr 466 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ran 𝑆 ⊆
ℝ*) |
391 | | ffn 6185 |
. . . . . . . 8
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ 𝑆 Fn
ℕ) |
392 | 175, 391 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆 Fn ℕ) |
393 | 392 | adantr 466 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑆 Fn ℕ) |
394 | | fnfvelrn 6499 |
. . . . . 6
⊢ ((𝑆 Fn ℕ ∧ 𝑧 ∈ ℕ) → (𝑆‘𝑧) ∈ ran 𝑆) |
395 | 393, 384,
394 | syl2anc 565 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆‘𝑧) ∈ ran 𝑆) |
396 | | supxrub 12358 |
. . . . 5
⊢ ((ran
𝑆 ⊆
ℝ* ∧ (𝑆‘𝑧) ∈ ran 𝑆) → (𝑆‘𝑧) ≤ sup(ran 𝑆, ℝ*, <
)) |
397 | 390, 395,
396 | syl2anc 565 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆‘𝑧) ≤ sup(ran 𝑆, ℝ*, <
)) |
398 | 389, 397 | eqbrtrd 4806 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ sup(ran 𝑆, ℝ*, <
)) |
399 | 160, 173,
184, 382, 398 | xrletrd 12197 |
. 2
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, <
)) |
400 | 157, 399 | rexlimddv 3182 |
1
⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, <
)) |