Theorem mbfi1fseqlem5

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

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

Proof

Step	Hyp	Ref	Expression
1		mbfi1fseq.1	⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2		mbfi1fseq.2	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
3		mbfi1fseq.3	⊢ 𝐽 = ( 𝑚 ∈ ℕ , 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) )
4		mbfi1fseq.4	⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 𝐽 𝑥 ) ≤ 𝑚 , ( 𝑚 𝐽 𝑥 ) , 𝑚 ) , 0 ) ) )
5	2	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
6	5	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
7		elrege0	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
8	6 7	sylib	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
9	8	simpld	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
10		2nn	⊢ 2 ∈ ℕ
11		nnnn0	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ0 )
12		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝐴 ∈ ℕ0 ) → ( 2 ↑ 𝐴 ) ∈ ℕ )
13	10 11 12	sylancr	⊢ ( 𝐴 ∈ ℕ → ( 2 ↑ 𝐴 ) ∈ ℕ )
14	13	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝐴 ) ∈ ℕ )
15	14	nnred	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝐴 ) ∈ ℝ )
16	9 15	remulcld	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ℝ )
17	14	nnnn0d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝐴 ) ∈ ℕ0 )
18	17	nn0ge0d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( 2 ↑ 𝐴 ) )
19		mulge0	⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ ( ( 2 ↑ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ 𝐴 ) ) ) → 0 ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) )
20	8 15 18 19	syl12anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) )
21		flge0nn0	⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ℕ0 )
22	16 20 21	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ℕ0 )
23	22	nn0red	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ℝ )
24	22	nn0ge0d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) )
25	14	nngt0d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 < ( 2 ↑ 𝐴 ) )
26		divge0	⊢ ( ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ) ∧ ( ( 2 ↑ 𝐴 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝐴 ) ) ) → 0 ≤ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) )
27	23 24 15 25 26	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) )
28		simpr	⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 )
29	28	fveq2d	⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
30		simpl	⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → 𝑚 = 𝐴 )
31	30	oveq2d	⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝐴 ) )
32	29 31	oveq12d	⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) )
33	32	fveq2d	⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) = ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) )
34	33 31	oveq12d	⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) )
35		ovex	⊢ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) ∈ V
36	34 3 35	ovmpoa	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 𝐴 𝐽 𝑥 ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) )
37	36	adantll	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 𝐽 𝑥 ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) )
38	27 37	breqtrrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( 𝐴 𝐽 𝑥 ) )
39	11	nn0ge0d	⊢ ( 𝐴 ∈ ℕ → 0 ≤ 𝐴 )
40	39	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ 𝐴 )
41		breq2	⊢ ( ( 𝐴 𝐽 𝑥 ) = if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) → ( 0 ≤ ( 𝐴 𝐽 𝑥 ) ↔ 0 ≤ if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ) )
42		breq2	⊢ ( 𝐴 = if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) → ( 0 ≤ 𝐴 ↔ 0 ≤ if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ) )
43	41 42	ifboth	⊢ ( ( 0 ≤ ( 𝐴 𝐽 𝑥 ) ∧ 0 ≤ 𝐴 ) → 0 ≤ if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) )
44	38 40 43	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) )
45		0le0	⊢ 0 ≤ 0
46		breq2	⊢ ( if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) = if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) → ( 0 ≤ if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ↔ 0 ≤ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) )
47		breq2	⊢ ( 0 = if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) )
48	46 47	ifboth	⊢ ( ( 0 ≤ if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ∧ 0 ≤ 0 ) → 0 ≤ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) )
49	44 45 48	sylancl	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) )
50	49	ralrimiva	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ∀ 𝑥 ∈ ℝ 0 ≤ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) )
51		0re	⊢ 0 ∈ ℝ
52		fnconstg	⊢ ( 0 ∈ ℝ → ( ℂ × { 0 } ) Fn ℂ )
53	51 52	ax-mp	⊢ ( ℂ × { 0 } ) Fn ℂ
54		df-0p	⊢ 0𝑝 = ( ℂ × { 0 } )
55	54	fneq1i	⊢ ( 0𝑝 Fn ℂ ↔ ( ℂ × { 0 } ) Fn ℂ )
56	53 55	mpbir	⊢ 0𝑝 Fn ℂ
57	56	a1i	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → 0𝑝 Fn ℂ )
58	1 2 3 4	mbfi1fseqlem4	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ dom ∫1 )
59	58	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 𝐺 ‘ 𝐴 ) ∈ dom ∫1 )
60		i1ff	⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ dom ∫1 → ( 𝐺 ‘ 𝐴 ) : ℝ ⟶ ℝ )
61		ffn	⊢ ( ( 𝐺 ‘ 𝐴 ) : ℝ ⟶ ℝ → ( 𝐺 ‘ 𝐴 ) Fn ℝ )
62	59 60 61	3syl	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 𝐺 ‘ 𝐴 ) Fn ℝ )
63		cnex	⊢ ℂ ∈ V
64	63	a1i	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ℂ ∈ V )
65		reex	⊢ ℝ ∈ V
66	65	a1i	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ℝ ∈ V )
67		ax-resscn	⊢ ℝ ⊆ ℂ
68		sseqin2	⊢ ( ℝ ⊆ ℂ ↔ ( ℂ ∩ ℝ ) = ℝ )
69	67 68	mpbi	⊢ ( ℂ ∩ ℝ ) = ℝ
70		0pval	⊢ ( 𝑥 ∈ ℂ → ( 0𝑝 ‘ 𝑥 ) = 0 )
71	70	adantl	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℂ ) → ( 0𝑝 ‘ 𝑥 ) = 0 )
72	1 2 3 4	mbfi1fseqlem2	⊢ ( 𝐴 ∈ ℕ → ( 𝐺 ‘ 𝐴 ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) )
73	72	fveq1d	⊢ ( 𝐴 ∈ ℕ → ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) ‘ 𝑥 ) )
74	73	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) ‘ 𝑥 ) )
75		simpr	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
76		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
77		simpr	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
78		ffvelrn	⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
79	2 77 78	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
80	76 79	sselid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
81		nnnn0	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ0 )
82		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑚 ∈ ℕ0 ) → ( 2 ↑ 𝑚 ) ∈ ℕ )
83	10 81 82	sylancr	⊢ ( 𝑚 ∈ ℕ → ( 2 ↑ 𝑚 ) ∈ ℕ )
84	83	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 2 ↑ 𝑚 ) ∈ ℕ )
85	84	nnred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 2 ↑ 𝑚 ) ∈ ℝ )
86	80 85	remulcld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ∈ ℝ )
87		reflcl	⊢ ( ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) ∈ ℝ )
88	86 87	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) ∈ ℝ )
89	88 84	nndivred	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ℝ )
90	89	ralrimivva	⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ∀ 𝑦 ∈ ℝ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ℝ )
91	3	fmpo	⊢ ( ∀ 𝑚 ∈ ℕ ∀ 𝑦 ∈ ℝ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ℝ ↔ 𝐽 : ( ℕ × ℝ ) ⟶ ℝ )
92	90 91	sylib	⊢ ( 𝜑 → 𝐽 : ( ℕ × ℝ ) ⟶ ℝ )
93		fovrn	⊢ ( ( 𝐽 : ( ℕ × ℝ ) ⟶ ℝ ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 𝐴 𝐽 𝑥 ) ∈ ℝ )
94	92 93	syl3an1	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 𝐴 𝐽 𝑥 ) ∈ ℝ )
95	94	3expa	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 𝐽 𝑥 ) ∈ ℝ )
96		nnre	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
97	96	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ )
98	95 97	ifcld	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ∈ ℝ )
99		ifcl	⊢ ( ( if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ∈ ℝ )
100	98 51 99	sylancl	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ∈ ℝ )
101		eqid	⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) )
102	101	fvmpt2	⊢ ( ( 𝑥 ∈ ℝ ∧ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ∈ ℝ ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) )
103	75 100 102	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) )
104	74 103	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝐴 ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) )
105	57 62 64 66 69 71 104	ofrfval	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 0𝑝 ∘r ≤ ( 𝐺 ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ ℝ 0 ≤ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) )
106	50 105	mpbird	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → 0𝑝 ∘r ≤ ( 𝐺 ‘ 𝐴 ) )
107	1 2 3	mbfi1fseqlem1	⊢ ( 𝜑 → 𝐽 : ( ℕ × ℝ ) ⟶ ( 0 [,) +∞ ) )
108	107	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝐽 : ( ℕ × ℝ ) ⟶ ( 0 [,) +∞ ) )
109		peano2nn	⊢ ( 𝐴 ∈ ℕ → ( 𝐴 + 1 ) ∈ ℕ )
110	109	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 + 1 ) ∈ ℕ )
111	108 110 75	fovrnd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ∈ ( 0 [,) +∞ ) )
112		elrege0	⊢ ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ) )
113	111 112	sylib	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ) )
114	113	simpld	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ∈ ℝ )
115		min1	⊢ ( ( ( 𝐴 𝐽 𝑥 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ ( 𝐴 𝐽 𝑥 ) )
116	95 97 115	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ ( 𝐴 𝐽 𝑥 ) )
117		2cn	⊢ 2 ∈ ℂ
118	11	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℕ0 )
119		expp1	⊢ ( ( 2 ∈ ℂ ∧ 𝐴 ∈ ℕ0 ) → ( 2 ↑ ( 𝐴 + 1 ) ) = ( ( 2 ↑ 𝐴 ) · 2 ) )
120	117 118 119	sylancr	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ ( 𝐴 + 1 ) ) = ( ( 2 ↑ 𝐴 ) · 2 ) )
121	120	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) = ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) · ( ( 2 ↑ 𝐴 ) · 2 ) ) )
122	37 95	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) ∈ ℝ )
123	122	recnd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) ∈ ℂ )
124	15	recnd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝐴 ) ∈ ℂ )
125		2cnd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 2 ∈ ℂ )
126	123 124 125	mulassd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) · ( 2 ↑ 𝐴 ) ) · 2 ) = ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) · ( ( 2 ↑ 𝐴 ) · 2 ) ) )
127	23	recnd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ℂ )
128	14	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝐴 ) ≠ 0 )
129	127 124 128	divcan1d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) · ( 2 ↑ 𝐴 ) ) = ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) )
130	129	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) · ( 2 ↑ 𝐴 ) ) · 2 ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) )
131	121 126 130	3eqtr2d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) )
132		flle	⊢ ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) )
133	16 132	syl	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) )
134		2re	⊢ 2 ∈ ℝ
135		2pos	⊢ 0 < 2
136	134 135	pm3.2i	⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
137	136	a1i	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
138		lemul1	⊢ ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ↔ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) ≤ ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) · 2 ) ) )
139	23 16 137 138	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ↔ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) ≤ ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) · 2 ) ) )
140	133 139	mpbid	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) ≤ ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) · 2 ) )
141	120	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( ( 2 ↑ 𝐴 ) · 2 ) ) )
142	9	recnd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
143	142 124 125	mulassd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) · 2 ) = ( ( 𝐹 ‘ 𝑥 ) · ( ( 2 ↑ 𝐴 ) · 2 ) ) )
144	141 143	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) = ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) · 2 ) )
145	140 144	breqtrrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) )
146	110	nnnn0d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 + 1 ) ∈ ℕ0 )
147		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ ( 𝐴 + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℕ )
148	10 146 147	sylancr	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℕ )
149	148	nnred	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ ( 𝐴 + 1 ) ) ∈ ℝ )
150	9 149	remulcld	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ∈ ℝ )
151	16	flcld	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ℤ )
152		2z	⊢ 2 ∈ ℤ
153		zmulcl	⊢ ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ℤ ∧ 2 ∈ ℤ ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) ∈ ℤ )
154	151 152 153	sylancl	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) ∈ ℤ )
155		flge	⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ∈ ℝ ∧ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) ∈ ℤ ) → ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ↔ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) ) )
156	150 154 155	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ↔ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) ) )
157	145 156	mpbid	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) · 2 ) ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) )
158	131 157	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) )
159		reflcl	⊢ ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) ∈ ℝ )
160	150 159	syl	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) ∈ ℝ )
161	148	nngt0d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 < ( 2 ↑ ( 𝐴 + 1 ) ) )
162		lemuldiv	⊢ ( ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 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	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) ↔ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) ≤ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) / ( 2 ↑ ( 𝐴 + 1 ) ) ) ) )
164	158 163	mpbid	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) ≤ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) / ( 2 ↑ ( 𝐴 + 1 ) ) ) )
165		simpr	⊢ ( ( 𝑚 = ( 𝐴 + 1 ) ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 )
166	165	fveq2d	⊢ ( ( 𝑚 = ( 𝐴 + 1 ) ∧ 𝑦 = 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
167		simpl	⊢ ( ( 𝑚 = ( 𝐴 + 1 ) ∧ 𝑦 = 𝑥 ) → 𝑚 = ( 𝐴 + 1 ) )
168	167	oveq2d	⊢ ( ( 𝑚 = ( 𝐴 + 1 ) ∧ 𝑦 = 𝑥 ) → ( 2 ↑ 𝑚 ) = ( 2 ↑ ( 𝐴 + 1 ) ) )
169	166 168	oveq12d	⊢ ( ( 𝑚 = ( 𝐴 + 1 ) ∧ 𝑦 = 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) )
170	169	fveq2d	⊢ ( ( 𝑚 = ( 𝐴 + 1 ) ∧ 𝑦 = 𝑥 ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) = ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) )
171	170 168	oveq12d	⊢ ( ( 𝑚 = ( 𝐴 + 1 ) ∧ 𝑦 = 𝑥 ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) / ( 2 ↑ ( 𝐴 + 1 ) ) ) )
172		ovex	⊢ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) / ( 2 ↑ ( 𝐴 + 1 ) ) ) ∈ V
173	171 3 172	ovmpoa	⊢ ( ( ( 𝐴 + 1 ) ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 + 1 ) 𝐽 𝑥 ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) / ( 2 ↑ ( 𝐴 + 1 ) ) ) )
174	110 75 173	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 + 1 ) 𝐽 𝑥 ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ ( 𝐴 + 1 ) ) ) ) / ( 2 ↑ ( 𝐴 + 1 ) ) ) )
175	164 37 174	3brtr4d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 𝐽 𝑥 ) ≤ ( ( 𝐴 + 1 ) 𝐽 𝑥 ) )
176	98 95 114 116 175	letrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ ( ( 𝐴 + 1 ) 𝐽 𝑥 ) )
177	110	nnred	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 + 1 ) ∈ ℝ )
178		min2	⊢ ( ( ( 𝐴 𝐽 𝑥 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ 𝐴 )
179	95 97 178	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ 𝐴 )
180	97	lep1d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ≤ ( 𝐴 + 1 ) )
181	98 97 177 179 180	letrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ ( 𝐴 + 1 ) )
182		breq2	⊢ ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) = if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) → ( if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ↔ if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) ) )
183		breq2	⊢ ( ( 𝐴 + 1 ) = if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) → ( if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ ( 𝐴 + 1 ) ↔ if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) ) )
184	182 183	ifboth	⊢ ( ( if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ∧ if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ ( 𝐴 + 1 ) ) → if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) )
185	176 181 184	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) )
186	185	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) ) → if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ≤ if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) )
187		iftrue	⊢ ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) → if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) = if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) )
188	187	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) ) → if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) = if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) )
189	177	renegcld	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → - ( 𝐴 + 1 ) ∈ ℝ )
190	97 177	lenegd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 ≤ ( 𝐴 + 1 ) ↔ - ( 𝐴 + 1 ) ≤ - 𝐴 ) )
191	180 190	mpbid	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → - ( 𝐴 + 1 ) ≤ - 𝐴 )
192		iccss	⊢ ( ( ( - ( 𝐴 + 1 ) ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℝ ) ∧ ( - ( 𝐴 + 1 ) ≤ - 𝐴 ∧ 𝐴 ≤ ( 𝐴 + 1 ) ) ) → ( - 𝐴 [,] 𝐴 ) ⊆ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) )
193	189 177 191 180 192	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( - 𝐴 [,] 𝐴 ) ⊆ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) )
194	193	sselda	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) ) → 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) )
195	194	iftrued	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) ) → if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) = if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) )
196	186 188 195	3brtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) ) → if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ≤ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) )
197		iffalse	⊢ ( ¬ 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) → if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) = 0 )
198	197	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) ) → if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) = 0 )
199	113	simprd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ( 𝐴 + 1 ) 𝐽 𝑥 ) )
200	146	nn0ge0d	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( 𝐴 + 1 ) )
201		breq2	⊢ ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) = if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) → ( 0 ≤ ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ↔ 0 ≤ if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) ) )
202		breq2	⊢ ( ( 𝐴 + 1 ) = if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) → ( 0 ≤ ( 𝐴 + 1 ) ↔ 0 ≤ if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) ) )
203	201 202	ifboth	⊢ ( ( 0 ≤ ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ∧ 0 ≤ ( 𝐴 + 1 ) ) → 0 ≤ if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) )
204	199 200 203	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) )
205		breq2	⊢ ( 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	⊢ ( 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	⊢ ( ( 0 ≤ if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) ∧ 0 ≤ 0 ) → 0 ≤ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) )
208	204 45 207	sylancl	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) )
209	208	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) ) → 0 ≤ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) )
210	198 209	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) ) → if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ≤ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) )
211	196 210	pm2.61dan	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ≤ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) )
212	211	ralrimiva	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ≤ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) )
213		ffvelrn	⊢ ( ( 𝐺 : ℕ ⟶ dom ∫1 ∧ ( 𝐴 + 1 ) ∈ ℕ ) → ( 𝐺 ‘ ( 𝐴 + 1 ) ) ∈ dom ∫1 )
214	58 109 213	syl2an	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 𝐺 ‘ ( 𝐴 + 1 ) ) ∈ dom ∫1 )
215		i1ff	⊢ ( ( 𝐺 ‘ ( 𝐴 + 1 ) ) ∈ dom ∫1 → ( 𝐺 ‘ ( 𝐴 + 1 ) ) : ℝ ⟶ ℝ )
216		ffn	⊢ ( ( 𝐺 ‘ ( 𝐴 + 1 ) ) : ℝ ⟶ ℝ → ( 𝐺 ‘ ( 𝐴 + 1 ) ) Fn ℝ )
217	214 215 216	3syl	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 𝐺 ‘ ( 𝐴 + 1 ) ) Fn ℝ )
218		inidm	⊢ ( ℝ ∩ ℝ ) = ℝ
219	1 2 3 4	mbfi1fseqlem2	⊢ ( ( 𝐴 + 1 ) ∈ ℕ → ( 𝐺 ‘ ( 𝐴 + 1 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) ) )
220	219	fveq1d	⊢ ( ( 𝐴 + 1 ) ∈ ℕ → ( ( 𝐺 ‘ ( 𝐴 + 1 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) ) ‘ 𝑥 ) )
221	110 220	syl	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ ( 𝐴 + 1 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) ) ‘ 𝑥 ) )
222	114 177	ifcld	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) ∈ ℝ )
223		ifcl	⊢ ( ( if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) ∈ ℝ )
224	222 51 223	sylancl	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) ∈ ℝ )
225		eqid	⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) )
226	225	fvmpt2	⊢ ( ( 𝑥 ∈ ℝ ∧ 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	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) )
228	221 227	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ ( 𝐴 + 1 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) )
229	62 217 66 66 218 104 228	ofrfval	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( ( 𝐺 ‘ 𝐴 ) ∘r ≤ ( 𝐺 ‘ ( 𝐴 + 1 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ≤ if ( 𝑥 ∈ ( - ( 𝐴 + 1 ) [,] ( 𝐴 + 1 ) ) , if ( ( ( 𝐴 + 1 ) 𝐽 𝑥 ) ≤ ( 𝐴 + 1 ) , ( ( 𝐴 + 1 ) 𝐽 𝑥 ) , ( 𝐴 + 1 ) ) , 0 ) ) )
230	212 229	mpbird	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 𝐺 ‘ 𝐴 ) ∘r ≤ ( 𝐺 ‘ ( 𝐴 + 1 ) ) )
231	106 230	jca	⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 0𝑝 ∘r ≤ ( 𝐺 ‘ 𝐴 ) ∧ ( 𝐺 ‘ 𝐴 ) ∘r ≤ ( 𝐺 ‘ ( 𝐴 + 1 ) ) ) )