itg2monolem3

	Ref	Expression
Hypotheses	itg2mono.1	$⊢ G = (x \in ℝ ⟼ sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <))$
	itg2mono.2	$⊢ (φ \land n \in ℕ) \to F (n) \in MblFn$
	itg2mono.3	$⊢ (φ \land n \in ℕ) \to F (n) : ℝ ⟶ [0, +∞)$
	itg2mono.4	$⊢ (φ \land n \in ℕ) \to F (n) \leq_{f} F (n + 1)$
	itg2mono.5	$⊢ (φ \land x \in ℝ) \to \exists y \in ℝ \forall n \in ℕ F (n) (x) \leq y$
	itg2mono.6	$⊢ S = sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <)$
	itg2monolem2.7	$⊢ φ \to P \in dom \int^{1}$
	itg2monolem2.8	$⊢ φ \to P \leq_{f} G$
	itg2monolem2.9	$⊢ φ \to \neg \int^{1} (P) \leq S$
Assertion	itg2monolem3	$⊢ φ \to \int^{1} (P) \leq S$

Proof

Step	Hyp	Ref	Expression
1		itg2mono.1	$⊢ G = (x \in ℝ ⟼ sup (ran (n \in ℕ ⟼ F (n) (x)) ℝ <))$
2		itg2mono.2	$⊢ (φ \land n \in ℕ) \to F (n) \in MblFn$
3		itg2mono.3	$⊢ (φ \land n \in ℕ) \to F (n) : ℝ ⟶ [0, +∞)$
4		itg2mono.4	$⊢ (φ \land n \in ℕ) \to F (n) \leq_{f} F (n + 1)$
5		itg2mono.5	$⊢ (φ \land x \in ℝ) \to \exists y \in ℝ \forall n \in ℕ F (n) (x) \leq y$
6		itg2mono.6	$⊢ S = sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <)$
7		itg2monolem2.7	$⊢ φ \to P \in dom \int^{1}$
8		itg2monolem2.8	$⊢ φ \to P \leq_{f} G$
9		itg2monolem2.9	$⊢ φ \to \neg \int^{1} (P) \leq S$
10	1 2 3 4 5 6 7 8 9	itg2monolem2	$⊢ φ \to S \in ℝ$
11	10	adantr	$⊢ (φ \land t \in ℝ^{+}) \to S \in ℝ$
12	11	recnd	$⊢ (φ \land t \in ℝ^{+}) \to S \in ℂ$
13	7	adantr	$⊢ (φ \land t \in ℝ^{+}) \to P \in dom \int^{1}$
14		itg1cl	$⊢ P \in dom \int^{1} \to \int^{1} (P) \in ℝ$
15	13 14	syl	$⊢ (φ \land t \in ℝ^{+}) \to \int^{1} (P) \in ℝ$
16	15	recnd	$⊢ (φ \land t \in ℝ^{+}) \to \int^{1} (P) \in ℂ$
17		simpr	$⊢ (φ \land t \in ℝ^{+}) \to t \in ℝ^{+}$
18	17	rpred	$⊢ (φ \land t \in ℝ^{+}) \to t \in ℝ$
19	11 18	readdcld	$⊢ (φ \land t \in ℝ^{+}) \to S + t \in ℝ$
20	19	recnd	$⊢ (φ \land t \in ℝ^{+}) \to S + t \in ℂ$
21		0red	$⊢ (φ \land t \in ℝ^{+}) \to 0 \in ℝ$
22		0xr	$⊢ 0 \in ℝ^{*}$
23	22	a1i	$⊢ φ \to 0 \in ℝ^{*}$
24		fveq2	$⊢ n = 1 \to F (n) = F (1)$
25	24	feq1d	$⊢ n = 1 \to (F (n) : ℝ ⟶ [0, +∞] \leftrightarrow F (1) : ℝ ⟶ [0, +∞])$
26		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
27		fss	$⊢ (F (n) : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to F (n) : ℝ ⟶ [0, +∞]$
28	3 26 27	sylancl	$⊢ (φ \land n \in ℕ) \to F (n) : ℝ ⟶ [0, +∞]$
29	28	ralrimiva	$⊢ φ \to \forall n \in ℕ F (n) : ℝ ⟶ [0, +∞]$
30		1nn	$⊢ 1 \in ℕ$
31	30	a1i	$⊢ φ \to 1 \in ℕ$
32	25 29 31	rspcdva	$⊢ φ \to F (1) : ℝ ⟶ [0, +∞]$
33		itg2cl	$⊢ F (1) : ℝ ⟶ [0, +∞] \to \int^{2} (F (1)) \in ℝ^{*}$
34	32 33	syl	$⊢ φ \to \int^{2} (F (1)) \in ℝ^{*}$
35		itg2cl	$⊢ F (n) : ℝ ⟶ [0, +∞] \to \int^{2} (F (n)) \in ℝ^{*}$
36	28 35	syl	$⊢ (φ \land n \in ℕ) \to \int^{2} (F (n)) \in ℝ^{*}$
37	36	fmpttd	$⊢ φ \to (n \in ℕ ⟼ \int^{2} (F (n))) : ℕ ⟶ ℝ^{*}$
38	37	frnd	$⊢ φ \to ran (n \in ℕ ⟼ \int^{2} (F (n))) \subseteq ℝ^{*}$
39		supxrcl	$⊢ ran (n \in ℕ ⟼ \int^{2} (F (n))) \subseteq ℝ^{} \to sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{} <) \in ℝ^{*}$
40	38 39	syl	$⊢ φ \to sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{} <) \in ℝ^{}$
41	6 40	eqeltrid	$⊢ φ \to S \in ℝ^{*}$
42		itg2ge0	$⊢ F (1) : ℝ ⟶ [0, +∞] \to 0 \leq \int^{2} (F (1))$
43	32 42	syl	$⊢ φ \to 0 \leq \int^{2} (F (1))$
44		2fveq3	$⊢ n = 1 \to \int^{2} (F (n)) = \int^{2} (F (1))$
45		eqid	$⊢ (n \in ℕ ⟼ \int^{2} (F (n))) = (n \in ℕ ⟼ \int^{2} (F (n)))$
46		fvex	$⊢ \int^{2} (F (1)) \in V$
47	44 45 46	fvmpt	$⊢ 1 \in ℕ \to (n \in ℕ ⟼ \int^{2} (F (n))) (1) = \int^{2} (F (1))$
48	30 47	ax-mp	$⊢ (n \in ℕ ⟼ \int^{2} (F (n))) (1) = \int^{2} (F (1))$
49	37	ffnd	$⊢ φ \to (n \in ℕ ⟼ \int^{2} (F (n))) Fn ℕ$
50		fnfvelrn	$⊢ ((n \in ℕ ⟼ \int^{2} (F (n))) Fn ℕ \land 1 \in ℕ) \to (n \in ℕ ⟼ \int^{2} (F (n))) (1) \in ran (n \in ℕ ⟼ \int^{2} (F (n)))$
51	49 30 50	sylancl	$⊢ φ \to (n \in ℕ ⟼ \int^{2} (F (n))) (1) \in ran (n \in ℕ ⟼ \int^{2} (F (n)))$
52	48 51	eqeltrrid	$⊢ φ \to \int^{2} (F (1)) \in ran (n \in ℕ ⟼ \int^{2} (F (n)))$
53		supxrub	$⊢ (ran (n \in ℕ ⟼ \int^{2} (F (n))) \subseteq ℝ^{} \land \int^{2} (F (1)) \in ran (n \in ℕ ⟼ \int^{2} (F (n)))) \to \int^{2} (F (1)) \leq sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{} <)$
54	38 52 53	syl2anc	$⊢ φ \to \int^{2} (F (1)) \leq sup (ran (n \in ℕ ⟼ \int^{2} (F (n))) ℝ^{*} <)$
55	54 6	breqtrrdi	$⊢ φ \to \int^{2} (F (1)) \leq S$
56	23 34 41 43 55	xrletrd	$⊢ φ \to 0 \leq S$
57	56	adantr	$⊢ (φ \land t \in ℝ^{+}) \to 0 \leq S$
58	11 17	ltaddrpd	$⊢ (φ \land t \in ℝ^{+}) \to S < S + t$
59	21 11 19 57 58	lelttrd	$⊢ (φ \land t \in ℝ^{+}) \to 0 < S + t$
60	59	gt0ne0d	$⊢ (φ \land t \in ℝ^{+}) \to S + t \neq 0$
61	12 16 20 60	div23d	$⊢ (φ \land t \in ℝ^{+}) \to \frac{S \int^{1} (P)}{S + t} = (\frac{S}{S + t}) \int^{1} (P)$
62	11 19 60	redivcld	$⊢ (φ \land t \in ℝ^{+}) \to \frac{S}{S + t} \in ℝ$
63	62 15	remulcld	$⊢ (φ \land t \in ℝ^{+}) \to (\frac{S}{S + t}) \int^{1} (P) \in ℝ$
64		halfre	$⊢ \frac{1}{2} \in ℝ$
65		ifcl	$⊢ (\frac{S}{S + t} \in ℝ \land \frac{1}{2} \in ℝ) \to if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \in ℝ$
66	62 64 65	sylancl	$⊢ (φ \land t \in ℝ^{+}) \to if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \in ℝ$
67	66 15	remulcld	$⊢ (φ \land t \in ℝ^{+}) \to if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \int^{1} (P) \in ℝ$
68		max2	$⊢ (\frac{1}{2} \in ℝ \land \frac{S}{S + t} \in ℝ) \to \frac{S}{S + t} \leq if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2})$
69	64 62 68	sylancr	$⊢ (φ \land t \in ℝ^{+}) \to \frac{S}{S + t} \leq if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2})$
70	7 14	syl	$⊢ φ \to \int^{1} (P) \in ℝ$
71	70	rexrd	$⊢ φ \to \int^{1} (P) \in ℝ^{*}$
72		xrltnle	$⊢ (S \in ℝ^{} \land \int^{1} (P) \in ℝ^{}) \to (S < \int^{1} (P) \leftrightarrow \neg \int^{1} (P) \leq S)$
73	41 71 72	syl2anc	$⊢ φ \to (S < \int^{1} (P) \leftrightarrow \neg \int^{1} (P) \leq S)$
74	9 73	mpbird	$⊢ φ \to S < \int^{1} (P)$
75	74	adantr	$⊢ (φ \land t \in ℝ^{+}) \to S < \int^{1} (P)$
76	21 11 15 57 75	lelttrd	$⊢ (φ \land t \in ℝ^{+}) \to 0 < \int^{1} (P)$
77		lemul1	$⊢ (\frac{S}{S + t} \in ℝ \land if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \in ℝ \land (\int^{1} (P) \in ℝ \land 0 < \int^{1} (P))) \to (\frac{S}{S + t} \leq if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \leftrightarrow (\frac{S}{S + t}) \int^{1} (P) \leq if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \int^{1} (P))$
78	62 66 15 76 77	syl112anc	$⊢ (φ \land t \in ℝ^{+}) \to (\frac{S}{S + t} \leq if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \leftrightarrow (\frac{S}{S + t}) \int^{1} (P) \leq if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \int^{1} (P))$
79	69 78	mpbid	$⊢ (φ \land t \in ℝ^{+}) \to (\frac{S}{S + t}) \int^{1} (P) \leq if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \int^{1} (P)$
80	2	adantlr	$⊢ ((φ \land t \in ℝ^{+}) \land n \in ℕ) \to F (n) \in MblFn$
81	3	adantlr	$⊢ ((φ \land t \in ℝ^{+}) \land n \in ℕ) \to F (n) : ℝ ⟶ [0, +∞)$
82	4	adantlr	$⊢ ((φ \land t \in ℝ^{+}) \land n \in ℕ) \to F (n) \leq_{f} F (n + 1)$
83	5	adantlr	$⊢ ((φ \land t \in ℝ^{+}) \land x \in ℝ) \to \exists y \in ℝ \forall n \in ℕ F (n) (x) \leq y$
84	64	a1i	$⊢ (φ \land t \in ℝ^{+}) \to \frac{1}{2} \in ℝ$
85		halfgt0	$⊢ 0 < \frac{1}{2}$
86	85	a1i	$⊢ (φ \land t \in ℝ^{+}) \to 0 < \frac{1}{2}$
87		max1	$⊢ (\frac{1}{2} \in ℝ \land \frac{S}{S + t} \in ℝ) \to \frac{1}{2} \leq if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2})$
88	64 62 87	sylancr	$⊢ (φ \land t \in ℝ^{+}) \to \frac{1}{2} \leq if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2})$
89	21 84 66 86 88	ltletrd	$⊢ (φ \land t \in ℝ^{+}) \to 0 < if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2})$
90	20	mulid1d	$⊢ (φ \land t \in ℝ^{+}) \to (S + t) \cdot 1 = S + t$
91	58 90	breqtrrd	$⊢ (φ \land t \in ℝ^{+}) \to S < (S + t) \cdot 1$
92		1red	$⊢ (φ \land t \in ℝ^{+}) \to 1 \in ℝ$
93		ltdivmul	$⊢ (S \in ℝ \land 1 \in ℝ \land (S + t \in ℝ \land 0 < S + t)) \to (\frac{S}{S + t} < 1 \leftrightarrow S < (S + t) \cdot 1)$
94	11 92 19 59 93	syl112anc	$⊢ (φ \land t \in ℝ^{+}) \to (\frac{S}{S + t} < 1 \leftrightarrow S < (S + t) \cdot 1)$
95	91 94	mpbird	$⊢ (φ \land t \in ℝ^{+}) \to \frac{S}{S + t} < 1$
96		halflt1	$⊢ \frac{1}{2} < 1$
97		breq1	$⊢ \frac{S}{S + t} = if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \to (\frac{S}{S + t} < 1 \leftrightarrow if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) < 1)$
98		breq1	$⊢ \frac{1}{2} = if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \to (\frac{1}{2} < 1 \leftrightarrow if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) < 1)$
99	97 98	ifboth	$⊢ (\frac{S}{S + t} < 1 \land \frac{1}{2} < 1) \to if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) < 1$
100	95 96 99	sylancl	$⊢ (φ \land t \in ℝ^{+}) \to if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) < 1$
101		1xr	$⊢ 1 \in ℝ^{*}$
102		elioo2	$⊢ (0 \in ℝ^{} \land 1 \in ℝ^{}) \to (if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \in (0, 1) \leftrightarrow (if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \in ℝ \land 0 < if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \land if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) < 1))$
103	22 101 102	mp2an	$⊢ if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \in (0, 1) \leftrightarrow (if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \in ℝ \land 0 < if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \land if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) < 1)$
104	66 89 100 103	syl3anbrc	$⊢ (φ \land t \in ℝ^{+}) \to if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \in (0, 1)$
105	8	adantr	$⊢ (φ \land t \in ℝ^{+}) \to P \leq_{f} G$
106		fveq2	$⊢ y = x \to P (y) = P (x)$
107	106	oveq2d	$⊢ y = x \to if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) P (y) = if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) P (x)$
108		fveq2	$⊢ y = x \to F (n) (y) = F (n) (x)$
109	107 108	breq12d	$⊢ y = x \to (if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) P (y) \leq F (n) (y) \leftrightarrow if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) P (x) \leq F (n) (x))$
110	109	cbvrabv	$⊢ \{y \in ℝ \| if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) P (y) \leq F (n) (y)\} = \{x \in ℝ \| if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) P (x) \leq F (n) (x)\}$
111	110	mpteq2i	$⊢ (n \in ℕ ⟼ \{y \in ℝ \| if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) P (y) \leq F (n) (y)\}) = (n \in ℕ ⟼ \{x \in ℝ \| if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) P (x) \leq F (n) (x)\})$
112	1 80 81 82 83 6 104 13 105 11 111	itg2monolem1	$⊢ (φ \land t \in ℝ^{+}) \to if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \int^{1} (P) \leq S$
113	63 67 11 79 112	letrd	$⊢ (φ \land t \in ℝ^{+}) \to (\frac{S}{S + t}) \int^{1} (P) \leq S$
114	61 113	eqbrtrd	$⊢ (φ \land t \in ℝ^{+}) \to \frac{S \int^{1} (P)}{S + t} \leq S$
115	11 15	remulcld	$⊢ (φ \land t \in ℝ^{+}) \to S \int^{1} (P) \in ℝ$
116		ledivmul2	$⊢ (S \int^{1} (P) \in ℝ \land S \in ℝ \land (S + t \in ℝ \land 0 < S + t)) \to (\frac{S \int^{1} (P)}{S + t} \leq S \leftrightarrow S \int^{1} (P) \leq S (S + t))$
117	115 11 19 59 116	syl112anc	$⊢ (φ \land t \in ℝ^{+}) \to (\frac{S \int^{1} (P)}{S + t} \leq S \leftrightarrow S \int^{1} (P) \leq S (S + t))$
118	114 117	mpbid	$⊢ (φ \land t \in ℝ^{+}) \to S \int^{1} (P) \leq S (S + t)$
119	66 15 89 76	mulgt0d	$⊢ (φ \land t \in ℝ^{+}) \to 0 < if (\frac{1}{2} \leq \frac{S}{S + t}, \frac{S}{S + t}, \frac{1}{2}) \int^{1} (P)$
120	21 67 11 119 112	ltletrd	$⊢ (φ \land t \in ℝ^{+}) \to 0 < S$
121		lemul2	$⊢ (\int^{1} (P) \in ℝ \land S + t \in ℝ \land (S \in ℝ \land 0 < S)) \to (\int^{1} (P) \leq S + t \leftrightarrow S \int^{1} (P) \leq S (S + t))$
122	15 19 11 120 121	syl112anc	$⊢ (φ \land t \in ℝ^{+}) \to (\int^{1} (P) \leq S + t \leftrightarrow S \int^{1} (P) \leq S (S + t))$
123	118 122	mpbird	$⊢ (φ \land t \in ℝ^{+}) \to \int^{1} (P) \leq S + t$
124	123	ralrimiva	$⊢ φ \to \forall t \in ℝ^{+} \int^{1} (P) \leq S + t$
125		alrple	$⊢ (\int^{1} (P) \in ℝ \land S \in ℝ) \to (\int^{1} (P) \leq S \leftrightarrow \forall t \in ℝ^{+} \int^{1} (P) \leq S + t)$
126	70 10 125	syl2anc	$⊢ φ \to (\int^{1} (P) \leq S \leftrightarrow \forall t \in ℝ^{+} \int^{1} (P) \leq S + t)$
127	124 126	mpbird	$⊢ φ \to \int^{1} (P) \leq S$

Metamath Proof Explorer

Theorem itg2monolem3

Proof