Proof of Theorem ovolshftlem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ovolshft.7 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 2 |  | ovolfcl 25501 | . . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) | 
| 3 | 1, 2 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) ∈ ℝ ∧
(2nd ‘(𝐹‘𝑛)) ∈ ℝ ∧ (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛)))) | 
| 4 | 3 | simp1d 1143 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ) | 
| 5 | 3 | simp2d 1144 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ) | 
| 6 |  | ovolshft.2 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 7 | 6 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ ℝ) | 
| 8 | 3 | simp3d 1145 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ≤ (2nd
‘(𝐹‘𝑛))) | 
| 9 | 4, 5, 7, 8 | leadd1dd 11877 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) + 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) + 𝐶)) | 
| 10 |  | df-br 5144 | . . . . . . . . . . 11
⊢
(((1st ‘(𝐹‘𝑛)) + 𝐶) ≤ ((2nd ‘(𝐹‘𝑛)) + 𝐶) ↔ 〈((1st
‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉 ∈ ≤ ) | 
| 11 | 9, 10 | sylib 218 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉 ∈ ≤ ) | 
| 12 | 4, 7 | readdcld 11290 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐹‘𝑛)) + 𝐶) ∈ ℝ) | 
| 13 | 5, 7 | readdcld 11290 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐹‘𝑛)) + 𝐶) ∈ ℝ) | 
| 14 | 12, 13 | opelxpd 5724 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉 ∈ (ℝ ×
ℝ)) | 
| 15 | 11, 14 | elind 4200 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉 ∈ ( ≤ ∩ (ℝ ×
ℝ))) | 
| 16 |  | ovolshft.6 | . . . . . . . . 9
⊢ 𝐺 = (𝑛 ∈ ℕ ↦
〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) | 
| 17 | 15, 16 | fmptd 7134 | . . . . . . . 8
⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) | 
| 18 |  | eqid 2737 | . . . . . . . . 9
⊢ ((abs
∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺) | 
| 19 | 18 | ovolfsf 25506 | . . . . . . . 8
⊢ (𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞)) | 
| 20 |  | ffn 6736 | . . . . . . . 8
⊢ (((abs
∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) → ((abs
∘ − ) ∘ 𝐺) Fn ℕ) | 
| 21 | 17, 19, 20 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐺) Fn
ℕ) | 
| 22 |  | eqid 2737 | . . . . . . . . 9
⊢ ((abs
∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹) | 
| 23 | 22 | ovolfsf 25506 | . . . . . . . 8
⊢ (𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞)) | 
| 24 |  | ffn 6736 | . . . . . . . 8
⊢ (((abs
∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) → ((abs
∘ − ) ∘ 𝐹) Fn ℕ) | 
| 25 | 1, 23, 24 | 3syl 18 | . . . . . . 7
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐹) Fn
ℕ) | 
| 26 |  | opex 5469 | . . . . . . . . . . . . . 14
⊢
〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉 ∈ V | 
| 27 | 16 | fvmpt2 7027 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧
〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉 ∈ V) → (𝐺‘𝑛) = 〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) | 
| 28 | 26, 27 | mpan2 691 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = 〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) | 
| 29 | 28 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(2nd ‘(𝐺‘𝑛)) = (2nd
‘〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉)) | 
| 30 |  | ovex 7464 | . . . . . . . . . . . . 13
⊢
((1st ‘(𝐹‘𝑛)) + 𝐶) ∈ V | 
| 31 |  | ovex 7464 | . . . . . . . . . . . . 13
⊢
((2nd ‘(𝐹‘𝑛)) + 𝐶) ∈ V | 
| 32 | 30, 31 | op2nd 8023 | . . . . . . . . . . . 12
⊢
(2nd ‘〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) = ((2nd ‘(𝐹‘𝑛)) + 𝐶) | 
| 33 | 29, 32 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(2nd ‘(𝐺‘𝑛)) = ((2nd ‘(𝐹‘𝑛)) + 𝐶)) | 
| 34 | 28 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ →
(1st ‘(𝐺‘𝑛)) = (1st
‘〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉)) | 
| 35 | 30, 31 | op1st 8022 | . . . . . . . . . . . 12
⊢
(1st ‘〈((1st ‘(𝐹‘𝑛)) + 𝐶), ((2nd ‘(𝐹‘𝑛)) + 𝐶)〉) = ((1st ‘(𝐹‘𝑛)) + 𝐶) | 
| 36 | 34, 35 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ →
(1st ‘(𝐺‘𝑛)) = ((1st ‘(𝐹‘𝑛)) + 𝐶)) | 
| 37 | 33, 36 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛))) = (((2nd ‘(𝐹‘𝑛)) + 𝐶) − ((1st ‘(𝐹‘𝑛)) + 𝐶))) | 
| 38 | 37 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐺‘𝑛)) − (1st
‘(𝐺‘𝑛))) = (((2nd
‘(𝐹‘𝑛)) + 𝐶) − ((1st ‘(𝐹‘𝑛)) + 𝐶))) | 
| 39 | 5 | recnd 11289 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℂ) | 
| 40 | 4 | recnd 11289 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℂ) | 
| 41 | 7 | recnd 11289 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ ℂ) | 
| 42 | 39, 40, 41 | pnpcan2d 11658 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((2nd
‘(𝐹‘𝑛)) + 𝐶) − ((1st ‘(𝐹‘𝑛)) + 𝐶)) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) | 
| 43 | 38, 42 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2nd
‘(𝐺‘𝑛)) − (1st
‘(𝐺‘𝑛))) = ((2nd
‘(𝐹‘𝑛)) − (1st
‘(𝐹‘𝑛)))) | 
| 44 | 18 | ovolfsval 25505 | . . . . . . . . 9
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛)))) | 
| 45 | 17, 44 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺‘𝑛)) − (1st ‘(𝐺‘𝑛)))) | 
| 46 | 22 | ovolfsval 25505 | . . . . . . . . 9
⊢ ((𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) | 
| 47 | 1, 46 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹‘𝑛)) − (1st ‘(𝐹‘𝑛)))) | 
| 48 | 43, 45, 47 | 3eqtr4d 2787 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐺)‘𝑛) = (((abs ∘ − ) ∘ 𝐹)‘𝑛)) | 
| 49 | 21, 25, 48 | eqfnfvd 7054 | . . . . . 6
⊢ (𝜑 → ((abs ∘ − )
∘ 𝐺) = ((abs ∘
− ) ∘ 𝐹)) | 
| 50 | 49 | seqeq3d 14050 | . . . . 5
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐺)) =
seq1( + , ((abs ∘ − ) ∘ 𝐹))) | 
| 51 |  | ovolshft.5 | . . . . 5
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ 𝐹)) | 
| 52 | 50, 51 | eqtr4di 2795 | . . . 4
⊢ (𝜑 → seq1( + , ((abs ∘
− ) ∘ 𝐺)) =
𝑆) | 
| 53 | 52 | rneqd 5949 | . . 3
⊢ (𝜑 → ran seq1( + , ((abs
∘ − ) ∘ 𝐺)) = ran 𝑆) | 
| 54 | 53 | supeq1d 9486 | . 2
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) = sup(ran
𝑆, ℝ*,
< )) | 
| 55 |  | ovolshft.3 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 = {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴}) | 
| 56 | 55 | eleq2d 2827 | . . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴})) | 
| 57 |  | oveq1 7438 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 − 𝐶) = (𝑦 − 𝐶)) | 
| 58 | 57 | eleq1d 2826 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑥 − 𝐶) ∈ 𝐴 ↔ (𝑦 − 𝐶) ∈ 𝐴)) | 
| 59 | 58 | elrab 3692 | . . . . . . . 8
⊢ (𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴} ↔ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) | 
| 60 | 56, 59 | bitrdi 287 | . . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴))) | 
| 61 | 60 | biimpa 476 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) | 
| 62 |  | breq2 5147 | . . . . . . . . . 10
⊢ (𝑥 = (𝑦 − 𝐶) → ((1st ‘(𝐹‘𝑛)) < 𝑥 ↔ (1st ‘(𝐹‘𝑛)) < (𝑦 − 𝐶))) | 
| 63 |  | breq1 5146 | . . . . . . . . . 10
⊢ (𝑥 = (𝑦 − 𝐶) → (𝑥 < (2nd ‘(𝐹‘𝑛)) ↔ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛)))) | 
| 64 | 62, 63 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑥 = (𝑦 − 𝐶) → (((1st ‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) ↔ ((1st ‘(𝐹‘𝑛)) < (𝑦 − 𝐶) ∧ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛))))) | 
| 65 | 64 | rexbidv 3179 | . . . . . . . 8
⊢ (𝑥 = (𝑦 − 𝐶) → (∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝑦 − 𝐶) ∧ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛))))) | 
| 66 |  | ovolshft.8 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ ∪ ran
((,) ∘ 𝐹)) | 
| 67 |  | ovolshft.1 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ ℝ) | 
| 68 |  | ovolfioo 25502 | . . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))) | 
| 69 | 67, 1, 68 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 ⊆ ∪ ran
((,) ∘ 𝐹) ↔
∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛))))) | 
| 70 | 66, 69 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))) | 
| 71 | 70 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < 𝑥 ∧ 𝑥 < (2nd ‘(𝐹‘𝑛)))) | 
| 72 |  | simprr 773 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) → (𝑦 − 𝐶) ∈ 𝐴) | 
| 73 | 65, 71, 72 | rspcdva 3623 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝑦 − 𝐶) ∧ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛)))) | 
| 74 | 36 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐺‘𝑛)) = ((1st
‘(𝐹‘𝑛)) + 𝐶)) | 
| 75 | 74 | breq1d 5153 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐺‘𝑛)) < 𝑦 ↔ ((1st ‘(𝐹‘𝑛)) + 𝐶) < 𝑦)) | 
| 76 | 4 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st
‘(𝐹‘𝑛)) ∈
ℝ) | 
| 77 | 6 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ ℝ) | 
| 78 |  | simplrl 777 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑦 ∈ ℝ) | 
| 79 | 76, 77, 78 | ltaddsubd 11863 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st
‘(𝐹‘𝑛)) + 𝐶) < 𝑦 ↔ (1st ‘(𝐹‘𝑛)) < (𝑦 − 𝐶))) | 
| 80 | 75, 79 | bitrd 279 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st
‘(𝐺‘𝑛)) < 𝑦 ↔ (1st ‘(𝐹‘𝑛)) < (𝑦 − 𝐶))) | 
| 81 | 33 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐺‘𝑛)) = ((2nd
‘(𝐹‘𝑛)) + 𝐶)) | 
| 82 | 81 | breq2d 5155 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑦 < (2nd ‘(𝐺‘𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹‘𝑛)) + 𝐶))) | 
| 83 | 5 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd
‘(𝐹‘𝑛)) ∈
ℝ) | 
| 84 | 78, 77, 83 | ltsubaddd 11859 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹‘𝑛)) + 𝐶))) | 
| 85 | 82, 84 | bitr4d 282 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑦 < (2nd ‘(𝐺‘𝑛)) ↔ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛)))) | 
| 86 | 80, 85 | anbi12d 632 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))) ↔ ((1st ‘(𝐹‘𝑛)) < (𝑦 − 𝐶) ∧ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛))))) | 
| 87 | 86 | rexbidva 3177 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) → (∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st
‘(𝐹‘𝑛)) < (𝑦 − 𝐶) ∧ (𝑦 − 𝐶) < (2nd ‘(𝐹‘𝑛))))) | 
| 88 | 73, 87 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦 − 𝐶) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛)))) | 
| 89 | 61, 88 | syldan 591 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛)))) | 
| 90 | 89 | ralrimiva 3146 | . . . 4
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛)))) | 
| 91 |  | ssrab2 4080 | . . . . . 6
⊢ {𝑥 ∈ ℝ ∣ (𝑥 − 𝐶) ∈ 𝐴} ⊆ ℝ | 
| 92 | 55, 91 | eqsstrdi 4028 | . . . . 5
⊢ (𝜑 → 𝐵 ⊆ ℝ) | 
| 93 |  | ovolfioo 25502 | . . . . 5
⊢ ((𝐵 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ))) → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) | 
| 94 | 92, 17, 93 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐵 ⊆ ∪ ran
((,) ∘ 𝐺) ↔
∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℕ ((1st
‘(𝐺‘𝑛)) < 𝑦 ∧ 𝑦 < (2nd ‘(𝐺‘𝑛))))) | 
| 95 | 90, 94 | mpbird 257 | . . 3
⊢ (𝜑 → 𝐵 ⊆ ∪ ran
((,) ∘ 𝐺)) | 
| 96 |  | ovolshft.4 | . . . 4
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ)(𝐵 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, <
))} | 
| 97 |  | eqid 2737 | . . . 4
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝐺)) = seq1( + , ((abs ∘ − )
∘ 𝐺)) | 
| 98 | 96, 97 | elovolmr 25511 | . . 3
⊢ ((𝐺:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝐵 ⊆ ∪ ran
((,) ∘ 𝐺)) →
sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈ 𝑀) | 
| 99 | 17, 95, 98 | syl2anc 584 | . 2
⊢ (𝜑 → sup(ran seq1( + , ((abs
∘ − ) ∘ 𝐺)), ℝ*, < ) ∈ 𝑀) | 
| 100 | 54, 99 | eqeltrrd 2842 | 1
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀) |