Metamath Proof Explorer

Theorem mbfi1fseqlem3

Description: Lemma for mbfi1fseq . (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 mbfi1fseqlem3 ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 𝐺 ‘ 𝐴 ) : ℝ ⟶ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )

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 1 2 3 4 mbfi1fseqlem2 ⊢ ( 𝐴 ∈ ℕ → ( 𝐺 ‘ 𝐴 ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) )
6 5 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 𝐺 ‘ 𝐴 ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) )
7 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
8 simpr ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
9 ffvelcdm ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
10 2 8 9 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
11 7 10 sselid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
12 2nn ⊢ 2 ∈ ℕ
13 nnnn0 ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ0 )
14 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑚 ∈ ℕ0 ) → ( 2 ↑ 𝑚 ) ∈ ℕ )
15 12 13 14 sylancr ⊢ ( 𝑚 ∈ ℕ → ( 2 ↑ 𝑚 ) ∈ ℕ )
16 15 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 2 ↑ 𝑚 ) ∈ ℕ )
17 16 nnred ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 2 ↑ 𝑚 ) ∈ ℝ )
18 11 17 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ∈ ℝ )
19 reflcl ⊢ ( ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) ∈ ℝ )
20 18 19 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) ∈ ℝ )
21 20 16 nndivred ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ℝ )
22 21 ralrimivva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ∀ 𝑦 ∈ ℝ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ℝ )
23 3 fmpo ⊢ ( ∀ 𝑚 ∈ ℕ ∀ 𝑦 ∈ ℝ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ℝ ↔ 𝐽 : ( ℕ × ℝ ) ⟶ ℝ )
24 22 23 sylib ⊢ ( 𝜑 → 𝐽 : ( ℕ × ℝ ) ⟶ ℝ )
25 fovcdm ⊢ ( ( 𝐽 : ( ℕ × ℝ ) ⟶ ℝ ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 𝐴 𝐽 𝑥 ) ∈ ℝ )
26 24 25 syl3an1 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 𝐴 𝐽 𝑥 ) ∈ ℝ )
27 26 3expa ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 𝐽 𝑥 ) ∈ ℝ )
28 nnre ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
29 28 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ )
30 nnnn0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ0 )
31 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝐴 ∈ ℕ0 ) → ( 2 ↑ 𝐴 ) ∈ ℕ )
32 12 30 31 sylancr ⊢ ( 𝐴 ∈ ℕ → ( 2 ↑ 𝐴 ) ∈ ℕ )
33 32 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝐴 ) ∈ ℕ )
34 nnre ⊢ ( ( 2 ↑ 𝐴 ) ∈ ℕ → ( 2 ↑ 𝐴 ) ∈ ℝ )
35 nngt0 ⊢ ( ( 2 ↑ 𝐴 ) ∈ ℕ → 0 < ( 2 ↑ 𝐴 ) )
36 34 35 jca ⊢ ( ( 2 ↑ 𝐴 ) ∈ ℕ → ( ( 2 ↑ 𝐴 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝐴 ) ) )
37 33 36 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 2 ↑ 𝐴 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝐴 ) ) )
38 lemul1 ⊢ ( ( ( 𝐴 𝐽 𝑥 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( ( 2 ↑ 𝐴 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝐴 ) ) ) → ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ↔ ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ≤ ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) )
39 27 29 37 38 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ↔ ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ≤ ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) )
40 39 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ≤ ( 𝐴 · ( 2 ↑ 𝐴 ) ) )
41 simpr ⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 )
42 41 fveq2d ⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
43 simpl ⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → 𝑚 = 𝐴 )
44 43 oveq2d ⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝐴 ) )
45 42 44 oveq12d ⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) )
46 45 fveq2d ⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) = ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) )
47 46 44 oveq12d ⊢ ( ( 𝑚 = 𝐴 ∧ 𝑦 = 𝑥 ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) )
48 ovex ⊢ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) ∈ V
49 47 3 48 ovmpoa ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 𝐴 𝐽 𝑥 ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) )
50 49 ad4ant23 ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( 𝐴 𝐽 𝑥 ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) )
51 50 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) = ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) · ( 2 ↑ 𝐴 ) ) )
52 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
53 52 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
54 elrege0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
55 53 54 sylib ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
56 55 simpld ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
57 33 nnred ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝐴 ) ∈ ℝ )
58 56 57 remulcld ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ℝ )
59 33 nnnn0d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝐴 ) ∈ ℕ0 )
60 59 nn0ge0d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( 2 ↑ 𝐴 ) )
61 mulge0 ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ ( ( 2 ↑ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ 𝐴 ) ) ) → 0 ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) )
62 55 57 60 61 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) )
63 flge0nn0 ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ℕ0 )
64 58 62 63 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ℕ0 )
65 64 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ℕ0 )
66 65 nn0cnd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ℂ )
67 33 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( 2 ↑ 𝐴 ) ∈ ℕ )
68 67 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( 2 ↑ 𝐴 ) ∈ ℂ )
69 67 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( 2 ↑ 𝐴 ) ≠ 0 )
70 66 68 69 divcan1d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) / ( 2 ↑ 𝐴 ) ) · ( 2 ↑ 𝐴 ) ) = ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) )
71 51 70 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) = ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) )
72 71 65 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ℕ0 )
73 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
74 72 73 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) )
75 nnmulcl ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 2 ↑ 𝐴 ) ∈ ℕ ) → ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ℕ )
76 32 75 mpdan ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ℕ )
77 76 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ℕ )
78 77 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ℕ )
79 78 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ℤ )
80 elfz5 ⊢ ( ( ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) ∧ ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ℤ ) → ( ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↔ ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ≤ ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) )
81 74 79 80 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↔ ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ≤ ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) )
82 40 81 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) )
83 oveq1 ⊢ ( 𝑚 = ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) → ( 𝑚 / ( 2 ↑ 𝐴 ) ) = ( ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) / ( 2 ↑ 𝐴 ) ) )
84 eqid ⊢ ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) = ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) )
85 ovex ⊢ ( ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) / ( 2 ↑ 𝐴 ) ) ∈ V
86 83 84 85 fvmpt ⊢ ( ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) = ( ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) / ( 2 ↑ 𝐴 ) ) )
87 82 86 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) = ( ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) / ( 2 ↑ 𝐴 ) ) )
88 27 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( 𝐴 𝐽 𝑥 ) ∈ ℝ )
89 88 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( 𝐴 𝐽 𝑥 ) ∈ ℂ )
90 89 68 69 divcan4d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) / ( 2 ↑ 𝐴 ) ) = ( 𝐴 𝐽 𝑥 ) )
91 87 90 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) = ( 𝐴 𝐽 𝑥 ) )
92 elfznn0 ⊢ ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) → 𝑚 ∈ ℕ0 )
93 92 nn0red ⊢ ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) → 𝑚 ∈ ℝ )
94 32 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 2 ↑ 𝐴 ) ∈ ℕ )
95 nndivre ⊢ ( ( 𝑚 ∈ ℝ ∧ ( 2 ↑ 𝐴 ) ∈ ℕ ) → ( 𝑚 / ( 2 ↑ 𝐴 ) ) ∈ ℝ )
96 93 94 95 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ) → ( 𝑚 / ( 2 ↑ 𝐴 ) ) ∈ ℝ )
97 96 fmpttd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) : ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ⟶ ℝ )
98 97 ffnd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) Fn ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) )
99 98 adantr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) Fn ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) )
100 99 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) Fn ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) )
101 fnfvelrn ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) Fn ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ∧ ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )
102 100 82 101 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ ( ( 𝐴 𝐽 𝑥 ) · ( 2 ↑ 𝐴 ) ) ) ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )
103 91 102 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → ( 𝐴 𝐽 𝑥 ) ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )
104 77 nnnn0d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ℕ0 )
105 104 73 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) )
106 eluzfz2 ⊢ ( ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) → ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) )
107 105 106 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) )
108 oveq1 ⊢ ( 𝑚 = ( 𝐴 · ( 2 ↑ 𝐴 ) ) → ( 𝑚 / ( 2 ↑ 𝐴 ) ) = ( ( 𝐴 · ( 2 ↑ 𝐴 ) ) / ( 2 ↑ 𝐴 ) ) )
109 ovex ⊢ ( ( 𝐴 · ( 2 ↑ 𝐴 ) ) / ( 2 ↑ 𝐴 ) ) ∈ V
110 108 84 109 fvmpt ⊢ ( ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) = ( ( 𝐴 · ( 2 ↑ 𝐴 ) ) / ( 2 ↑ 𝐴 ) ) )
111 107 110 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) = ( ( 𝐴 · ( 2 ↑ 𝐴 ) ) / ( 2 ↑ 𝐴 ) ) )
112 29 recnd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℂ )
113 33 nncnd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝐴 ) ∈ ℂ )
114 33 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝐴 ) ≠ 0 )
115 112 113 114 divcan4d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 · ( 2 ↑ 𝐴 ) ) / ( 2 ↑ 𝐴 ) ) = 𝐴 )
116 111 115 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) = 𝐴 )
117 fnfvelrn ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) Fn ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ∧ ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )
118 99 107 117 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )
119 116 118 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )
120 119 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) → 𝐴 ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )
121 103 120 ifclda ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )
122 eluzfz1 ⊢ ( ( 𝐴 · ( 2 ↑ 𝐴 ) ) ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) )
123 105 122 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) )
124 oveq1 ⊢ ( 𝑚 = 0 → ( 𝑚 / ( 2 ↑ 𝐴 ) ) = ( 0 / ( 2 ↑ 𝐴 ) ) )
125 ovex ⊢ ( 0 / ( 2 ↑ 𝐴 ) ) ∈ V
126 124 84 125 fvmpt ⊢ ( 0 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ 0 ) = ( 0 / ( 2 ↑ 𝐴 ) ) )
127 123 126 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ 0 ) = ( 0 / ( 2 ↑ 𝐴 ) ) )
128 nncn ⊢ ( ( 2 ↑ 𝐴 ) ∈ ℕ → ( 2 ↑ 𝐴 ) ∈ ℂ )
129 nnne0 ⊢ ( ( 2 ↑ 𝐴 ) ∈ ℕ → ( 2 ↑ 𝐴 ) ≠ 0 )
130 128 129 div0d ⊢ ( ( 2 ↑ 𝐴 ) ∈ ℕ → ( 0 / ( 2 ↑ 𝐴 ) ) = 0 )
131 33 130 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 0 / ( 2 ↑ 𝐴 ) ) = 0 )
132 127 131 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ 0 ) = 0 )
133 fnfvelrn ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) Fn ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ∧ 0 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ 0 ) ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )
134 99 123 133 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) ‘ 0 ) ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )
135 132 134 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )
136 121 135 ifcld ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )
137 6 136 fmpt3d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℕ ) → ( 𝐺 ‘ 𝐴 ) : ℝ ⟶ ran ( 𝑚 ∈ ( 0 ... ( 𝐴 · ( 2 ↑ 𝐴 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝐴 ) ) ) )