Theorem mbfi1fseqlem4 23291

Description: Lemma for mbfi1fseq 23294. This lemma is not as interesting as it is long - it is simply checking that 𝐺 is in fact a sequence of simple functions, by verifying that its range is in (0...𝑛2↑𝑛) / (2↑𝑛) (which is to say, the numbers from 0 to 𝑛 in increments of 1 / (2↑𝑛)), and also that the preimage of each point 𝑘 is measurable, because it is equal to (-𝑛[,]𝑛) ∩ (^◡𝐹 “ (𝑘[,)𝑘 + 1 / (2↑𝑛))) for 𝑘 < 𝑛 and (-𝑛[,]𝑛) ∩ (^◡𝐹 “ (𝑘[,)+∞)) for 𝑘 = 𝑛. (Contributed by Mario Carneiro, 16-Aug-2014.)

Hypotheses

Ref	Expression
mbfi1fseq.1	⊢ (𝜑 → 𝐹 ∈ MblFn)
mbfi1fseq.2	⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))
mbfi1fseq.3	⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))
mbfi1fseq.4	⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))

Assertion

Ref	Expression
mbfi1fseqlem4	⊢ (𝜑 → 𝐺:ℕ⟶dom ∫1)

Distinct variable groups:   𝑥,𝑚,𝑦,𝐹   𝑥,𝐺   𝑚,𝐽   𝜑,𝑚,𝑥,𝑦

Allowed substitution hints:   𝐺(𝑦,𝑚)   𝐽(𝑥,𝑦)

Proof of Theorem mbfi1fseqlem4

Dummy variables 𝑘 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reex 9906	. . . . 5 ⊢ ℝ ∈ V
2	1	mptex 6390	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)) ∈ V
3		mbfi1fseq.4	. . . 4 ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
4	2, 3	fnmpti 5935	. . 3 ⊢ 𝐺 Fn ℕ
5	4	a1i 11	. 2 ⊢ (𝜑 → 𝐺 Fn ℕ)
6		mbfi1fseq.1	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ MblFn)
7		mbfi1fseq.2	. . . . . 6 ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))
8		mbfi1fseq.3	. . . . . 6 ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))
9	6, 7, 8, 3	mbfi1fseqlem3 23290	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛):ℝ⟶ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
10		elfznn0 12302	. . . . . . . . 9 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℕ0)
11	10	nn0red 11229	. . . . . . . 8 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℝ)
12		2nn 11062	. . . . . . . . . 10 ⊢ 2 ∈ ℕ
13		nnnn0 11176	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
14		nnexpcl 12735	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
15	12, 13, 14	sylancr 694	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
16	15	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℕ)
17		nndivre 10933	. . . . . . . 8 ⊢ ((𝑚 ∈ ℝ ∧ (2↑𝑛) ∈ ℕ) → (𝑚 / (2↑𝑛)) ∈ ℝ)
18	11, 16, 17	syl2anr 494	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑚 / (2↑𝑛)) ∈ ℝ)
19		eqid 2610	. . . . . . 7 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))
20	18, 19	fmptd 6292	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ℝ)
21		frn 5966	. . . . . 6 ⊢ ((𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ℝ → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ⊆ ℝ)
22	20, 21	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ⊆ ℝ)
23	9, 22	fssd 5970	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛):ℝ⟶ℝ)
24		fzfid 12634	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0...(𝑛 · (2↑𝑛))) ∈ Fin)
25		ffn 5958	. . . . . . . 8 ⊢ ((𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ℝ → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))))
26	20, 25	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))))
27		dffn4 6034	. . . . . . 7 ⊢ ((𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))) ↔ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
28	26, 27	sylib 207	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
29		fofi 8135	. . . . . 6 ⊢ (((0...(𝑛 · (2↑𝑛))) ∈ Fin ∧ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
30	24, 28, 29	syl2anc 691	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
31		frn 5966	. . . . . 6 ⊢ ((𝐺‘𝑛):ℝ⟶ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) → ran (𝐺‘𝑛) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
32	9, 31	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
33		ssfi 8065	. . . . 5 ⊢ ((ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin ∧ ran (𝐺‘𝑛) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → ran (𝐺‘𝑛) ∈ Fin)
34	30, 32, 33	syl2anc 691	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ∈ Fin)
35	6, 7, 8, 3	mbfi1fseqlem2 23289	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)))
36	35	fveq1d 6105	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝐺‘𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
37	36	ad2antlr 759	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
38		simpr 476	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
39		ovex 6577	. . . . . . . . . . . . . . 15 ⊢ (𝑛𝐽𝑥) ∈ V
40		vex 3176	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ∈ V
41	39, 40	ifex 4106	. . . . . . . . . . . . . 14 ⊢ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ V
42		c0ex 9913	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
43	41, 42	ifex 4106	. . . . . . . . . . . . 13 ⊢ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V
44		eqid 2610	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
45	44	fvmpt2 6200	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
46	38, 43, 45	sylancl 693	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
47	37, 46	eqtrd 2644	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
48	47	adantlr 747	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
49	48	eqeq1d 2612	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
50		eldifsni 4261	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0}) → 𝑘 ≠ 0)
51	50	ad2antlr 759	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0)
52		neeq1 2844	. . . . . . . . . . . 12 ⊢ (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 ↔ 𝑘 ≠ 0))
53	51, 52	syl5ibrcom 236	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0))
54		iffalse 4045	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 0)
55	54	necon1ai 2809	. . . . . . . . . . 11 ⊢ (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 → 𝑥 ∈ (-𝑛[,]𝑛))
56	53, 55	syl6 34	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → 𝑥 ∈ (-𝑛[,]𝑛)))
57	56	pm4.71rd 665	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘)))
58		iftrue 4042	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))
59	58	eqeq1d 2612	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-𝑛[,]𝑛) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘))
60		simpllr 795	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ)
61	60	nnred 10912	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
62	61	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ∈ ℝ)
63		rge0ssre 12151	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0[,)+∞) ⊆ ℝ
64		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
65		ffvelrn 6265	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ (0[,)+∞))
66	7, 64, 65	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ (0[,)+∞))
67	63, 66	sseldi 3566	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ ℝ)
68		nnnn0 11176	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
69		nnexpcl 12735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ0) → (2↑𝑚) ∈ ℕ)
70	12, 68, 69	sylancr 694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
71	70	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
72	71	nnred 10912	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
73	67, 72	remulcld 9949	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ)
74		reflcl 12459	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
75	73, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
76	75, 71	nndivred 10946	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
77	76	ralrimivva 2954	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
78	8	fmpt2 7126	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
79	77, 78	sylib 207	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶ℝ)
80		fovrn 6702	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
81	79, 80	syl3an1 1351	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
82	81	3expa 1257	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
83	82	adantlr 747	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
84	83	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛𝐽𝑥) ∈ ℝ)
85		lemin 11897	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
86	62, 84, 62, 85	syl3anc 1318	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
87	84, 62	ifcld 4081	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
88	87, 62	letri3d 10058	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛 ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
89		simpr 476	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
90	89	eqeq2d 2620	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛))
91		min2 11895	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
92	84, 62, 91	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
93	92	biantrurd 528	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
94	88, 90, 93	3bitr4d 299	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ 𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛)))
95	62	leidd 10473	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ≤ 𝑛)
96	95	biantrud 527	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
97	86, 94, 96	3bitr4d 299	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
98		breq1 4586	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (𝑘 ≤ (𝐹‘𝑥) ↔ 𝑛 ≤ (𝐹‘𝑥)))
99	7	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞))
100	99	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
101		elrege0 12149	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
102	100, 101	sylib 207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
103	102	simpld 474	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
104	103	adantlr 747	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
105	60, 15	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℕ)
106	105	nnred 10912	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℝ)
107	104, 106	remulcld 9949	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ)
108		reflcl 12459	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ)
109	107, 108	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ)
110	105	nngt0d 10941	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝑛))
111		lemuldiv 10782	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℝ ∧ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
112	61, 109, 106, 110, 111	syl112anc 1322	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
113		lemul1 10754	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
114	61, 104, 106, 110, 113	syl112anc 1322	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
115		nnmulcl 10920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ ∧ (2↑𝑛) ∈ ℕ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
116	15, 115	mpdan 699	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → (𝑛 · (2↑𝑛)) ∈ ℕ)
117	60, 116	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
118	117	nnzd 11357	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℤ)
119		flge 12468	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑛 · (2↑𝑛)) ∈ ℤ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛)))))
120	107, 118, 119	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛)))))
121	114, 120	bitrd 267	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛)))))
122		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
123		simpr 476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
124	123	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
125		simpl 472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → 𝑚 = 𝑛)
126	125	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑛))
127	124, 126	oveq12d 6567	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝑛)))
128	127	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝑛))))
129	128, 126	oveq12d 6567	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
130		ovex 6577	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) ∈ V
131	129, 8, 130	ovmpt2a 6689	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
132	60, 122, 131	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
133	132	breq2d 4595	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
134	112, 121, 133	3bitr4d 299	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹‘𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
135	98, 134	sylan9bbr 733	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹‘𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
136	122	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ ℝ)
137		iftrue 4042	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
138	137	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
139	136, 138	eleqtrrd 2691	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
140	139	biantrurd 528	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
141	97, 135, 140	3bitr2d 295	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
142	32	ssdifssd 3710	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran (𝐺‘𝑛) ∖ {0}) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
143	142	sselda 3568	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
144	19	rnmpt 5292	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = {𝑘 ∣ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛))}
145	144	abeq2i 2722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ↔ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)))
146		elfzelz 12213	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℤ)
147	146	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℤ)
148	147	zcnd 11359	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℂ)
149	15	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℕ)
150	149	nncnd 10913	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℂ)
151	149	nnne0d 10942	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ≠ 0)
152	148, 150, 151	divcan1d 10681	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) = 𝑚)
153	152, 147	eqeltrd 2688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ)
154		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) = ((𝑚 / (2↑𝑛)) · (2↑𝑛)))
155	154	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑚 / (2↑𝑛)) → ((𝑘 · (2↑𝑛)) ∈ ℤ ↔ ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ))
156	153, 155	syl5ibrcom 236	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
157	156	rexlimdva 3013	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
158	145, 157	syl5bi 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) → (𝑘 · (2↑𝑛)) ∈ ℤ))
159	158	imp 444	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → (𝑘 · (2↑𝑛)) ∈ ℤ)
160	143, 159	syldan 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑘 · (2↑𝑛)) ∈ ℤ)
161	160	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 · (2↑𝑛)) ∈ ℤ)
162		flbi 12479	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑘 · (2↑𝑛)) ∈ ℤ) → ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
163	107, 161, 162	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
164	163	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
165		neeq1 2844	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 ↔ 𝑘 ≠ 𝑛))
166	165	biimparc 503	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛)
167		iffalse 4045	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑛𝐽𝑥) ≤ 𝑛 → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛)
168	167	necon1ai 2809	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 → (𝑛𝐽𝑥) ≤ 𝑛)
169	166, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
170	169	iftrued 4044	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
171		simpr 476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
172	170, 171	eqtr3d 2646	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
173	172, 169	eqbrtrrd 4607	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → 𝑘 ≤ 𝑛)
174	173, 172	jca 553	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘))
175	174	ex 449	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ≠ 𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
176		breq1 4586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛𝐽𝑥) = 𝑘 → ((𝑛𝐽𝑥) ≤ 𝑛 ↔ 𝑘 ≤ 𝑛))
177	176	biimparc 503	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
178	177	iftrued 4044	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
179		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
180	178, 179	eqtrd 2644	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
181	175, 180	impbid1 214	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ≠ 𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
182	181	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
183		eldifi 3694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0}) → 𝑘 ∈ ran (𝐺‘𝑛))
184		nnre 10904	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
185	184	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
186	82, 185, 91	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
187	13	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ0)
188	187	nn0ge0d 11231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝑛)
189		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
190		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (0 ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
191	189, 190	ifboth 4074	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 0 ≤ 𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
192	186, 188, 191	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
193	47, 192	eqbrtrd 4605	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) ≤ 𝑛)
194	193	ralrimiva 2949	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛)
195		ffn 5958	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺‘𝑛):ℝ⟶ℝ → (𝐺‘𝑛) Fn ℝ)
196	23, 195	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) Fn ℝ)
197		breq1 4586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = ((𝐺‘𝑛)‘𝑥) → (𝑘 ≤ 𝑛 ↔ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
198	197	ralrn 6270	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺‘𝑛) Fn ℝ → (∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
199	196, 198	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
200	194, 199	mpbird 246	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛)
201	200	r19.21bi 2916	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝐺‘𝑛)) → 𝑘 ≤ 𝑛)
202	183, 201	sylan2 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ≤ 𝑛)
203	202	ad2antrr 758	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → 𝑘 ≤ 𝑛)
204	203	biantrurd 528	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
205	132	eqeq1d 2612	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘))
206	109	recnd 9947	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℂ)
207	32, 22	sstrd 3578	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ⊆ ℝ)
208	207	ssdifssd 3710	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran (𝐺‘𝑛) ∖ {0}) ⊆ ℝ)
209	208	sselda 3568	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ∈ ℝ)
210	209	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ)
211	210	recnd 9947	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℂ)
212	105	nncnd 10913	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℂ)
213	105	nnne0d 10942	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ≠ 0)
214	206, 211, 212, 213	divmul3d 10714	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
215	205, 214	bitrd 267	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
216	215	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
217	182, 204, 216	3bitr2d 295	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
218		ifnefalse 4048	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ≠ 𝑛 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
219	218	eleq2d 2673	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ≠ 𝑛 → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ 𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
220	105	nnrecred 10943	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℝ)
221	210, 220	readdcld 9948	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ)
222	221	rexrd 9968	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ*)
223		elioomnf 12139	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 + (1 / (2↑𝑛))) ∈ ℝ* → ((𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
224	222, 223	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
225	99	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶(0[,)+∞))
226		ffn 5958	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐹:ℝ⟶(0[,)+∞) → 𝐹 Fn ℝ)
227	225, 226	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
228		elpreima 6245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
229	227, 228	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
230	122	biantrurd 528	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
231	229, 230	bitr4d 270	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
232	104	biantrurd 528	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
233	224, 231, 232	3bitr4d 299	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛)))))
234		ltmul1 10752	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘𝑥) ∈ ℝ ∧ (𝑘 + (1 / (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
235	104, 221, 106, 110, 234	syl112anc 1322	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
236	220	recnd 9947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℂ)
237	211, 236, 212	adddird 9944	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) = ((𝑘 · (2↑𝑛)) + ((1 / (2↑𝑛)) · (2↑𝑛))))
238	212, 213	recid2d 10676	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((1 / (2↑𝑛)) · (2↑𝑛)) = 1)
239	238	oveq2d 6565	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 · (2↑𝑛)) + ((1 / (2↑𝑛)) · (2↑𝑛))) = ((𝑘 · (2↑𝑛)) + 1))
240	237, 239	eqtrd 2644	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) = ((𝑘 · (2↑𝑛)) + 1))
241	240	breq2d 4595	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
242	233, 235, 241	3bitrd 293	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
243	219, 242	sylan9bbr 733	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
244		lemul1 10754	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
245	210, 104, 106, 110, 244	syl112anc 1322	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
246	245	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
247	243, 246	anbi12d 743	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥)) ↔ (((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1) ∧ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)))))
248		ancom 465	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1) ∧ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
249	247, 248	syl6bb 275	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
250	164, 217, 249	3bitr4d 299	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
251	141, 250	pm2.61dane 2869	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
252		eldif 3550	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘))))
253	210	rexrd 9968	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ*)
254		elioomnf 12139	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ* → ((𝐹‘𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
255	253, 254	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
256		elpreima 6245	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)𝑘))))
257	227, 256	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)𝑘))))
258	122	biantrurd 528	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (-∞(,)𝑘) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)𝑘))))
259	257, 258	bitr4d 270	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝐹‘𝑥) ∈ (-∞(,)𝑘)))
260	104	biantrurd 528	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) < 𝑘 ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
261	255, 259, 260	3bitr4d 299	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝐹‘𝑥) < 𝑘))
262	261	notbid 307	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ ¬ (𝐹‘𝑥) < 𝑘))
263	210, 104	lenltd 10062	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑥) < 𝑘))
264	262, 263	bitr4d 270	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ 𝑘 ≤ (𝐹‘𝑥)))
265	264	anbi2d 736	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
266	252, 265	syl5bb 271	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
267	251, 266	bitr4d 270	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
268	59, 267	sylan9bbr 733	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝑛[,]𝑛)) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
269	268	pm5.32da 671	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))))))
270	49, 57, 269	3bitrd 293	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))))))
271	270	pm5.32da 671	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))))
272	23	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛):ℝ⟶ℝ)
273	272, 195	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛) Fn ℝ)
274		fniniseg 6246	. . . . . . . 8 ⊢ ((𝐺‘𝑛) Fn ℝ → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
275	273, 274	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
276		elin 3758	. . . . . . . 8 ⊢ (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
277	184	ad2antlr 759	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑛 ∈ ℝ)
278	277	renegcld 10336	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → -𝑛 ∈ ℝ)
279		iccmbl 23141	. . . . . . . . . . . . 13 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol)
280	278, 277, 279	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (-𝑛[,]𝑛) ∈ dom vol)
281		mblss 23106	. . . . . . . . . . . 12 ⊢ ((-𝑛[,]𝑛) ∈ dom vol → (-𝑛[,]𝑛) ⊆ ℝ)
282	280, 281	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
283	282	sseld 3567	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (-𝑛[,]𝑛) → 𝑥 ∈ ℝ))
284	283	adantrd 483	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) → 𝑥 ∈ ℝ))
285	284	pm4.71rd 665	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))))
286	276, 285	syl5bb 271	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))))
287	271, 275, 286	3bitr4d 299	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ 𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))))))
288	287	eqrdv 2608	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) = ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
289		rembl 23115	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
290		fss 5969	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
291	7, 63, 290	sylancl 693	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
292		mbfima 23205	. . . . . . . . . 10 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
293	6, 291, 292	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
294		ifcl 4080	. . . . . . . . 9 ⊢ ((ℝ ∈ dom vol ∧ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol) → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
295	289, 293, 294	sylancr 694	. . . . . . . 8 ⊢ (𝜑 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
296		mbfima 23205	. . . . . . . . 9 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
297	6, 291, 296	syl2anc 691	. . . . . . . 8 ⊢ (𝜑 → (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
298		difmbl 23118	. . . . . . . 8 ⊢ ((if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol ∧ (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol) → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
299	295, 297, 298	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
300	299	ad2antrr 758	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
301		inmbl 23117	. . . . . 6 ⊢ (((-𝑛[,]𝑛) ∈ dom vol ∧ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
302	280, 300, 301	syl2anc 691	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
303	288, 302	eqeltrd 2688	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) ∈ dom vol)
304		mblvol 23105	. . . . . 6 ⊢ ((◡(𝐺‘𝑛) “ {𝑘}) ∈ dom vol → (vol‘(◡(𝐺‘𝑛) “ {𝑘})) = (vol*‘(◡(𝐺‘𝑛) “ {𝑘})))
305	303, 304	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(◡(𝐺‘𝑛) “ {𝑘})) = (vol*‘(◡(𝐺‘𝑛) “ {𝑘})))
306	196	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛) Fn ℝ)
307	306, 274	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
308	82, 185	ifcld 4081	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
309		0re 9919	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
310		ifcl 4080	. . . . . . . . . . . . . . 15 ⊢ ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
311	308, 309, 310	sylancl 693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
312	44	fvmpt2 6200	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
313	38, 311, 312	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
314	37, 313	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
315	314	adantlr 747	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
316	315	eqeq1d 2612	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
317	316, 56	sylbid 229	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 → 𝑥 ∈ (-𝑛[,]𝑛)))
318	317	expimpd 627	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘) → 𝑥 ∈ (-𝑛[,]𝑛)))
319	307, 318	sylbid 229	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) → 𝑥 ∈ (-𝑛[,]𝑛)))
320	319	ssrdv 3574	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛))
321		iccssre 12126	. . . . . . 7 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ⊆ ℝ)
322	278, 277, 321	syl2anc 691	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
323		mblvol 23105	. . . . . . . 8 ⊢ ((-𝑛[,]𝑛) ∈ dom vol → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
324	280, 323	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
325		iccvolcl 23142	. . . . . . . 8 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
326	278, 277, 325	syl2anc 691	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
327	324, 326	eqeltrrd 2689	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol*‘(-𝑛[,]𝑛)) ∈ ℝ)
328		ovolsscl 23061	. . . . . 6 ⊢ (((◡(𝐺‘𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛) ∧ (-𝑛[,]𝑛) ⊆ ℝ ∧ (vol*‘(-𝑛[,]𝑛)) ∈ ℝ) → (vol*‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
329	320, 322, 327, 328	syl3anc 1318	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol*‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
330	305, 329	eqeltrd 2688	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
331	23, 34, 303, 330	i1fd 23254	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ dom ∫1)
332	331	ralrimiva 2949	. 2 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ dom ∫1)
333		ffnfv 6295	. 2 ⊢ (𝐺:ℕ⟶dom ∫1 ↔ (𝐺 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ dom ∫1))
334	5, 332, 333	sylanbrc 695	1 ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫1)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∩ cin 3539   ⊆ wss 3540  ifcif 4036  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  ^◡ccnv 5037  dom cdm 5038  ran crn 5039   “ cima 5041   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  Fincfn 7841  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  +∞cpnf 9950  -∞cmnf 9951  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954  -cneg 10146   / cdiv 10563  ℕcn 10897  2c2 10947  ℕ₀cn0 11169  ℤcz 11254  (,)cioo 12046  [,)cico 12048  [,]cicc 12049  ...cfz 12197  ⌊cfl 12453  ↑cexp 12722  vol*covol 23038  volcvol 23039  MblFncmbf 23189  ∫₁citg1 23190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-rlim 14068  df-sum 14265  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cmp 21000  df-ovol 23040  df-vol 23041  df-mbf 23194  df-itg1 23195

This theorem is referenced by:  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293