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 24320

Description: Lemma for mbfi1fseq 24322. 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 6851	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
4		elrege0 12843	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
5	3, 4	sylib 220	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
6	5	simpld 497	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
7		2nn 11711	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
8		nnnn0 11905	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ₀)
9		nnexpcl 13443	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ ∧ 𝐴 ∈ ℕ₀) → (2↑𝐴) ∈ ℕ)
10	7, 8, 9	sylancr 589	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℕ → (2↑𝐴) ∈ ℕ)
11	10	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℕ)
12	11	nnred 11653	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℝ)
13	6, 12	remulcld 10671	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ)
14	11	nnnn0d 11956	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℕ₀)
15	14	nn0ge0d 11959	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (2↑𝐴))
16		mulge0 11158	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 ≤ (2↑𝐴))) → 0 ≤ ((𝐹‘𝑥) · (2↑𝐴)))
17	5, 12, 15, 16	syl12anc 834	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹‘𝑥) · (2↑𝐴)))
18		flge0nn0 13191	. . . . . . . . . 10 ⊢ ((((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑥) · (2↑𝐴))) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℕ₀)
19	13, 17, 18	syl2anc 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℕ₀)
20	19	nn0red 11957	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℝ)
21	19	nn0ge0d 11959	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (⌊‘((𝐹‘𝑥) · (2↑𝐴))))
22	11	nngt0d 11687	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝐴))
23		divge0 11509	. . . . . . . 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 6674	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
27		simpl 485	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → 𝑚 = 𝐴)
28	27	oveq2d 7172	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝐴))
29	26, 28	oveq12d 7174	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝐴)))
30	29	fveq2d 6674	. . . . . . . . . 10 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝐴))))
31	30, 28	oveq12d 7174	. . . . . . . . 9 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
32		mbfi1fseq.3	. . . . . . . . 9 ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))
33		ovex 7189	. . . . . . . . 9 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ V
34	31, 32, 33	ovmpoa 7305	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
35	34	adantll 712	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
36	24, 35	breqtrrd 5094	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐴𝐽𝑥))
37	8	nn0ge0d 11959	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → 0 ≤ 𝐴)
38	37	ad2antlr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝐴)
39		breq2 5070	. . . . . . 7 ⊢ ((𝐴𝐽𝑥) = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) → (0 ≤ (𝐴𝐽𝑥) ↔ 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴)))
40		breq2 5070	. . . . . . 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 11739	. . . . 5 ⊢ 0 ≤ 0
44		breq2 5070	. . . . . 6 ⊢ (if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) → (0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ↔ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
45		breq2 5070	. . . . . 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 10643	. . . . . . 7 ⊢ 0 ∈ ℝ
50		fnconstg 6567	. . . . . . 7 ⊢ (0 ∈ ℝ → (ℂ × {0}) Fn ℂ)
51	49, 50	ax-mp 5	. . . . . 6 ⊢ (ℂ × {0}) Fn ℂ
52		df-0p 24271	. . . . . . 7 ⊢ 0_𝑝 = (ℂ × {0})
53	52	fneq1i 6450	. . . . . 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 24319	. . . . . 6 ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫₁)
59	58	ffvelrnda 6851	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) ∈ dom ∫₁)
60		i1ff 24277	. . . . 5 ⊢ ((𝐺‘𝐴) ∈ dom ∫₁ → (𝐺‘𝐴):ℝ⟶ℝ)
61		ffn 6514	. . . . 5 ⊢ ((𝐺‘𝐴):ℝ⟶ℝ → (𝐺‘𝐴) Fn ℝ)
62	59, 60, 61	3syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) Fn ℝ)
63		cnex 10618	. . . . 5 ⊢ ℂ ∈ V
64	63	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ℂ ∈ V)
65		reex 10628	. . . . 5 ⊢ ℝ ∈ V
66	65	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ℝ ∈ V)
67		ax-resscn 10594	. . . . 5 ⊢ ℝ ⊆ ℂ
68		sseqin2 4192	. . . . 5 ⊢ (ℝ ⊆ ℂ ↔ (ℂ ∩ ℝ) = ℝ)
69	67, 68	mpbi 232	. . . 4 ⊢ (ℂ ∩ ℝ) = ℝ
70		0pval 24272	. . . . 5 ⊢ (𝑥 ∈ ℂ → (0_𝑝‘𝑥) = 0)
71	70	adantl 484	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℂ) → (0_𝑝‘𝑥) = 0)
72	56, 1, 32, 57	mbfi1fseqlem2 24317	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → (𝐺‘𝐴) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
73	72	fveq1d 6672	. . . . . 6 ⊢ (𝐴 ∈ ℕ → ((𝐺‘𝐴)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥))
74	73	ad2antlr 725	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝐴)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥))
75		simpr 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
76		rge0ssre 12845	. . . . . . . . . . . . . . . 16 ⊢ (0[,)+∞) ⊆ ℝ
77		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
78		ffvelrn 6849	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ (0[,)+∞))
79	1, 77, 78	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ (0[,)+∞))
80	76, 79	sseldi 3965	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ ℝ)
81		nnnn0 11905	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ₀)
82		nnexpcl 13443	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ₀) → (2↑𝑚) ∈ ℕ)
83	7, 81, 82	sylancr 589	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
84	83	ad2antrl 726	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
85	84	nnred 11653	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
86	80, 85	remulcld 10671	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ)
87		reflcl 13167	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
88	86, 87	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
89	88, 84	nndivred 11692	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
90	89	ralrimivva 3191	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
91	32	fmpo 7766	. . . . . . . . . . 11 ⊢ (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
92	90, 91	sylib 220	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶ℝ)
93		fovrn 7318	. . . . . . . . . 10 ⊢ ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
94	92, 93	syl3an1 1159	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
95	94	3expa 1114	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
96		nnre 11645	. . . . . . . . 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 6779	. . . . . 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 7417	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (0_𝑝 ∘_r ≤ (𝐺‘𝐴) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
106	48, 105	mpbird 259	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 0_𝑝 ∘_r ≤ (𝐺‘𝐴))
107	56, 1, 32	mbfi1fseqlem1 24316	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶(0[,)+∞))
108	107	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐽:(ℕ × ℝ)⟶(0[,)+∞))
109		peano2nn 11650	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
110	109	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℕ)
111	108, 110, 75	fovrnd 7320	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) ∈ (0[,)+∞))
112		elrege0 12843	. . . . . . . . . . 11 ⊢ (((𝐴 + 1)𝐽𝑥) ∈ (0[,)+∞) ↔ (((𝐴 + 1)𝐽𝑥) ∈ ℝ ∧ 0 ≤ ((𝐴 + 1)𝐽𝑥)))
113	111, 112	sylib 220	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐴 + 1)𝐽𝑥) ∈ ℝ ∧ 0 ≤ ((𝐴 + 1)𝐽𝑥)))
114	113	simpld 497	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) ∈ ℝ)
115		min1 12583	. . . . . . . . . 10 ⊢ (((𝐴𝐽𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴𝐽𝑥))
116	95, 97, 115	syl2anc 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴𝐽𝑥))
117		2cn 11713	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
118	8	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℕ₀)
119		expp1 13437	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℕ₀) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
120	117, 118, 119	sylancr 589	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
121	120	oveq2d 7172	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) = (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · ((2↑𝐴) · 2)))
122	35, 95	eqeltrrd 2914	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ ℝ)
123	122	recnd 10669	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ ℂ)
124	12	recnd 10669	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℂ)
125		2cnd 11716	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 2 ∈ ℂ)
126	123, 124, 125	mulassd 10664	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) · 2) = (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · ((2↑𝐴) · 2)))
127	20	recnd 10669	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℂ)
128	11	nnne0d 11688	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ≠ 0)
129	127, 124, 128	divcan1d 11417	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) = (⌊‘((𝐹‘𝑥) · (2↑𝐴))))
130	129	oveq1d 7171	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) · 2) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2))
131	121, 126, 130	3eqtr2d 2862	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2))
132		flle 13170	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)))
133	13, 132	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)))
134		2re 11712	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
135		2pos 11741	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
136	134, 135	pm3.2i 473	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℝ ∧ 0 < 2)
137	136	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2 ∈ ℝ ∧ 0 < 2))
138		lemul1 11492	. . . . . . . . . . . . . . . 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 7172	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) = ((𝐹‘𝑥) · ((2↑𝐴) · 2)))
142	6	recnd 10669	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
143	142, 124, 125	mulassd 10664	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑥) · (2↑𝐴)) · 2) = ((𝐹‘𝑥) · ((2↑𝐴) · 2)))
144	141, 143	eqtr4d 2859	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) = (((𝐹‘𝑥) · (2↑𝐴)) · 2))
145	140, 144	breqtrrd 5094	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ ((𝐹‘𝑥) · (2↑(𝐴 + 1))))
146	110	nnnn0d 11956	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℕ₀)
147		nnexpcl 13443	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ ∧ (𝐴 + 1) ∈ ℕ₀) → (2↑(𝐴 + 1)) ∈ ℕ)
148	7, 146, 147	sylancr 589	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) ∈ ℕ)
149	148	nnred 11653	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) ∈ ℝ)
150	6, 149	remulcld 10671	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ)
151	13	flcld 13169	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℤ)
152		2z 12015	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
153		zmulcl 12032	. . . . . . . . . . . . . . 15 ⊢ (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℤ ∧ 2 ∈ ℤ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈ ℤ)
154	151, 152, 153	sylancl 588	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈ ℤ)
155		flge 13176	. . . . . . . . . . . . . 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 5088	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))))
159		reflcl 13167	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ∈ ℝ)
160	150, 159	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ∈ ℝ)
161	148	nngt0d 11687	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 < (2↑(𝐴 + 1)))
162		lemuldiv 11520	. . . . . . . . . . . 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 6674	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
167		simpl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → 𝑚 = (𝐴 + 1))
168	167	oveq2d 7172	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑(𝐴 + 1)))
169	166, 168	oveq12d 7174	. . . . . . . . . . . . . 14 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑(𝐴 + 1))))
170	169	fveq2d 6674	. . . . . . . . . . . . 13 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))))
171	170, 168	oveq12d 7174	. . . . . . . . . . . 12 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
172		ovex 7189	. . . . . . . . . . . 12 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))) ∈ V
173	171, 32, 172	ovmpoa 7305	. . . . . . . . . . 11 ⊢ (((𝐴 + 1) ∈ ℕ ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
174	110, 75, 173	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
175	164, 35, 174	3brtr4d 5098	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ≤ ((𝐴 + 1)𝐽𝑥))
176	98, 95, 114, 116, 175	letrd 10797	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥))
177	110	nnred 11653	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
178		min2 12584	. . . . . . . . . 10 ⊢ (((𝐴𝐽𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ 𝐴)
179	95, 97, 178	syl2anc 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ 𝐴)
180	97	lep1d 11571	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ≤ (𝐴 + 1))
181	98, 97, 177, 179, 180	letrd 10797	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴 + 1))
182		breq2 5070	. . . . . . . . 9 ⊢ (((𝐴 + 1)𝐽𝑥) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥) ↔ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
183		breq2 5070	. . . . . . . . 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 11067	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → -(𝐴 + 1) ∈ ℝ)
190	97, 177	lenegd 11219	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 ≤ (𝐴 + 1) ↔ -(𝐴 + 1) ≤ -𝐴))
191	180, 190	mpbid 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → -(𝐴 + 1) ≤ -𝐴)
192		iccss 12805	. . . . . . . . 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 5098	. . . . 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 11959	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐴 + 1))
201		breq2 5070	. . . . . . . . . 10 ⊢ (((𝐴 + 1)𝐽𝑥) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (0 ≤ ((𝐴 + 1)𝐽𝑥) ↔ 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
202		breq2 5070	. . . . . . . . . 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 5070	. . . . . . . . 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 5070	. . . . . . . . 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 5088	. . . . 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 6849	. . . . . 6 ⊢ ((𝐺:ℕ⟶dom ∫₁ ∧ (𝐴 + 1) ∈ ℕ) → (𝐺‘(𝐴 + 1)) ∈ dom ∫₁)
214	58, 109, 213	syl2an 597	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘(𝐴 + 1)) ∈ dom ∫₁)
215		i1ff 24277	. . . . 5 ⊢ ((𝐺‘(𝐴 + 1)) ∈ dom ∫₁ → (𝐺‘(𝐴 + 1)):ℝ⟶ℝ)
216		ffn 6514	. . . . 5 ⊢ ((𝐺‘(𝐴 + 1)):ℝ⟶ℝ → (𝐺‘(𝐴 + 1)) Fn ℝ)
217	214, 215, 216	3syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘(𝐴 + 1)) Fn ℝ)
218		inidm 4195	. . . 4 ⊢ (ℝ ∩ ℝ) = ℝ
219	56, 1, 32, 57	mbfi1fseqlem2 24317	. . . . . . 7 ⊢ ((𝐴 + 1) ∈ ℕ → (𝐺‘(𝐴 + 1)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)))
220	219	fveq1d 6672	. . . . . 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 6779	. . . . . 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 7417	. . 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 1537 ∈ wcel 2114 ∀wral 3138 Vcvv 3494 ∩ cin 3935 ⊆ wss 3936 ifcif 4467 {csn 4567 class class class wbr 5066 ↦ cmpt 5146 × cxp 5553 dom cdm 5555 Fn wfn 6350 ⟶wf 6351 ‘cfv 6355 (class class class)co 7156 ∈ cmpo 7158 ∘_r cofr 7408 ℂcc 10535 ℝcr 10536 0cc0 10537 1c1 10538 + caddc 10540 · cmul 10542 +∞cpnf 10672 < clt 10675 ≤ cle 10676 -cneg 10871 / cdiv 11297 ℕcn 11638 2c2 11693 ℕ₀cn0 11898 ℤcz 11982 [,)cico 12741 [,]cicc 12742 ⌊cfl 13161 ↑cexp 13430 MblFncmbf 24215 ∫₁citg1 24216 0_𝑝c0p 24270

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-inf2 9104 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 ax-pre-sup 10615

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 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 3496 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 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-se 5515 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-isom 6364 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7409 df-ofr 7410 df-om 7581 df-1st 7689 df-2nd 7690 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-2o 8103 df-oadd 8106 df-er 8289 df-map 8408 df-pm 8409 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-fi 8875 df-sup 8906 df-inf 8907 df-oi 8974 df-dju 9330 df-card 9368 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-2 11701 df-3 11702 df-n0 11899 df-z 11983 df-uz 12245 df-q 12350 df-rp 12391 df-xneg 12508 df-xadd 12509 df-xmul 12510 df-ioo 12743 df-ico 12745 df-icc 12746 df-fz 12894 df-fzo 13035 df-fl 13163 df-seq 13371 df-exp 13431 df-hash 13692 df-cj 14458 df-re 14459 df-im 14460 df-sqrt 14594 df-abs 14595 df-clim 14845 df-rlim 14846 df-sum 15043 df-rest 16696 df-topgen 16717 df-psmet 20537 df-xmet 20538 df-met 20539 df-bl 20540 df-mopn 20541 df-top 21502 df-topon 21519 df-bases 21554 df-cmp 21995 df-ovol 24065 df-vol 24066 df-mbf 24220 df-itg1 24221 df-0p 24271

This theorem is referenced by: mbfi1fseqlem6 24321

W3C validator