ovolshftlem1

	Ref	Expression
Hypotheses	ovolshft.1	$⊢ φ \to A \subseteq ℝ$
	ovolshft.2	$⊢ φ \to C \in ℝ$
	ovolshft.3	$⊢ φ \to B = \{x \in ℝ \| x - C \in A\}$
	ovolshft.4	$⊢ M = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
	ovolshft.5	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
	ovolshft.6	$⊢ G = (n \in ℕ ⟼ ⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩)$
	ovolshft.7	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	ovolshft.8	$⊢ φ \to A \subseteq ⋃ ran ((.) \circ F)$
Assertion	ovolshftlem1	$⊢ φ \to sup (ran S ℝ^{*} <) \in M$

Proof

Step	Hyp	Ref	Expression
1		ovolshft.1	$⊢ φ \to A \subseteq ℝ$
2		ovolshft.2	$⊢ φ \to C \in ℝ$
3		ovolshft.3	$⊢ φ \to B = \{x \in ℝ \| x - C \in A\}$
4		ovolshft.4	$⊢ M = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
5		ovolshft.5	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
6		ovolshft.6	$⊢ G = (n \in ℕ ⟼ ⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩)$
7		ovolshft.7	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
8		ovolshft.8	$⊢ φ \to A \subseteq ⋃ ran ((.) \circ F)$
9		ovolfcl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ \land 1^{st} (F (n)) \leq 2^{nd} (F (n)))$
10	7 9	sylan	$⊢ (φ \land n \in ℕ) \to (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ \land 1^{st} (F (n)) \leq 2^{nd} (F (n)))$
11	10	simp1d	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) \in ℝ$
12	10	simp2d	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) \in ℝ$
13	2	adantr	$⊢ (φ \land n \in ℕ) \to C \in ℝ$
14	10	simp3d	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) \leq 2^{nd} (F (n))$
15	11 12 13 14	leadd1dd	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) + C \leq 2^{nd} (F (n)) + C$
16		df-br	$⊢ 1^{st} (F (n)) + C \leq 2^{nd} (F (n)) + C \leftrightarrow ⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩ \in \leq$
17	15 16	sylib	$⊢ (φ \land n \in ℕ) \to ⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩ \in \leq$
18	11 13	readdcld	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) + C \in ℝ$
19	12 13	readdcld	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) + C \in ℝ$
20	18 19	opelxpd	$⊢ (φ \land n \in ℕ) \to ⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩ \in ℝ^{2}$
21	17 20	elind	$⊢ (φ \land n \in ℕ) \to ⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩ \in (\leq \cap ℝ^{2})$
22	21 6	fmptd	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
23		eqid	$⊢ (abs \circ -) \circ G = (abs \circ -) \circ G$
24	23	ovolfsf	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to ((abs \circ -) \circ G) : ℕ ⟶ [0, +∞)$
25		ffn	$⊢ ((abs \circ -) \circ G) : ℕ ⟶ [0, +∞) \to ((abs \circ -) \circ G) Fn ℕ$
26	22 24 25	3syl	$⊢ φ \to ((abs \circ -) \circ G) Fn ℕ$
27		eqid	$⊢ (abs \circ -) \circ F = (abs \circ -) \circ F$
28	27	ovolfsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ((abs \circ -) \circ F) : ℕ ⟶ [0, +∞)$
29		ffn	$⊢ ((abs \circ -) \circ F) : ℕ ⟶ [0, +∞) \to ((abs \circ -) \circ F) Fn ℕ$
30	7 28 29	3syl	$⊢ φ \to ((abs \circ -) \circ F) Fn ℕ$
31		opex	$⊢ ⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩ \in V$
32	6	fvmpt2	$⊢ (n \in ℕ \land ⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩ \in V) \to G (n) = ⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩$
33	31 32	mpan2	$⊢ n \in ℕ \to G (n) = ⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩$
34	33	fveq2d	$⊢ n \in ℕ \to 2^{nd} (G (n)) = 2^{nd} (⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩)$
35		ovex	$⊢ 1^{st} (F (n)) + C \in V$
36		ovex	$⊢ 2^{nd} (F (n)) + C \in V$
37	35 36	op2nd	$⊢ 2^{nd} (⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩) = 2^{nd} (F (n)) + C$
38	34 37	eqtrdi	$⊢ n \in ℕ \to 2^{nd} (G (n)) = 2^{nd} (F (n)) + C$
39	33	fveq2d	$⊢ n \in ℕ \to 1^{st} (G (n)) = 1^{st} (⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩)$
40	35 36	op1st	$⊢ 1^{st} (⟨1^{st} (F (n)) + C, 2^{nd} (F (n)) + C⟩) = 1^{st} (F (n)) + C$
41	39 40	eqtrdi	$⊢ n \in ℕ \to 1^{st} (G (n)) = 1^{st} (F (n)) + C$
42	38 41	oveq12d	$⊢ n \in ℕ \to 2^{nd} (G (n)) - 1^{st} (G (n)) = 2^{nd} (F (n)) + C - (1^{st} (F (n)) + C)$
43	42	adantl	$⊢ (φ \land n \in ℕ) \to 2^{nd} (G (n)) - 1^{st} (G (n)) = 2^{nd} (F (n)) + C - (1^{st} (F (n)) + C)$
44	12	recnd	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) \in ℂ$
45	11	recnd	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) \in ℂ$
46	13	recnd	$⊢ (φ \land n \in ℕ) \to C \in ℂ$
47	44 45 46	pnpcan2d	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) + C - (1^{st} (F (n)) + C) = 2^{nd} (F (n)) - 1^{st} (F (n))$
48	43 47	eqtrd	$⊢ (φ \land n \in ℕ) \to 2^{nd} (G (n)) - 1^{st} (G (n)) = 2^{nd} (F (n)) - 1^{st} (F (n))$
49	23	ovolfsval	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to ((abs \circ -) \circ G) (n) = 2^{nd} (G (n)) - 1^{st} (G (n))$
50	22 49	sylan	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ G) (n) = 2^{nd} (G (n)) - 1^{st} (G (n))$
51	27	ovolfsval	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to ((abs \circ -) \circ F) (n) = 2^{nd} (F (n)) - 1^{st} (F (n))$
52	7 51	sylan	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ F) (n) = 2^{nd} (F (n)) - 1^{st} (F (n))$
53	48 50 52	3eqtr4d	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ G) (n) = ((abs \circ -) \circ F) (n)$
54	26 30 53	eqfnfvd	$⊢ φ \to (abs \circ -) \circ G = (abs \circ -) \circ F$
55	54	seqeq3d	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ G)) = seq 1 (+ ((abs \circ -) \circ F))$
56	55 5	eqtr4di	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ G)) = S$
57	56	rneqd	$⊢ φ \to ran seq 1 (+ ((abs \circ -) \circ G)) = ran S$
58	57	supeq1d	$⊢ φ \to sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{} <) = sup (ran S ℝ^{} <)$
59	3	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in \{x \in ℝ \| x - C \in A\})$
60		oveq1	$⊢ x = y \to x - C = y - C$
61	60	eleq1d	$⊢ x = y \to (x - C \in A \leftrightarrow y - C \in A)$
62	61	elrab	$⊢ y \in \{x \in ℝ \| x - C \in A\} \leftrightarrow (y \in ℝ \land y - C \in A)$
63	59 62	bitrdi	$⊢ φ \to (y \in B \leftrightarrow (y \in ℝ \land y - C \in A))$
64	63	biimpa	$⊢ (φ \land y \in B) \to (y \in ℝ \land y - C \in A)$
65		breq2	$⊢ x = y - C \to (1^{st} (F (n)) < x \leftrightarrow 1^{st} (F (n)) < y - C)$
66		breq1	$⊢ x = y - C \to (x < 2^{nd} (F (n)) \leftrightarrow y - C < 2^{nd} (F (n)))$
67	65 66	anbi12d	$⊢ x = y - C \to ((1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \leftrightarrow (1^{st} (F (n)) < y - C \land y - C < 2^{nd} (F (n))))$
68	67	rexbidv	$⊢ x = y - C \to (\exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \leftrightarrow \exists n \in ℕ (1^{st} (F (n)) < y - C \land y - C < 2^{nd} (F (n))))$
69		ovolfioo	$⊢ (A \subseteq ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (A \subseteq ⋃ ran ((.) \circ F) \leftrightarrow \forall x \in A \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))))$
70	1 7 69	syl2anc	$⊢ φ \to (A \subseteq ⋃ ran ((.) \circ F) \leftrightarrow \forall x \in A \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))))$
71	8 70	mpbid	$⊢ φ \to \forall x \in A \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n)))$
72	71	adantr	$⊢ (φ \land (y \in ℝ \land y - C \in A)) \to \forall x \in A \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n)))$
73		simprr	$⊢ (φ \land (y \in ℝ \land y - C \in A)) \to y - C \in A$
74	68 72 73	rspcdva	$⊢ (φ \land (y \in ℝ \land y - C \in A)) \to \exists n \in ℕ (1^{st} (F (n)) < y - C \land y - C < 2^{nd} (F (n)))$
75	41	adantl	$⊢ ((φ \land (y \in ℝ \land y - C \in A)) \land n \in ℕ) \to 1^{st} (G (n)) = 1^{st} (F (n)) + C$
76	75	breq1d	$⊢ ((φ \land (y \in ℝ \land y - C \in A)) \land n \in ℕ) \to (1^{st} (G (n)) < y \leftrightarrow 1^{st} (F (n)) + C < y)$
77	11	adantlr	$⊢ ((φ \land (y \in ℝ \land y - C \in A)) \land n \in ℕ) \to 1^{st} (F (n)) \in ℝ$
78	2	ad2antrr	$⊢ ((φ \land (y \in ℝ \land y - C \in A)) \land n \in ℕ) \to C \in ℝ$
79		simplrl	$⊢ ((φ \land (y \in ℝ \land y - C \in A)) \land n \in ℕ) \to y \in ℝ$
80	77 78 79	ltaddsubd	$⊢ ((φ \land (y \in ℝ \land y - C \in A)) \land n \in ℕ) \to (1^{st} (F (n)) + C < y \leftrightarrow 1^{st} (F (n)) < y - C)$
81	76 80	bitrd	$⊢ ((φ \land (y \in ℝ \land y - C \in A)) \land n \in ℕ) \to (1^{st} (G (n)) < y \leftrightarrow 1^{st} (F (n)) < y - C)$
82	38	adantl	$⊢ ((φ \land (y \in ℝ \land y - C \in A)) \land n \in ℕ) \to 2^{nd} (G (n)) = 2^{nd} (F (n)) + C$
83	82	breq2d	$⊢ ((φ \land (y \in ℝ \land y - C \in A)) \land n \in ℕ) \to (y < 2^{nd} (G (n)) \leftrightarrow y < 2^{nd} (F (n)) + C)$
84	12	adantlr	$⊢ ((φ \land (y \in ℝ \land y - C \in A)) \land n \in ℕ) \to 2^{nd} (F (n)) \in ℝ$
85	79 78 84	ltsubaddd	$⊢ ((φ \land (y \in ℝ \land y - C \in A)) \land n \in ℕ) \to (y - C < 2^{nd} (F (n)) \leftrightarrow y < 2^{nd} (F (n)) + C)$
86	83 85	bitr4d	$⊢ ((φ \land (y \in ℝ \land y - C \in A)) \land n \in ℕ) \to (y < 2^{nd} (G (n)) \leftrightarrow y - C < 2^{nd} (F (n)))$
87	81 86	anbi12d	$⊢ ((φ \land (y \in ℝ \land y - C \in A)) \land n \in ℕ) \to ((1^{st} (G (n)) < y \land y < 2^{nd} (G (n))) \leftrightarrow (1^{st} (F (n)) < y - C \land y - C < 2^{nd} (F (n))))$
88	87	rexbidva	$⊢ (φ \land (y \in ℝ \land y - C \in A)) \to (\exists n \in ℕ (1^{st} (G (n)) < y \land y < 2^{nd} (G (n))) \leftrightarrow \exists n \in ℕ (1^{st} (F (n)) < y - C \land y - C < 2^{nd} (F (n))))$
89	74 88	mpbird	$⊢ (φ \land (y \in ℝ \land y - C \in A)) \to \exists n \in ℕ (1^{st} (G (n)) < y \land y < 2^{nd} (G (n)))$
90	64 89	syldan	$⊢ (φ \land y \in B) \to \exists n \in ℕ (1^{st} (G (n)) < y \land y < 2^{nd} (G (n)))$
91	90	ralrimiva	$⊢ φ \to \forall y \in B \exists n \in ℕ (1^{st} (G (n)) < y \land y < 2^{nd} (G (n)))$
92		ssrab2	$⊢ \{x \in ℝ \| x - C \in A\} \subseteq ℝ$
93	3 92	eqsstrdi	$⊢ φ \to B \subseteq ℝ$
94		ovolfioo	$⊢ (B \subseteq ℝ \land G : ℕ ⟶ \leq \cap ℝ^{2}) \to (B \subseteq ⋃ ran ((.) \circ G) \leftrightarrow \forall y \in B \exists n \in ℕ (1^{st} (G (n)) < y \land y < 2^{nd} (G (n))))$
95	93 22 94	syl2anc	$⊢ φ \to (B \subseteq ⋃ ran ((.) \circ G) \leftrightarrow \forall y \in B \exists n \in ℕ (1^{st} (G (n)) < y \land y < 2^{nd} (G (n))))$
96	91 95	mpbird	$⊢ φ \to B \subseteq ⋃ ran ((.) \circ G)$
97		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ G)) = seq 1 (+ ((abs \circ -) \circ G))$
98	4 97	elovolmr	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land B \subseteq ⋃ ran ((.) \circ G)) \to sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{*} <) \in M$
99	22 96 98	syl2anc	$⊢ φ \to sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{*} <) \in M$
100	58 99	eqeltrrd	$⊢ φ \to sup (ran S ℝ^{*} <) \in M$

Metamath Proof Explorer

Theorem ovolshftlem1

Proof