Theorem mbfi1fseqlem1

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

	Ref	Expression
Hypotheses	mbfi1fseq.1	⊢ ( 𝜑 → 𝐹 ∈ MblFn )
	mbfi1fseq.2	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
	mbfi1fseq.3	⊢ 𝐽 = ( 𝑚 ∈ ℕ , 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) )
Assertion	mbfi1fseqlem1	⊢ ( 𝜑 → 𝐽 : ( ℕ × ℝ ) ⟶ ( 0 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		mbfi1fseq.1	⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2		mbfi1fseq.2	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
3		mbfi1fseq.3	⊢ 𝐽 = ( 𝑚 ∈ ℕ , 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) )
4		simpr	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
5		ffvelrn	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
6	2 4 5	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
7		elrege0	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑦 ) ) )
8	6 7	sylib	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑦 ) ) )
9	8	simpld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
10		2nn	⊢ 2 ∈ ℕ
11		nnnn0	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ0 )
12		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑚 ∈ ℕ0 ) → ( 2 ↑ 𝑚 ) ∈ ℕ )
13	10 11 12	sylancr	⊢ ( 𝑚 ∈ ℕ → ( 2 ↑ 𝑚 ) ∈ ℕ )
14	13	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 2 ↑ 𝑚 ) ∈ ℕ )
15	14	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 2 ↑ 𝑚 ) ∈ ℝ )
16	9 15	remulcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ∈ ℝ )
17		reflcl	⊢ ( ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) ∈ ℝ )
18	16 17	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) ∈ ℝ )
19	18 14	nndivred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ℝ )
20	14	nnnn0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 2 ↑ 𝑚 ) ∈ ℕ0 )
21	20	nn0ge0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → 0 ≤ ( 2 ↑ 𝑚 ) )
22		mulge0	⊢ ( ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 2 ↑ 𝑚 ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ 𝑚 ) ) ) → 0 ≤ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) )
23	8 15 21 22	syl12anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → 0 ≤ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) )
24		flge0nn0	⊢ ( ( ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) ∈ ℕ0 )
25	16 23 24	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) ∈ ℕ0 )
26	25	nn0ge0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → 0 ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) )
27	14	nngt0d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → 0 < ( 2 ↑ 𝑚 ) )
28		divge0	⊢ ( ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) ∈ ℝ ∧ 0 ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) ) ∧ ( ( 2 ↑ 𝑚 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝑚 ) ) ) → 0 ≤ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) )
29	18 26 15 27 28	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → 0 ≤ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) )
30		elrege0	⊢ ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ℝ ∧ 0 ≤ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ) )
31	19 29 30	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ( 0 [,) +∞ ) )
32	31	ralrimivva	⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ∀ 𝑦 ∈ ℝ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ( 0 [,) +∞ ) )
33	3	fmpo	⊢ ( ∀ 𝑚 ∈ ℕ ∀ 𝑦 ∈ ℝ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ( 0 [,) +∞ ) ↔ 𝐽 : ( ℕ × ℝ ) ⟶ ( 0 [,) +∞ ) )
34	32 33	sylib	⊢ ( 𝜑 → 𝐽 : ( ℕ × ℝ ) ⟶ ( 0 [,) +∞ ) )