Metamath Proof Explorer


Theorem ovolshftlem1

Description: Lemma for ovolshft . (Contributed by Mario Carneiro, 22-Mar-2014)

Ref Expression
Hypotheses ovolshft.1 ( 𝜑𝐴 ⊆ ℝ )
ovolshft.2 ( 𝜑𝐶 ∈ ℝ )
ovolshft.3 ( 𝜑𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥𝐶 ) ∈ 𝐴 } )
ovolshft.4 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
ovolshft.5 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
ovolshft.6 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ )
ovolshft.7 ( 𝜑𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
ovolshft.8 ( 𝜑𝐴 ran ( (,) ∘ 𝐹 ) )
Assertion ovolshftlem1 ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ 𝑀 )

Proof

Step Hyp Ref Expression
1 ovolshft.1 ( 𝜑𝐴 ⊆ ℝ )
2 ovolshft.2 ( 𝜑𝐶 ∈ ℝ )
3 ovolshft.3 ( 𝜑𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥𝐶 ) ∈ 𝐴 } )
4 ovolshft.4 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
5 ovolshft.5 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
6 ovolshft.6 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ )
7 ovolshft.7 ( 𝜑𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
8 ovolshft.8 ( 𝜑𝐴 ran ( (,) ∘ 𝐹 ) )
9 ovolfcl ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
10 7 9 sylan ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ ∧ ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
11 10 simp1d ( ( 𝜑𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ )
12 10 simp2d ( ( 𝜑𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ )
13 2 adantr ( ( 𝜑𝑛 ∈ ℕ ) → 𝐶 ∈ ℝ )
14 10 simp3d ( ( 𝜑𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐹𝑛 ) ) ≤ ( 2nd ‘ ( 𝐹𝑛 ) ) )
15 11 12 13 14 leadd1dd ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ≤ ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) )
16 df-br ( ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ≤ ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ↔ ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ ∈ ≤ )
17 15 16 sylib ( ( 𝜑𝑛 ∈ ℕ ) → ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ ∈ ≤ )
18 11 13 readdcld ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ∈ ℝ )
19 12 13 readdcld ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ∈ ℝ )
20 18 19 opelxpd ( ( 𝜑𝑛 ∈ ℕ ) → ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ ∈ ( ℝ × ℝ ) )
21 17 20 elind ( ( 𝜑𝑛 ∈ ℕ ) → ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
22 21 6 fmptd ( 𝜑𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
23 eqid ( ( abs ∘ − ) ∘ 𝐺 ) = ( ( abs ∘ − ) ∘ 𝐺 )
24 23 ovolfsf ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐺 ) : ℕ ⟶ ( 0 [,) +∞ ) )
25 ffn ( ( ( abs ∘ − ) ∘ 𝐺 ) : ℕ ⟶ ( 0 [,) +∞ ) → ( ( abs ∘ − ) ∘ 𝐺 ) Fn ℕ )
26 22 24 25 3syl ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐺 ) Fn ℕ )
27 eqid ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝐹 )
28 27 ovolfsf ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) )
29 ffn ( ( ( abs ∘ − ) ∘ 𝐹 ) : ℕ ⟶ ( 0 [,) +∞ ) → ( ( abs ∘ − ) ∘ 𝐹 ) Fn ℕ )
30 7 28 29 3syl ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐹 ) Fn ℕ )
31 opex ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ ∈ V
32 6 fvmpt2 ( ( 𝑛 ∈ ℕ ∧ ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ ∈ V ) → ( 𝐺𝑛 ) = ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ )
33 31 32 mpan2 ( 𝑛 ∈ ℕ → ( 𝐺𝑛 ) = ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ )
34 33 fveq2d ( 𝑛 ∈ ℕ → ( 2nd ‘ ( 𝐺𝑛 ) ) = ( 2nd ‘ ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ ) )
35 ovex ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ∈ V
36 ovex ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ∈ V
37 35 36 op2nd ( 2nd ‘ ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ ) = ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 )
38 34 37 eqtrdi ( 𝑛 ∈ ℕ → ( 2nd ‘ ( 𝐺𝑛 ) ) = ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) )
39 33 fveq2d ( 𝑛 ∈ ℕ → ( 1st ‘ ( 𝐺𝑛 ) ) = ( 1st ‘ ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ ) )
40 35 36 op1st ( 1st ‘ ⟨ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ⟩ ) = ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 )
41 39 40 eqtrdi ( 𝑛 ∈ ℕ → ( 1st ‘ ( 𝐺𝑛 ) ) = ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) )
42 38 41 oveq12d ( 𝑛 ∈ ℕ → ( ( 2nd ‘ ( 𝐺𝑛 ) ) − ( 1st ‘ ( 𝐺𝑛 ) ) ) = ( ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) − ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ) )
43 42 adantl ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐺𝑛 ) ) − ( 1st ‘ ( 𝐺𝑛 ) ) ) = ( ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) − ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ) )
44 12 recnd ( ( 𝜑𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℂ )
45 11 recnd ( ( 𝜑𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℂ )
46 13 recnd ( ( 𝜑𝑛 ∈ ℕ ) → 𝐶 ∈ ℂ )
47 44 45 46 pnpcan2d ( ( 𝜑𝑛 ∈ ℕ ) → ( ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) − ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ) = ( ( 2nd ‘ ( 𝐹𝑛 ) ) − ( 1st ‘ ( 𝐹𝑛 ) ) ) )
48 43 47 eqtrd ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 2nd ‘ ( 𝐺𝑛 ) ) − ( 1st ‘ ( 𝐺𝑛 ) ) ) = ( ( 2nd ‘ ( 𝐹𝑛 ) ) − ( 1st ‘ ( 𝐹𝑛 ) ) ) )
49 23 ovolfsval ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( 2nd ‘ ( 𝐺𝑛 ) ) − ( 1st ‘ ( 𝐺𝑛 ) ) ) )
50 22 49 sylan ( ( 𝜑𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( 2nd ‘ ( 𝐺𝑛 ) ) − ( 1st ‘ ( 𝐺𝑛 ) ) ) )
51 27 ovolfsval ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( 2nd ‘ ( 𝐹𝑛 ) ) − ( 1st ‘ ( 𝐹𝑛 ) ) ) )
52 7 51 sylan ( ( 𝜑𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( 2nd ‘ ( 𝐹𝑛 ) ) − ( 1st ‘ ( 𝐹𝑛 ) ) ) )
53 48 50 52 3eqtr4d ( ( 𝜑𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) )
54 26 30 53 eqfnfvd ( 𝜑 → ( ( abs ∘ − ) ∘ 𝐺 ) = ( ( abs ∘ − ) ∘ 𝐹 ) )
55 54 seqeq3d ( 𝜑 → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) )
56 55 5 eqtr4di ( 𝜑 → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) = 𝑆 )
57 56 rneqd ( 𝜑 → ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) = ran 𝑆 )
58 57 supeq1d ( 𝜑 → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ* , < ) = sup ( ran 𝑆 , ℝ* , < ) )
59 3 eleq2d ( 𝜑 → ( 𝑦𝐵𝑦 ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐶 ) ∈ 𝐴 } ) )
60 oveq1 ( 𝑥 = 𝑦 → ( 𝑥𝐶 ) = ( 𝑦𝐶 ) )
61 60 eleq1d ( 𝑥 = 𝑦 → ( ( 𝑥𝐶 ) ∈ 𝐴 ↔ ( 𝑦𝐶 ) ∈ 𝐴 ) )
62 61 elrab ( 𝑦 ∈ { 𝑥 ∈ ℝ ∣ ( 𝑥𝐶 ) ∈ 𝐴 } ↔ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) )
63 59 62 bitrdi ( 𝜑 → ( 𝑦𝐵 ↔ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) )
64 63 biimpa ( ( 𝜑𝑦𝐵 ) → ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) )
65 breq2 ( 𝑥 = ( 𝑦𝐶 ) → ( ( 1st ‘ ( 𝐹𝑛 ) ) < 𝑥 ↔ ( 1st ‘ ( 𝐹𝑛 ) ) < ( 𝑦𝐶 ) ) )
66 breq1 ( 𝑥 = ( 𝑦𝐶 ) → ( 𝑥 < ( 2nd ‘ ( 𝐹𝑛 ) ) ↔ ( 𝑦𝐶 ) < ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
67 65 66 anbi12d ( 𝑥 = ( 𝑦𝐶 ) → ( ( ( 1st ‘ ( 𝐹𝑛 ) ) < 𝑥𝑥 < ( 2nd ‘ ( 𝐹𝑛 ) ) ) ↔ ( ( 1st ‘ ( 𝐹𝑛 ) ) < ( 𝑦𝐶 ) ∧ ( 𝑦𝐶 ) < ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
68 67 rexbidv ( 𝑥 = ( 𝑦𝐶 ) → ( ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) < 𝑥𝑥 < ( 2nd ‘ ( 𝐹𝑛 ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) < ( 𝑦𝐶 ) ∧ ( 𝑦𝐶 ) < ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
69 ovolfioo ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑥𝐴𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) < 𝑥𝑥 < ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
70 1 7 69 syl2anc ( 𝜑 → ( 𝐴 ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑥𝐴𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) < 𝑥𝑥 < ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
71 8 70 mpbid ( 𝜑 → ∀ 𝑥𝐴𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) < 𝑥𝑥 < ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
72 71 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) → ∀ 𝑥𝐴𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) < 𝑥𝑥 < ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
73 simprr ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) → ( 𝑦𝐶 ) ∈ 𝐴 )
74 68 72 73 rspcdva ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) < ( 𝑦𝐶 ) ∧ ( 𝑦𝐶 ) < ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
75 41 adantl ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐺𝑛 ) ) = ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) )
76 75 breq1d ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺𝑛 ) ) < 𝑦 ↔ ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) < 𝑦 ) )
77 11 adantlr ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 1st ‘ ( 𝐹𝑛 ) ) ∈ ℝ )
78 2 ad2antrr ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ℝ )
79 simplrl ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑦 ∈ ℝ )
80 77 78 79 ltaddsubd ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 1st ‘ ( 𝐹𝑛 ) ) + 𝐶 ) < 𝑦 ↔ ( 1st ‘ ( 𝐹𝑛 ) ) < ( 𝑦𝐶 ) ) )
81 76 80 bitrd ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1st ‘ ( 𝐺𝑛 ) ) < 𝑦 ↔ ( 1st ‘ ( 𝐹𝑛 ) ) < ( 𝑦𝐶 ) ) )
82 38 adantl ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐺𝑛 ) ) = ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) )
83 82 breq2d ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑦 < ( 2nd ‘ ( 𝐺𝑛 ) ) ↔ 𝑦 < ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ) )
84 12 adantlr ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 2nd ‘ ( 𝐹𝑛 ) ) ∈ ℝ )
85 79 78 84 ltsubaddd ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑦𝐶 ) < ( 2nd ‘ ( 𝐹𝑛 ) ) ↔ 𝑦 < ( ( 2nd ‘ ( 𝐹𝑛 ) ) + 𝐶 ) ) )
86 83 85 bitr4d ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑦 < ( 2nd ‘ ( 𝐺𝑛 ) ) ↔ ( 𝑦𝐶 ) < ( 2nd ‘ ( 𝐹𝑛 ) ) ) )
87 81 86 anbi12d ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 1st ‘ ( 𝐺𝑛 ) ) < 𝑦𝑦 < ( 2nd ‘ ( 𝐺𝑛 ) ) ) ↔ ( ( 1st ‘ ( 𝐹𝑛 ) ) < ( 𝑦𝐶 ) ∧ ( 𝑦𝐶 ) < ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
88 87 rexbidva ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) → ( ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺𝑛 ) ) < 𝑦𝑦 < ( 2nd ‘ ( 𝐺𝑛 ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐹𝑛 ) ) < ( 𝑦𝐶 ) ∧ ( 𝑦𝐶 ) < ( 2nd ‘ ( 𝐹𝑛 ) ) ) ) )
89 74 88 mpbird ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦𝐶 ) ∈ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺𝑛 ) ) < 𝑦𝑦 < ( 2nd ‘ ( 𝐺𝑛 ) ) ) )
90 64 89 syldan ( ( 𝜑𝑦𝐵 ) → ∃ 𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺𝑛 ) ) < 𝑦𝑦 < ( 2nd ‘ ( 𝐺𝑛 ) ) ) )
91 90 ralrimiva ( 𝜑 → ∀ 𝑦𝐵𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺𝑛 ) ) < 𝑦𝑦 < ( 2nd ‘ ( 𝐺𝑛 ) ) ) )
92 ssrab2 { 𝑥 ∈ ℝ ∣ ( 𝑥𝐶 ) ∈ 𝐴 } ⊆ ℝ
93 3 92 eqsstrdi ( 𝜑𝐵 ⊆ ℝ )
94 ovolfioo ( ( 𝐵 ⊆ ℝ ∧ 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐵 ran ( (,) ∘ 𝐺 ) ↔ ∀ 𝑦𝐵𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺𝑛 ) ) < 𝑦𝑦 < ( 2nd ‘ ( 𝐺𝑛 ) ) ) ) )
95 93 22 94 syl2anc ( 𝜑 → ( 𝐵 ran ( (,) ∘ 𝐺 ) ↔ ∀ 𝑦𝐵𝑛 ∈ ℕ ( ( 1st ‘ ( 𝐺𝑛 ) ) < 𝑦𝑦 < ( 2nd ‘ ( 𝐺𝑛 ) ) ) ) )
96 91 95 mpbird ( 𝜑𝐵 ran ( (,) ∘ 𝐺 ) )
97 eqid seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
98 4 97 elovolmr ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐵 ran ( (,) ∘ 𝐺 ) ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ* , < ) ∈ 𝑀 )
99 22 96 98 syl2anc ( 𝜑 → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) ) , ℝ* , < ) ∈ 𝑀 )
100 58 99 eqeltrrd ( 𝜑 → sup ( ran 𝑆 , ℝ* , < ) ∈ 𝑀 )