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 ↑ 𝐴 ) ) ) )