Metamath Proof Explorer

Theorem mbfi1fseqlem4

Description: Lemma for mbfi1fseq . This lemma is not as interesting as it is long - it is simply checking that G is in fact a sequence of simple functions, by verifying that its range is in ( 0 ... n 2 ^ n ) / ( 2 ^ n ) (which is to say, the numbers from 0 to n in increments of 1 / ( 2 ^ n ) ), and also that the preimage of each point k is measurable, because it is equal to ( -u n , n ) i^i (`' F " ( k [,) k + 1 / ( 2 ^ n ) ) ) for k < n and ( -u n , n ) i^i ( ``' F " ( k [,) +oo ) ) for k = n ` . (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 mbfi1fseqlem4 ( 𝜑 → 𝐺 : ℕ ⟶ dom ∫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 reex ⊢ ℝ ∈ V
6 5 mptex ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 𝐽 𝑥 ) ≤ 𝑚 , ( 𝑚 𝐽 𝑥 ) , 𝑚 ) , 0 ) ) ∈ V
7 6 4 fnmpti ⊢ 𝐺 Fn ℕ
8 7 a1i ⊢ ( 𝜑 → 𝐺 Fn ℕ )
9 1 2 3 4 mbfi1fseqlem3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) : ℝ ⟶ ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) )
10 elfznn0 ⊢ ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) → 𝑚 ∈ ℕ0 )
11 10 nn0red ⊢ ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) → 𝑚 ∈ ℝ )
12 2nn ⊢ 2 ∈ ℕ
13 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
14 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
15 12 13 14 sylancr ⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℕ )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
17 nndivre ⊢ ( ( 𝑚 ∈ ℝ ∧ ( 2 ↑ 𝑛 ) ∈ ℕ ) → ( 𝑚 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
18 11 16 17 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑚 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
19 18 fmpttd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) : ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ⟶ ℝ )
20 19 frnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) ⊆ ℝ )
21 9 20 fssd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) : ℝ ⟶ ℝ )
22 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ∈ Fin )
23 19 ffnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) Fn ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) )
24 dffn4 ⊢ ( ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) Fn ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↔ ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) : ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) –onto→ ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) )
25 23 24 sylib ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) : ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) –onto→ ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) )
26 fofi ⊢ ( ( ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ∈ Fin ∧ ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) : ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) –onto→ ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) ) → ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) ∈ Fin )
27 22 25 26 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) ∈ Fin )
28 9 frnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ran ( 𝐺 ‘ 𝑛 ) ⊆ ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) )
29 27 28 ssfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ran ( 𝐺 ‘ 𝑛 ) ∈ Fin )
30 1 2 3 4 mbfi1fseqlem2 ⊢ ( 𝑛 ∈ ℕ → ( 𝐺 ‘ 𝑛 ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ) )
31 30 fveq1d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ) ‘ 𝑥 ) )
32 31 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ) ‘ 𝑥 ) )
33 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
34 ovex ⊢ ( 𝑛 𝐽 𝑥 ) ∈ V
35 vex ⊢ 𝑛 ∈ V
36 34 35 ifex ⊢ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ∈ V
37 c0ex ⊢ 0 ∈ V
38 36 37 ifex ⊢ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ∈ V
39 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) )
40 39 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ∈ V ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) )
41 33 38 40 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) )
42 32 41 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) )
43 42 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) )
44 43 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = 𝑘 ↔ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) = 𝑘 ) )
45 eldifsni ⊢ ( 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) → 𝑘 ≠ 0 )
46 45 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → 𝑘 ≠ 0 )
47 neeq1 ⊢ ( if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) = 𝑘 → ( if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ≠ 0 ↔ 𝑘 ≠ 0 ) )
48 46 47 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) = 𝑘 → if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ≠ 0 ) )
49 iffalse ⊢ ( ¬ 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) → if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) = 0 )
50 49 necon1ai ⊢ ( if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ≠ 0 → 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) )
51 48 50 syl6 ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) = 𝑘 → 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ) )
52 51 pm4.71rd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) = 𝑘 ↔ ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ∧ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) = 𝑘 ) ) )
53 iftrue ⊢ ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) → if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) = if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) )
54 53 eqeq1d ⊢ ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) → ( if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) = 𝑘 ↔ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ) )
55 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → 𝑛 ∈ ℕ )
56 55 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → 𝑛 ∈ ℝ )
57 56 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → 𝑛 ∈ ℝ )
58 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
59 simpr ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
60 ffvelcdm ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
61 2 59 60 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,) +∞ ) )
62 58 61 sselid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
63 nnnn0 ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ0 )
64 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑚 ∈ ℕ0 ) → ( 2 ↑ 𝑚 ) ∈ ℕ )
65 12 63 64 sylancr ⊢ ( 𝑚 ∈ ℕ → ( 2 ↑ 𝑚 ) ∈ ℕ )
66 65 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 2 ↑ 𝑚 ) ∈ ℕ )
67 66 nnred ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( 2 ↑ 𝑚 ) ∈ ℝ )
68 62 67 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ∈ ℝ )
69 reflcl ⊢ ( ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) ∈ ℝ )
70 68 69 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) ∈ ℝ )
71 70 66 nndivred ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ ) ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ℝ )
72 71 ralrimivva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ∀ 𝑦 ∈ ℝ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ℝ )
73 3 fmpo ⊢ ( ∀ 𝑚 ∈ ℕ ∀ 𝑦 ∈ ℝ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) ∈ ℝ ↔ 𝐽 : ( ℕ × ℝ ) ⟶ ℝ )
74 72 73 sylib ⊢ ( 𝜑 → 𝐽 : ( ℕ × ℝ ) ⟶ ℝ )
75 fovcdm ⊢ ( ( 𝐽 : ( ℕ × ℝ ) ⟶ ℝ ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 𝑛 𝐽 𝑥 ) ∈ ℝ )
76 74 75 syl3an1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 𝑛 𝐽 𝑥 ) ∈ ℝ )
77 76 3expa ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑛 𝐽 𝑥 ) ∈ ℝ )
78 77 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑛 𝐽 𝑥 ) ∈ ℝ )
79 78 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → ( 𝑛 𝐽 𝑥 ) ∈ ℝ )
80 lemin ⊢ ( ( 𝑛 ∈ ℝ ∧ ( 𝑛 𝐽 𝑥 ) ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( 𝑛 ≤ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ↔ ( 𝑛 ≤ ( 𝑛 𝐽 𝑥 ) ∧ 𝑛 ≤ 𝑛 ) ) )
81 57 79 57 80 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → ( 𝑛 ≤ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ↔ ( 𝑛 ≤ ( 𝑛 𝐽 𝑥 ) ∧ 𝑛 ≤ 𝑛 ) ) )
82 79 57 ifcld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ∈ ℝ )
83 82 57 letri3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑛 ↔ ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ≤ 𝑛 ∧ 𝑛 ≤ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ) ) )
84 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → 𝑘 = 𝑛 )
85 84 eqeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ↔ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑛 ) )
86 min2 ⊢ ( ( ( 𝑛 𝐽 𝑥 ) ∈ ℝ ∧ 𝑛 ∈ ℝ ) → if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ≤ 𝑛 )
87 79 57 86 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ≤ 𝑛 )
88 87 biantrurd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → ( 𝑛 ≤ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ↔ ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ≤ 𝑛 ∧ 𝑛 ≤ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ) ) )
89 83 85 88 3bitr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ↔ 𝑛 ≤ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ) )
90 57 leidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → 𝑛 ≤ 𝑛 )
91 90 biantrud ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → ( 𝑛 ≤ ( 𝑛 𝐽 𝑥 ) ↔ ( 𝑛 ≤ ( 𝑛 𝐽 𝑥 ) ∧ 𝑛 ≤ 𝑛 ) ) )
92 81 89 91 3bitr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ↔ 𝑛 ≤ ( 𝑛 𝐽 𝑥 ) ) )
93 breq1 ⊢ ( 𝑘 = 𝑛 → ( 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ↔ 𝑛 ≤ ( 𝐹 ‘ 𝑥 ) ) )
94 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
95 94 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
96 elrege0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
97 95 96 sylib ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
98 97 simpld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
99 98 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
100 55 15 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
101 100 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝑛 ) ∈ ℝ )
102 99 101 remulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ∈ ℝ )
103 reflcl ⊢ ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
104 102 103 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
105 100 nngt0d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → 0 < ( 2 ↑ 𝑛 ) )
106 lemuldiv ⊢ ( ( 𝑛 ∈ ℝ ∧ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) ∈ ℝ ∧ ( ( 2 ↑ 𝑛 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝑛 ) ) ) → ( ( 𝑛 · ( 2 ↑ 𝑛 ) ) ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) ↔ 𝑛 ≤ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ) )
107 56 104 101 105 106 syl112anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑛 · ( 2 ↑ 𝑛 ) ) ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) ↔ 𝑛 ≤ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ) )
108 lemul1 ⊢ ( ( 𝑛 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( ( 2 ↑ 𝑛 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝑛 ) ) ) → ( 𝑛 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑛 · ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) )
109 56 99 101 105 108 syl112anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑛 · ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) )
110 nnmulcl ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 2 ↑ 𝑛 ) ∈ ℕ ) → ( 𝑛 · ( 2 ↑ 𝑛 ) ) ∈ ℕ )
111 55 15 110 syl2anc2 ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑛 · ( 2 ↑ 𝑛 ) ) ∈ ℕ )
112 111 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑛 · ( 2 ↑ 𝑛 ) ) ∈ ℤ )
113 flge ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ∈ ℝ ∧ ( 𝑛 · ( 2 ↑ 𝑛 ) ) ∈ ℤ ) → ( ( 𝑛 · ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ↔ ( 𝑛 · ( 2 ↑ 𝑛 ) ) ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) ) )
114 102 112 113 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑛 · ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ↔ ( 𝑛 · ( 2 ↑ 𝑛 ) ) ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) ) )
115 109 114 bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑛 · ( 2 ↑ 𝑛 ) ) ≤ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) ) )
116 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
117 simpr ⊢ ( ( 𝑚 = 𝑛 ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 )
118 117 fveq2d ⊢ ( ( 𝑚 = 𝑛 ∧ 𝑦 = 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
119 simpl ⊢ ( ( 𝑚 = 𝑛 ∧ 𝑦 = 𝑥 ) → 𝑚 = 𝑛 )
120 119 oveq2d ⊢ ( ( 𝑚 = 𝑛 ∧ 𝑦 = 𝑥 ) → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝑛 ) )
121 118 120 oveq12d ⊢ ( ( 𝑚 = 𝑛 ∧ 𝑦 = 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) )
122 121 fveq2d ⊢ ( ( 𝑚 = 𝑛 ∧ 𝑦 = 𝑥 ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) = ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) )
123 122 120 oveq12d ⊢ ( ( 𝑚 = 𝑛 ∧ 𝑦 = 𝑥 ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) )
124 ovex ⊢ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ∈ V
125 123 3 124 ovmpoa ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 𝑛 𝐽 𝑥 ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) )
126 55 116 125 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑛 𝐽 𝑥 ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) )
127 126 breq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ≤ ( 𝑛 𝐽 𝑥 ) ↔ 𝑛 ≤ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ) )
128 107 115 127 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑛 ≤ ( 𝐹 ‘ 𝑥 ) ↔ 𝑛 ≤ ( 𝑛 𝐽 𝑥 ) ) )
129 93 128 sylan9bbr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → ( 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ↔ 𝑛 ≤ ( 𝑛 𝐽 𝑥 ) ) )
130 116 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → 𝑥 ∈ ℝ )
131 iftrue ⊢ ( 𝑘 = 𝑛 → if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) = ℝ )
132 131 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) = ℝ )
133 130 132 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → 𝑥 ∈ if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) )
134 133 biantrurd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → ( 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑥 ∈ if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
135 92 129 134 3bitr2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 = 𝑛 ) → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ↔ ( 𝑥 ∈ if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
136 28 ssdifssd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ⊆ ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) )
137 136 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → 𝑘 ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) )
138 eqid ⊢ ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) = ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) )
139 138 rnmpt ⊢ ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) = { 𝑘 ∣ ∃ 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) 𝑘 = ( 𝑚 / ( 2 ↑ 𝑛 ) ) }
140 139 eqabri ⊢ ( 𝑘 ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) 𝑘 = ( 𝑚 / ( 2 ↑ 𝑛 ) ) )
141 elfzelz ⊢ ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) → 𝑚 ∈ ℤ )
142 141 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ) → 𝑚 ∈ ℤ )
143 142 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ) → 𝑚 ∈ ℂ )
144 15 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
145 144 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ) → ( 2 ↑ 𝑛 ) ∈ ℂ )
146 144 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ) → ( 2 ↑ 𝑛 ) ≠ 0 )
147 143 145 146 divcan1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ) → ( ( 𝑚 / ( 2 ↑ 𝑛 ) ) · ( 2 ↑ 𝑛 ) ) = 𝑚 )
148 147 142 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ) → ( ( 𝑚 / ( 2 ↑ 𝑛 ) ) · ( 2 ↑ 𝑛 ) ) ∈ ℤ )
149 oveq1 ⊢ ( 𝑘 = ( 𝑚 / ( 2 ↑ 𝑛 ) ) → ( 𝑘 · ( 2 ↑ 𝑛 ) ) = ( ( 𝑚 / ( 2 ↑ 𝑛 ) ) · ( 2 ↑ 𝑛 ) ) )
150 149 eleq1d ⊢ ( 𝑘 = ( 𝑚 / ( 2 ↑ 𝑛 ) ) → ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) ∈ ℤ ↔ ( ( 𝑚 / ( 2 ↑ 𝑛 ) ) · ( 2 ↑ 𝑛 ) ) ∈ ℤ ) )
151 148 150 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑘 = ( 𝑚 / ( 2 ↑ 𝑛 ) ) → ( 𝑘 · ( 2 ↑ 𝑛 ) ) ∈ ℤ ) )
152 151 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∃ 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) 𝑘 = ( 𝑚 / ( 2 ↑ 𝑛 ) ) → ( 𝑘 · ( 2 ↑ 𝑛 ) ) ∈ ℤ ) )
153 140 152 biimtrid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑘 ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) → ( 𝑘 · ( 2 ↑ 𝑛 ) ) ∈ ℤ ) )
154 153 imp ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ran ( 𝑚 ∈ ( 0 ... ( 𝑛 · ( 2 ↑ 𝑛 ) ) ) ↦ ( 𝑚 / ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑘 · ( 2 ↑ 𝑛 ) ) ∈ ℤ )
155 137 154 syldan ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( 𝑘 · ( 2 ↑ 𝑛 ) ) ∈ ℤ )
156 155 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑘 · ( 2 ↑ 𝑛 ) ) ∈ ℤ )
157 flbi ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ∈ ℝ ∧ ( 𝑘 · ( 2 ↑ 𝑛 ) ) ∈ ℤ ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) = ( 𝑘 · ( 2 ↑ 𝑛 ) ) ↔ ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) < ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) + 1 ) ) ) )
158 102 156 157 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) = ( 𝑘 · ( 2 ↑ 𝑛 ) ) ↔ ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) < ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) + 1 ) ) ) )
159 158 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ≠ 𝑛 ) → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) = ( 𝑘 · ( 2 ↑ 𝑛 ) ) ↔ ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) < ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) + 1 ) ) ) )
160 neeq1 ⊢ ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ≠ 𝑛 ↔ 𝑘 ≠ 𝑛 ) )
161 160 biimparc ⊢ ( ( 𝑘 ≠ 𝑛 ∧ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ) → if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ≠ 𝑛 )
162 iffalse ⊢ ( ¬ ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 → if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑛 )
163 162 necon1ai ⊢ ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ≠ 𝑛 → ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 )
164 161 163 syl ⊢ ( ( 𝑘 ≠ 𝑛 ∧ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ) → ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 )
165 164 iftrued ⊢ ( ( 𝑘 ≠ 𝑛 ∧ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ) → if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = ( 𝑛 𝐽 𝑥 ) )
166 simpr ⊢ ( ( 𝑘 ≠ 𝑛 ∧ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ) → if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 )
167 165 166 eqtr3d ⊢ ( ( 𝑘 ≠ 𝑛 ∧ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ) → ( 𝑛 𝐽 𝑥 ) = 𝑘 )
168 167 164 eqbrtrrd ⊢ ( ( 𝑘 ≠ 𝑛 ∧ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ) → 𝑘 ≤ 𝑛 )
169 168 167 jca ⊢ ( ( 𝑘 ≠ 𝑛 ∧ if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ) → ( 𝑘 ≤ 𝑛 ∧ ( 𝑛 𝐽 𝑥 ) = 𝑘 ) )
170 169 ex ⊢ ( 𝑘 ≠ 𝑛 → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 → ( 𝑘 ≤ 𝑛 ∧ ( 𝑛 𝐽 𝑥 ) = 𝑘 ) ) )
171 breq1 ⊢ ( ( 𝑛 𝐽 𝑥 ) = 𝑘 → ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 ↔ 𝑘 ≤ 𝑛 ) )
172 171 biimparc ⊢ ( ( 𝑘 ≤ 𝑛 ∧ ( 𝑛 𝐽 𝑥 ) = 𝑘 ) → ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 )
173 172 iftrued ⊢ ( ( 𝑘 ≤ 𝑛 ∧ ( 𝑛 𝐽 𝑥 ) = 𝑘 ) → if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = ( 𝑛 𝐽 𝑥 ) )
174 simpr ⊢ ( ( 𝑘 ≤ 𝑛 ∧ ( 𝑛 𝐽 𝑥 ) = 𝑘 ) → ( 𝑛 𝐽 𝑥 ) = 𝑘 )
175 173 174 eqtrd ⊢ ( ( 𝑘 ≤ 𝑛 ∧ ( 𝑛 𝐽 𝑥 ) = 𝑘 ) → if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 )
176 170 175 impbid1 ⊢ ( 𝑘 ≠ 𝑛 → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ↔ ( 𝑘 ≤ 𝑛 ∧ ( 𝑛 𝐽 𝑥 ) = 𝑘 ) ) )
177 176 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ≠ 𝑛 ) → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ↔ ( 𝑘 ≤ 𝑛 ∧ ( 𝑛 𝐽 𝑥 ) = 𝑘 ) ) )
178 eldifi ⊢ ( 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) → 𝑘 ∈ ran ( 𝐺 ‘ 𝑛 ) )
179 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
180 179 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝑛 ∈ ℝ )
181 77 180 86 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ≤ 𝑛 )
182 13 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 𝑛 ∈ ℕ0 )
183 182 nn0ge0d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ 𝑛 )
184 breq1 ⊢ ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ≤ 𝑛 ↔ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ≤ 𝑛 ) )
185 breq1 ⊢ ( 0 = if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) → ( 0 ≤ 𝑛 ↔ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ≤ 𝑛 ) )
186 184 185 ifboth ⊢ ( ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ≤ 𝑛 ∧ 0 ≤ 𝑛 ) → if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ≤ 𝑛 )
187 181 183 186 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ≤ 𝑛 )
188 42 187 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑛 )
189 188 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑥 ∈ ℝ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑛 )
190 9 ffnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) Fn ℝ )
191 breq1 ⊢ ( 𝑘 = ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) → ( 𝑘 ≤ 𝑛 ↔ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑛 ) )
192 191 ralrn ⊢ ( ( 𝐺 ‘ 𝑛 ) Fn ℝ → ( ∀ 𝑘 ∈ ran ( 𝐺 ‘ 𝑛 ) 𝑘 ≤ 𝑛 ↔ ∀ 𝑥 ∈ ℝ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑛 ) )
193 190 192 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ∀ 𝑘 ∈ ran ( 𝐺 ‘ 𝑛 ) 𝑘 ≤ 𝑛 ↔ ∀ 𝑥 ∈ ℝ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) ≤ 𝑛 ) )
194 189 193 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∀ 𝑘 ∈ ran ( 𝐺 ‘ 𝑛 ) 𝑘 ≤ 𝑛 )
195 194 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ran ( 𝐺 ‘ 𝑛 ) ) → 𝑘 ≤ 𝑛 )
196 178 195 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → 𝑘 ≤ 𝑛 )
197 196 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ≠ 𝑛 ) → 𝑘 ≤ 𝑛 )
198 197 biantrurd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ≠ 𝑛 ) → ( ( 𝑛 𝐽 𝑥 ) = 𝑘 ↔ ( 𝑘 ≤ 𝑛 ∧ ( 𝑛 𝐽 𝑥 ) = 𝑘 ) ) )
199 126 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑛 𝐽 𝑥 ) = 𝑘 ↔ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) = 𝑘 ) )
200 104 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) ∈ ℂ )
201 28 20 sstrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ran ( 𝐺 ‘ 𝑛 ) ⊆ ℝ )
202 201 ssdifssd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ⊆ ℝ )
203 202 sselda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → 𝑘 ∈ ℝ )
204 203 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → 𝑘 ∈ ℝ )
205 204 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → 𝑘 ∈ ℂ )
206 100 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝑛 ) ∈ ℂ )
207 100 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 2 ↑ 𝑛 ) ≠ 0 )
208 200 205 206 207 divmul3d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) = 𝑘 ↔ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) = ( 𝑘 · ( 2 ↑ 𝑛 ) ) ) )
209 199 208 bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑛 𝐽 𝑥 ) = 𝑘 ↔ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) = ( 𝑘 · ( 2 ↑ 𝑛 ) ) ) )
210 209 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ≠ 𝑛 ) → ( ( 𝑛 𝐽 𝑥 ) = 𝑘 ↔ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) = ( 𝑘 · ( 2 ↑ 𝑛 ) ) ) )
211 177 198 210 3bitr2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ≠ 𝑛 ) → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ↔ ( ⌊ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) = ( 𝑘 · ( 2 ↑ 𝑛 ) ) ) )
212 ifnefalse ⊢ ( 𝑘 ≠ 𝑛 → if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) = ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) )
213 212 eleq2d ⊢ ( 𝑘 ≠ 𝑛 → ( 𝑥 ∈ if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) )
214 100 nnrecred ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 1 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
215 204 214 readdcld ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
216 215 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ* )
217 elioomnf ⊢ ( ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ* → ( ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) < ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) )
218 216 217 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) < ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) )
219 94 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
220 219 ffnd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → 𝐹 Fn ℝ )
221 elpreima ⊢ ( 𝐹 Fn ℝ → ( 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) )
222 220 221 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) )
223 116 222 mpbirand ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) )
224 99 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) < ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) < ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) )
225 218 223 224 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ↔ ( 𝐹 ‘ 𝑥 ) < ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) )
226 ltmul1 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ ∧ ( ( 2 ↑ 𝑛 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝑛 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) < ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) < ( ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) · ( 2 ↑ 𝑛 ) ) ) )
227 99 215 101 105 226 syl112anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) < ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) < ( ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) · ( 2 ↑ 𝑛 ) ) ) )
228 214 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 1 / ( 2 ↑ 𝑛 ) ) ∈ ℂ )
229 206 207 recid2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 1 / ( 2 ↑ 𝑛 ) ) · ( 2 ↑ 𝑛 ) ) = 1 )
230 229 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) + ( ( 1 / ( 2 ↑ 𝑛 ) ) · ( 2 ↑ 𝑛 ) ) ) = ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) + 1 ) )
231 205 206 228 230 joinlmuladdmuld ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) · ( 2 ↑ 𝑛 ) ) = ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) + 1 ) )
232 231 breq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) < ( ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) · ( 2 ↑ 𝑛 ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) < ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) + 1 ) ) )
233 225 227 232 3bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) < ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) + 1 ) ) )
234 213 233 sylan9bbr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ≠ 𝑛 ) → ( 𝑥 ∈ if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) < ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) + 1 ) ) )
235 lemul1 ⊢ ( ( 𝑘 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( ( 2 ↑ 𝑛 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝑛 ) ) ) → ( 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑘 · ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) )
236 204 99 101 105 235 syl112anc ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑘 · ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) )
237 236 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ≠ 𝑛 ) → ( 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑘 · ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) )
238 234 237 anbi12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ≠ 𝑛 ) → ( ( 𝑥 ∈ if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) < ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) + 1 ) ∧ ( 𝑘 · ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ) ) )
239 238 biancomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ≠ 𝑛 ) → ( ( 𝑥 ∈ if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) · ( 2 ↑ 𝑛 ) ) < ( ( 𝑘 · ( 2 ↑ 𝑛 ) ) + 1 ) ) ) )
240 159 211 239 3bitr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ≠ 𝑛 ) → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ↔ ( 𝑥 ∈ if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
241 135 240 pm2.61dane ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ↔ ( 𝑥 ∈ if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
242 eldif ⊢ ( 𝑥 ∈ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ↔ ( 𝑥 ∈ if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) )
243 204 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → 𝑘 ∈ ℝ* )
244 elioomnf ⊢ ( 𝑘 ∈ ℝ* → ( ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) 𝑘 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) < 𝑘 ) ) )
245 243 244 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) 𝑘 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) < 𝑘 ) ) )
246 elpreima ⊢ ( 𝐹 Fn ℝ → ( 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) 𝑘 ) ) ) )
247 220 246 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) 𝑘 ) ) ) )
248 116 247 mpbirand ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( -∞ (,) 𝑘 ) ) )
249 99 biantrurd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) < 𝑘 ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) < 𝑘 ) ) )
250 245 248 249 3bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ↔ ( 𝐹 ‘ 𝑥 ) < 𝑘 ) )
251 250 notbid ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑘 ) )
252 204 99 lenltd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑘 ) )
253 251 252 bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ↔ 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ) )
254 253 anbi2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 ∈ if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ↔ ( 𝑥 ∈ if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
255 242 254 bitrid ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ↔ ( 𝑥 ∈ if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
256 241 255 bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) = 𝑘 ↔ 𝑥 ∈ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) )
257 54 256 sylan9bbr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ) → ( if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) = 𝑘 ↔ 𝑥 ∈ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) )
258 257 pm5.32da ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ∧ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) = 𝑘 ) ↔ ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ∧ 𝑥 ∈ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) ) )
259 44 52 258 3bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = 𝑘 ↔ ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ∧ 𝑥 ∈ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) ) )
260 259 pm5.32da ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( ( 𝑥 ∈ ℝ ∧ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = 𝑘 ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ∧ 𝑥 ∈ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) ) ) )
261 21 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( 𝐺 ‘ 𝑛 ) : ℝ ⟶ ℝ )
262 261 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( 𝐺 ‘ 𝑛 ) Fn ℝ )
263 fniniseg ⊢ ( ( 𝐺 ‘ 𝑛 ) Fn ℝ → ( 𝑥 ∈ ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ↔ ( 𝑥 ∈ ℝ ∧ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = 𝑘 ) ) )
264 262 263 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( 𝑥 ∈ ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ↔ ( 𝑥 ∈ ℝ ∧ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = 𝑘 ) ) )
265 elin ⊢ ( 𝑥 ∈ ( ( - 𝑛 [,] 𝑛 ) ∩ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) ↔ ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ∧ 𝑥 ∈ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) )
266 179 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → 𝑛 ∈ ℝ )
267 266 renegcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → - 𝑛 ∈ ℝ )
268 iccmbl ⊢ ( ( - 𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( - 𝑛 [,] 𝑛 ) ∈ dom vol )
269 267 266 268 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( - 𝑛 [,] 𝑛 ) ∈ dom vol )
270 mblss ⊢ ( ( - 𝑛 [,] 𝑛 ) ∈ dom vol → ( - 𝑛 [,] 𝑛 ) ⊆ ℝ )
271 269 270 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( - 𝑛 [,] 𝑛 ) ⊆ ℝ )
272 271 sseld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) → 𝑥 ∈ ℝ ) )
273 272 adantrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ∧ 𝑥 ∈ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) → 𝑥 ∈ ℝ ) )
274 273 pm4.71rd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ∧ 𝑥 ∈ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ∧ 𝑥 ∈ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) ) ) )
275 265 274 bitrid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( 𝑥 ∈ ( ( - 𝑛 [,] 𝑛 ) ∩ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ∧ 𝑥 ∈ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) ) ) )
276 260 264 275 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( 𝑥 ∈ ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ↔ 𝑥 ∈ ( ( - 𝑛 [,] 𝑛 ) ∩ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) ) )
277 276 eqrdv ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) = ( ( - 𝑛 [,] 𝑛 ) ∩ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) )
278 rembl ⊢ ℝ ∈ dom vol
279 fss ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
280 2 58 279 sylancl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
281 mbfima ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : ℝ ⟶ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ∈ dom vol )
282 1 280 281 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ∈ dom vol )
283 ifcl ⊢ ( ( ℝ ∈ dom vol ∧ ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ∈ dom vol ) → if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∈ dom vol )
284 278 282 283 sylancr ⊢ ( 𝜑 → if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∈ dom vol )
285 mbfima ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : ℝ ⟶ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ∈ dom vol )
286 1 280 285 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ∈ dom vol )
287 difmbl ⊢ ( ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∈ dom vol ∧ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ∈ dom vol ) → ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ∈ dom vol )
288 284 286 287 syl2anc ⊢ ( 𝜑 → ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ∈ dom vol )
289 288 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ∈ dom vol )
290 inmbl ⊢ ( ( ( - 𝑛 [,] 𝑛 ) ∈ dom vol ∧ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ∈ dom vol ) → ( ( - 𝑛 [,] 𝑛 ) ∩ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) ∈ dom vol )
291 269 289 290 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( ( - 𝑛 [,] 𝑛 ) ∩ ( if ( 𝑘 = 𝑛 , ℝ , ( ◡ 𝐹 “ ( -∞ (,) ( 𝑘 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ) ) ) ∖ ( ◡ 𝐹 “ ( -∞ (,) 𝑘 ) ) ) ) ∈ dom vol )
292 277 291 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ∈ dom vol )
293 mblvol ⊢ ( ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ∈ dom vol → ( vol ‘ ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ) = ( vol* ‘ ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ) )
294 292 293 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( vol ‘ ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ) = ( vol* ‘ ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ) )
295 190 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( 𝐺 ‘ 𝑛 ) Fn ℝ )
296 295 263 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( 𝑥 ∈ ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ↔ ( 𝑥 ∈ ℝ ∧ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = 𝑘 ) ) )
297 77 180 ifcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ∈ ℝ )
298 0re ⊢ 0 ∈ ℝ
299 ifcl ⊢ ( ( if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ∈ ℝ )
300 297 298 299 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ∈ ℝ )
301 39 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ∈ ℝ ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) )
302 33 300 301 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) )
303 32 302 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) )
304 303 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) )
305 304 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = 𝑘 ↔ if ( 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) , if ( ( 𝑛 𝐽 𝑥 ) ≤ 𝑛 , ( 𝑛 𝐽 𝑥 ) , 𝑛 ) , 0 ) = 𝑘 ) )
306 305 51 sylbid ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = 𝑘 → 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ) )
307 306 expimpd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( ( 𝑥 ∈ ℝ ∧ ( ( 𝐺 ‘ 𝑛 ) ‘ 𝑥 ) = 𝑘 ) → 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ) )
308 296 307 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( 𝑥 ∈ ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) → 𝑥 ∈ ( - 𝑛 [,] 𝑛 ) ) )
309 308 ssrdv ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ⊆ ( - 𝑛 [,] 𝑛 ) )
310 iccssre ⊢ ( ( - 𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( - 𝑛 [,] 𝑛 ) ⊆ ℝ )
311 267 266 310 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( - 𝑛 [,] 𝑛 ) ⊆ ℝ )
312 mblvol ⊢ ( ( - 𝑛 [,] 𝑛 ) ∈ dom vol → ( vol ‘ ( - 𝑛 [,] 𝑛 ) ) = ( vol* ‘ ( - 𝑛 [,] 𝑛 ) ) )
313 269 312 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( vol ‘ ( - 𝑛 [,] 𝑛 ) ) = ( vol* ‘ ( - 𝑛 [,] 𝑛 ) ) )
314 iccvolcl ⊢ ( ( - 𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( vol ‘ ( - 𝑛 [,] 𝑛 ) ) ∈ ℝ )
315 267 266 314 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( vol ‘ ( - 𝑛 [,] 𝑛 ) ) ∈ ℝ )
316 313 315 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( vol* ‘ ( - 𝑛 [,] 𝑛 ) ) ∈ ℝ )
317 ovolsscl ⊢ ( ( ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ⊆ ( - 𝑛 [,] 𝑛 ) ∧ ( - 𝑛 [,] 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( - 𝑛 [,] 𝑛 ) ) ∈ ℝ ) → ( vol* ‘ ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ) ∈ ℝ )
318 309 311 316 317 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( vol* ‘ ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ) ∈ ℝ )
319 294 318 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ran ( 𝐺 ‘ 𝑛 ) ∖ { 0 } ) ) → ( vol ‘ ( ◡ ( 𝐺 ‘ 𝑛 ) “ { 𝑘 } ) ) ∈ ℝ )
320 21 29 292 319 i1fd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) ∈ dom ∫1 )
321 320 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐺 ‘ 𝑛 ) ∈ dom ∫1 )
322 ffnfv ⊢ ( 𝐺 : ℕ ⟶ dom ∫1 ↔ ( 𝐺 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝐺 ‘ 𝑛 ) ∈ dom ∫1 ) )
323 8 321 322 sylanbrc ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ dom ∫1 )