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 25166

Description: Lemma for mbfi1fseq 25168. 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 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞))
3	2	ffvelcdmda 7071	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
4		elrege0 13413	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
5	3, 4	sylib 217	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
6	5	simpld 495	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
7		2nn 12267	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℕ
8		nnnn0 12461	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ₀)
9		nnexpcl 14022	. . . . . . . . . . . . . 14 ⊢ ((2 ∈ ℕ ∧ 𝐴 ∈ ℕ₀) → (2↑𝐴) ∈ ℕ)
10	7, 8, 9	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℕ → (2↑𝐴) ∈ ℕ)
11	10	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℕ)
12	11	nnred 12209	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℝ)
13	6, 12	remulcld 11226	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ)
14	11	nnnn0d 12514	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℕ₀)
15	14	nn0ge0d 12517	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (2↑𝐴))
16		mulge0 11714	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 ≤ (2↑𝐴))) → 0 ≤ ((𝐹‘𝑥) · (2↑𝐴)))
17	5, 12, 15, 16	syl12anc 835	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹‘𝑥) · (2↑𝐴)))
18		flge0nn0 13767	. . . . . . . . . 10 ⊢ ((((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑥) · (2↑𝐴))) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℕ₀)
19	13, 17, 18	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℕ₀)
20	19	nn0red 12515	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℝ)
21	19	nn0ge0d 12517	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (⌊‘((𝐹‘𝑥) · (2↑𝐴))))
22	11	nngt0d 12243	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝐴))
23		divge0 12065	. . . . . . . 8 ⊢ ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℝ ∧ 0 ≤ (⌊‘((𝐹‘𝑥) · (2↑𝐴)))) ∧ ((2↑𝐴) ∈ ℝ ∧ 0 < (2↑𝐴))) → 0 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
24	20, 21, 12, 22, 23	syl22anc 837	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
25		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
26	25	fveq2d 6882	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
27		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → 𝑚 = 𝐴)
28	27	oveq2d 7409	. . . . . . . . . . . 12 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝐴))
29	26, 28	oveq12d 7411	. . . . . . . . . . 11 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝐴)))
30	29	fveq2d 6882	. . . . . . . . . 10 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝐴))))
31	30, 28	oveq12d 7411	. . . . . . . . 9 ⊢ ((𝑚 = 𝐴 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
32		mbfi1fseq.3	. . . . . . . . 9 ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))
33		ovex 7426	. . . . . . . . 9 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ V
34	31, 32, 33	ovmpoa 7546	. . . . . . . 8 ⊢ ((𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
35	34	adantll 712	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)))
36	24, 35	breqtrrd 5169	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐴𝐽𝑥))
37	8	nn0ge0d 12517	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → 0 ≤ 𝐴)
38	37	ad2antlr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝐴)
39		breq2 5145	. . . . . . 7 ⊢ ((𝐴𝐽𝑥) = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) → (0 ≤ (𝐴𝐽𝑥) ↔ 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴)))
40		breq2 5145	. . . . . . 7 ⊢ (𝐴 = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) → (0 ≤ 𝐴 ↔ 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴)))
41	39, 40	ifboth 4561	. . . . . 6 ⊢ ((0 ≤ (𝐴𝐽𝑥) ∧ 0 ≤ 𝐴) → 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))
42	36, 38, 41	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))
43		0le0 12295	. . . . 5 ⊢ 0 ≤ 0
44		breq2 5145	. . . . . 6 ⊢ (if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) → (0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ↔ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
45		breq2 5145	. . . . . 6 ⊢ (0 = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
46	44, 45	ifboth 4561	. . . . 5 ⊢ ((0 ≤ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∧ 0 ≤ 0) → 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
47	42, 43, 46	sylancl 586	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
48	47	ralrimiva 3145	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ∀𝑥 ∈ ℝ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
49		0re 11198	. . . . . . 7 ⊢ 0 ∈ ℝ
50		fnconstg 6766	. . . . . . 7 ⊢ (0 ∈ ℝ → (ℂ × {0}) Fn ℂ)
51	49, 50	ax-mp 5	. . . . . 6 ⊢ (ℂ × {0}) Fn ℂ
52		df-0p 25116	. . . . . . 7 ⊢ 0_𝑝 = (ℂ × {0})
53	52	fneq1i 6635	. . . . . 6 ⊢ (0_𝑝 Fn ℂ ↔ (ℂ × {0}) Fn ℂ)
54	51, 53	mpbir 230	. . . . 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 25165	. . . . . 6 ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫₁)
59	58	ffvelcdmda 7071	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) ∈ dom ∫₁)
60		i1ff 25122	. . . . 5 ⊢ ((𝐺‘𝐴) ∈ dom ∫₁ → (𝐺‘𝐴):ℝ⟶ℝ)
61		ffn 6704	. . . . 5 ⊢ ((𝐺‘𝐴):ℝ⟶ℝ → (𝐺‘𝐴) Fn ℝ)
62	59, 60, 61	3syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) Fn ℝ)
63		cnex 11173	. . . . 5 ⊢ ℂ ∈ V
64	63	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ℂ ∈ V)
65		reex 11183	. . . . 5 ⊢ ℝ ∈ V
66	65	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ℝ ∈ V)
67		ax-resscn 11149	. . . . 5 ⊢ ℝ ⊆ ℂ
68		sseqin2 4211	. . . . 5 ⊢ (ℝ ⊆ ℂ ↔ (ℂ ∩ ℝ) = ℝ)
69	67, 68	mpbi 229	. . . 4 ⊢ (ℂ ∩ ℝ) = ℝ
70		0pval 25117	. . . . 5 ⊢ (𝑥 ∈ ℂ → (0_𝑝‘𝑥) = 0)
71	70	adantl 482	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℂ) → (0_𝑝‘𝑥) = 0)
72	56, 1, 32, 57	mbfi1fseqlem2 25163	. . . . . . 7 ⊢ (𝐴 ∈ ℕ → (𝐺‘𝐴) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
73	72	fveq1d 6880	. . . . . 6 ⊢ (𝐴 ∈ ℕ → ((𝐺‘𝐴)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥))
74	73	ad2antlr 725	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝐴)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥))
75		simpr 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
76		rge0ssre 13415	. . . . . . . . . . . . . . . 16 ⊢ (0[,)+∞) ⊆ ℝ
77		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
78		ffvelcdm 7068	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ (0[,)+∞))
79	1, 77, 78	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ (0[,)+∞))
80	76, 79	sselid 3976	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ ℝ)
81		nnnn0 12461	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ₀)
82		nnexpcl 14022	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ₀) → (2↑𝑚) ∈ ℕ)
83	7, 81, 82	sylancr 587	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
84	83	ad2antrl 726	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
85	84	nnred 12209	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
86	80, 85	remulcld 11226	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ)
87		reflcl 13743	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
88	86, 87	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
89	88, 84	nndivred 12248	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
90	89	ralrimivva 3199	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
91	32	fmpo 8036	. . . . . . . . . . 11 ⊢ (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
92	90, 91	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶ℝ)
93		fovcdm 7560	. . . . . . . . . 10 ⊢ ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
94	92, 93	syl3an1 1163	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
95	94	3expa 1118	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ∈ ℝ)
96		nnre 12201	. . . . . . . . 9 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
97	96	ad2antlr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)
98	95, 97	ifcld 4568	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∈ ℝ)
99		ifcl 4567	. . . . . . 7 ⊢ ((if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ℝ)
100	98, 49, 99	sylancl 586	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ℝ)
101		eqid 2731	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
102	101	fvmpt2 6995	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
103	75, 100, 102	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))‘𝑥) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
104	74, 103	eqtrd 2771	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝐴)‘𝑥) = if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0))
105	55, 62, 64, 66, 69, 71, 104	ofrfval 7663	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (0_𝑝 ∘_r ≤ (𝐺‘𝐴) ↔ ∀𝑥 ∈ ℝ 0 ≤ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
106	48, 105	mpbird 256	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → 0_𝑝 ∘_r ≤ (𝐺‘𝐴))
107	56, 1, 32	mbfi1fseqlem1 25162	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶(0[,)+∞))
108	107	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐽:(ℕ × ℝ)⟶(0[,)+∞))
109		peano2nn 12206	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
110	109	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℕ)
111	108, 110, 75	fovcdmd 7562	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) ∈ (0[,)+∞))
112		elrege0 13413	. . . . . . . . . . 11 ⊢ (((𝐴 + 1)𝐽𝑥) ∈ (0[,)+∞) ↔ (((𝐴 + 1)𝐽𝑥) ∈ ℝ ∧ 0 ≤ ((𝐴 + 1)𝐽𝑥)))
113	111, 112	sylib 217	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐴 + 1)𝐽𝑥) ∈ ℝ ∧ 0 ≤ ((𝐴 + 1)𝐽𝑥)))
114	113	simpld 495	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) ∈ ℝ)
115		min1 13150	. . . . . . . . . 10 ⊢ (((𝐴𝐽𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴𝐽𝑥))
116	95, 97, 115	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴𝐽𝑥))
117		2cn 12269	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
118	8	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℕ₀)
119		expp1 14016	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝐴 ∈ ℕ₀) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
120	117, 118, 119	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
121	120	oveq2d 7409	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) = (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · ((2↑𝐴) · 2)))
122	35, 95	eqeltrrd 2833	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ ℝ)
123	122	recnd 11224	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ∈ ℂ)
124	12	recnd 11224	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ∈ ℂ)
125		2cnd 12272	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 2 ∈ ℂ)
126	123, 124, 125	mulassd 11219	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) · 2) = (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · ((2↑𝐴) · 2)))
127	20	recnd 11224	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℂ)
128	11	nnne0d 12244	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑𝐴) ≠ 0)
129	127, 124, 128	divcan1d 11973	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) = (⌊‘((𝐹‘𝑥) · (2↑𝐴))))
130	129	oveq1d 7408	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑𝐴)) · 2) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2))
131	121, 126, 130	3eqtr2d 2777	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) = ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2))
132		flle 13746	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)))
133	13, 132	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)))
134		2re 12268	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℝ
135		2pos 12297	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 2
136	134, 135	pm3.2i 471	. . . . . . . . . . . . . . . . 17 ⊢ (2 ∈ ℝ ∧ 0 < 2)
137	136	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2 ∈ ℝ ∧ 0 < 2))
138		lemul1 12048	. . . . . . . . . . . . . . . 16 ⊢ (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℝ ∧ ((𝐹‘𝑥) · (2↑𝐴)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (((𝐹‘𝑥) · (2↑𝐴)) · 2)))
139	20, 13, 137, 138	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ≤ ((𝐹‘𝑥) · (2↑𝐴)) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (((𝐹‘𝑥) · (2↑𝐴)) · 2)))
140	133, 139	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (((𝐹‘𝑥) · (2↑𝐴)) · 2))
141	120	oveq2d 7409	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) = ((𝐹‘𝑥) · ((2↑𝐴) · 2)))
142	6	recnd 11224	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
143	142, 124, 125	mulassd 11219	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑥) · (2↑𝐴)) · 2) = ((𝐹‘𝑥) · ((2↑𝐴) · 2)))
144	141, 143	eqtr4d 2774	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) = (((𝐹‘𝑥) · (2↑𝐴)) · 2))
145	140, 144	breqtrrd 5169	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ ((𝐹‘𝑥) · (2↑(𝐴 + 1))))
146	110	nnnn0d 12514	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℕ₀)
147		nnexpcl 14022	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℕ ∧ (𝐴 + 1) ∈ ℕ₀) → (2↑(𝐴 + 1)) ∈ ℕ)
148	7, 146, 147	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) ∈ ℕ)
149	148	nnred 12209	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (2↑(𝐴 + 1)) ∈ ℝ)
150	6, 149	remulcld 11226	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ)
151	13	flcld 13745	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℤ)
152		2z 12576	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
153		zmulcl 12593	. . . . . . . . . . . . . . 15 ⊢ (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) ∈ ℤ ∧ 2 ∈ ℤ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈ ℤ)
154	151, 152, 153	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈ ℤ)
155		flge 13752	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ ∧ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ∈ ℤ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ ((𝐹‘𝑥) · (2↑(𝐴 + 1))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1))))))
156	150, 154, 155	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ ((𝐹‘𝑥) · (2↑(𝐴 + 1))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1))))))
157	145, 156	mpbid 231	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) · 2) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))))
158	131, 157	eqbrtrd 5163	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))))
159		reflcl 13743	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) · (2↑(𝐴 + 1))) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ∈ ℝ)
160	150, 159	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ∈ ℝ)
161	148	nngt0d 12243	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 < (2↑(𝐴 + 1)))
162		lemuldiv 12076	. . . . . . . . . . . 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 1374	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) · (2↑(𝐴 + 1))) ≤ (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1)))))
164	158, 163	mpbid 231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝐴))) / (2↑𝐴)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
165		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
166	165	fveq2d 6882	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
167		simpl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → 𝑚 = (𝐴 + 1))
168	167	oveq2d 7409	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑(𝐴 + 1)))
169	166, 168	oveq12d 7411	. . . . . . . . . . . . . 14 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑(𝐴 + 1))))
170	169	fveq2d 6882	. . . . . . . . . . . . 13 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))))
171	170, 168	oveq12d 7411	. . . . . . . . . . . 12 ⊢ ((𝑚 = (𝐴 + 1) ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
172		ovex 7426	. . . . . . . . . . . 12 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))) ∈ V
173	171, 32, 172	ovmpoa 7546	. . . . . . . . . . 11 ⊢ (((𝐴 + 1) ∈ ℕ ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
174	110, 75, 173	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 1)𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑(𝐴 + 1)))) / (2↑(𝐴 + 1))))
175	164, 35, 174	3brtr4d 5173	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴𝐽𝑥) ≤ ((𝐴 + 1)𝐽𝑥))
176	98, 95, 114, 116, 175	letrd 11353	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥))
177	110	nnred 12209	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
178		min2 13151	. . . . . . . . . 10 ⊢ (((𝐴𝐽𝑥) ∈ ℝ ∧ 𝐴 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ 𝐴)
179	95, 97, 178	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ 𝐴)
180	97	lep1d 12127	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝐴 ≤ (𝐴 + 1))
181	98, 97, 177, 179, 180	letrd 11353	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴 + 1))
182		breq2 5145	. . . . . . . . 9 ⊢ (((𝐴 + 1)𝐽𝑥) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥) ↔ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
183		breq2 5145	. . . . . . . . 9 ⊢ ((𝐴 + 1) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴 + 1) ↔ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
184	182, 183	ifboth 4561	. . . . . . . 8 ⊢ ((if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ ((𝐴 + 1)𝐽𝑥) ∧ if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ (𝐴 + 1)) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
185	176, 181, 184	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
186	185	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴) ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
187		iftrue 4528	. . . . . . 7 ⊢ (𝑥 ∈ (-𝐴[,]𝐴) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))
188	187	adantl 482	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴))
189	177	renegcld 11623	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → -(𝐴 + 1) ∈ ℝ)
190	97, 177	lenegd 11775	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐴 ≤ (𝐴 + 1) ↔ -(𝐴 + 1) ≤ -𝐴))
191	180, 190	mpbid 231	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → -(𝐴 + 1) ≤ -𝐴)
192		iccss 13374	. . . . . . . . 9 ⊢ (((-(𝐴 + 1) ∈ ℝ ∧ (𝐴 + 1) ∈ ℝ) ∧ (-(𝐴 + 1) ≤ -𝐴 ∧ 𝐴 ≤ (𝐴 + 1))) → (-𝐴[,]𝐴) ⊆ (-(𝐴 + 1)[,](𝐴 + 1)))
193	189, 177, 191, 180, 192	syl22anc 837	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (-𝐴[,]𝐴) ⊆ (-(𝐴 + 1)[,](𝐴 + 1)))
194	193	sselda 3978	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → 𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)))
195	194	iftrued 4530	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
196	186, 188, 195	3brtr4d 5173	. . . . 5 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
197		iffalse 4531	. . . . . . 7 ⊢ (¬ 𝑥 ∈ (-𝐴[,]𝐴) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = 0)
198	197	adantl 482	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (-𝐴[,]𝐴)) → if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) = 0)
199	113	simprd 496	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐴 + 1)𝐽𝑥))
200	146	nn0ge0d 12517	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐴 + 1))
201		breq2 5145	. . . . . . . . . 10 ⊢ (((𝐴 + 1)𝐽𝑥) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (0 ≤ ((𝐴 + 1)𝐽𝑥) ↔ 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
202		breq2 5145	. . . . . . . . . 10 ⊢ ((𝐴 + 1) = if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) → (0 ≤ (𝐴 + 1) ↔ 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1))))
203	201, 202	ifboth 4561	. . . . . . . . 9 ⊢ ((0 ≤ ((𝐴 + 1)𝐽𝑥) ∧ 0 ≤ (𝐴 + 1)) → 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
204	199, 200, 203	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)))
205		breq2 5145	. . . . . . . . 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 5145	. . . . . . . . 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 4561	. . . . . . . 8 ⊢ ((0 ≤ if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ∧ 0 ≤ 0) → 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
208	204, 43, 207	sylancl 586	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
209	208	adantr 481	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) ∧ ¬ 𝑥 ∈ (-𝐴[,]𝐴)) → 0 ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
210	198, 209	eqbrtrd 5163	. . . . 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 3145	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
213		ffvelcdm 7068	. . . . . 6 ⊢ ((𝐺:ℕ⟶dom ∫₁ ∧ (𝐴 + 1) ∈ ℕ) → (𝐺‘(𝐴 + 1)) ∈ dom ∫₁)
214	58, 109, 213	syl2an 596	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘(𝐴 + 1)) ∈ dom ∫₁)
215		i1ff 25122	. . . . 5 ⊢ ((𝐺‘(𝐴 + 1)) ∈ dom ∫₁ → (𝐺‘(𝐴 + 1)):ℝ⟶ℝ)
216		ffn 6704	. . . . 5 ⊢ ((𝐺‘(𝐴 + 1)):ℝ⟶ℝ → (𝐺‘(𝐴 + 1)) Fn ℝ)
217	214, 215, 216	3syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘(𝐴 + 1)) Fn ℝ)
218		inidm 4214	. . . 4 ⊢ (ℝ ∩ ℝ) = ℝ
219	56, 1, 32, 57	mbfi1fseqlem2 25163	. . . . . . 7 ⊢ ((𝐴 + 1) ∈ ℕ → (𝐺‘(𝐴 + 1)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)))
220	219	fveq1d 6880	. . . . . 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 4568	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ∈ ℝ)
223		ifcl 4567	. . . . . . 7 ⊢ ((if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) ∈ ℝ)
224	222, 49, 223	sylancl 586	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0) ∈ ℝ)
225		eqid 2731	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
226	225	fvmpt2 6995	. . . . . 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 584	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))‘𝑥) = if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
228	221, 227	eqtrd 2771	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘(𝐴 + 1))‘𝑥) = if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0))
229	62, 217, 66, 66, 218, 104, 228	ofrfval 7663	. . 3 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → ((𝐺‘𝐴) ∘_r ≤ (𝐺‘(𝐴 + 1)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0) ≤ if(𝑥 ∈ (-(𝐴 + 1)[,](𝐴 + 1)), if(((𝐴 + 1)𝐽𝑥) ≤ (𝐴 + 1), ((𝐴 + 1)𝐽𝑥), (𝐴 + 1)), 0)))
230	212, 229	mpbird 256	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴) ∘_r ≤ (𝐺‘(𝐴 + 1)))
231	106, 230	jca 512	1 ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (0_𝑝 ∘_r ≤ (𝐺‘𝐴) ∧ (𝐺‘𝐴) ∘_r ≤ (𝐺‘(𝐴 + 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3060 Vcvv 3473 ∩ cin 3943 ⊆ wss 3944 ifcif 4522 {csn 4622 class class class wbr 5141 ↦ cmpt 5224 × cxp 5667 dom cdm 5669 Fn wfn 6527 ⟶wf 6528 ‘cfv 6532 (class class class)co 7393 ∈ cmpo 7395 ∘_r cofr 7652 ℂcc 11090 ℝcr 11091 0cc0 11092 1c1 11093 + caddc 11095 · cmul 11097 +∞cpnf 11227 < clt 11230 ≤ cle 11231 -cneg 11427 / cdiv 11853 ℕcn 12194 2c2 12249 ℕ₀cn0 12454 ℤcz 12540 [,)cico 13308 [,]cicc 13309 ⌊cfl 13737 ↑cexp 14009 MblFncmbf 25060 ∫₁citg1 25061 0_𝑝c0p 25115

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7708 ax-inf2 9618 ax-cnex 11148 ax-resscn 11149 ax-1cn 11150 ax-icn 11151 ax-addcl 11152 ax-addrcl 11153 ax-mulcl 11154 ax-mulrcl 11155 ax-mulcom 11156 ax-addass 11157 ax-mulass 11158 ax-distr 11159 ax-i2m1 11160 ax-1ne0 11161 ax-1rid 11162 ax-rnegex 11163 ax-rrecex 11164 ax-cnre 11165 ax-pre-lttri 11166 ax-pre-lttrn 11167 ax-pre-ltadd 11168 ax-pre-mulgt0 11169 ax-pre-sup 11170

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4523 df-pw 4598 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-int 4944 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-se 5625 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6289 df-ord 6356 df-on 6357 df-lim 6358 df-suc 6359 df-iota 6484 df-fun 6534 df-fn 6535 df-f 6536 df-f1 6537 df-fo 6538 df-f1o 6539 df-fv 6540 df-isom 6541 df-riota 7349 df-ov 7396 df-oprab 7397 df-mpo 7398 df-of 7653 df-ofr 7654 df-om 7839 df-1st 7957 df-2nd 7958 df-frecs 8248 df-wrecs 8279 df-recs 8353 df-rdg 8392 df-1o 8448 df-2o 8449 df-er 8686 df-map 8805 df-pm 8806 df-en 8923 df-dom 8924 df-sdom 8925 df-fin 8926 df-fi 9388 df-sup 9419 df-inf 9420 df-oi 9487 df-dju 9878 df-card 9916 df-pnf 11232 df-mnf 11233 df-xr 11234 df-ltxr 11235 df-le 11236 df-sub 11428 df-neg 11429 df-div 11854 df-nn 12195 df-2 12257 df-3 12258 df-n0 12455 df-z 12541 df-uz 12805 df-q 12915 df-rp 12957 df-xneg 13074 df-xadd 13075 df-xmul 13076 df-ioo 13310 df-ico 13312 df-icc 13313 df-fz 13467 df-fzo 13610 df-fl 13739 df-seq 13949 df-exp 14010 df-hash 14273 df-cj 15028 df-re 15029 df-im 15030 df-sqrt 15164 df-abs 15165 df-clim 15414 df-rlim 15415 df-sum 15615 df-rest 17350 df-topgen 17371 df-psmet 20870 df-xmet 20871 df-met 20872 df-bl 20873 df-mopn 20874 df-top 22325 df-topon 22342 df-bases 22378 df-cmp 22820 df-ovol 24910 df-vol 24911 df-mbf 25065 df-itg1 25066 df-0p 25116

This theorem is referenced by: mbfi1fseqlem6 25167

W3C validator