MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovolshftlem1 Structured version   Visualization version   GIF version

Theorem ovolshftlem1 23028
Description: Lemma for ovolshft 23030. (Contributed by Mario Carneiro, 22-Mar-2014.)
Hypotheses
Ref Expression
ovolshft.1 (𝜑𝐴 ⊆ ℝ)
ovolshft.2 (𝜑𝐶 ∈ ℝ)
ovolshft.3 (𝜑𝐵 = {𝑥 ∈ ℝ ∣ (𝑥𝐶) ∈ 𝐴})
ovolshft.4 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐵 ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}
ovolshft.5 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
ovolshft.6 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩)
ovolshft.7 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
ovolshft.8 (𝜑𝐴 ran ((,) ∘ 𝐹))
Assertion
Ref Expression
ovolshftlem1 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀)
Distinct variable groups:   𝑓,𝑛,𝑥,𝑦,𝐴   𝐶,𝑓,𝑛,𝑥,𝑦   𝑛,𝐹,𝑥   𝑓,𝐺,𝑛,𝑦   𝐵,𝑓,𝑛,𝑦   𝜑,𝑓,𝑛,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑆(𝑥,𝑦,𝑓,𝑛)   𝐹(𝑦,𝑓)   𝐺(𝑥)   𝑀(𝑥,𝑦,𝑓,𝑛)

