ovolshftlem1

	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	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ )
	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	⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ )
7		ovolshft.7	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
8		ovolshft.8	⊢ ( 𝜑 → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) )
9		ovolfcl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
10	7 9	sylan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
11	10	simp1d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
12	10	simp2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
13	2	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ℝ )
14	10	simp3d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) )
15	11 12 13 14	leadd1dd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ≤ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) )
16		df-br	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ≤ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ↔ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ ∈ ≤ )
17	15 16	sylib	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ ∈ ≤ )
18	11 13	readdcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ∈ ℝ )
19	12 13	readdcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ∈ ℝ )
20	18 19	opelxpd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ ∈ ( ℝ × ℝ ) )
21	17 20	elind	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
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	⊢ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ ∈ V
32	6	fvmpt2	⊢ ( ( 𝑛 ∈ ℕ ∧ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ ∈ V ) → ( 𝐺 ‘ 𝑛 ) = ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ )
33	31 32	mpan2	⊢ ( 𝑛 ∈ ℕ → ( 𝐺 ‘ 𝑛 ) = ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ )
34	33	fveq2d	⊢ ( 𝑛 ∈ ℕ → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 2^nd ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ ) )
35		ovex	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ∈ V
36		ovex	⊢ ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ∈ V
37	35 36	op2nd	⊢ ( 2^nd ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 )
38	34 37	eqtrdi	⊢ ( 𝑛 ∈ ℕ → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) )
39	33	fveq2d	⊢ ( 𝑛 ∈ ℕ → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 1^st ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ ) )
40	35 36	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ⟩ ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 )
41	39 40	eqtrdi	⊢ ( 𝑛 ∈ ℕ → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) )
42	38 41	oveq12d	⊢ ( 𝑛 ∈ ℕ → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ) )
43	42	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ) )
44	12	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℂ )
45	11	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℂ )
46	13	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ℂ )
47	44 45 46	pnpcan2d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) − ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
48	43 47	eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
49	23	ovolfsval	⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
50	22 49	sylan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐺 ) ‘ 𝑛 ) = ( ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
51	27	ovolfsval	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
52	7 51	sylan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( abs ∘ − ) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) − ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
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	⊢ ( 𝑥 = ( 𝑦 − 𝐶 ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ↔ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝑦 − 𝐶 ) ) )
66		breq1	⊢ ( 𝑥 = ( 𝑦 − 𝐶 ) → ( 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ ( 𝑦 − 𝐶 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
67	65 66	anbi12d	⊢ ( 𝑥 = ( 𝑦 − 𝐶 ) → ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝑦 − 𝐶 ) ∧ ( 𝑦 − 𝐶 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
68	67	rexbidv	⊢ ( 𝑥 = ( 𝑦 − 𝐶 ) → ( ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝑦 − 𝐶 ) ∧ ( 𝑦 − 𝐶 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
69		ovolfioo	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
70	1 7 69	syl2anc	⊢ ( 𝜑 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
71	8 70	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
72	71	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ∧ 𝑥 < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
73		simprr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) → ( 𝑦 − 𝐶 ) ∈ 𝐴 )
74	68 72 73	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝑦 − 𝐶 ) ∧ ( 𝑦 − 𝐶 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
75	41	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) )
76	75	breq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) < 𝑦 ) )
77	11	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
78	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → 𝐶 ∈ ℝ )
79		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → 𝑦 ∈ ℝ )
80	77 78 79	ltaddsubd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) < 𝑦 ↔ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝑦 − 𝐶 ) ) )
81	76 80	bitrd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ↔ ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝑦 − 𝐶 ) ) )
82	38	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) )
83	82	breq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ 𝑦 < ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ) )
84	12	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
85	79 78 84	ltsubaddd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑦 − 𝐶 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ 𝑦 < ( ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) + 𝐶 ) ) )
86	83 85	bitr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ↔ ( 𝑦 − 𝐶 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
87	81 86	anbi12d	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ↔ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝑦 − 𝐶 ) ∧ ( 𝑦 − 𝐶 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
88	87	rexbidva	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) → ( ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐹 ‘ 𝑛 ) ) < ( 𝑦 − 𝐶 ) ∧ ( 𝑦 − 𝐶 ) < ( 2^nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
89	74 88	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ( 𝑦 − 𝐶 ) ∈ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
90	64 89	syldan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
91	90	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
92		ssrab2	⊢ { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } ⊆ ℝ
93	3 92	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
94		ovolfioo	⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ) → ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
95	93 22 94	syl2anc	⊢ ( 𝜑 → ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℕ ( ( 1^st ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
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 𝑆 , ℝ^* , < ) ∈ 𝑀 )

Metamath Proof Explorer

Theorem ovolshftlem1

Proof