Step | Hyp | Ref
| Expression |
1 | | arch 11644 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
∃𝑧 ∈ ℕ
𝑥 < 𝑧) |
2 | 1 | ad2antlr 717 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → ∃𝑧 ∈ ℕ 𝑥 < 𝑧) |
3 | | df-ima 5370 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∘ 𝐾) “ (1...𝑀)) = ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) |
4 | | ovolicc2.8 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐺:𝑈⟶ℕ) |
5 | | nnuz 12034 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℕ =
(ℤ≥‘1) |
6 | | ovolicc2.15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ ×
{𝐶})) |
7 | | 1zzd 11765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ∈
ℤ) |
8 | | ovolicc2.14 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐶 ∈ 𝑇) |
9 | | ovolicc2.11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐻:𝑇⟶𝑇) |
10 | 5, 6, 7, 8, 9 | algrf 15702 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾:ℕ⟶𝑇) |
11 | | ovolicc2.10 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} |
12 | | ssrab2 3908 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⊆ 𝑈 |
13 | 11, 12 | eqsstri 3854 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑇 ⊆ 𝑈 |
14 | | fss 6306 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑇 ⊆ 𝑈) → 𝐾:ℕ⟶𝑈) |
15 | 10, 13, 14 | sylancl 580 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾:ℕ⟶𝑈) |
16 | | fco 6310 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺:𝑈⟶ℕ ∧ 𝐾:ℕ⟶𝑈) → (𝐺 ∘ 𝐾):ℕ⟶ℕ) |
17 | 4, 15, 16 | syl2anc 579 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺 ∘ 𝐾):ℕ⟶ℕ) |
18 | | elfznn 12692 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ) |
19 | 18 | ssriv 3825 |
. . . . . . . . . . . . . . . . . 18
⊢
(1...𝑀) ⊆
ℕ |
20 | | fssres 6322 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∘ 𝐾):ℕ⟶ℕ ∧ (1...𝑀) ⊆ ℕ) →
((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ) |
21 | 17, 19, 20 | sylancl 580 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ) |
22 | 21 | frnd 6300 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) ⊆ ℕ) |
23 | 3, 22 | syl5eqss 3868 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℕ) |
24 | | nnssre 11383 |
. . . . . . . . . . . . . . 15
⊢ ℕ
⊆ ℝ |
25 | 23, 24 | syl6ss 3833 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ) |
26 | 25 | ad3antrrr 720 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ) |
27 | | simpr 479 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) |
28 | 26, 27 | sseldd 3822 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ) |
29 | | simpllr 766 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑥 ∈ ℝ) |
30 | | nnre 11387 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) |
31 | 30 | ad2antlr 717 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ) |
32 | | lelttr 10469 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧) → 𝑦 < 𝑧)) |
33 | 28, 29, 31, 32 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧) → 𝑦 < 𝑧)) |
34 | 33 | ancomsd 459 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝑥 < 𝑧 ∧ 𝑦 ≤ 𝑥) → 𝑦 < 𝑧)) |
35 | 34 | expdimp 446 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) ∧ 𝑥 < 𝑧) → (𝑦 ≤ 𝑥 → 𝑦 < 𝑧)) |
36 | 35 | an32s 642 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 ≤ 𝑥 → 𝑦 < 𝑧)) |
37 | 36 | ralimdva 3144 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) → (∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) |
38 | 37 | impancom 445 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) |
39 | 38 | an32s 642 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) ∧ 𝑧 ∈ ℕ) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) |
40 | 39 | reximdva 3198 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → (∃𝑧 ∈ ℕ 𝑥 < 𝑧 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) |
41 | 2, 40 | mpd 15 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧) |
42 | | fzfid 13096 |
. . . . 5
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
43 | | fvres 6467 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑀) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺 ∘ 𝐾)‘𝑖)) |
44 | 43 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺 ∘ 𝐾)‘𝑖)) |
45 | | fvco3 6537 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑖 ∈ ℕ) → ((𝐺 ∘ 𝐾)‘𝑖) = (𝐺‘(𝐾‘𝑖))) |
46 | 10, 18, 45 | syl2an 589 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝐾)‘𝑖) = (𝐺‘(𝐾‘𝑖))) |
47 | 44, 46 | eqtrd 2814 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾‘𝑖))) |
48 | 47 | adantrr 707 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾‘𝑖))) |
49 | | fvres 6467 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺 ∘ 𝐾)‘𝑗)) |
50 | 49 | ad2antll 719 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺 ∘ 𝐾)‘𝑗)) |
51 | | elfznn 12692 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ) |
52 | 51 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ) |
53 | | fvco3 6537 |
. . . . . . . . . . . . . 14
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑗 ∈ ℕ) → ((𝐺 ∘ 𝐾)‘𝑗) = (𝐺‘(𝐾‘𝑗))) |
54 | 10, 52, 53 | syl2an 589 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺 ∘ 𝐾)‘𝑗) = (𝐺‘(𝐾‘𝑗))) |
55 | 50, 54 | eqtrd 2814 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = (𝐺‘(𝐾‘𝑗))) |
56 | 48, 55 | eqeq12d 2793 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) ↔ (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)))) |
57 | | 2fveq3 6453 |
. . . . . . . . . . . 12
⊢ ((𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))) |
58 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...𝑀) ⊆ ℕ) |
59 | | elfznn 12692 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ) |
60 | 59 | ad2antlr 717 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ∈ ℕ) |
61 | 60 | nnred 11396 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ∈ ℝ) |
62 | | ovolicc2.16 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} |
63 | | ssrab2 3908 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} ⊆ ℕ |
64 | 62, 63 | eqsstri 3854 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑊 ⊆
ℕ |
65 | 64, 24 | sstri 3830 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑊 ⊆
ℝ |
66 | | ovolicc2.17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑀 = inf(𝑊, ℝ, < ) |
67 | 64, 5 | sseqtri 3856 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑊 ⊆
(ℤ≥‘1) |
68 | | 1z 11764 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℤ |
69 | 5 | uzinf 13088 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 ∈
ℤ → ¬ ℕ ∈ Fin) |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ¬
ℕ ∈ Fin |
71 | | ovolicc2.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) |
72 | | elin 4019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑈 ∈ (𝒫 ran ((,)
∘ 𝐹) ∩ Fin)
↔ (𝑈 ∈ 𝒫
ran ((,) ∘ 𝐹) ∧
𝑈 ∈
Fin)) |
73 | 71, 72 | sylib 210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin)) |
74 | 73 | simprd 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑈 ∈ Fin) |
75 | | ssfi 8470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑈 ∈ Fin ∧ 𝑇 ⊆ 𝑈) → 𝑇 ∈ Fin) |
76 | 74, 13, 75 | sylancl 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑇 ∈ Fin) |
77 | 76 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑇 ∈ Fin) |
78 | 10 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐾:ℕ⟶𝑇) |
79 | | 2fveq3 6453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑗)))) |
80 | 79 | fveq2d 6452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))) |
81 | | simpll 757 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝜑) |
82 | | simprl 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℕ) |
83 | | ral0 4299 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
∀𝑚 ∈
∅ 𝑛 ≤ 𝑚 |
84 | | simplr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑊 = ∅) |
85 | 84 | raleqdv 3340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 ↔ ∀𝑚 ∈ ∅ 𝑛 ≤ 𝑚)) |
86 | 83, 85 | mpbiri 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚) |
87 | 86 | ralrimivw 3149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚) |
88 | | rabid2 3305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (ℕ
= {𝑛 ∈ ℕ ∣
∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ↔ ∀𝑛 ∈ ℕ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚) |
89 | 87, 88 | sylibr 226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ℕ = {𝑛 ∈ ℕ ∣
∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
90 | 82, 89 | eleqtrd 2861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
91 | | simprr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℕ) |
92 | 91, 89 | eleqtrd 2861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
93 | | ovolicc.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐴 ∈ ℝ) |
94 | | ovolicc.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐵 ∈ ℝ) |
95 | | ovolicc.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
96 | | ovolicc2.4 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
97 | | ovolicc2.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
98 | | ovolicc2.7 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) |
99 | | ovolicc2.9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑈) → (((,) ∘ 𝐹)‘(𝐺‘𝑡)) = 𝑡) |
100 | | ovolicc2.12 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) |
101 | | ovolicc2.13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐴 ∈ 𝐶) |
102 | 93, 94, 95, 96, 97, 71, 98, 4, 99, 11, 9, 100, 101, 8, 6, 62 | ovolicc2lem3 23734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))) |
103 | 81, 90, 92, 102 | syl12anc 827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))) |
104 | 80, 103 | syl5ibr 238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗)) |
105 | 104 | ralrimivva 3153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑊 = ∅) → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗)) |
106 | | dff13 6786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐾:ℕ–1-1→𝑇 ↔ (𝐾:ℕ⟶𝑇 ∧ ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗))) |
107 | 78, 105, 106 | sylanbrc 578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐾:ℕ–1-1→𝑇) |
108 | | f1domg 8263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑇 ∈ Fin → (𝐾:ℕ–1-1→𝑇 → ℕ ≼ 𝑇)) |
109 | 77, 107, 108 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑊 = ∅) → ℕ ≼ 𝑇) |
110 | | domfi 8471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑇 ∈ Fin ∧ ℕ
≼ 𝑇) → ℕ
∈ Fin) |
111 | 77, 109, 110 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑊 = ∅) → ℕ ∈
Fin) |
112 | 111 | ex 403 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑊 = ∅ → ℕ ∈
Fin)) |
113 | 112 | necon3bd 2983 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (¬ ℕ ∈ Fin
→ 𝑊 ≠
∅)) |
114 | 70, 113 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑊 ≠ ∅) |
115 | | infssuzcl 12084 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑊 ⊆
(ℤ≥‘1) ∧ 𝑊 ≠ ∅) → inf(𝑊, ℝ, < ) ∈ 𝑊) |
116 | 67, 114, 115 | sylancr 581 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → inf(𝑊, ℝ, < ) ∈ 𝑊) |
117 | 66, 116 | syl5eqel 2863 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ∈ 𝑊) |
118 | 65, 117 | sseldi 3819 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℝ) |
119 | 118 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑀 ∈ ℝ) |
120 | 65 | sseli 3817 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ 𝑊 → 𝑚 ∈ ℝ) |
121 | 120 | adantl 475 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑚 ∈ ℝ) |
122 | | elfzle2 12667 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ≤ 𝑀) |
123 | 122 | ad2antlr 717 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ≤ 𝑀) |
124 | | infssuzle 12083 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ⊆
(ℤ≥‘1) ∧ 𝑚 ∈ 𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑚) |
125 | 67, 124 | mpan 680 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ 𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑚) |
126 | 66, 125 | syl5eqbr 4923 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ 𝑊 → 𝑀 ≤ 𝑚) |
127 | 126 | adantl 475 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑀 ≤ 𝑚) |
128 | 61, 119, 121, 123, 127 | letrd 10535 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ≤ 𝑚) |
129 | 128 | ralrimiva 3148 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚) |
130 | 58, 129 | ssrabdv 3902 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
131 | 130 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
132 | | simprl 761 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ (1...𝑀)) |
133 | 131, 132 | sseldd 3822 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
134 | | simprr 763 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ (1...𝑀)) |
135 | 131, 134 | sseldd 3822 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
136 | 133, 135 | jca 507 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) |
137 | 136, 102 | syldan 585 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))) |
138 | 57, 137 | syl5ibr 238 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)) → 𝑖 = 𝑗)) |
139 | 56, 138 | sylbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗)) |
140 | 139 | ralrimivva 3153 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗)) |
141 | | dff13 6786 |
. . . . . . . . 9
⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ ↔ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ ∧ ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))) |
142 | 21, 140, 141 | sylanbrc 578 |
. . . . . . . 8
⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ) |
143 | | f1f1orn 6404 |
. . . . . . . 8
⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran
((𝐺 ∘ 𝐾) ↾ (1...𝑀))) |
144 | 142, 143 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran
((𝐺 ∘ 𝐾) ↾ (1...𝑀))) |
145 | | f1oeq3 6384 |
. . . . . . . 8
⊢ (((𝐺 ∘ 𝐾) “ (1...𝑀)) = ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀)) ↔ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran
((𝐺 ∘ 𝐾) ↾ (1...𝑀)))) |
146 | 3, 145 | ax-mp 5 |
. . . . . . 7
⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀)) ↔ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→ran
((𝐺 ∘ 𝐾) ↾ (1...𝑀))) |
147 | 144, 146 | sylibr 226 |
. . . . . 6
⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀))) |
148 | | f1ofo 6400 |
. . . . . 6
⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀)) → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀))) |
149 | 147, 148 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀))) |
150 | | fofi 8542 |
. . . . 5
⊢
(((1...𝑀) ∈ Fin
∧ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin) |
151 | 42, 149, 150 | syl2anc 579 |
. . . 4
⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin) |
152 | | fimaxre2 11327 |
. . . 4
⊢ ((((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ ∧ ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) |
153 | 25, 151, 152 | syl2anc 579 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) |
154 | 41, 153 | r19.29a 3264 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧) |
155 | 94, 93 | resubcld 10806 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
156 | 155 | rexrd 10428 |
. . . 4
⊢ (𝜑 → (𝐵 − 𝐴) ∈
ℝ*) |
157 | 156 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ∈
ℝ*) |
158 | | fzfid 13096 |
. . . . . 6
⊢ (𝜑 → (1...𝑧) ∈ Fin) |
159 | | elfznn 12692 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...𝑧) → 𝑗 ∈ ℕ) |
160 | | eqid 2778 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) |
161 | 160 | ovolfsf 23686 |
. . . . . . . . . . 11
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞)) |
162 | 97, 161 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐹):ℕ⟶(0[,)+∞)) |
163 | 162 | ffvelrnda 6625 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞)) |
164 | 159, 163 | sylan2 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ (0[,)+∞)) |
165 | | elrege0 12597 |
. . . . . . . 8
⊢ ((((abs
∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs
∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐹)‘𝑗))) |
166 | 164, 165 | sylib 210 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → ((((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐹)‘𝑗))) |
167 | 166 | simpld 490 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℝ) |
168 | 158, 167 | fsumrecl 14881 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
169 | 168 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
170 | 169 | rexrd 10428 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈
ℝ*) |
171 | 160, 96 | ovolsf 23687 |
. . . . . . . . 9
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
172 | 97, 171 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞)) |
173 | 172 | frnd 6300 |
. . . . . . 7
⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞)) |
174 | | rge0ssre 12599 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
175 | 173, 174 | syl6ss 3833 |
. . . . . 6
⊢ (𝜑 → ran 𝑆 ⊆ ℝ) |
176 | | ressxr 10422 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
177 | 175, 176 | syl6ss 3833 |
. . . . 5
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
178 | | supxrcl 12462 |
. . . . 5
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
179 | 177, 178 | syl 17 |
. . . 4
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
180 | 179 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
181 | 155 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ∈ ℝ) |
182 | 23 | sselda 3821 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑗 ∈ ℕ) |
183 | 174, 163 | sseldi 3819 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
184 | 182, 183 | syldan 585 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℝ) |
185 | 151, 184 | fsumrecl 14881 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
186 | 185 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
187 | | inss2 4054 |
. . . . . . . . . . 11
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
188 | | fss 6306 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
189 | 97, 187, 188 | sylancl 580 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
190 | 64, 117 | sseldi 3819 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℕ) |
191 | 15, 190 | ffvelrnd 6626 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘𝑀) ∈ 𝑈) |
192 | 4, 191 | ffvelrnd 6626 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘(𝐾‘𝑀)) ∈ ℕ) |
193 | 189, 192 | ffvelrnd 6626 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝐺‘(𝐾‘𝑀))) ∈ (ℝ ×
ℝ)) |
194 | | xp2nd 7480 |
. . . . . . . . 9
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑀))) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℝ) |
195 | 193, 194 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℝ) |
196 | 13, 8 | sseldi 3819 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ 𝑈) |
197 | 4, 196 | ffvelrnd 6626 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝐶) ∈ ℕ) |
198 | 189, 197 | ffvelrnd 6626 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝐺‘𝐶)) ∈ (ℝ ×
ℝ)) |
199 | | xp1st 7479 |
. . . . . . . . 9
⊢ ((𝐹‘(𝐺‘𝐶)) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘(𝐺‘𝐶))) ∈ ℝ) |
200 | 198, 199 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘(𝐹‘(𝐺‘𝐶))) ∈ ℝ) |
201 | 195, 200 | resubcld 10806 |
. . . . . . 7
⊢ (𝜑 → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) ∈ ℝ) |
202 | | fveq2 6448 |
. . . . . . . . . 10
⊢ (𝑗 = (𝐺‘(𝐾‘𝑖)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖)))) |
203 | 183 | recnd 10407 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑗) ∈ ℂ) |
204 | 182, 203 | syldan 585 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℂ) |
205 | 202, 42, 147, 47, 204 | fsumf1o 14870 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖)))) |
206 | 97 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
207 | 4 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐺:𝑈⟶ℕ) |
208 | | ffvelrn 6623 |
. . . . . . . . . . . . 13
⊢ ((𝐾:ℕ⟶𝑈 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑈) |
209 | 15, 18, 208 | syl2an 589 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝑈) |
210 | 207, 209 | ffvelrnd 6626 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐾‘𝑖)) ∈ ℕ) |
211 | 160 | ovolfsval 23685 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝐺‘(𝐾‘𝑖)) ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
212 | 206, 210,
211 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((abs ∘ − ) ∘
𝐹)‘(𝐺‘(𝐾‘𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
213 | 212 | sumeq2dv 14850 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
214 | 189 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
215 | 4 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐺:𝑈⟶ℕ) |
216 | 15 | ffvelrnda 6625 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑈) |
217 | 215, 216 | ffvelrnd 6626 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐺‘(𝐾‘𝑖)) ∈ ℕ) |
218 | 214, 217 | ffvelrnd 6626 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ ×
ℝ)) |
219 | | xp2nd 7480 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
220 | 218, 219 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
221 | 18, 220 | sylan2 586 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
222 | 221 | recnd 10407 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ) |
223 | 189 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
224 | 223, 210 | ffvelrnd 6626 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ ×
ℝ)) |
225 | | xp1st 7479 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
226 | 224, 225 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
227 | 226 | recnd 10407 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ) |
228 | 42, 222, 227 | fsumsub 14933 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
229 | 67, 117 | sseldi 3819 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
230 | | 2fveq3 6453 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑀 → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑀))) |
231 | 230 | fveq2d 6452 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑀 → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑀)))) |
232 | 231 | fveq2d 6452 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑀 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))) |
233 | 229, 222,
232 | fsumm1 14896 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))) |
234 | | fzfid 13096 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...(𝑀 − 1)) ∈ Fin) |
235 | | elfznn 12692 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℕ) |
236 | 235, 220 | sylan2 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
237 | 234, 236 | fsumrecl 14881 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
238 | 237 | recnd 10407 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ) |
239 | 195 | recnd 10407 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℂ) |
240 | 238, 239 | addcomd 10580 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
241 | 233, 240 | eqtrd 2814 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
242 | | 2fveq3 6453 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 1 → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘1))) |
243 | 242 | fveq2d 6452 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 1 → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘1)))) |
244 | 243 | fveq2d 6452 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 1 → (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘1))))) |
245 | 229, 227,
244 | fsum1p 14898 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
246 | 5, 6, 7, 8 | algr0 15701 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐾‘1) = 𝐶) |
247 | 246 | fveq2d 6452 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺‘(𝐾‘1)) = (𝐺‘𝐶)) |
248 | 247 | fveq2d 6452 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘(𝐺‘(𝐾‘1))) = (𝐹‘(𝐺‘𝐶))) |
249 | 248 | fveq2d 6452 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1st
‘(𝐹‘(𝐺‘(𝐾‘1)))) = (1st ‘(𝐹‘(𝐺‘𝐶)))) |
250 | 7 | peano2zd 11842 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 + 1) ∈
ℤ) |
251 | 190 | nnzd 11838 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℤ) |
252 | | fzp1ss 12714 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℤ → ((1 + 1)...𝑀) ⊆ (1...𝑀)) |
253 | 68, 252 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 + 1)...𝑀) ⊆ (1...𝑀)) |
254 | 253 | sselda 3821 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((1 + 1)...𝑀)) → 𝑖 ∈ (1...𝑀)) |
255 | 254, 227 | syldan 585 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((1 + 1)...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ) |
256 | | 2fveq3 6453 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑗 + 1) → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘(𝑗 + 1)))) |
257 | 256 | fveq2d 6452 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑗 + 1) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) |
258 | 257 | fveq2d 6452 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑗 + 1) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))) |
259 | 7, 250, 251, 255, 258 | fsumshftm 14926 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))) |
260 | | ax-1cn 10332 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
261 | 260, 260 | pncan3oi 10641 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 + 1)
− 1) = 1 |
262 | 261 | oveq1i 6934 |
. . . . . . . . . . . . . . . 16
⊢ (((1 + 1)
− 1)...(𝑀 − 1))
= (1...(𝑀 −
1)) |
263 | 262 | sumeq1i 14845 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑗 ∈ (((1
+ 1) − 1)...(𝑀
− 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) |
264 | | fvoveq1 6947 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑖 → (𝐾‘(𝑗 + 1)) = (𝐾‘(𝑖 + 1))) |
265 | 264 | fveq2d 6452 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑖 → (𝐺‘(𝐾‘(𝑗 + 1))) = (𝐺‘(𝐾‘(𝑖 + 1)))) |
266 | 265 | fveq2d 6452 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑖 → (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))) = (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) |
267 | 266 | fveq2d 6452 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑖 → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) |
268 | 267 | cbvsumv 14843 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑗 ∈
(1...(𝑀 −
1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) |
269 | 263, 268 | eqtri 2802 |
. . . . . . . . . . . . . 14
⊢
Σ𝑗 ∈ (((1
+ 1) − 1)...(𝑀
− 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) |
270 | 259, 269 | syl6eq 2830 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) |
271 | 249, 270 | oveq12d 6942 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1st
‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) |
272 | 245, 271 | eqtrd 2814 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) |
273 | 241, 272 | oveq12d 6942 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) − ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
274 | 200 | recnd 10407 |
. . . . . . . . . . 11
⊢ (𝜑 → (1st
‘(𝐹‘(𝐺‘𝐶))) ∈ ℂ) |
275 | | peano2nn 11393 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℕ → (𝑖 + 1) ∈
ℕ) |
276 | | ffvelrn 6623 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾:ℕ⟶𝑈 ∧ (𝑖 + 1) ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈) |
277 | 15, 275, 276 | syl2an 589 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈) |
278 | 215, 277 | ffvelrnd 6626 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐺‘(𝐾‘(𝑖 + 1))) ∈ ℕ) |
279 | 214, 278 | ffvelrnd 6626 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ ×
ℝ)) |
280 | | xp1st 7479 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ)
→ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ) |
281 | 279, 280 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ) |
282 | 235, 281 | sylan2 586 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ) |
283 | 234, 282 | fsumrecl 14881 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ) |
284 | 283 | recnd 10407 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℂ) |
285 | 239, 238,
274, 284 | addsub4d 10783 |
. . . . . . . . . 10
⊢ (𝜑 → (((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) − ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
286 | 228, 273,
285 | 3eqtrd 2818 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
287 | 205, 213,
286 | 3eqtrd 2818 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
288 | 287, 185 | eqeltrrd 2860 |
. . . . . . 7
⊢ (𝜑 → (((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) ∈ ℝ) |
289 | | fveq2 6448 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑀 → (𝐾‘𝑛) = (𝐾‘𝑀)) |
290 | 289 | eleq2d 2845 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑀 → (𝐵 ∈ (𝐾‘𝑛) ↔ 𝐵 ∈ (𝐾‘𝑀))) |
291 | 290, 62 | elrab2 3576 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ 𝑊 ↔ (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾‘𝑀))) |
292 | 117, 291 | sylib 210 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾‘𝑀))) |
293 | 292 | simprd 491 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ (𝐾‘𝑀)) |
294 | 93, 94, 95, 96, 97, 71, 98, 4, 99 | ovolicc2lem1 23732 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐾‘𝑀) ∈ 𝑈) → (𝐵 ∈ (𝐾‘𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))))) |
295 | 191, 294 | mpdan 677 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 ∈ (𝐾‘𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))))) |
296 | 293, 295 | mpbid 224 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))) |
297 | 296 | simp3d 1135 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))) |
298 | 93, 94, 95, 96, 97, 71, 98, 4, 99 | ovolicc2lem1 23732 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 ∈ 𝑈) → (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2nd ‘(𝐹‘(𝐺‘𝐶)))))) |
299 | 196, 298 | mpdan 677 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2nd ‘(𝐹‘(𝐺‘𝐶)))))) |
300 | 101, 299 | mpbid 224 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2nd ‘(𝐹‘(𝐺‘𝐶))))) |
301 | 300 | simp2d 1134 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘(𝐹‘(𝐺‘𝐶))) < 𝐴) |
302 | 94, 200, 195, 93, 297, 301 | lt2subd 11002 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐴) < ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶))))) |
303 | 155, 201,
302 | ltled 10526 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ≤ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶))))) |
304 | 235 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℕ) |
305 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (1...(𝑀 − 1))) |
306 | 251 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ) |
307 | | elfzm11 12734 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℤ ∧ 𝑀
∈ ℤ) → (𝑖
∈ (1...(𝑀 − 1))
↔ (𝑖 ∈ ℤ
∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀))) |
308 | 68, 306, 307 | sylancr 581 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀))) |
309 | 305, 308 | mpbid 224 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀)) |
310 | 309 | simp3d 1135 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀) |
311 | 304 | nnred 11396 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ) |
312 | 118 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ) |
313 | 311, 312 | ltnled 10525 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 < 𝑀 ↔ ¬ 𝑀 ≤ 𝑖)) |
314 | 310, 313 | mpbid 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑀 ≤ 𝑖) |
315 | | infssuzle 12083 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ⊆
(ℤ≥‘1) ∧ 𝑖 ∈ 𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑖) |
316 | 67, 315 | mpan 680 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ 𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑖) |
317 | 66, 316 | syl5eqbr 4923 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ 𝑊 → 𝑀 ≤ 𝑖) |
318 | 314, 317 | nsyl 138 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑖 ∈ 𝑊) |
319 | 304, 318 | jca 507 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℕ ∧ ¬ 𝑖 ∈ 𝑊)) |
320 | 93, 94, 95, 96, 97, 71, 98, 4, 99, 11, 9, 100, 101, 8, 6, 62 | ovolicc2lem2 23733 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑖 ∈ ℕ ∧ ¬ 𝑖 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵) |
321 | 319, 320 | syldan 585 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵) |
322 | 321 | iftrued 4315 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → if((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
323 | | 2fveq3 6453 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = (𝐾‘𝑖) → (𝐹‘(𝐺‘𝑡)) = (𝐹‘(𝐺‘(𝐾‘𝑖)))) |
324 | 323 | fveq2d 6452 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = (𝐾‘𝑖) → (2nd ‘(𝐹‘(𝐺‘𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
325 | 324 | breq1d 4898 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (𝐾‘𝑖) → ((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵)) |
326 | 325, 324 | ifbieq1d 4330 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (𝐾‘𝑖) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵)) |
327 | | fveq2 6448 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (𝐾‘𝑖) → (𝐻‘𝑡) = (𝐻‘(𝐾‘𝑖))) |
328 | 326, 327 | eleq12d 2853 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝐾‘𝑖) → (if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑖)))) |
329 | 100 | ralrimiva 3148 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) |
330 | 329 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) |
331 | | ffvelrn 6623 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑇) |
332 | 10, 235, 331 | syl2an 589 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘𝑖) ∈ 𝑇) |
333 | 328, 330,
332 | rspcdva 3517 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → if((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑖))) |
334 | 322, 333 | eqeltrrd 2860 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐻‘(𝐾‘𝑖))) |
335 | 5, 6, 7, 8, 9 | algrp1 15703 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾‘𝑖))) |
336 | 235, 335 | sylan2 586 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾‘𝑖))) |
337 | 334, 336 | eleqtrrd 2862 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1))) |
338 | 235, 277 | sylan2 586 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) ∈ 𝑈) |
339 | 93, 94, 95, 96, 97, 71, 98, 4, 99 | ovolicc2lem1 23732 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐾‘(𝑖 + 1)) ∈ 𝑈) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
340 | 338, 339 | syldan 585 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
341 | 337, 340 | mpbid 224 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) |
342 | 341 | simp2d 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
343 | 282, 236,
342 | ltled 10526 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
344 | 234, 282,
236, 343 | fsumle 14944 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
345 | 237, 283 | subge0d 10968 |
. . . . . . . . 9
⊢ (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
346 | 344, 345 | mpbird 249 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) |
347 | 237, 283 | resubcld 10806 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ∈ ℝ) |
348 | 201, 347 | addge01d 10966 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))) |
349 | 346, 348 | mpbid 224 |
. . . . . . 7
⊢ (𝜑 → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
350 | 155, 201,
288, 303, 349 | letrd 10535 |
. . . . . 6
⊢ (𝜑 → (𝐵 − 𝐴) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
351 | 350, 287 | breqtrrd 4916 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
352 | 351 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
353 | | fzfid 13096 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (1...𝑧) ∈ Fin) |
354 | 167 | adantlr 705 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℝ) |
355 | 166 | simprd 491 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − )
∘ 𝐹)‘𝑗)) |
356 | 355 | adantlr 705 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − )
∘ 𝐹)‘𝑗)) |
357 | 23 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℕ) |
358 | 357 | sselda 3821 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℕ) |
359 | 358 | nnred 11396 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ) |
360 | 30 | ad2antlr 717 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ) |
361 | | ltle 10467 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧)) |
362 | 359, 360,
361 | syl2anc 579 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧)) |
363 | 358, 5 | syl6eleq 2869 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈
(ℤ≥‘1)) |
364 | | nnz 11756 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℤ) |
365 | 364 | ad2antlr 717 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℤ) |
366 | | elfz5 12656 |
. . . . . . . . . 10
⊢ ((𝑦 ∈
(ℤ≥‘1) ∧ 𝑧 ∈ ℤ) → (𝑦 ∈ (1...𝑧) ↔ 𝑦 ≤ 𝑧)) |
367 | 363, 365,
366 | syl2anc 579 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 ∈ (1...𝑧) ↔ 𝑦 ≤ 𝑧)) |
368 | 362, 367 | sylibrd 251 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 < 𝑧 → 𝑦 ∈ (1...𝑧))) |
369 | 368 | ralimdva 3144 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))) |
370 | 369 | impr 448 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)) |
371 | | dfss3 3810 |
. . . . . 6
⊢ (((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ (1...𝑧) ↔ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)) |
372 | 370, 371 | sylibr 226 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ (1...𝑧)) |
373 | 353, 354,
356, 372 | fsumless 14941 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
374 | 181, 186,
169, 352, 373 | letrd 10535 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
375 | | eqidd 2779 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
376 | | simprl 761 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ ℕ) |
377 | 376, 5 | syl6eleq 2869 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈
(ℤ≥‘1)) |
378 | 354 | recnd 10407 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℂ) |
379 | 375, 377,
378 | fsumser 14877 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑧)) |
380 | 96 | fveq1i 6449 |
. . . . 5
⊢ (𝑆‘𝑧) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑧) |
381 | 379, 380 | syl6eqr 2832 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (𝑆‘𝑧)) |
382 | 177 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ran 𝑆 ⊆
ℝ*) |
383 | 172 | ffnd 6294 |
. . . . . . 7
⊢ (𝜑 → 𝑆 Fn ℕ) |
384 | 383 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑆 Fn ℕ) |
385 | | fnfvelrn 6622 |
. . . . . 6
⊢ ((𝑆 Fn ℕ ∧ 𝑧 ∈ ℕ) → (𝑆‘𝑧) ∈ ran 𝑆) |
386 | 384, 376,
385 | syl2anc 579 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆‘𝑧) ∈ ran 𝑆) |
387 | | supxrub 12471 |
. . . . 5
⊢ ((ran
𝑆 ⊆
ℝ* ∧ (𝑆‘𝑧) ∈ ran 𝑆) → (𝑆‘𝑧) ≤ sup(ran 𝑆, ℝ*, <
)) |
388 | 382, 386,
387 | syl2anc 579 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆‘𝑧) ≤ sup(ran 𝑆, ℝ*, <
)) |
389 | 381, 388 | eqbrtrd 4910 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ sup(ran 𝑆, ℝ*, <
)) |
390 | 157, 170,
180, 374, 389 | xrletrd 12310 |
. 2
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, <
)) |
391 | 154, 390 | rexlimddv 3218 |
1
⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, <
)) |