Proof of Theorem ovolshftlem1
StepHypRef Expression
1 ovolshft.7 . . . . . . . . . . . . . 14 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
2 ovolfcl 22986 . . . . . . . . . . . . . 14 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
31, 2sylan 486 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
43simp1d 1065 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
53simp2d 1066 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
6 ovolshft.2 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ ℝ)
76adantr 479 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → 𝐶 ∈ ℝ)
83simp3d 1067 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)))
94, 5, 7, 8leadd1dd 10492 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) + 𝐶) ≤ ((2nd ‘(𝐹𝑛)) + 𝐶))
10 df-br 4578 . . . . . . . . . . 11 (((1st ‘(𝐹𝑛)) + 𝐶) ≤ ((2nd ‘(𝐹𝑛)) + 𝐶) ↔ ⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩ ∈ ≤ )
119, 10sylib 206 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩ ∈ ≤ )
124, 7readdcld 9925 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) + 𝐶) ∈ ℝ)
135, 7readdcld 9925 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((2nd ‘(𝐹𝑛)) + 𝐶) ∈ ℝ)
14 opelxp 5059 . . . . . . . . . . 11 (⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩ ∈ (ℝ × ℝ) ↔ (((1st ‘(𝐹𝑛)) + 𝐶) ∈ ℝ ∧ ((2nd ‘(𝐹𝑛)) + 𝐶) ∈ ℝ))
1512, 13, 14sylanbrc 694 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩ ∈ (ℝ × ℝ))
1611, 15elind 3759 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩ ∈ ( ≤ ∩ (ℝ × ℝ)))
17 ovolshft.6 . . . . . . . . 9 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩)
1816, 17fmptd 6276 . . . . . . . 8 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
19 eqid 2609 . . . . . . . . 9 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
2019ovolfsf 22991 . . . . . . . 8 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
21 ffn 5943 . . . . . . . 8 (((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞) → ((abs ∘ − ) ∘ 𝐺) Fn ℕ)
2218, 20, 213syl 18 . . . . . . 7 (𝜑 → ((abs ∘ − ) ∘ 𝐺) Fn ℕ)
23 eqid 2609 . . . . . . . . 9 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
2423ovolfsf 22991 . . . . . . . 8 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
25 ffn 5943 . . . . . . . 8 (((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) → ((abs ∘ − ) ∘ 𝐹) Fn ℕ)
261, 24, 253syl 18 . . . . . . 7 (𝜑 → ((abs ∘ − ) ∘ 𝐹) Fn ℕ)
27 opex 4852 . . . . . . . . . . . . . 14 ⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩ ∈ V
2817fvmpt2 6184 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ ∧ ⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩ ∈ V) → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩)
2927, 28mpan2 702 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩)
3029fveq2d 6091 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = (2nd ‘⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩))
31 ovex 6554 . . . . . . . . . . . . 13 ((1st ‘(𝐹𝑛)) + 𝐶) ∈ V
32 ovex 6554 . . . . . . . . . . . . 13 ((2nd ‘(𝐹𝑛)) + 𝐶) ∈ V
3331, 32op2nd 7045 . . . . . . . . . . . 12 (2nd ‘⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩) = ((2nd ‘(𝐹𝑛)) + 𝐶)
3430, 33syl6eq 2659 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = ((2nd ‘(𝐹𝑛)) + 𝐶))
3529fveq2d 6091 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = (1st ‘⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩))
3631, 32op1st 7044 . . . . . . . . . . . 12 (1st ‘⟨((1st ‘(𝐹𝑛)) + 𝐶), ((2nd ‘(𝐹𝑛)) + 𝐶)⟩) = ((1st ‘(𝐹𝑛)) + 𝐶)
3735, 36syl6eq 2659 . . . . . . . . . . 11 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) + 𝐶))
3834, 37oveq12d 6544 . . . . . . . . . 10 (𝑛 ∈ ℕ → ((2nd ‘(𝐺𝑛)) − (1st ‘(𝐺𝑛))) = (((2nd ‘(𝐹𝑛)) + 𝐶) − ((1st ‘(𝐹𝑛)) + 𝐶)))
3938adantl 480 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((2nd ‘(𝐺𝑛)) − (1st ‘(𝐺𝑛))) = (((2nd ‘(𝐹𝑛)) + 𝐶) − ((1st ‘(𝐹𝑛)) + 𝐶)))
405recnd 9924 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℂ)
414recnd 9924 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℂ)
427recnd 9924 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 𝐶 ∈ ℂ)
4340, 41, 42pnpcan2d 10281 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((2nd ‘(𝐹𝑛)) + 𝐶) − ((1st ‘(𝐹𝑛)) + 𝐶)) = ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))))
4439, 43eqtrd 2643 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((2nd ‘(𝐺𝑛)) − (1st ‘(𝐺𝑛))) = ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))))
4519ovolfsval 22990 . . . . . . . . 9 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺𝑛)) − (1st ‘(𝐺𝑛))))
4618, 45sylan 486 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺𝑛)) − (1st ‘(𝐺𝑛))))
4723ovolfsval 22990 . . . . . . . . 9 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))))
481, 47sylan 486 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))))
4944, 46, 483eqtr4d 2653 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = (((abs ∘ − ) ∘ 𝐹)‘𝑛))
5022, 26, 49eqfnfvd 6206 . . . . . 6 (𝜑 → ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐹))
5150seqeq3d 12628 . . . . 5 (𝜑 → seq1( + , ((abs ∘ − ) ∘ 𝐺)) = seq1( + , ((abs ∘ − ) ∘ 𝐹)))
52 ovolshft.5 . . . . 5 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
5351, 52syl6eqr 2661 . . . 4 (𝜑 → seq1( + , ((abs ∘ − ) ∘ 𝐺)) = 𝑆)
5453rneqd 5260 . . 3 (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) = ran 𝑆)
5554supeq1d 8212 . 2 (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) = sup(ran 𝑆, ℝ*, < ))
56 ovolshft.3 . . . . . . . . 9 (𝜑𝐵 = {𝑥 ∈ ℝ ∣ (𝑥𝐶) ∈ 𝐴})
5756eleq2d 2672 . . . . . . . 8 (𝜑 → (𝑦𝐵𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝑥𝐶) ∈ 𝐴}))
58 oveq1 6533 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥𝐶) = (𝑦𝐶))
5958eleq1d 2671 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑥𝐶) ∈ 𝐴 ↔ (𝑦𝐶) ∈ 𝐴))
6059elrab 3330 . . . . . . . 8 (𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝑥𝐶) ∈ 𝐴} ↔ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴))
6157, 60syl6bb 274 . . . . . . 7 (𝜑 → (𝑦𝐵 ↔ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)))
6261biimpa 499 . . . . . 6 ((𝜑𝑦𝐵) → (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴))
63 simprr 791 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) → (𝑦𝐶) ∈ 𝐴)
64 ovolshft.8 . . . . . . . . . 10 (𝜑𝐴 ran ((,) ∘ 𝐹))
65 ovolshft.1 . . . . . . . . . . 11 (𝜑𝐴 ⊆ ℝ)
66 ovolfioo 22987 . . . . . . . . . . 11 ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ran ((,) ∘ 𝐹) ↔ ∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
6765, 1, 66syl2anc 690 . . . . . . . . . 10 (𝜑 → (𝐴 ran ((,) ∘ 𝐹) ↔ ∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
6864, 67mpbid 220 . . . . . . . . 9 (𝜑 → ∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))))
6968adantr 479 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) → ∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))))
70 breq2 4581 . . . . . . . . . . 11 (𝑥 = (𝑦𝐶) → ((1st ‘(𝐹𝑛)) < 𝑥 ↔ (1st ‘(𝐹𝑛)) < (𝑦𝐶)))
71 breq1 4580 . . . . . . . . . . 11 (𝑥 = (𝑦𝐶) → (𝑥 < (2nd ‘(𝐹𝑛)) ↔ (𝑦𝐶) < (2nd ‘(𝐹𝑛))))
7270, 71anbi12d 742 . . . . . . . . . 10 (𝑥 = (𝑦𝐶) → (((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) ↔ ((1st ‘(𝐹𝑛)) < (𝑦𝐶) ∧ (𝑦𝐶) < (2nd ‘(𝐹𝑛)))))
7372rexbidv 3033 . . . . . . . . 9 (𝑥 = (𝑦𝐶) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < (𝑦𝐶) ∧ (𝑦𝐶) < (2nd ‘(𝐹𝑛)))))
7473rspcv 3277 . . . . . . . 8 ((𝑦𝐶) ∈ 𝐴 → (∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < (𝑦𝐶) ∧ (𝑦𝐶) < (2nd ‘(𝐹𝑛)))))
7563, 69, 74sylc 62 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < (𝑦𝐶) ∧ (𝑦𝐶) < (2nd ‘(𝐹𝑛))))
7637adantl 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) + 𝐶))
7776breq1d 4587 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛)) < 𝑦 ↔ ((1st ‘(𝐹𝑛)) + 𝐶) < 𝑦))
784adantlr 746 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
796ad2antrr 757 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ ℝ)
80 simplrl 795 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑦 ∈ ℝ)
8178, 79, 80ltaddsubd 10478 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹𝑛)) + 𝐶) < 𝑦 ↔ (1st ‘(𝐹𝑛)) < (𝑦𝐶)))
8277, 81bitrd 266 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛)) < 𝑦 ↔ (1st ‘(𝐹𝑛)) < (𝑦𝐶)))
8334adantl 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = ((2nd ‘(𝐹𝑛)) + 𝐶))
8483breq2d 4589 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑦 < (2nd ‘(𝐺𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹𝑛)) + 𝐶)))
855adantlr 746 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
8680, 79, 85ltsubaddd 10474 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝑦𝐶) < (2nd ‘(𝐹𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹𝑛)) + 𝐶)))
8784, 86bitr4d 269 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑦 < (2nd ‘(𝐺𝑛)) ↔ (𝑦𝐶) < (2nd ‘(𝐹𝑛))))
8882, 87anbi12d 742 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛))) ↔ ((1st ‘(𝐹𝑛)) < (𝑦𝐶) ∧ (𝑦𝐶) < (2nd ‘(𝐹𝑛)))))
8988rexbidva 3030 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < (𝑦𝐶) ∧ (𝑦𝐶) < (2nd ‘(𝐹𝑛)))))
9075, 89mpbird 245 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝑦𝐶) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛))))
9162, 90syldan 485 . . . . 5 ((𝜑𝑦𝐵) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛))))
9291ralrimiva 2948 . . . 4 (𝜑 → ∀𝑦𝐵𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛))))
93 ssrab2 3649 . . . . . 6 {𝑥 ∈ ℝ ∣ (𝑥𝐶) ∈ 𝐴} ⊆ ℝ
9456, 93syl6eqss 3617 . . . . 5 (𝜑𝐵 ⊆ ℝ)
95 ovolfioo 22987 . . . . 5 ((𝐵 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐵 ran ((,) ∘ 𝐺) ↔ ∀𝑦𝐵𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
9694, 18, 95syl2anc 690 . . . 4 (𝜑 → (𝐵 ran ((,) ∘ 𝐺) ↔ ∀𝑦𝐵𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
9792, 96mpbird 245 . . 3 (𝜑𝐵 ran ((,) ∘ 𝐺))
98 ovolshft.4 . . . 4 𝑀 = {𝑦 ∈ ℝ* ∣ ∃𝑓 ∈ (( ≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐵 ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ))}
99 eqid 2609 . . . 4 seq1( + , ((abs ∘ − ) ∘ 𝐺)) = seq1( + , ((abs ∘ − ) ∘ 𝐺))
10098, 99elovolmr 22995 . . 3 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐵 ran ((,) ∘ 𝐺)) → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈ 𝑀)
10118, 97, 100syl2anc 690 . 2 (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈ 𝑀)
10255, 101eqeltrrd 2688 1 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ 𝑀)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wral 2895  wrex 2896  {crab 2899  Vcvv 3172  cin 3538  wss 3539  cop 4130   cuni 4366   class class class wbr 4577  cmpt 4637   × cxp 5025  ran crn 5028  ccom 5031   Fn wfn 5784  wf 5785  cfv 5789  (class class class)co 6526  1st c1st 7034  2nd c2nd 7035  𝑚 cmap 7721  supcsup 8206  cr 9791  0cc0 9792  1c1 9793   + caddc 9795  +∞cpnf 9927  *cxr 9929   < clt 9930  cle 9931  cmin 10117  cn 10869  (,)cioo 12004  [,)cico 12006  seqcseq 12620  abscabs 13770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-er 7606  df-map 7723  df-en 7819  df-dom 7820  df-sdom 7821  df-sup 8208  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10536  df-nn 10870  df-2 10928  df-3 10929  df-n0 11142  df-z 11213  df-uz 11522  df-rp 11667  df-ioo 12008  df-ico 12010  df-fz 12155  df-seq 12621  df-exp 12680  df-cj 13635  df-re 13636  df-im 13637  df-sqrt 13771  df-abs 13772
This theorem is referenced by:  ovolshftlem2  23029
  Copyright terms: Public domain W3C validator