Proof of Theorem ovolshftlem1
Step | Hyp | Ref
| Expression |
1 | | ovolshft.7 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
2 | | ovolfcl 23042 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
3 | 1, 2 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) |
4 | 3 | simp1d 1066 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ) |
5 | 3 | simp2d 1067 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ) |
6 | | ovolshft.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ℝ) |
7 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ ℝ) |
8 | 3 | simp3d 1068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) |
9 | 4, 5, 7, 8 | leadd1dd 10520 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) + 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) + 𝐶)) |
10 | | df-br 4584 |
. . . . . . . . . . 11
⊢
(((1st ‘(𝐹‘𝑛)) + 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) + 𝐶) ↔ 〈((1st
‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉 ∈ ≤ ) |
11 | 9, 10 | sylib 207 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉 ∈ ≤ ) |
12 | 4, 7 | readdcld 9948 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) + 𝐶) ∈ ℝ) |
13 | 5, 7 | readdcld 9948 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐹‘𝑛)) + 𝐶) ∈ ℝ) |
14 | | opelxp 5070 |
. . . . . . . . . . 11
⊢
(〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉 ∈ (ℝ × ℝ)
↔ (((1st ‘(𝐹‘𝑛)) + 𝐶) ∈ ℝ ∧ ((2nd
‘(𝐹‘𝑛)) + 𝐶) ∈ ℝ)) |
15 | 12, 13, 14 | sylanbrc 695 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉 ∈ (ℝ ×
ℝ)) |
16 | 11, 15 | elind 3760 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉 ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
17 | | ovolshft.6 |
. . . . . . . . 9
⊢ 𝐺 = (𝑛 ∈ ℕ ↦
〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) |
18 | 16, 17 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
19 | | eqid 2610 |
. . . . . . . . 9
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) |
20 | 19 | ovolfsf 23047 |
. . . . . . . 8
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞)) |
21 | | ffn 5958 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) → ((abs
∘ − ) ∘ 𝐺) Fn ℕ) |
22 | 18, 20, 21 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐺) Fn
ℕ) |
23 | | eqid 2610 |
. . . . . . . . 9
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) |
24 | 23 | ovolfsf 23047 |
. . . . . . . 8
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞)) |
25 | | ffn 5958 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) → ((abs
∘ − ) ∘ 𝐹) Fn ℕ) |
26 | 1, 24, 25 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐹) Fn
ℕ) |
27 | | opex 4859 |
. . . . . . . . . . . . . 14
⊢
〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉 ∈ V |
28 | 17 | fvmpt2 6200 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧
〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉 ∈ V) → (𝐺‘𝑛) = 〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) |
29 | 27, 28 | mpan2 703 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = 〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) |
30 | 29 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(2nd ‘(𝐺‘𝑛)) = (2nd
‘〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉)) |
31 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢
((1st ‘(𝐹‘𝑛)) + 𝐶) ∈ V |
32 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢
((2nd ‘(𝐹‘𝑛)) + 𝐶) ∈ V |
33 | 31, 32 | op2nd 7068 |
. . . . . . . . . . . 12
⊢
(2nd ‘〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) = ((2nd ‘(𝐹‘𝑛)) + 𝐶) |
34 | 30, 33 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(2nd ‘(𝐺‘𝑛)) = ((2nd ‘(𝐹‘𝑛)) + 𝐶)) |
35 | 29 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(1st ‘(𝐺‘𝑛)) = (1st
‘〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉)) |
36 | 31, 32 | op1st 7067 |
. . . . . . . . . . . 12
⊢
(1st ‘〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) = ((1st ‘(𝐹‘𝑛)) + 𝐶) |
37 | 35, 36 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(1st ‘(𝐺‘𝑛)) = ((1st ‘(𝐹‘𝑛)) + 𝐶)) |
38 | 34, 37 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛))) = (((2nd ‘(𝐹‘𝑛)) + 𝐶) − ((1st ‘(𝐹‘𝑛)) + 𝐶))) |
39 | 38 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐺‘𝑛)) − (1st
‘(𝐺‘𝑛))) = (((2nd
‘(𝐹‘𝑛)) + 𝐶) − ((1st ‘(𝐹‘𝑛)) + 𝐶))) |
40 | 5 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℂ) |
41 | 4 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℂ) |
42 | 7 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ ℂ) |
43 | 40, 41, 42 | pnpcan2d 10309 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((2nd
‘(𝐹‘𝑛)) + 𝐶) − ((1st ‘(𝐹‘𝑛)) + 𝐶)) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) |
44 | 39, 43 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐺‘𝑛)) − (1st
‘(𝐺‘𝑛))) = ((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛)))) |
45 | 19 | ovolfsval 23046 |
. . . . . . . . 9
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛)))) |
46 | 18, 45 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛)))) |
47 | 23 | ovolfsval 23046 |
. . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) |
48 | 1, 47 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) |
49 | 44, 46, 48 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = (((abs ∘ − ) ∘ 𝐹)‘𝑛)) |
50 | 22, 26, 49 | eqfnfvd 6222 |
. . . . . 6
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐺) = ((abs ∘
− ) ∘ 𝐹)) |
51 | 50 | seqeq3d 12671 |
. . . . 5
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐺)) =
seq1( + , ((abs ∘ − ) ∘ 𝐹))) |
52 | | ovolshft.5 |
. . . . 5
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) |
53 | 51, 52 | syl6eqr 2662 |
. . . 4
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐺)) =
𝑆) |
54 | 53 | rneqd 5274 |
. . 3
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ 𝐺)) = ran 𝑆) |
55 | 54 | supeq1d 8235 |
. 2
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) = sup(ran
𝑆, ℝ*,
< )) |
56 | | ovolshft.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴}) |
57 | 56 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴})) |
58 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 − 𝐶) = (𝑦 − 𝐶)) |
59 | 58 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑥 − 𝐶) ∈ 𝐴 ↔ (𝑦 − 𝐶) ∈ 𝐴)) |
60 | 59 | elrab 3331 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴} ↔ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) |
61 | 57, 60 | syl6bb 275 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴))) |
62 | 61 | biimpa 500 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) |
63 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) → (𝑦 − 𝐶) ∈ 𝐴) |
64 | | ovolshft.8 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ ∪ ran
((,) ∘ 𝐹)) |
65 | | ovolshft.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
66 | | ovolfioo 23043 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))) |
67 | 65, 1, 66 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))) |
68 | 64, 67 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))) |
69 | 68 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))) |
70 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 − 𝐶) → ((1st ‘(𝐹‘𝑛)) < 𝑥 ↔ (1st ‘(𝐹‘𝑛)) < (𝑦 − 𝐶))) |
71 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 − 𝐶) → (𝑥 < (2nd ‘(𝐹‘𝑛)) ↔ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛)))) |
72 | 70, 71 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑦 − 𝐶) → (((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) ↔ ((1st ‘(𝐹‘𝑛)) < (𝑦 − 𝐶) ∧ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛))))) |
73 | 72 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 − 𝐶) → (∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝑦 − 𝐶) ∧ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛))))) |
74 | 73 | rspcv 3278 |
. . . . . . . 8
⊢ ((𝑦 − 𝐶) ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) → ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝑦 − 𝐶) ∧ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛))))) |
75 | 63, 69, 74 | sylc 63 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝑦 − 𝐶) ∧ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛)))) |
76 | 37 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘𝑛)) = ((1st
‘(𝐹‘𝑛)) + 𝐶)) |
77 | 76 | breq1d 4593 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐺‘𝑛)) < 𝑦 ↔ ((1st ‘(𝐹‘𝑛)) + 𝐶) < 𝑦)) |
78 | 4 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ) |
79 | 6 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ ℝ) |
80 | | simplrl 796 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑦 ∈ ℝ) |
81 | 78, 79, 80 | ltaddsubd 10506 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st
‘(𝐹‘𝑛)) + 𝐶) < 𝑦 ↔ (1st ‘(𝐹‘𝑛)) < (𝑦 − 𝐶))) |
82 | 77, 81 | bitrd 267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐺‘𝑛)) < 𝑦 ↔ (1st ‘(𝐹‘𝑛)) < (𝑦 − 𝐶))) |
83 | 34 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐺‘𝑛)) = ((2nd
‘(𝐹‘𝑛)) + 𝐶)) |
84 | 83 | breq2d 4595 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑦 < (2nd ‘(𝐺‘𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹‘𝑛)) + 𝐶))) |
85 | 5 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ) |
86 | 80, 79, 85 | ltsubaddd 10502 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹‘𝑛)) + 𝐶))) |
87 | 84, 86 | bitr4d 270 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑦 < (2nd ‘(𝐺‘𝑛)) ↔ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛)))) |
88 | 82, 87 | anbi12d 743 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))) ↔ ((1st ‘(𝐹‘𝑛)) < (𝑦 − 𝐶) ∧ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛))))) |
89 | 88 | rexbidva 3031 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) → (∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝑦 − 𝐶) ∧ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛))))) |
90 | 75, 89 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛)))) |
91 | 62, 90 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛)))) |
92 | 91 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛)))) |
93 | | ssrab2 3650 |
. . . . . 6
⊢ {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴} ⊆ ℝ |
94 | 56, 93 | syl6eqss 3618 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
95 | | ovolfioo 23043 |
. . . . 5
⊢ ((𝐵 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
96 | 94, 18, 95 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) |
97 | 92, 96 | mpbird 246 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ ∪ ran
((,) ∘ 𝐺)) |
98 | | ovolshft.4 |
. . . 4
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐵 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} |
99 | | eqid 2610 |
. . . 4
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝐺)) = seq1( + , ((abs ∘ − )
∘ 𝐺)) |
100 | 98, 99 | elovolmr 23051 |
. . 3
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐵 ⊆ ∪ ran
((,) ∘ 𝐺)) →
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈ 𝑀) |
101 | 18, 97, 100 | syl2anc 691 |
. 2
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ∈ 𝑀) |
102 | 55, 101 | eqeltrrd 2689 |
1
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀) |