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 24314

Description: Lemma for mbfi1fseq 24316. 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 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞))
3	2	ffvelrnda 6846	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
4		elrege0 12836	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
5	3, 4	sylib 220	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
6	5	simpld 497	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
7		2nn 11704	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
8		nnnn0 11898	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ₀)
9		nnexpcl 13436	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ ∧ 𝐴 ∈ ℕ₀) → (2↑𝐴) ∈ ℕ)
10	7, 8, 9	sylancr 589	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℕ → (2↑𝐴) ∈ ℕ)
11	10	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℕ)
12	11	nnred 11647	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℝ)
13	6, 12	remulcld 10665	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ)
14	11	nnnn0d 11949	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℕ₀)
15	14	nn0ge0d 11952	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (2↑𝐴))
16		mulge0 11152	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 ≤ (2↑𝐴))) → 0 ≤ ((𝐹‘𝑥) · (2↑𝐴)))
17	5, 12, 15, 16	syl12anc 834	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹‘𝑥) · (2↑𝐴)))
18		flge0nn0 13184	. . . . . . . . . 10 ⊢ ((((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑥) · (2↑𝐴))) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℕ₀)
19	13, 17, 18	syl2anc 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℕ₀)
20	19	nn0red 11950	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℝ)
21	19	nn0ge0d 11952	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (⌊‘((𝐹‘𝑥) · (2↑𝐴))))
22	11	nngt0d 11680	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝐴))
23		divge0 11503	. . . . . . . 8 ⊢ ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℝ ∧ 0 ≤ (⌊‘((𝐹‘𝑥) · (2↑𝐴)))) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 < (2↑𝐴))) → 0 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
24	20, 21, 12, 22, 23	syl22anc 836	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
25		simpr 487	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
26	25	fveq2d 6669	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
27		simpl 485	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → 𝑚 = 𝐴)
28	27	oveq2d 7166	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝐴))
29	26, 28	oveq12d 7168	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝐴)))
30	29	fveq2d 6669	. . . . . . . . . 10 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝐴))))
31	30, 28	oveq12d 7168	. . . . . . . . 9 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
32		mbfi1fseq.3	. . . . . . . . 9 ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))
33		ovex 7183	. . . . . . . . 9 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ V
34	31, 32, 33	ovmpoa 7299	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
35	34	adantll 712	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
36	24, 35	breqtrrd 5087	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐴𝐽𝑥))
37	8	nn0ge0d 11952	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → 0 ≤ 𝐴)
38	37	ad2antlr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝐴)
39		breq2 5063	. . . . . . 7 ⊢ ((𝐴𝐽𝑥) = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) → (0 ≤ (𝐴𝐽𝑥) ↔ 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴)))
40		breq2 5063	. . . . . . 7 ⊢ (𝐴 = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) → (0 ≤ 𝐴 ↔ 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴)))
41	39, 40	ifboth 4505	. . . . . 6 ⊢ ((0 ≤ (𝐴𝐽𝑥) ∧ 0 ≤ 𝐴) → 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))
42	36, 38, 41	syl2anc 586	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))
43		0le0 11732	. . . . 5 ⊢ 0 ≤ 0
44		breq2 5063	. . . . . 6 ⊢ (if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) → (0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ↔ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
45		breq2 5063	. . . . . 6 ⊢ (0 = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
46	44, 45	ifboth 4505	. . . . 5 ⊢ ((0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∧ 0 ≤ 0) → 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
47	42, 43, 46	sylancl 588	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
48	47	ralrimiva 3182	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ∀𝑥 ∈ ℝ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
49		0re 10637	. . . . . . 7 ⊢ 0 ∈ ℝ
50		fnconstg 6562	. . . . . . 7 ⊢ (0 ∈ ℝ → (ℂ × {0}) Fn ℂ)
51	49, 50	ax-mp 5	. . . . . 6 ⊢ (ℂ × {0}) Fn ℂ
52		df-0p 24265	. . . . . . 7 ⊢ 0_𝑝 = (ℂ × {0})
53	52	fneq1i 6445	. . . . . 6 ⊢ (0_𝑝 Fn ℂ ↔ (ℂ × {0}) Fn ℂ)
54	51, 53	mpbir 233	. . . . 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 24313	. . . . . 6 ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫₁)
59	58	ffvelrnda 6846	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) ∈ dom ∫₁)
60		i1ff 24271	. . . . 5 ⊢ ((𝐺‘𝐴) ∈ dom ∫₁ → (𝐺‘𝐴):ℝ⟶ℝ)
61		ffn 6509	. . . . 5 ⊢ ((𝐺‘𝐴):ℝ⟶ℝ → (𝐺‘𝐴) Fn ℝ)
62	59, 60, 61	3syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) Fn ℝ)
63		cnex 10612	. . . . 5 ⊢ ℂ ∈ V
64	63	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ℂ ∈ V)
65		reex 10622	. . . . 5 ⊢ ℝ ∈ V
66	65	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ℝ ∈ V)
67		ax-resscn 10588	. . . . 5 ⊢ ℝ ⊆ ℂ
68		sseqin2 4192	. . . . 5 ⊢ (ℝ ⊆ ℂ ↔ (ℂ ∩ ℝ) = ℝ)
69	67, 68	mpbi 232	. . . 4 ⊢ (ℂ ∩ ℝ) = ℝ
70		0pval 24266	. . . . 5 ⊢ (𝑥 ∈ ℂ → (0_𝑝‘𝑥) = 0)
71	70	adantl 484	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℂ) → (0_𝑝‘𝑥) = 0)
72	56, 1, 32, 57	mbfi1fseqlem2 24311	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → (𝐺‘𝐴) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
73	72	fveq1d 6667	. . . . . 6 ⊢ (𝐴 ∈ ℕ → ((𝐺‘𝐴)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥))
74	73	ad2antlr 725	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝐴)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥))
75		simpr 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
76		rge0ssre 12838	. . . . . . . . . . . . . . . 16 ⊢ (0[,)+∞) ⊆ ℝ
77		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
78		ffvelrn 6844	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ (0[,)+∞))
79	1, 77, 78	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ (0[,)+∞))
80	76, 79	sseldi 3965	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ ℝ)
81		nnnn0 11898	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ₀)
82		nnexpcl 13436	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ₀) → (2↑𝑚) ∈ ℕ)
83	7, 81, 82	sylancr 589	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
84	83	ad2antrl 726	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
85	84	nnred 11647	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
86	80, 85	remulcld 10665	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ)
87		reflcl 13160	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
88	86, 87	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
89	88, 84	nndivred 11685	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
90	89	ralrimivva 3191	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
91	32	fmpo 7760	. . . . . . . . . . 11 ⊢ (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
92	90, 91	sylib 220	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶ℝ)
93		fovrn 7312	. . . . . . . . . 10 ⊢ ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
94	92, 93	syl3an1 1159	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
95	94	3expa 1114	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
96		nnre 11639	. . . . . . . . 9 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
97	96	ad2antlr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
98	95, 97	ifcld 4512	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∈ ℝ)
99		ifcl 4511	. . . . . . 7 ⊢ ((if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ℝ)
100	98, 49, 99	sylancl 588	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ℝ)
101		eqid 2821	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
102	101	fvmpt2 6774	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
103	75, 100, 102	syl2anc 586	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
104	74, 103	eqtrd 2856	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝐴)‘𝑥) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
105	55, 62, 64, 66, 69, 71, 104	ofrfval 7411	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (0_𝑝 ∘_r ≤ (𝐺‘𝐴) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
106	48, 105	mpbird 259	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 0_𝑝 ∘_r ≤ (𝐺‘𝐴))
107	56, 1, 32	mbfi1fseqlem1 24310	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶(0[,)+∞))
108	107	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐽:(ℕ × ℝ)⟶(0[,)+∞))
109		peano2nn 11644	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
110	109	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℕ)
111	108, 110, 75	fovrnd 7314	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) ∈ (0[,)+∞))
112		elrege0 12836	. . . . . . . . . . 11 ⊢ (((𝐴 + 1)𝐽𝑥) ∈ (0[,)+∞) ↔ (((𝐴 + 1)𝐽𝑥) ∈ ℝ ∧ 0 ≤ ((𝐴 + 1)𝐽𝑥)))
113	111, 112	sylib 220	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐴 + 1)𝐽𝑥) ∈ ℝ ∧ 0 ≤ ((𝐴 + 1)𝐽𝑥)))
114	113	simpld 497	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) ∈ ℝ)
115		min1 12576	. . . . . . . . . 10 ⊢ (((𝐴𝐽𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴𝐽𝑥))
116	95, 97, 115	syl2anc 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴𝐽𝑥))
117		2cn 11706	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
118	8	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℕ₀)
119		expp1 13430	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℕ₀) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
120	117, 118, 119	sylancr 589	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
121	120	oveq2d 7166	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) = (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · ((2↑𝐴) · 2)))
122	35, 95	eqeltrrd 2914	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ ℝ)
123	122	recnd 10663	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ ℂ)
124	12	recnd 10663	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℂ)
125		2cnd 11709	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 2 ∈ ℂ)
126	123, 124, 125	mulassd 10658	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) · 2) = (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · ((2↑𝐴) · 2)))
127	20	recnd 10663	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℂ)
128	11	nnne0d 11681	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ≠ 0)
129	127, 124, 128	divcan1d 11411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) = (⌊‘((𝐹‘𝑥) · (2↑𝐴))))
130	129	oveq1d 7165	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) · 2) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2))
131	121, 126, 130	3eqtr2d 2862	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2))
132		flle 13163	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)))
133	13, 132	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)))
134		2re 11705	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
135		2pos 11734	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
136	134, 135	pm3.2i 473	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℝ ∧ 0 < 2)
137	136	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2 ∈ ℝ ∧ 0 < 2))
138		lemul1 11486	. . . . . . . . . . . . . . . 16 ⊢ (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℝ ∧ ((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (((𝐹‘𝑥) · (2↑𝐴)) · 2)))
139	20, 13, 137, 138	syl3anc 1367	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (((𝐹‘𝑥) · (2↑𝐴)) · 2)))
140	133, 139	mpbid 234	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (((𝐹‘𝑥) · (2↑𝐴)) · 2))
141	120	oveq2d 7166	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) = ((𝐹‘𝑥) · ((2↑𝐴) · 2)))
142	6	recnd 10663	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
143	142, 124, 125	mulassd 10658	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑥) · (2↑𝐴)) · 2) = ((𝐹‘𝑥) · ((2↑𝐴) · 2)))
144	141, 143	eqtr4d 2859	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) = (((𝐹‘𝑥) · (2↑𝐴)) · 2))
145	140, 144	breqtrrd 5087	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ ((𝐹‘𝑥) · (2↑(𝐴 + 1))))
146	110	nnnn0d 11949	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℕ₀)
147		nnexpcl 13436	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ ∧ (𝐴 + 1) ∈ ℕ₀) → (2↑(𝐴 + 1)) ∈ ℕ)
148	7, 146, 147	sylancr 589	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) ∈ ℕ)
149	148	nnred 11647	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) ∈ ℝ)
150	6, 149	remulcld 10665	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ)
151	13	flcld 13162	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℤ)
152		2z 12008	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
153		zmulcl 12025	. . . . . . . . . . . . . . 15 ⊢ (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℤ ∧ 2 ∈ ℤ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈ ℤ)
154	151, 152, 153	sylancl 588	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈ ℤ)
155		flge 13169	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ ∧ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈ ℤ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ ((𝐹‘𝑥) · (2↑(𝐴 + 1))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1))))))
156	150, 154, 155	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ ((𝐹‘𝑥) · (2↑(𝐴 + 1))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1))))))
157	145, 156	mpbid 234	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))))
158	131, 157	eqbrtrd 5081	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))))
159		reflcl 13160	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ∈ ℝ)
160	150, 159	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ∈ ℝ)
161	148	nngt0d 11680	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 < (2↑(𝐴 + 1)))
162		lemuldiv 11514	. . . . . . . . . . . 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 1370	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1)))))
164	158, 163	mpbid 234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
165		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
166	165	fveq2d 6669	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
167		simpl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → 𝑚 = (𝐴 + 1))
168	167	oveq2d 7166	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑(𝐴 + 1)))
169	166, 168	oveq12d 7168	. . . . . . . . . . . . . 14 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑(𝐴 + 1))))
170	169	fveq2d 6669	. . . . . . . . . . . . 13 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))))
171	170, 168	oveq12d 7168	. . . . . . . . . . . 12 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
172		ovex 7183	. . . . . . . . . . . 12 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))) ∈ V
173	171, 32, 172	ovmpoa 7299	. . . . . . . . . . 11 ⊢ (((𝐴 + 1) ∈ ℕ ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
174	110, 75, 173	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
175	164, 35, 174	3brtr4d 5091	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ≤ ((𝐴 + 1)𝐽𝑥))
176	98, 95, 114, 116, 175	letrd 10791	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥))
177	110	nnred 11647	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
178		min2 12577	. . . . . . . . . 10 ⊢ (((𝐴𝐽𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ 𝐴)
179	95, 97, 178	syl2anc 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ 𝐴)
180	97	lep1d 11565	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ≤ (𝐴 + 1))
181	98, 97, 177, 179, 180	letrd 10791	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴 + 1))
182		breq2 5063	. . . . . . . . 9 ⊢ (((𝐴 + 1)𝐽𝑥) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥) ↔ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
183		breq2 5063	. . . . . . . . 9 ⊢ ((𝐴 + 1) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴 + 1) ↔ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
184	182, 183	ifboth 4505	. . . . . . . 8 ⊢ ((if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥) ∧ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴 + 1)) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
185	176, 181, 184	syl2anc 586	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
186	185	adantr 483	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
187		iftrue 4473	. . . . . . 7 ⊢ (𝑥 ∈ (-𝐴[,]𝐴) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))
188	187	adantl 484	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))
189	177	renegcld 11061	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → -(𝐴 + 1) ∈ ℝ)
190	97, 177	lenegd 11213	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 ≤ (𝐴 + 1) ↔ -(𝐴 + 1) ≤ -𝐴))
191	180, 190	mpbid 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → -(𝐴 + 1) ≤ -𝐴)
192		iccss 12798	. . . . . . . . 9 ⊢ (((-(𝐴 + 1) ∈ ℝ ∧ (𝐴 + 1) ∈ ℝ) ∧ (-(𝐴 + 1) ≤ -𝐴 ∧ 𝐴 ≤ (𝐴 + 1))) → (-𝐴[,]𝐴) ⊆ (-(𝐴 + 1)[,](𝐴 + 1)))
193	189, 177, 191, 180, 192	syl22anc 836	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (-𝐴[,]𝐴) ⊆ (-(𝐴 + 1)[,](𝐴 + 1)))
194	193	sselda 3967	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → 𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)))
195	194	iftrued 4475	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
196	186, 188, 195	3brtr4d 5091	. . . . 5 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
197		iffalse 4476	. . . . . . 7 ⊢ (¬ 𝑥 ∈ (-𝐴[,]𝐴) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = 0)
198	197	adantl 484	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = 0)
199	113	simprd 498	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐴 + 1)𝐽𝑥))
200	146	nn0ge0d 11952	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐴 + 1))
201		breq2 5063	. . . . . . . . . 10 ⊢ (((𝐴 + 1)𝐽𝑥) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (0 ≤ ((𝐴 + 1)𝐽𝑥) ↔ 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
202		breq2 5063	. . . . . . . . . 10 ⊢ ((𝐴 + 1) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (0 ≤ (𝐴 + 1) ↔ 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
203	201, 202	ifboth 4505	. . . . . . . . 9 ⊢ ((0 ≤ ((𝐴 + 1)𝐽𝑥) ∧ 0 ≤ (𝐴 + 1)) → 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
204	199, 200, 203	syl2anc 586	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
205		breq2 5063	. . . . . . . . 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 5063	. . . . . . . . 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 4505	. . . . . . . 8 ⊢ ((0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ∧ 0 ≤ 0) → 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
208	204, 43, 207	sylancl 588	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
209	208	adantr 483	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (-𝐴[,]𝐴)) → 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
210	198, 209	eqbrtrd 5081	. . . . 5 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
211	196, 210	pm2.61dan 811	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
212	211	ralrimiva 3182	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
213		ffvelrn 6844	. . . . . 6 ⊢ ((𝐺:ℕ⟶dom ∫₁ ∧ (𝐴 + 1) ∈ ℕ) → (𝐺‘(𝐴 + 1)) ∈ dom ∫₁)
214	58, 109, 213	syl2an 597	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘(𝐴 + 1)) ∈ dom ∫₁)
215		i1ff 24271	. . . . 5 ⊢ ((𝐺‘(𝐴 + 1)) ∈ dom ∫₁ → (𝐺‘(𝐴 + 1)):ℝ⟶ℝ)
216		ffn 6509	. . . . 5 ⊢ ((𝐺‘(𝐴 + 1)):ℝ⟶ℝ → (𝐺‘(𝐴 + 1)) Fn ℝ)
217	214, 215, 216	3syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘(𝐴 + 1)) Fn ℝ)
218		inidm 4195	. . . 4 ⊢ (ℝ ∩ ℝ) = ℝ
219	56, 1, 32, 57	mbfi1fseqlem2 24311	. . . . . . 7 ⊢ ((𝐴 + 1) ∈ ℕ → (𝐺‘(𝐴 + 1)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)))
220	219	fveq1d 6667	. . . . . 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 4512	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ∈ ℝ)
223		ifcl 4511	. . . . . . 7 ⊢ ((if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) ∈ ℝ)
224	222, 49, 223	sylancl 588	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) ∈ ℝ)
225		eqid 2821	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
226	225	fvmpt2 6774	. . . . . 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 586	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))‘𝑥) = if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
228	221, 227	eqtrd 2856	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘(𝐴 + 1))‘𝑥) = if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
229	62, 217, 66, 66, 218, 104, 228	ofrfval 7411	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ((𝐺‘𝐴) ∘_r ≤ (𝐺‘(𝐴 + 1)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)))
230	212, 229	mpbird 259	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) ∘_r ≤ (𝐺‘(𝐴 + 1)))
231	106, 230	jca 514	1 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (0_𝑝 ∘_r ≤ (𝐺‘𝐴) ∧ (𝐺‘𝐴) ∘_r ≤ (𝐺‘(𝐴 + 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1533 ∈ wcel 2110 ∀wral 3138 Vcvv 3495 ∩ cin 3935 ⊆ wss 3936 ifcif 4467 {csn 4561 class class class wbr 5059 ↦ cmpt 5139 × cxp 5548 dom cdm 5550 Fn wfn 6345 ⟶wf 6346 ‘cfv 6350 (class class class)co 7150 ∈ cmpo 7152 ∘_r cofr 7402 ℂcc 10529 ℝcr 10530 0cc0 10531 1c1 10532 + caddc 10534 · cmul 10536 +∞cpnf 10666 < clt 10669 ≤ cle 10670 -cneg 10865 / cdiv 11291 ℕcn 11632 2c2 11686 ℕ₀cn0 11891 ℤcz 11975 [,)cico 12734 [,]cicc 12735 ⌊cfl 13154 ↑cexp 13423 MblFncmbf 24209 ∫₁citg1 24210 0_𝑝c0p 24264

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-rep 5183 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455 ax-inf2 9098 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3497 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4833 df-int 4870 df-iun 4914 df-br 5060 df-opab 5122 df-mpt 5140 df-tr 5166 df-id 5455 df-eprel 5460 df-po 5469 df-so 5470 df-fr 5509 df-se 5510 df-we 5511 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-pred 6143 df-ord 6189 df-on 6190 df-lim 6191 df-suc 6192 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-isom 6359 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-of 7403 df-ofr 7404 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-2o 8097 df-oadd 8100 df-er 8283 df-map 8402 df-pm 8403 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-fi 8869 df-sup 8900 df-inf 8901 df-oi 8968 df-dju 9324 df-card 9362 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-n0 11892 df-z 11976 df-uz 12238 df-q 12343 df-rp 12384 df-xneg 12501 df-xadd 12502 df-xmul 12503 df-ioo 12736 df-ico 12738 df-icc 12739 df-fz 12887 df-fzo 13028 df-fl 13156 df-seq 13364 df-exp 13424 df-hash 13685 df-cj 14452 df-re 14453 df-im 14454 df-sqrt 14588 df-abs 14589 df-clim 14839 df-rlim 14840 df-sum 15037 df-rest 16690 df-topgen 16711 df-psmet 20531 df-xmet 20532 df-met 20533 df-bl 20534 df-mopn 20535 df-top 21496 df-topon 21513 df-bases 21548 df-cmp 21989 df-ovol 24059 df-vol 24060 df-mbf 24214 df-itg1 24215 df-0p 24265

This theorem is referenced by: mbfi1fseqlem6 24315

W3C validator