Step | Hyp | Ref
| Expression |
1 | | arch 11289 |
. . . . 5
⊢ (𝑥 ∈ ℝ →
∃𝑧 ∈ ℕ
𝑥 < 𝑧) |
2 | 1 | ad2antlr 763 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → ∃𝑧 ∈ ℕ 𝑥 < 𝑧) |
3 | | df-ima 5127 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∘ 𝐾) “ (1...𝑀)) = ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) |
4 | | ovolicc2.8 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐺:𝑈⟶ℕ) |
5 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℕ =
(ℤ≥‘1) |
6 | | ovolicc2.15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐾 = seq1((𝐻 ∘ 1st ), (ℕ ×
{𝐶})) |
7 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ∈
ℤ) |
8 | | ovolicc2.14 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐶 ∈ 𝑇) |
9 | | ovolicc2.11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐻:𝑇⟶𝑇) |
10 | 5, 6, 7, 8, 9 | algrf 15286 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾:ℕ⟶𝑇) |
11 | | ovolicc2.10 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑇 = {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} |
12 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑢 ∈ 𝑈 ∣ (𝑢 ∩ (𝐴[,]𝐵)) ≠ ∅} ⊆ 𝑈 |
13 | 11, 12 | eqsstri 3635 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑇 ⊆ 𝑈 |
14 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑇 ⊆ 𝑈) → 𝐾:ℕ⟶𝑈) |
15 | 10, 13, 14 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾:ℕ⟶𝑈) |
16 | | fco 6058 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺:𝑈⟶ℕ ∧ 𝐾:ℕ⟶𝑈) → (𝐺 ∘ 𝐾):ℕ⟶ℕ) |
17 | 4, 15, 16 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺 ∘ 𝐾):ℕ⟶ℕ) |
18 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (1...𝑀) → 𝑖 ∈ ℕ) |
19 | 18 | ssriv 3607 |
. . . . . . . . . . . . . . . . . 18
⊢
(1...𝑀) ⊆
ℕ |
20 | | fssres 6070 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∘ 𝐾):ℕ⟶ℕ ∧ (1...𝑀) ⊆ ℕ) →
((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ) |
21 | 17, 19, 20 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ) |
22 | | frn 6053 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ → ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) ⊆ ℕ) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ran ((𝐺 ∘ 𝐾) ↾ (1...𝑀)) ⊆ ℕ) |
24 | 3, 23 | syl5eqss 3649 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℕ) |
25 | | nnssre 11024 |
. . . . . . . . . . . . . . 15
⊢ ℕ
⊆ ℝ |
26 | 24, 25 | syl6ss 3615 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ) |
27 | 26 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ) |
28 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) |
29 | 27, 28 | sseldd 3604 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ) |
30 | | simpllr 799 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑥 ∈ ℝ) |
31 | | nnre 11027 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℝ) |
32 | 31 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ) |
33 | | lelttr 10128 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧) → 𝑦 < 𝑧)) |
34 | 29, 30, 32, 33 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝑦 ≤ 𝑥 ∧ 𝑥 < 𝑧) → 𝑦 < 𝑧)) |
35 | 34 | ancomsd 470 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝑥 < 𝑧 ∧ 𝑦 ≤ 𝑥) → 𝑦 < 𝑧)) |
36 | 35 | expdimp 453 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) ∧ 𝑥 < 𝑧) → (𝑦 ≤ 𝑥 → 𝑦 < 𝑧)) |
37 | 36 | an32s 846 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 ≤ 𝑥 → 𝑦 < 𝑧)) |
38 | 37 | ralimdva 2962 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ 𝑥 < 𝑧) → (∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) |
39 | 38 | impancom 456 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ℕ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) |
40 | 39 | an32s 846 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) ∧ 𝑧 ∈ ℕ) → (𝑥 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) |
41 | 40 | reximdva 3017 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → (∃𝑧 ∈ ℕ 𝑥 < 𝑧 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) |
42 | 2, 41 | mpd 15 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧) |
43 | | fzfid 12772 |
. . . . 5
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
44 | | fvres 6207 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑀) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺 ∘ 𝐾)‘𝑖)) |
45 | 44 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = ((𝐺 ∘ 𝐾)‘𝑖)) |
46 | | fvco3 6275 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑖 ∈ ℕ) → ((𝐺 ∘ 𝐾)‘𝑖) = (𝐺‘(𝐾‘𝑖))) |
47 | 10, 18, 46 | syl2an 494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺 ∘ 𝐾)‘𝑖) = (𝐺‘(𝐾‘𝑖))) |
48 | 45, 47 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾‘𝑖))) |
49 | 48 | adantrr 753 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (𝐺‘(𝐾‘𝑖))) |
50 | | fvres 6207 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (1...𝑀) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺 ∘ 𝐾)‘𝑗)) |
51 | 50 | ad2antll 765 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = ((𝐺 ∘ 𝐾)‘𝑗)) |
52 | | elfznn 12370 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀)) → 𝑗 ∈ ℕ) |
54 | | fvco3 6275 |
. . . . . . . . . . . . . 14
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑗 ∈ ℕ) → ((𝐺 ∘ 𝐾)‘𝑗) = (𝐺‘(𝐾‘𝑗))) |
55 | 10, 53, 54 | syl2an 494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((𝐺 ∘ 𝐾)‘𝑗) = (𝐺‘(𝐾‘𝑗))) |
56 | 51, 55 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) = (𝐺‘(𝐾‘𝑗))) |
57 | 49, 56 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → ((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) ↔ (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)))) |
58 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑗)))) |
59 | 58 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))) |
60 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (1...𝑀) ⊆ ℕ) |
61 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ) |
62 | 61 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ∈ ℕ) |
63 | 62 | nnred 11035 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ∈ ℝ) |
64 | | ovolicc2.16 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑊 = {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} |
65 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {𝑛 ∈ ℕ ∣ 𝐵 ∈ (𝐾‘𝑛)} ⊆ ℕ |
66 | 64, 65 | eqsstri 3635 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑊 ⊆
ℕ |
67 | 66, 25 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑊 ⊆
ℝ |
68 | | ovolicc2.17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑀 = inf(𝑊, ℝ, < ) |
69 | 66, 5 | sseqtri 3637 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑊 ⊆
(ℤ≥‘1) |
70 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℤ |
71 | 5 | uzinf 12764 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 ∈
ℤ → ¬ ℕ ∈ Fin) |
72 | 70, 71 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ¬
ℕ ∈ Fin |
73 | | ovolicc2.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → 𝑈 ∈ (𝒫 ran ((,) ∘ 𝐹) ∩ Fin)) |
74 | | elin 3796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑈 ∈ (𝒫 ran ((,)
∘ 𝐹) ∩ Fin)
↔ (𝑈 ∈ 𝒫
ran ((,) ∘ 𝐹) ∧
𝑈 ∈
Fin)) |
75 | 73, 74 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → (𝑈 ∈ 𝒫 ran ((,) ∘ 𝐹) ∧ 𝑈 ∈ Fin)) |
76 | 75 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝑈 ∈ Fin) |
77 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑈 ∈ Fin ∧ 𝑇 ⊆ 𝑈) → 𝑇 ∈ Fin) |
78 | 76, 13, 77 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑇 ∈ Fin) |
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝑇 ∈ Fin) |
80 | 10 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐾:ℕ⟶𝑇) |
81 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑗))) |
82 | 81 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑗)))) |
83 | 82 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐾‘𝑖) = (𝐾‘𝑗) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗))))) |
84 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝜑) |
85 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ ℕ) |
86 | | ral0 4076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
∀𝑚 ∈
∅ 𝑛 ≤ 𝑚 |
87 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑊 = ∅) |
88 | 87 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚 ↔ ∀𝑚 ∈ ∅ 𝑛 ≤ 𝑚)) |
89 | 86, 88 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚) |
90 | 89 | ralrimivw 2967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ∀𝑛 ∈ ℕ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚) |
91 | | rabid2 3118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (ℕ
= {𝑛 ∈ ℕ ∣
∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ↔ ∀𝑛 ∈ ℕ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚) |
92 | 90, 91 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ℕ = {𝑛 ∈ ℕ ∣
∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
93 | 85, 92 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
94 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → 𝑗 ∈ ℕ) |
95 | 94, 92 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 23287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝜑 ∧ (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))) |
106 | 84, 93, 95, 105 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → (𝑖 = 𝑗 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑗)))))) |
107 | 83, 106 | syl5ibr 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑊 = ∅) ∧ (𝑖 ∈ ℕ ∧ 𝑗 ∈ ℕ)) → ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗)) |
108 | 107 | ralrimivva 2971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑊 = ∅) → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗)) |
109 | | dff13 6512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐾:ℕ–1-1→𝑇 ↔ (𝐾:ℕ⟶𝑇 ∧ ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℕ ((𝐾‘𝑖) = (𝐾‘𝑗) → 𝑖 = 𝑗))) |
110 | 80, 108, 109 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐾:ℕ–1-1→𝑇) |
111 | | f1domg 7975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑇 ∈ Fin → (𝐾:ℕ–1-1→𝑇 → ℕ ≼ 𝑇)) |
112 | 79, 110, 111 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑊 = ∅) → ℕ ≼ 𝑇) |
113 | | domfi 8181 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑇 ∈ Fin ∧ ℕ
≼ 𝑇) → ℕ
∈ Fin) |
114 | 79, 112, 113 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑊 = ∅) → ℕ ∈
Fin) |
115 | 114 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑊 = ∅ → ℕ ∈
Fin)) |
116 | 115 | necon3bd 2808 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (¬ ℕ ∈ Fin
→ 𝑊 ≠
∅)) |
117 | 72, 116 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑊 ≠ ∅) |
118 | | infssuzcl 11772 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑊 ⊆
(ℤ≥‘1) ∧ 𝑊 ≠ ∅) → inf(𝑊, ℝ, < ) ∈ 𝑊) |
119 | 69, 117, 118 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → inf(𝑊, ℝ, < ) ∈ 𝑊) |
120 | 68, 119 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑀 ∈ 𝑊) |
121 | 67, 120 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑀 ∈ ℝ) |
122 | 121 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑀 ∈ ℝ) |
123 | 67 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ 𝑊 → 𝑚 ∈ ℝ) |
124 | 123 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑚 ∈ ℝ) |
125 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ≤ 𝑀) |
126 | 125 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ≤ 𝑀) |
127 | | infssuzle 11771 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑊 ⊆
(ℤ≥‘1) ∧ 𝑚 ∈ 𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑚) |
128 | 69, 127 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ 𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑚) |
129 | 68, 128 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ 𝑊 → 𝑀 ≤ 𝑚) |
130 | 129 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑀 ≤ 𝑚) |
131 | 63, 122, 124, 126, 130 | letrd 10194 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑀)) ∧ 𝑚 ∈ 𝑊) → 𝑛 ≤ 𝑚) |
132 | 131 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚) |
133 | 60, 132 | ssrabdv 3681 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
134 | 133 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (1...𝑀) ⊆ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
135 | | simprl 794 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ (1...𝑀)) |
136 | 134, 135 | sseldd 3604 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
137 | | simprr 796 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ (1...𝑀)) |
138 | 134, 137 | sseldd 3604 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚}) |
139 | 136, 138 | jca 554 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (1...𝑀) ∧ 𝑗 ∈ (1...𝑀))) → (𝑖 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚} ∧ 𝑗 ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑊 𝑛 ≤ 𝑚})) |
140 | 139, 105 | syldan 487 |
. . . . . . . . . . . 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 2971 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗)) |
144 | | dff13 6512 |
. . . . . . . . 9
⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ ↔ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)⟶ℕ ∧ ∀𝑖 ∈ (1...𝑀)∀𝑗 ∈ (1...𝑀)((((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑖) = (((𝐺 ∘ 𝐾) ↾ (1...𝑀))‘𝑗) → 𝑖 = 𝑗))) |
145 | 21, 143, 144 | sylanbrc 698 |
. . . . . . . 8
⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1→ℕ) |
146 | | f1f1orn 6148 |
. . . . . . . 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 6129 |
. . . . . . . 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 6144 |
. . . . . 6
⊢ (((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–1-1-onto→((𝐺 ∘ 𝐾) “ (1...𝑀)) → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀))) |
152 | 150, 151 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀))) |
153 | | fofi 8252 |
. . . . 5
⊢
(((1...𝑀) ∈ Fin
∧ ((𝐺 ∘ 𝐾) ↾ (1...𝑀)):(1...𝑀)–onto→((𝐺 ∘ 𝐾) “ (1...𝑀))) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin) |
154 | 43, 152, 153 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin) |
155 | | fimaxre2 10969 |
. . . 4
⊢ ((((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℝ ∧ ((𝐺 ∘ 𝐾) “ (1...𝑀)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) |
156 | 26, 154, 155 | syl2anc 693 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ≤ 𝑥) |
157 | 42, 156 | r19.29a 3078 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ ℕ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧) |
158 | 97, 96 | resubcld 10458 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
159 | 158 | rexrd 10089 |
. . . 4
⊢ (𝜑 → (𝐵 − 𝐴) ∈
ℝ*) |
160 | 159 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ∈
ℝ*) |
161 | | fzfid 12772 |
. . . . . 6
⊢ (𝜑 → (1...𝑧) ∈ Fin) |
162 | | elfznn 12370 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...𝑧) → 𝑗 ∈ ℕ) |
163 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) |
164 | 163 | ovolfsf 23240 |
. . . . . . . . . . 11
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞)) |
165 | 100, 164 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐹):ℕ⟶(0[,)+∞)) |
166 | 165 | ffvelrnda 6359 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞)) |
167 | 162, 166 | sylan2 491 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ (0[,)+∞)) |
168 | | elrege0 12278 |
. . . . . . . 8
⊢ ((((abs
∘ − ) ∘ 𝐹)‘𝑗) ∈ (0[,)+∞) ↔ ((((abs
∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐹)‘𝑗))) |
169 | 167, 168 | sylib 208 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → ((((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℝ ∧ 0 ≤ (((abs ∘
− ) ∘ 𝐹)‘𝑗))) |
170 | 169 | simpld 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℝ) |
171 | 161, 170 | fsumrecl 14465 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
172 | 171 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
173 | 172 | rexrd 10089 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈
ℝ*) |
174 | 163, 99 | ovolsf 23241 |
. . . . . . . . 9
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
175 | 100, 174 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆:ℕ⟶(0[,)+∞)) |
176 | | frn 6053 |
. . . . . . . 8
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ ran 𝑆 ⊆
(0[,)+∞)) |
177 | 175, 176 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝑆 ⊆ (0[,)+∞)) |
178 | | rge0ssre 12280 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
179 | 177, 178 | syl6ss 3615 |
. . . . . 6
⊢ (𝜑 → ran 𝑆 ⊆ ℝ) |
180 | | ressxr 10083 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
181 | 179, 180 | syl6ss 3615 |
. . . . 5
⊢ (𝜑 → ran 𝑆 ⊆
ℝ*) |
182 | | supxrcl 12145 |
. . . . 5
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
183 | 181, 182 | syl 17 |
. . . 4
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
184 | 183 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
185 | 158 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ∈ ℝ) |
186 | 24 | sselda 3603 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑗 ∈ ℕ) |
187 | 178, 166 | sseldi 3601 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
188 | 186, 187 | syldan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℝ) |
189 | 154, 188 | fsumrecl 14465 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
190 | 189 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ∈ ℝ) |
191 | | inss2 3834 |
. . . . . . . . . . 11
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
192 | | fss 6056 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ))
⊆ (ℝ × ℝ)) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
193 | 100, 191,
192 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
194 | 66, 120 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℕ) |
195 | 15, 194 | ffvelrnd 6360 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘𝑀) ∈ 𝑈) |
196 | 4, 195 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘(𝐾‘𝑀)) ∈ ℕ) |
197 | 193, 196 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝐺‘(𝐾‘𝑀))) ∈ (ℝ ×
ℝ)) |
198 | | xp2nd 7199 |
. . . . . . . . 9
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑀))) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℝ) |
199 | 197, 198 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℝ) |
200 | 13, 8 | sseldi 3601 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ 𝑈) |
201 | 4, 200 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝐶) ∈ ℕ) |
202 | 193, 201 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝐺‘𝐶)) ∈ (ℝ ×
ℝ)) |
203 | | xp1st 7198 |
. . . . . . . . 9
⊢ ((𝐹‘(𝐺‘𝐶)) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘(𝐺‘𝐶))) ∈ ℝ) |
204 | 202, 203 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘(𝐹‘(𝐺‘𝐶))) ∈ ℝ) |
205 | 199, 204 | resubcld 10458 |
. . . . . . 7
⊢ (𝜑 → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) ∈ ℝ) |
206 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑗 = (𝐺‘(𝐾‘𝑖)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖)))) |
207 | 187 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑗) ∈ ℂ) |
208 | 186, 207 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℂ) |
209 | 206, 43, 150, 48, 208 | fsumf1o 14454 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖)))) |
210 | 100 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
211 | 4 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐺:𝑈⟶ℕ) |
212 | | ffvelrn 6357 |
. . . . . . . . . . . . 13
⊢ ((𝐾:ℕ⟶𝑈 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑈) |
213 | 15, 18, 212 | syl2an 494 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐾‘𝑖) ∈ 𝑈) |
214 | 211, 213 | ffvelrnd 6360 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘(𝐾‘𝑖)) ∈ ℕ) |
215 | 163 | ovolfsval 23239 |
. . . . . . . . . . 11
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ (𝐺‘(𝐾‘𝑖)) ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
216 | 210, 214,
215 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (((abs ∘ − ) ∘
𝐹)‘(𝐺‘(𝐾‘𝑖))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
217 | 216 | sumeq2dv 14433 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(((abs ∘ − ) ∘ 𝐹)‘(𝐺‘(𝐾‘𝑖))) = Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
218 | 193 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
219 | 4 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐺:𝑈⟶ℕ) |
220 | 15 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑈) |
221 | 219, 220 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐺‘(𝐾‘𝑖)) ∈ ℕ) |
222 | 218, 221 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ ×
ℝ)) |
223 | | xp2nd 7199 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ) →
(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
224 | 222, 223 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
225 | 18, 224 | sylan2 491 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
226 | 225 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ) |
227 | 193 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐹:ℕ⟶(ℝ ×
ℝ)) |
228 | 227, 214 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ ×
ℝ)) |
229 | | xp1st 7198 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘(𝐺‘(𝐾‘𝑖))) ∈ (ℝ × ℝ) →
(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
230 | 228, 229 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
231 | 230 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ) |
232 | 43, 226, 231 | fsumsub 14520 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
233 | 69, 120 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
234 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑀 → (𝐾‘𝑖) = (𝐾‘𝑀)) |
235 | 234 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑀 → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘𝑀))) |
236 | 235 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑀 → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘𝑀)))) |
237 | 236 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑀 → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))) |
238 | 233, 226,
237 | fsumm1 14480 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))) |
239 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1...(𝑀 − 1)) ∈ Fin) |
240 | | elfznn 12370 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...(𝑀 − 1)) → 𝑖 ∈ ℕ) |
241 | 240, 224 | sylan2 491 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
242 | 239, 241 | fsumrecl 14465 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ) |
243 | 242 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ) |
244 | 199 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) ∈ ℂ) |
245 | 243, 244 | addcomd 10238 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) + (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
246 | 238, 245 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
247 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 1 → (𝐾‘𝑖) = (𝐾‘1)) |
248 | 247 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 1 → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘1))) |
249 | 248 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 1 → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘1)))) |
250 | 249 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 1 → (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘1))))) |
251 | 233, 231,
250 | fsum1p 14482 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((1st ‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
252 | 5, 6, 7, 8 | algr0 15285 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐾‘1) = 𝐶) |
253 | 252 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺‘(𝐾‘1)) = (𝐺‘𝐶)) |
254 | 253 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘(𝐺‘(𝐾‘1))) = (𝐹‘(𝐺‘𝐶))) |
255 | 254 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1st
‘(𝐹‘(𝐺‘(𝐾‘1)))) = (1st ‘(𝐹‘(𝐺‘𝐶)))) |
256 | 7 | peano2zd 11485 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 + 1) ∈
ℤ) |
257 | 194 | nnzd 11481 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℤ) |
258 | | fzp1ss 12392 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 ∈
ℤ → ((1 + 1)...𝑀) ⊆ (1...𝑀)) |
259 | 70, 258 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((1 + 1)...𝑀) ⊆ (1...𝑀)) |
260 | 259 | sselda 3603 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((1 + 1)...𝑀)) → 𝑖 ∈ (1...𝑀)) |
261 | 260, 231 | syldan 487 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((1 + 1)...𝑀)) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℂ) |
262 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = (𝑗 + 1) → (𝐾‘𝑖) = (𝐾‘(𝑗 + 1))) |
263 | 262 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑗 + 1) → (𝐺‘(𝐾‘𝑖)) = (𝐺‘(𝐾‘(𝑗 + 1)))) |
264 | 263 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑗 + 1) → (𝐹‘(𝐺‘(𝐾‘𝑖))) = (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) |
265 | 264 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑗 + 1) → (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))) |
266 | 7, 256, 257, 261, 265 | fsumshftm 14513 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = Σ𝑗 ∈ (((1 + 1) − 1)...(𝑀 − 1))(1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))))) |
267 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
268 | 267, 267 | pncan3oi 10297 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 + 1)
− 1) = 1 |
269 | 268 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
⊢ (((1 + 1)
− 1)...(𝑀 − 1))
= (1...(𝑀 −
1)) |
270 | 269 | sumeq1i 14428 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑗 ∈ (((1
+ 1) − 1)...(𝑀
− 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑗 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) |
271 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑖 → (𝑗 + 1) = (𝑖 + 1)) |
272 | 271 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑖 → (𝐾‘(𝑗 + 1)) = (𝐾‘(𝑖 + 1))) |
273 | 272 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑖 → (𝐺‘(𝐾‘(𝑗 + 1))) = (𝐺‘(𝐾‘(𝑖 + 1)))) |
274 | 273 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑖 → (𝐹‘(𝐺‘(𝐾‘(𝑗 + 1)))) = (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) |
275 | 274 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑖 → (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) |
276 | 275 | cbvsumv 14426 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑗 ∈
(1...(𝑀 −
1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) |
277 | 270, 276 | eqtri 2644 |
. . . . . . . . . . . . . 14
⊢
Σ𝑗 ∈ (((1
+ 1) − 1)...(𝑀
− 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑗 + 1))))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) |
278 | 266, 277 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) |
279 | 255, 278 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1st
‘(𝐹‘(𝐺‘(𝐾‘1)))) + Σ𝑖 ∈ ((1 + 1)...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) |
280 | 251, 279 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) = ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) |
281 | 246, 280 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑖 ∈ (1...𝑀)(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...𝑀)(1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) − ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
282 | 204 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝜑 → (1st
‘(𝐹‘(𝐺‘𝐶))) ∈ ℂ) |
283 | | peano2nn 11032 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ℕ → (𝑖 + 1) ∈
ℕ) |
284 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾:ℕ⟶𝑈 ∧ (𝑖 + 1) ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈) |
285 | 15, 283, 284 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) ∈ 𝑈) |
286 | 219, 285 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐺‘(𝐾‘(𝑖 + 1))) ∈ ℕ) |
287 | 218, 286 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ ×
ℝ)) |
288 | | xp1st 7198 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))) ∈ (ℝ × ℝ)
→ (1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ) |
289 | 287, 288 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ) |
290 | 240, 289 | sylan2 491 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ) |
291 | 239, 290 | fsumrecl 14465 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℝ) |
292 | 291 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ∈ ℂ) |
293 | 244, 243,
282, 292 | addsub4d 10439 |
. . . . . . . . . 10
⊢ (𝜑 → (((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) + Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) − ((1st ‘(𝐹‘(𝐺‘𝐶))) + Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
294 | 232, 281,
293 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − (1st ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
295 | 209, 217,
294 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
296 | 295, 189 | eqeltrrd 2702 |
. . . . . . 7
⊢ (𝜑 → (((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) ∈ ℝ) |
297 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑀 → (𝐾‘𝑛) = (𝐾‘𝑀)) |
298 | 297 | eleq2d 2687 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑀 → (𝐵 ∈ (𝐾‘𝑛) ↔ 𝐵 ∈ (𝐾‘𝑀))) |
299 | 298, 64 | elrab2 3366 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ 𝑊 ↔ (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾‘𝑀))) |
300 | 120, 299 | sylib 208 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝐵 ∈ (𝐾‘𝑀))) |
301 | 300 | simprd 479 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ (𝐾‘𝑀)) |
302 | 96, 97, 98, 99, 100, 73, 101, 4, 102 | ovolicc2lem1 23285 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐾‘𝑀) ∈ 𝑈) → (𝐵 ∈ (𝐾‘𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))))) |
303 | 195, 302 | mpdan 702 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 ∈ (𝐾‘𝑀) ↔ (𝐵 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))))) |
304 | 301, 303 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) < 𝐵 ∧ 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))))) |
305 | 304 | simp3d 1075 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀))))) |
306 | 96, 97, 98, 99, 100, 73, 101, 4, 102 | ovolicc2lem1 23285 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐶 ∈ 𝑈) → (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2nd ‘(𝐹‘(𝐺‘𝐶)))))) |
307 | 200, 306 | mpdan 702 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2nd ‘(𝐹‘(𝐺‘𝐶)))))) |
308 | 104, 307 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘𝐶))) < 𝐴 ∧ 𝐴 < (2nd ‘(𝐹‘(𝐺‘𝐶))))) |
309 | 308 | simp2d 1074 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘(𝐹‘(𝐺‘𝐶))) < 𝐴) |
310 | 97, 204, 199, 96, 305, 309 | lt2subd 10651 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐴) < ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶))))) |
311 | 158, 205,
310 | ltled 10185 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) ≤ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶))))) |
312 | 240 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℕ) |
313 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ (1...(𝑀 − 1))) |
314 | 257 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℤ) |
315 | | elfzm11 12411 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℤ ∧ 𝑀
∈ ℤ) → (𝑖
∈ (1...(𝑀 − 1))
↔ (𝑖 ∈ ℤ
∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀))) |
316 | 70, 314, 315 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ (1...(𝑀 − 1)) ↔ (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀))) |
317 | 313, 316 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℤ ∧ 1 ≤ 𝑖 ∧ 𝑖 < 𝑀)) |
318 | 317 | simp3d 1075 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 < 𝑀) |
319 | 312 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑖 ∈ ℝ) |
320 | 121 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → 𝑀 ∈ ℝ) |
321 | 319, 320 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 < 𝑀 ↔ ¬ 𝑀 ≤ 𝑖)) |
322 | 318, 321 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑀 ≤ 𝑖) |
323 | | infssuzle 11771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ⊆
(ℤ≥‘1) ∧ 𝑖 ∈ 𝑊) → inf(𝑊, ℝ, < ) ≤ 𝑖) |
324 | 69, 323 | mpan 706 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ 𝑊 → inf(𝑊, ℝ, < ) ≤ 𝑖) |
325 | 68, 324 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ 𝑊 → 𝑀 ≤ 𝑖) |
326 | 322, 325 | nsyl 135 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ¬ 𝑖 ∈ 𝑊) |
327 | 312, 326 | jca 554 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝑖 ∈ ℕ ∧ ¬ 𝑖 ∈ 𝑊)) |
328 | 96, 97, 98, 99, 100, 73, 101, 4, 102, 11, 9, 103, 104, 8, 6, 64 | ovolicc2lem2 23286 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑖 ∈ ℕ ∧ ¬ 𝑖 ∈ 𝑊)) → (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵) |
329 | 327, 328 | syldan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵) |
330 | 329 | iftrued 4094 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → if((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
331 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾:ℕ⟶𝑇 ∧ 𝑖 ∈ ℕ) → (𝐾‘𝑖) ∈ 𝑇) |
332 | 10, 240, 331 | syl2an 494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘𝑖) ∈ 𝑇) |
333 | 103 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) |
334 | 333 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡)) |
335 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = (𝐾‘𝑖) → (𝐺‘𝑡) = (𝐺‘(𝐾‘𝑖))) |
336 | 335 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = (𝐾‘𝑖) → (𝐹‘(𝐺‘𝑡)) = (𝐹‘(𝐺‘(𝐾‘𝑖)))) |
337 | 336 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = (𝐾‘𝑖) → (2nd ‘(𝐹‘(𝐺‘𝑡))) = (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
338 | 337 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = (𝐾‘𝑖) → ((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵 ↔ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵)) |
339 | 338, 337 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (𝐾‘𝑖) → if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) = if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵)) |
340 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = (𝐾‘𝑖) → (𝐻‘𝑡) = (𝐻‘(𝐾‘𝑖))) |
341 | 339, 340 | eleq12d 2695 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = (𝐾‘𝑖) → (if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡) ↔ if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑖)))) |
342 | 341 | rspcv 3305 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾‘𝑖) ∈ 𝑇 → (∀𝑡 ∈ 𝑇 if((2nd ‘(𝐹‘(𝐺‘𝑡))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘𝑡))), 𝐵) ∈ (𝐻‘𝑡) → if((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑖)))) |
343 | 332, 334,
342 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → if((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ≤ 𝐵, (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))), 𝐵) ∈ (𝐻‘(𝐾‘𝑖))) |
344 | 330, 343 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐻‘(𝐾‘𝑖))) |
345 | 5, 6, 7, 8, 9 | algrp1 15287 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾‘𝑖))) |
346 | 240, 345 | sylan2 491 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) = (𝐻‘(𝐾‘𝑖))) |
347 | 344, 346 | eleqtrrd 2704 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1))) |
348 | 240, 285 | sylan2 491 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (𝐾‘(𝑖 + 1)) ∈ 𝑈) |
349 | 96, 97, 98, 99, 100, 73, 101, 4, 102 | ovolicc2lem1 23285 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐾‘(𝑖 + 1)) ∈ 𝑈) → ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
350 | 348, 349 | syldan 487 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ (𝐾‘(𝑖 + 1)) ↔ ((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
351 | 347, 350 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∈ ℝ ∧ (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) ∧ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) |
352 | 351 | simp2d 1074 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) < (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
353 | 290, 241,
352 | ltled 10185 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (1...(𝑀 − 1))) → (1st
‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ (2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
354 | 239, 290,
241, 353 | fsumle 14531 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖))))) |
355 | 242, 291 | subge0d 10617 |
. . . . . . . . 9
⊢ (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))) ≤ Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))))) |
356 | 354, 355 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))) |
357 | 242, 291 | resubcld 10458 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ∈ ℝ) |
358 | 205, 357 | addge01d 10615 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))) ↔ ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1))))))))) |
359 | 356, 358 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → ((2nd
‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
360 | 158, 205,
296, 311, 359 | letrd 10194 |
. . . . . 6
⊢ (𝜑 → (𝐵 − 𝐴) ≤ (((2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑀)))) − (1st ‘(𝐹‘(𝐺‘𝐶)))) + (Σ𝑖 ∈ (1...(𝑀 − 1))(2nd ‘(𝐹‘(𝐺‘(𝐾‘𝑖)))) − Σ𝑖 ∈ (1...(𝑀 − 1))(1st ‘(𝐹‘(𝐺‘(𝐾‘(𝑖 + 1)))))))) |
361 | 360, 295 | breqtrrd 4681 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
362 | 361 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
363 | | fzfid 12772 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (1...𝑧) ∈ Fin) |
364 | 170 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℝ) |
365 | 169 | simprd 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − )
∘ 𝐹)‘𝑗)) |
366 | 365 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → 0 ≤ (((abs ∘ − )
∘ 𝐹)‘𝑗)) |
367 | 24 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ ℕ) |
368 | 367 | sselda 3603 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℕ) |
369 | 368 | nnred 11035 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈ ℝ) |
370 | 31 | ad2antlr 763 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℝ) |
371 | | ltle 10126 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧)) |
372 | 369, 370,
371 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 < 𝑧 → 𝑦 ≤ 𝑧)) |
373 | 368, 5 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑦 ∈
(ℤ≥‘1)) |
374 | | nnz 11399 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℤ) |
375 | 374 | ad2antlr 763 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → 𝑧 ∈ ℤ) |
376 | | elfz5 12334 |
. . . . . . . . . 10
⊢ ((𝑦 ∈
(ℤ≥‘1) ∧ 𝑧 ∈ ℤ) → (𝑦 ∈ (1...𝑧) ↔ 𝑦 ≤ 𝑧)) |
377 | 373, 375,
376 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 ∈ (1...𝑧) ↔ 𝑦 ≤ 𝑧)) |
378 | 372, 377 | sylibrd 249 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℕ) ∧ 𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))) → (𝑦 < 𝑧 → 𝑦 ∈ (1...𝑧))) |
379 | 378 | ralimdva 2962 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℕ) → (∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧 → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧))) |
380 | 379 | impr 649 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)) |
381 | | dfss3 3592 |
. . . . . 6
⊢ (((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ (1...𝑧) ↔ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 ∈ (1...𝑧)) |
382 | 380, 381 | sylibr 224 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ((𝐺 ∘ 𝐾) “ (1...𝑀)) ⊆ (1...𝑧)) |
383 | 363, 364,
366, 382 | fsumless 14528 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
384 | 185, 190,
172, 362, 383 | letrd 10194 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
385 | | eqidd 2623 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) = (((abs ∘ − ) ∘ 𝐹)‘𝑗)) |
386 | | simprl 794 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈ ℕ) |
387 | 386, 5 | syl6eleq 2711 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑧 ∈
(ℤ≥‘1)) |
388 | 364 | recnd 10068 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) ∧ 𝑗 ∈ (1...𝑧)) → (((abs ∘ − ) ∘
𝐹)‘𝑗) ∈ ℂ) |
389 | 385, 387,
388 | fsumser 14461 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑧)) |
390 | 99 | fveq1i 6192 |
. . . . 5
⊢ (𝑆‘𝑧) = (seq1( + , ((abs ∘ − )
∘ 𝐹))‘𝑧) |
391 | 389, 390 | syl6eqr 2674 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) = (𝑆‘𝑧)) |
392 | 181 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → ran 𝑆 ⊆
ℝ*) |
393 | | ffn 6045 |
. . . . . . . 8
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ 𝑆 Fn
ℕ) |
394 | 175, 393 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆 Fn ℕ) |
395 | 394 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → 𝑆 Fn ℕ) |
396 | | fnfvelrn 6356 |
. . . . . 6
⊢ ((𝑆 Fn ℕ ∧ 𝑧 ∈ ℕ) → (𝑆‘𝑧) ∈ ran 𝑆) |
397 | 395, 386,
396 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆‘𝑧) ∈ ran 𝑆) |
398 | | supxrub 12154 |
. . . . 5
⊢ ((ran
𝑆 ⊆
ℝ* ∧ (𝑆‘𝑧) ∈ ran 𝑆) → (𝑆‘𝑧) ≤ sup(ran 𝑆, ℝ*, <
)) |
399 | 392, 397,
398 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝑆‘𝑧) ≤ sup(ran 𝑆, ℝ*, <
)) |
400 | 391, 399 | eqbrtrd 4675 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → Σ𝑗 ∈ (1...𝑧)(((abs ∘ − ) ∘ 𝐹)‘𝑗) ≤ sup(ran 𝑆, ℝ*, <
)) |
401 | 160, 173,
184, 384, 400 | xrletrd 11993 |
. 2
⊢ ((𝜑 ∧ (𝑧 ∈ ℕ ∧ ∀𝑦 ∈ ((𝐺 ∘ 𝐾) “ (1...𝑀))𝑦 < 𝑧)) → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, <
)) |
402 | 157, 401 | rexlimddv 3035 |
1
⊢ (𝜑 → (𝐵 − 𝐴) ≤ sup(ran 𝑆, ℝ*, <
)) |