Theorem itg2monolem2

Description: Lemma for itg2mono . (Contributed by Mario Carneiro, 16-Aug-2014)

	Ref	Expression
Hypotheses	itg2mono.1	⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
	itg2mono.2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ MblFn )
	itg2mono.3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) )
	itg2mono.4	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∘r ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
	itg2mono.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
	itg2mono.6	⊢ 𝑆 = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < )
	itg2monolem2.7	⊢ ( 𝜑 → 𝑃 ∈ dom ∫1 )
	itg2monolem2.8	⊢ ( 𝜑 → 𝑃 ∘r ≤ 𝐺 )
	itg2monolem2.9	⊢ ( 𝜑 → ¬ ( ∫1 ‘ 𝑃 ) ≤ 𝑆 )
Assertion	itg2monolem2	⊢ ( 𝜑 → 𝑆 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		itg2mono.1	⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) , ℝ , < ) )
2		itg2mono.2	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ MblFn )
3		itg2mono.3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) )
4		itg2mono.4	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∘r ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
5		itg2mono.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℕ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑦 )
6		itg2mono.6	⊢ 𝑆 = sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < )
7		itg2monolem2.7	⊢ ( 𝜑 → 𝑃 ∈ dom ∫1 )
8		itg2monolem2.8	⊢ ( 𝜑 → 𝑃 ∘r ≤ 𝐺 )
9		itg2monolem2.9	⊢ ( 𝜑 → ¬ ( ∫1 ‘ 𝑃 ) ≤ 𝑆 )
10		icossicc	⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
11		fss	⊢ ( ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
12	3 10 11	sylancl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
13		itg2cl	⊢ ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ* )
14	12 13	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ* )
15	14	fmpttd	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) : ℕ ⟶ ℝ* )
16	15	frnd	⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* )
17		supxrcl	⊢ ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) ∈ ℝ* )
18	16 17	syl	⊢ ( 𝜑 → sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) ∈ ℝ* )
19	6 18	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
20		itg1cl	⊢ ( 𝑃 ∈ dom ∫1 → ( ∫1 ‘ 𝑃 ) ∈ ℝ )
21	7 20	syl	⊢ ( 𝜑 → ( ∫1 ‘ 𝑃 ) ∈ ℝ )
22		mnfxr	⊢ -∞ ∈ ℝ*
23	22	a1i	⊢ ( 𝜑 → -∞ ∈ ℝ* )
24		fveq2	⊢ ( 𝑛 = 1 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 1 ) )
25	24	feq1d	⊢ ( 𝑛 = 1 → ( ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) ↔ ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,] +∞ ) ) )
26	12	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) : ℝ ⟶ ( 0 [,] +∞ ) )
27		1nn	⊢ 1 ∈ ℕ
28	27	a1i	⊢ ( 𝜑 → 1 ∈ ℕ )
29	25 26 28	rspcdva	⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,] +∞ ) )
30		itg2cl	⊢ ( ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ℝ* )
31	29 30	syl	⊢ ( 𝜑 → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ℝ* )
32		itg2ge0	⊢ ( ( 𝐹 ‘ 1 ) : ℝ ⟶ ( 0 [,] +∞ ) → 0 ≤ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
33	29 32	syl	⊢ ( 𝜑 → 0 ≤ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
34		mnflt0	⊢ -∞ < 0
35		0xr	⊢ 0 ∈ ℝ*
36		xrltletr	⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ℝ* ) → ( ( -∞ < 0 ∧ 0 ≤ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ) → -∞ < ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ) )
37	22 35 31 36	mp3an12i	⊢ ( 𝜑 → ( ( -∞ < 0 ∧ 0 ≤ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ) → -∞ < ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ) )
38	34 37	mpani	⊢ ( 𝜑 → ( 0 ≤ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) → -∞ < ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ) )
39	33 38	mpd	⊢ ( 𝜑 → -∞ < ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
40		2fveq3	⊢ ( 𝑛 = 1 → ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
41		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) )
42		fvex	⊢ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ V
43	40 41 42	fvmpt	⊢ ( 1 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 1 ) = ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) )
44	27 43	ax-mp	⊢ ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 1 ) = ( ∫2 ‘ ( 𝐹 ‘ 1 ) )
45	15	ffnd	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) Fn ℕ )
46		fnfvelrn	⊢ ( ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) Fn ℕ ∧ 1 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 1 ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
47	45 27 46	sylancl	⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ‘ 1 ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
48	44 47	eqeltrrid	⊢ ( 𝜑 → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
49		supxrub	⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⊆ ℝ* ∧ ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ∈ ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) )
50	16 48 49	syl2anc	⊢ ( 𝜑 → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ≤ sup ( ran ( 𝑛 ∈ ℕ ↦ ( ∫2 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ* , < ) )
51	50 6	breqtrrdi	⊢ ( 𝜑 → ( ∫2 ‘ ( 𝐹 ‘ 1 ) ) ≤ 𝑆 )
52	23 31 19 39 51	xrltletrd	⊢ ( 𝜑 → -∞ < 𝑆 )
53	21	rexrd	⊢ ( 𝜑 → ( ∫1 ‘ 𝑃 ) ∈ ℝ* )
54		xrltnle	⊢ ( ( 𝑆 ∈ ℝ* ∧ ( ∫1 ‘ 𝑃 ) ∈ ℝ* ) → ( 𝑆 < ( ∫1 ‘ 𝑃 ) ↔ ¬ ( ∫1 ‘ 𝑃 ) ≤ 𝑆 ) )
55	19 53 54	syl2anc	⊢ ( 𝜑 → ( 𝑆 < ( ∫1 ‘ 𝑃 ) ↔ ¬ ( ∫1 ‘ 𝑃 ) ≤ 𝑆 ) )
56	9 55	mpbird	⊢ ( 𝜑 → 𝑆 < ( ∫1 ‘ 𝑃 ) )
57	19 53 56	xrltled	⊢ ( 𝜑 → 𝑆 ≤ ( ∫1 ‘ 𝑃 ) )
58		xrre	⊢ ( ( ( 𝑆 ∈ ℝ* ∧ ( ∫1 ‘ 𝑃 ) ∈ ℝ ) ∧ ( -∞ < 𝑆 ∧ 𝑆 ≤ ( ∫1 ‘ 𝑃 ) ) ) → 𝑆 ∈ ℝ )
59	19 21 52 57 58	syl22anc	⊢ ( 𝜑 → 𝑆 ∈ ℝ )