Metamath Proof Explorer

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 sseldi ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
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 ) ) ) )