itg2i1fseqle

Description: Subject to the conditions coming from mbfi1fseq , the sequence of simple functions are all less than the target function F . (Contributed by Mario Carneiro, 17-Aug-2014)

	Ref	Expression
Hypotheses	itg2i1fseq.1	$⊢ φ \to F \in MblFn$
	itg2i1fseq.2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
	itg2i1fseq.3	$⊢ φ \to P : ℕ ⟶ dom \int^{1}$
	itg2i1fseq.4	$⊢ φ \to \forall n \in ℕ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1))$
	itg2i1fseq.5	$⊢ φ \to \forall x \in ℝ (n \in ℕ ⟼ P (n) (x)) ⇝ F (x)$
Assertion	itg2i1fseqle	$⊢ (φ \land M \in ℕ) \to P (M) \leq_{f} F$

Proof

Step	Hyp	Ref	Expression
1		itg2i1fseq.1	$⊢ φ \to F \in MblFn$
2		itg2i1fseq.2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
3		itg2i1fseq.3	$⊢ φ \to P : ℕ ⟶ dom \int^{1}$
4		itg2i1fseq.4	$⊢ φ \to \forall n \in ℕ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1))$
5		itg2i1fseq.5	$⊢ φ \to \forall x \in ℝ (n \in ℕ ⟼ P (n) (x)) ⇝ F (x)$
6		fveq2	$⊢ n = M \to P (n) = P (M)$
7	6	fveq1d	$⊢ n = M \to P (n) (y) = P (M) (y)$
8		eqid	$⊢ (n \in ℕ ⟼ P (n) (y)) = (n \in ℕ ⟼ P (n) (y))$
9		fvex	$⊢ P (M) (y) \in V$
10	7 8 9	fvmpt	$⊢ M \in ℕ \to (n \in ℕ ⟼ P (n) (y)) (M) = P (M) (y)$
11	10	ad2antlr	$⊢ ((φ \land M \in ℕ) \land y \in ℝ) \to (n \in ℕ ⟼ P (n) (y)) (M) = P (M) (y)$
12		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
13		simplr	$⊢ ((φ \land M \in ℕ) \land y \in ℝ) \to M \in ℕ$
14		fveq2	$⊢ x = y \to P (n) (x) = P (n) (y)$
15	14	mpteq2dv	$⊢ x = y \to (n \in ℕ ⟼ P (n) (x)) = (n \in ℕ ⟼ P (n) (y))$
16		fveq2	$⊢ x = y \to F (x) = F (y)$
17	15 16	breq12d	$⊢ x = y \to ((n \in ℕ ⟼ P (n) (x)) ⇝ F (x) \leftrightarrow (n \in ℕ ⟼ P (n) (y)) ⇝ F (y))$
18	17	rspccva	$⊢ (\forall x \in ℝ (n \in ℕ ⟼ P (n) (x)) ⇝ F (x) \land y \in ℝ) \to (n \in ℕ ⟼ P (n) (y)) ⇝ F (y)$
19	5 18	sylan	$⊢ (φ \land y \in ℝ) \to (n \in ℕ ⟼ P (n) (y)) ⇝ F (y)$
20	19	adantlr	$⊢ ((φ \land M \in ℕ) \land y \in ℝ) \to (n \in ℕ ⟼ P (n) (y)) ⇝ F (y)$
21		fveq2	$⊢ n = k \to P (n) = P (k)$
22	21	fveq1d	$⊢ n = k \to P (n) (y) = P (k) (y)$
23		fvex	$⊢ P (k) (y) \in V$
24	22 8 23	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ P (n) (y)) (k) = P (k) (y)$
25	24	adantl	$⊢ ((φ \land y \in ℝ) \land k \in ℕ) \to (n \in ℕ ⟼ P (n) (y)) (k) = P (k) (y)$
26	3	ffvelrnda	$⊢ (φ \land k \in ℕ) \to P (k) \in dom \int^{1}$
27		i1ff	$⊢ P (k) \in dom \int^{1} \to P (k) : ℝ ⟶ ℝ$
28	26 27	syl	$⊢ (φ \land k \in ℕ) \to P (k) : ℝ ⟶ ℝ$
29	28	ffvelrnda	$⊢ ((φ \land k \in ℕ) \land y \in ℝ) \to P (k) (y) \in ℝ$
30	29	an32s	$⊢ ((φ \land y \in ℝ) \land k \in ℕ) \to P (k) (y) \in ℝ$
31	25 30	eqeltrd	$⊢ ((φ \land y \in ℝ) \land k \in ℕ) \to (n \in ℕ ⟼ P (n) (y)) (k) \in ℝ$
32	31	adantllr	$⊢ (((φ \land M \in ℕ) \land y \in ℝ) \land k \in ℕ) \to (n \in ℕ ⟼ P (n) (y)) (k) \in ℝ$
33		simpr	$⊢ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1)) \to P (n) \leq_{f} P (n + 1)$
34	33	ralimi	$⊢ \forall n \in ℕ (0_{𝑝} \leq_{f} P (n) \land P (n) \leq_{f} P (n + 1)) \to \forall n \in ℕ P (n) \leq_{f} P (n + 1)$
35	4 34	syl	$⊢ φ \to \forall n \in ℕ P (n) \leq_{f} P (n + 1)$
36		fvoveq1	$⊢ n = k \to P (n + 1) = P (k + 1)$
37	21 36	breq12d	$⊢ n = k \to (P (n) \leq_{f} P (n + 1) \leftrightarrow P (k) \leq_{f} P (k + 1))$
38	37	rspccva	$⊢ (\forall n \in ℕ P (n) \leq_{f} P (n + 1) \land k \in ℕ) \to P (k) \leq_{f} P (k + 1)$
39	35 38	sylan	$⊢ (φ \land k \in ℕ) \to P (k) \leq_{f} P (k + 1)$
40		ffn	$⊢ P (k) : ℝ ⟶ ℝ \to P (k) Fn ℝ$
41	26 27 40	3syl	$⊢ (φ \land k \in ℕ) \to P (k) Fn ℝ$
42		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
43		ffvelrn	$⊢ (P : ℕ ⟶ dom \int^{1} \land k + 1 \in ℕ) \to P (k + 1) \in dom \int^{1}$
44	3 42 43	syl2an	$⊢ (φ \land k \in ℕ) \to P (k + 1) \in dom \int^{1}$
45		i1ff	$⊢ P (k + 1) \in dom \int^{1} \to P (k + 1) : ℝ ⟶ ℝ$
46		ffn	$⊢ P (k + 1) : ℝ ⟶ ℝ \to P (k + 1) Fn ℝ$
47	44 45 46	3syl	$⊢ (φ \land k \in ℕ) \to P (k + 1) Fn ℝ$
48		reex	$⊢ ℝ \in V$
49	48	a1i	$⊢ (φ \land k \in ℕ) \to ℝ \in V$
50		inidm	$⊢ ℝ \cap ℝ = ℝ$
51		eqidd	$⊢ ((φ \land k \in ℕ) \land y \in ℝ) \to P (k) (y) = P (k) (y)$
52		eqidd	$⊢ ((φ \land k \in ℕ) \land y \in ℝ) \to P (k + 1) (y) = P (k + 1) (y)$
53	41 47 49 49 50 51 52	ofrfval	$⊢ (φ \land k \in ℕ) \to (P (k) \leq_{f} P (k + 1) \leftrightarrow \forall y \in ℝ P (k) (y) \leq P (k + 1) (y))$
54	39 53	mpbid	$⊢ (φ \land k \in ℕ) \to \forall y \in ℝ P (k) (y) \leq P (k + 1) (y)$
55	54	r19.21bi	$⊢ ((φ \land k \in ℕ) \land y \in ℝ) \to P (k) (y) \leq P (k + 1) (y)$
56	55	an32s	$⊢ ((φ \land y \in ℝ) \land k \in ℕ) \to P (k) (y) \leq P (k + 1) (y)$
57		fveq2	$⊢ n = k + 1 \to P (n) = P (k + 1)$
58	57	fveq1d	$⊢ n = k + 1 \to P (n) (y) = P (k + 1) (y)$
59		fvex	$⊢ P (k + 1) (y) \in V$
60	58 8 59	fvmpt	$⊢ k + 1 \in ℕ \to (n \in ℕ ⟼ P (n) (y)) (k + 1) = P (k + 1) (y)$
61	42 60	syl	$⊢ k \in ℕ \to (n \in ℕ ⟼ P (n) (y)) (k + 1) = P (k + 1) (y)$
62	61	adantl	$⊢ ((φ \land y \in ℝ) \land k \in ℕ) \to (n \in ℕ ⟼ P (n) (y)) (k + 1) = P (k + 1) (y)$
63	56 25 62	3brtr4d	$⊢ ((φ \land y \in ℝ) \land k \in ℕ) \to (n \in ℕ ⟼ P (n) (y)) (k) \leq (n \in ℕ ⟼ P (n) (y)) (k + 1)$
64	63	adantllr	$⊢ (((φ \land M \in ℕ) \land y \in ℝ) \land k \in ℕ) \to (n \in ℕ ⟼ P (n) (y)) (k) \leq (n \in ℕ ⟼ P (n) (y)) (k + 1)$
65	12 13 20 32 64	climub	$⊢ ((φ \land M \in ℕ) \land y \in ℝ) \to (n \in ℕ ⟼ P (n) (y)) (M) \leq F (y)$
66	11 65	eqbrtrrd	$⊢ ((φ \land M \in ℕ) \land y \in ℝ) \to P (M) (y) \leq F (y)$
67	66	ralrimiva	$⊢ (φ \land M \in ℕ) \to \forall y \in ℝ P (M) (y) \leq F (y)$
68	3	ffvelrnda	$⊢ (φ \land M \in ℕ) \to P (M) \in dom \int^{1}$
69		i1ff	$⊢ P (M) \in dom \int^{1} \to P (M) : ℝ ⟶ ℝ$
70		ffn	$⊢ P (M) : ℝ ⟶ ℝ \to P (M) Fn ℝ$
71	68 69 70	3syl	$⊢ (φ \land M \in ℕ) \to P (M) Fn ℝ$
72	2	ffnd	$⊢ φ \to F Fn ℝ$
73	72	adantr	$⊢ (φ \land M \in ℕ) \to F Fn ℝ$
74	48	a1i	$⊢ (φ \land M \in ℕ) \to ℝ \in V$
75		eqidd	$⊢ ((φ \land M \in ℕ) \land y \in ℝ) \to P (M) (y) = P (M) (y)$
76		eqidd	$⊢ ((φ \land M \in ℕ) \land y \in ℝ) \to F (y) = F (y)$
77	71 73 74 74 50 75 76	ofrfval	$⊢ (φ \land M \in ℕ) \to (P (M) \leq_{f} F \leftrightarrow \forall y \in ℝ P (M) (y) \leq F (y))$
78	67 77	mpbird	$⊢ (φ \land M \in ℕ) \to P (M) \leq_{f} F$

Metamath Proof Explorer

Theorem itg2i1fseqle

Proof