mbfi1fseqlem5 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mbfi1fseqlem5		Structured version Visualization version GIF version

Theorem mbfi1fseqlem5 25688

Description: Lemma for mbfi1fseq 25690. Verify that 𝐺 describes an increasing sequence of positive functions. (Contributed by Mario Carneiro, 16-Aug-2014.)

**Hypotheses**
Ref	Expression
mbfi1fseq.1	⊢ (𝜑 → 𝐹 ∈ MblFn)
mbfi1fseq.2	⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))
mbfi1fseq.3	⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))
mbfi1fseq.4	⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))

**Assertion**
Ref	Expression
mbfi1fseqlem5	⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (0_𝑝 ∘_r ≤ (𝐺‘𝐴) ∧ (𝐺‘𝐴) ∘_r ≤ (𝐺‘(𝐴 + 1))))

Distinct variable groups: 𝑥,𝑚,𝑦,𝐹 𝑥,𝐺 𝑚,𝐽 𝜑,𝑚,𝑥,𝑦 𝐴,𝑚,𝑥,𝑦 Allowed substitution hints: 𝐺(𝑦,𝑚) 𝐽(𝑥,𝑦)

**Proof of Theorem mbfi1fseqlem5**
Step	Hyp	Ref	Expression
1		mbfi1fseq.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))
2	1	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞))
3	2	ffvelcdmda 7038	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
4		elrege0 13382	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
5	3, 4	sylib 218	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
6	5	simpld 494	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
7		2nn 12230	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
8		nnnn0 12420	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ₀)
9		nnexpcl 14009	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ ∧ 𝐴 ∈ ℕ₀) → (2↑𝐴) ∈ ℕ)
10	7, 8, 9	sylancr 588	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℕ → (2↑𝐴) ∈ ℕ)
11	10	ad2antlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℕ)
12	11	nnred 12172	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℝ)
13	6, 12	remulcld 11174	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ)
14	11	nnnn0d 12474	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℕ₀)
15	14	nn0ge0d 12477	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (2↑𝐴))
16		mulge0 11667	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 ≤ (2↑𝐴))) → 0 ≤ ((𝐹‘𝑥) · (2↑𝐴)))
17	5, 12, 15, 16	syl12anc 837	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹‘𝑥) · (2↑𝐴)))
18		flge0nn0 13752	. . . . . . . . . 10 ⊢ ((((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑥) · (2↑𝐴))) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℕ₀)
19	13, 17, 18	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℕ₀)
20	19	nn0red 12475	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℝ)
21	19	nn0ge0d 12477	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (⌊‘((𝐹‘𝑥) · (2↑𝐴))))
22	11	nngt0d 12206	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝐴))
23		divge0 12023	. . . . . . . 8 ⊢ ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℝ ∧ 0 ≤ (⌊‘((𝐹‘𝑥) · (2↑𝐴)))) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 < (2↑𝐴))) → 0 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
24	20, 21, 12, 22, 23	syl22anc 839	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
25		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
26	25	fveq2d 6846	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
27		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → 𝑚 = 𝐴)
28	27	oveq2d 7384	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝐴))
29	26, 28	oveq12d 7386	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝐴)))
30	29	fveq2d 6846	. . . . . . . . . 10 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝐴))))
31	30, 28	oveq12d 7386	. . . . . . . . 9 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
32		mbfi1fseq.3	. . . . . . . . 9 ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))
33		ovex 7401	. . . . . . . . 9 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ V
34	31, 32, 33	ovmpoa 7523	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
35	34	adantll 715	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
36	24, 35	breqtrrd 5128	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐴𝐽𝑥))
37	8	nn0ge0d 12477	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → 0 ≤ 𝐴)
38	37	ad2antlr 728	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝐴)
39		breq2 5104	. . . . . . 7 ⊢ ((𝐴𝐽𝑥) = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) → (0 ≤ (𝐴𝐽𝑥) ↔ 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴)))
40		breq2 5104	. . . . . . 7 ⊢ (𝐴 = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) → (0 ≤ 𝐴 ↔ 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴)))
41	39, 40	ifboth 4521	. . . . . 6 ⊢ ((0 ≤ (𝐴𝐽𝑥) ∧ 0 ≤ 𝐴) → 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))
42	36, 38, 41	syl2anc 585	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))
43		0le0 12258	. . . . 5 ⊢ 0 ≤ 0
44		breq2 5104	. . . . . 6 ⊢ (if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) → (0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ↔ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
45		breq2 5104	. . . . . 6 ⊢ (0 = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
46	44, 45	ifboth 4521	. . . . 5 ⊢ ((0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∧ 0 ≤ 0) → 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
47	42, 43, 46	sylancl 587	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
48	47	ralrimiva 3130	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ∀𝑥 ∈ ℝ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
49		0re 11146	. . . . . . 7 ⊢ 0 ∈ ℝ
50		fnconstg 6730	. . . . . . 7 ⊢ (0 ∈ ℝ → (ℂ × {0}) Fn ℂ)
51	49, 50	ax-mp 5	. . . . . 6 ⊢ (ℂ × {0}) Fn ℂ
52		df-0p 25639	. . . . . . 7 ⊢ 0_𝑝 = (ℂ × {0})
53	52	fneq1i 6597	. . . . . 6 ⊢ (0_𝑝 Fn ℂ ↔ (ℂ × {0}) Fn ℂ)
54	51, 53	mpbir 231	. . . . 5 ⊢ 0_𝑝 Fn ℂ
55	54	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 0_𝑝 Fn ℂ)
56		mbfi1fseq.1	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ MblFn)
57		mbfi1fseq.4	. . . . . . 7 ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
58	56, 1, 32, 57	mbfi1fseqlem4 25687	. . . . . 6 ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫₁)
59	58	ffvelcdmda 7038	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) ∈ dom ∫₁)
60		i1ff 25645	. . . . 5 ⊢ ((𝐺‘𝐴) ∈ dom ∫₁ → (𝐺‘𝐴):ℝ⟶ℝ)
61		ffn 6670	. . . . 5 ⊢ ((𝐺‘𝐴):ℝ⟶ℝ → (𝐺‘𝐴) Fn ℝ)
62	59, 60, 61	3syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) Fn ℝ)
63		cnex 11119	. . . . 5 ⊢ ℂ ∈ V
64	63	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ℂ ∈ V)
65		reex 11129	. . . . 5 ⊢ ℝ ∈ V
66	65	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ℝ ∈ V)
67		ax-resscn 11095	. . . . 5 ⊢ ℝ ⊆ ℂ
68		sseqin2 4177	. . . . 5 ⊢ (ℝ ⊆ ℂ ↔ (ℂ ∩ ℝ) = ℝ)
69	67, 68	mpbi 230	. . . 4 ⊢ (ℂ ∩ ℝ) = ℝ
70		0pval 25640	. . . . 5 ⊢ (𝑥 ∈ ℂ → (0_𝑝‘𝑥) = 0)
71	70	adantl 481	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℂ) → (0_𝑝‘𝑥) = 0)
72	56, 1, 32, 57	mbfi1fseqlem2 25685	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → (𝐺‘𝐴) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
73	72	fveq1d 6844	. . . . . 6 ⊢ (𝐴 ∈ ℕ → ((𝐺‘𝐴)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥))
74	73	ad2antlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝐴)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥))
75		simpr 484	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
76		rge0ssre 13384	. . . . . . . . . . . . . . . 16 ⊢ (0[,)+∞) ⊆ ℝ
77		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
78		ffvelcdm 7035	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ (0[,)+∞))
79	1, 77, 78	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ (0[,)+∞))
80	76, 79	sselid 3933	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ ℝ)
81		nnnn0 12420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ₀)
82		nnexpcl 14009	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ₀) → (2↑𝑚) ∈ ℕ)
83	7, 81, 82	sylancr 588	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
84	83	ad2antrl 729	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
85	84	nnred 12172	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
86	80, 85	remulcld 11174	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ)
87		reflcl 13728	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
88	86, 87	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
89	88, 84	nndivred 12211	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
90	89	ralrimivva 3181	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
91	32	fmpo 8022	. . . . . . . . . . 11 ⊢ (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
92	90, 91	sylib 218	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶ℝ)
93		fovcdm 7538	. . . . . . . . . 10 ⊢ ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
94	92, 93	syl3an1 1164	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
95	94	3expa 1119	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
96		nnre 12164	. . . . . . . . 9 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
97	96	ad2antlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
98	95, 97	ifcld 4528	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∈ ℝ)
99		ifcl 4527	. . . . . . 7 ⊢ ((if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ℝ)
100	98, 49, 99	sylancl 587	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ℝ)
101		eqid 2737	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
102	101	fvmpt2 6961	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
103	75, 100, 102	syl2anc 585	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
104	74, 103	eqtrd 2772	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝐴)‘𝑥) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
105	55, 62, 64, 66, 69, 71, 104	ofrfval 7642	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (0_𝑝 ∘_r ≤ (𝐺‘𝐴) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
106	48, 105	mpbird 257	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 0_𝑝 ∘_r ≤ (𝐺‘𝐴))
107	56, 1, 32	mbfi1fseqlem1 25684	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶(0[,)+∞))
108	107	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐽:(ℕ × ℝ)⟶(0[,)+∞))
109		peano2nn 12169	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
110	109	ad2antlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℕ)
111	108, 110, 75	fovcdmd 7540	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) ∈ (0[,)+∞))
112		elrege0 13382	. . . . . . . . . . 11 ⊢ (((𝐴 + 1)𝐽𝑥) ∈ (0[,)+∞) ↔ (((𝐴 + 1)𝐽𝑥) ∈ ℝ ∧ 0 ≤ ((𝐴 + 1)𝐽𝑥)))
113	111, 112	sylib 218	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐴 + 1)𝐽𝑥) ∈ ℝ ∧ 0 ≤ ((𝐴 + 1)𝐽𝑥)))
114	113	simpld 494	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) ∈ ℝ)
115		min1 13116	. . . . . . . . . 10 ⊢ (((𝐴𝐽𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴𝐽𝑥))
116	95, 97, 115	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴𝐽𝑥))
117		2cn 12232	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
118	8	ad2antlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℕ₀)
119		expp1 14003	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℕ₀) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
120	117, 118, 119	sylancr 588	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
121	120	oveq2d 7384	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) = (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · ((2↑𝐴) · 2)))
122	35, 95	eqeltrrd 2838	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ ℝ)
123	122	recnd 11172	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ ℂ)
124	12	recnd 11172	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℂ)
125		2cnd 12235	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 2 ∈ ℂ)
126	123, 124, 125	mulassd 11167	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) · 2) = (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · ((2↑𝐴) · 2)))
127	20	recnd 11172	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℂ)
128	11	nnne0d 12207	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ≠ 0)
129	127, 124, 128	divcan1d 11930	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) = (⌊‘((𝐹‘𝑥) · (2↑𝐴))))
130	129	oveq1d 7383	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) · 2) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2))
131	121, 126, 130	3eqtr2d 2778	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2))
132		flle 13731	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)))
133	13, 132	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)))
134		2re 12231	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
135		2pos 12260	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
136	134, 135	pm3.2i 470	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℝ ∧ 0 < 2)
137	136	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2 ∈ ℝ ∧ 0 < 2))
138		lemul1 12005	. . . . . . . . . . . . . . . 16 ⊢ (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℝ ∧ ((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (((𝐹‘𝑥) · (2↑𝐴)) · 2)))
139	20, 13, 137, 138	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (((𝐹‘𝑥) · (2↑𝐴)) · 2)))
140	133, 139	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (((𝐹‘𝑥) · (2↑𝐴)) · 2))
141	120	oveq2d 7384	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) = ((𝐹‘𝑥) · ((2↑𝐴) · 2)))
142	6	recnd 11172	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
143	142, 124, 125	mulassd 11167	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑥) · (2↑𝐴)) · 2) = ((𝐹‘𝑥) · ((2↑𝐴) · 2)))
144	141, 143	eqtr4d 2775	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) = (((𝐹‘𝑥) · (2↑𝐴)) · 2))
145	140, 144	breqtrrd 5128	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ ((𝐹‘𝑥) · (2↑(𝐴 + 1))))
146	110	nnnn0d 12474	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℕ₀)
147		nnexpcl 14009	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ ∧ (𝐴 + 1) ∈ ℕ₀) → (2↑(𝐴 + 1)) ∈ ℕ)
148	7, 146, 147	sylancr 588	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) ∈ ℕ)
149	148	nnred 12172	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) ∈ ℝ)
150	6, 149	remulcld 11174	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ)
151	13	flcld 13730	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℤ)
152		2z 12535	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
153		zmulcl 12552	. . . . . . . . . . . . . . 15 ⊢ (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℤ ∧ 2 ∈ ℤ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈ ℤ)
154	151, 152, 153	sylancl 587	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈ ℤ)
155		flge 13737	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ ∧ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈ ℤ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ ((𝐹‘𝑥) · (2↑(𝐴 + 1))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1))))))
156	150, 154, 155	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ ((𝐹‘𝑥) · (2↑(𝐴 + 1))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1))))))
157	145, 156	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))))
158	131, 157	eqbrtrd 5122	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))))
159		reflcl 13728	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ∈ ℝ)
160	150, 159	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ∈ ℝ)
161	148	nngt0d 12206	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 < (2↑(𝐴 + 1)))
162		lemuldiv 12034	. . . . . . . . . . . 12 ⊢ ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ ℝ ∧ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ∈ ℝ ∧ ((2↑(𝐴 + 1)) ∈ ℝ ∧ 0 < (2↑(𝐴 + 1)))) → ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1)))))
163	122, 160, 149, 161, 162	syl112anc 1377	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1)))))
164	158, 163	mpbid 232	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
165		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
166	165	fveq2d 6846	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
167		simpl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → 𝑚 = (𝐴 + 1))
168	167	oveq2d 7384	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑(𝐴 + 1)))
169	166, 168	oveq12d 7386	. . . . . . . . . . . . . 14 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑(𝐴 + 1))))
170	169	fveq2d 6846	. . . . . . . . . . . . 13 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))))
171	170, 168	oveq12d 7386	. . . . . . . . . . . 12 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
172		ovex 7401	. . . . . . . . . . . 12 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))) ∈ V
173	171, 32, 172	ovmpoa 7523	. . . . . . . . . . 11 ⊢ (((𝐴 + 1) ∈ ℕ ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
174	110, 75, 173	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
175	164, 35, 174	3brtr4d 5132	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ≤ ((𝐴 + 1)𝐽𝑥))
176	98, 95, 114, 116, 175	letrd 11302	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥))
177	110	nnred 12172	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
178		min2 13117	. . . . . . . . . 10 ⊢ (((𝐴𝐽𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ 𝐴)
179	95, 97, 178	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ 𝐴)
180	97	lep1d 12085	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ≤ (𝐴 + 1))
181	98, 97, 177, 179, 180	letrd 11302	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴 + 1))
182		breq2 5104	. . . . . . . . 9 ⊢ (((𝐴 + 1)𝐽𝑥) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥) ↔ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
183		breq2 5104	. . . . . . . . 9 ⊢ ((𝐴 + 1) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴 + 1) ↔ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
184	182, 183	ifboth 4521	. . . . . . . 8 ⊢ ((if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥) ∧ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴 + 1)) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
185	176, 181, 184	syl2anc 585	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
186	185	adantr 480	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
187		iftrue 4487	. . . . . . 7 ⊢ (𝑥 ∈ (-𝐴[,]𝐴) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))
188	187	adantl 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))
189	177	renegcld 11576	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → -(𝐴 + 1) ∈ ℝ)
190	97, 177	lenegd 11728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 ≤ (𝐴 + 1) ↔ -(𝐴 + 1) ≤ -𝐴))
191	180, 190	mpbid 232	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → -(𝐴 + 1) ≤ -𝐴)
192		iccss 13342	. . . . . . . . 9 ⊢ (((-(𝐴 + 1) ∈ ℝ ∧ (𝐴 + 1) ∈ ℝ) ∧ (-(𝐴 + 1) ≤ -𝐴 ∧ 𝐴 ≤ (𝐴 + 1))) → (-𝐴[,]𝐴) ⊆ (-(𝐴 + 1)[,](𝐴 + 1)))
193	189, 177, 191, 180, 192	syl22anc 839	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (-𝐴[,]𝐴) ⊆ (-(𝐴 + 1)[,](𝐴 + 1)))
194	193	sselda 3935	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → 𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)))
195	194	iftrued 4489	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
196	186, 188, 195	3brtr4d 5132	. . . . 5 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
197		iffalse 4490	. . . . . . 7 ⊢ (¬ 𝑥 ∈ (-𝐴[,]𝐴) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = 0)
198	197	adantl 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = 0)
199	113	simprd 495	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐴 + 1)𝐽𝑥))
200	146	nn0ge0d 12477	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐴 + 1))
201		breq2 5104	. . . . . . . . . 10 ⊢ (((𝐴 + 1)𝐽𝑥) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (0 ≤ ((𝐴 + 1)𝐽𝑥) ↔ 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
202		breq2 5104	. . . . . . . . . 10 ⊢ ((𝐴 + 1) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (0 ≤ (𝐴 + 1) ↔ 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
203	201, 202	ifboth 4521	. . . . . . . . 9 ⊢ ((0 ≤ ((𝐴 + 1)𝐽𝑥) ∧ 0 ≤ (𝐴 + 1)) → 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
204	199, 200, 203	syl2anc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
205		breq2 5104	. . . . . . . . 9 ⊢ (if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) = if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) → (0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ↔ 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)))
206		breq2 5104	. . . . . . . . 9 ⊢ (0 = if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)))
207	205, 206	ifboth 4521	. . . . . . . 8 ⊢ ((0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ∧ 0 ≤ 0) → 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
208	204, 43, 207	sylancl 587	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
209	208	adantr 480	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (-𝐴[,]𝐴)) → 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
210	198, 209	eqbrtrd 5122	. . . . 5 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
211	196, 210	pm2.61dan 813	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
212	211	ralrimiva 3130	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
213		ffvelcdm 7035	. . . . . 6 ⊢ ((𝐺:ℕ⟶dom ∫₁ ∧ (𝐴 + 1) ∈ ℕ) → (𝐺‘(𝐴 + 1)) ∈ dom ∫₁)
214	58, 109, 213	syl2an 597	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘(𝐴 + 1)) ∈ dom ∫₁)
215		i1ff 25645	. . . . 5 ⊢ ((𝐺‘(𝐴 + 1)) ∈ dom ∫₁ → (𝐺‘(𝐴 + 1)):ℝ⟶ℝ)
216		ffn 6670	. . . . 5 ⊢ ((𝐺‘(𝐴 + 1)):ℝ⟶ℝ → (𝐺‘(𝐴 + 1)) Fn ℝ)
217	214, 215, 216	3syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘(𝐴 + 1)) Fn ℝ)
218		inidm 4181	. . . 4 ⊢ (ℝ ∩ ℝ) = ℝ
219	56, 1, 32, 57	mbfi1fseqlem2 25685	. . . . . . 7 ⊢ ((𝐴 + 1) ∈ ℕ → (𝐺‘(𝐴 + 1)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)))
220	219	fveq1d 6844	. . . . . 6 ⊢ ((𝐴 + 1) ∈ ℕ → ((𝐺‘(𝐴 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))‘𝑥))
221	110, 220	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘(𝐴 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))‘𝑥))
222	114, 177	ifcld 4528	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ∈ ℝ)
223		ifcl 4527	. . . . . . 7 ⊢ ((if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) ∈ ℝ)
224	222, 49, 223	sylancl 587	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) ∈ ℝ)
225		eqid 2737	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
226	225	fvmpt2 6961	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))‘𝑥) = if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
227	75, 224, 226	syl2anc 585	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))‘𝑥) = if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
228	221, 227	eqtrd 2772	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘(𝐴 + 1))‘𝑥) = if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
229	62, 217, 66, 66, 218, 104, 228	ofrfval 7642	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ((𝐺‘𝐴) ∘_r ≤ (𝐺‘(𝐴 + 1)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)))
230	212, 229	mpbird 257	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) ∘_r ≤ (𝐺‘(𝐴 + 1)))
231	106, 230	jca 511	1 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (0_𝑝 ∘_r ≤ (𝐺‘𝐴) ∧ (𝐺‘𝐴) ∘_r ≤ (𝐺‘(𝐴 + 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3052 Vcvv 3442 ∩ cin 3902 ⊆ wss 3903 ifcif 4481 {csn 4582 class class class wbr 5100 ↦ cmpt 5181 × cxp 5630 dom cdm 5632 Fn wfn 6495 ⟶wf 6496 ‘cfv 6500 (class class class)co 7368 ∈ cmpo 7370 ∘_r cofr 7631 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 +∞cpnf 11175 < clt 11178 ≤ cle 11179 -cneg 11377 / cdiv 11806 ℕcn 12157 2c2 12212 ℕ₀cn0 12413 ℤcz 12500 [,)cico 13275 [,]cicc 13276 ⌊cfl 13722 ↑cexp 13996 MblFncmbf 25583 ∫₁citg1 25584 0_𝑝c0p 25638

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-of 7632 df-ofr 7633 df-om 7819 df-1st 7943 df-2nd 7944 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-2o 8408 df-er 8645 df-map 8777 df-pm 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fi 9326 df-sup 9357 df-inf 9358 df-oi 9427 df-dju 9825 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-n0 12414 df-z 12501 df-uz 12764 df-q 12874 df-rp 12918 df-xneg 13038 df-xadd 13039 df-xmul 13040 df-ioo 13277 df-ico 13279 df-icc 13280 df-fz 13436 df-fzo 13583 df-fl 13724 df-seq 13937 df-exp 13997 df-hash 14266 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-clim 15423 df-rlim 15424 df-sum 15622 df-rest 17354 df-topgen 17375 df-psmet 21313 df-xmet 21314 df-met 21315 df-bl 21316 df-mopn 21317 df-top 22850 df-topon 22867 df-bases 22902 df-cmp 23343 df-ovol 25433 df-vol 25434 df-mbf 25588 df-itg1 25589 df-0p 25639

This theorem is referenced by: mbfi1fseqlem6 25689

W3C validator