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		ffvelrn	⊢ ( ( 𝐹 : ℝ ⟶ ( 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		fovrn	⊢ ( ( 𝐽 : ( ℕ × ℝ ) ⟶ ℝ ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ ) → ( 𝑛 𝐽 𝑥 ) ∈ ℝ )
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	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 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	abeq2i	⊢ ( 𝑘 ∈ 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	syl5bi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝑘 ∈ 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	syl5bb	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 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	syl5bb	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 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 )