Theorem mbfi1fseqlem4 25773

Description: Lemma for mbfi1fseq 25776. 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 11275	. . . . 5 ⊢ ℝ ∈ V
2	1	mptex 7260	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)) ∈ V
3		mbfi1fseq.4	. . . 4 ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
4	2, 3	fnmpti 6723	. . 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 25772	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛):ℝ⟶ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
10		elfznn0 13677	. . . . . . . . 9 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℕ0)
11	10	nn0red 12614	. . . . . . . 8 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℝ)
12		2nn 12366	. . . . . . . . . 10 ⊢ 2 ∈ ℕ
13		nnnn0 12560	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
14		nnexpcl 14125	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
15	12, 13, 14	sylancr 586	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
16	15	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℕ)
17		nndivre 12334	. . . . . . . 8 ⊢ ((𝑚 ∈ ℝ ∧ (2↑𝑛) ∈ ℕ) → (𝑚 / (2↑𝑛)) ∈ ℝ)
18	11, 16, 17	syl2anr 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑚 / (2↑𝑛)) ∈ ℝ)
19	18	fmpttd 7149	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ℝ)
20	19	frnd 6755	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ⊆ ℝ)
21	9, 20	fssd 6764	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛):ℝ⟶ℝ)
22		fzfid 14024	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0...(𝑛 · (2↑𝑛))) ∈ Fin)
23	19	ffnd 6748	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))))
24		dffn4 6840	. . . . . . 7 ⊢ ((𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))) ↔ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
25	23, 24	sylib 218	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
26		fofi 9379	. . . . . 6 ⊢ (((0...(𝑛 · (2↑𝑛))) ∈ Fin ∧ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
27	22, 25, 26	syl2anc 583	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
28	9	frnd 6755	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
29	27, 28	ssfid 9329	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ∈ Fin)
30	6, 7, 8, 3	mbfi1fseqlem2 25771	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)))
31	30	fveq1d 6922	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝐺‘𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
32	31	ad2antlr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
33		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
34		ovex 7481	. . . . . . . . . . . . . . 15 ⊢ (𝑛𝐽𝑥) ∈ V
35		vex 3492	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ∈ V
36	34, 35	ifex 4598	. . . . . . . . . . . . . 14 ⊢ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ V
37		c0ex 11284	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
38	36, 37	ifex 4598	. . . . . . . . . . . . 13 ⊢ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V
39		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
40	39	fvmpt2 7040	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
41	33, 38, 40	sylancl 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
42	32, 41	eqtrd 2780	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
43	42	adantlr 714	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
44	43	eqeq1d 2742	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
45		eldifsni 4815	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0}) → 𝑘 ≠ 0)
46	45	ad2antlr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0)
47		neeq1 3009	. . . . . . . . . . . 12 ⊢ (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 ↔ 𝑘 ≠ 0))
48	46, 47	syl5ibrcom 247	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0))
49		iffalse 4557	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 0)
50	49	necon1ai 2974	. . . . . . . . . . 11 ⊢ (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 → 𝑥 ∈ (-𝑛[,]𝑛))
51	48, 50	syl6 35	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → 𝑥 ∈ (-𝑛[,]𝑛)))
52	51	pm4.71rd 562	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘)))
53		iftrue 4554	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))
54	53	eqeq1d 2742	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-𝑛[,]𝑛) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘))
55		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ)
56	55	nnred 12308	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
57	56	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ∈ ℝ)
58		rge0ssre 13516	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0[,)+∞) ⊆ ℝ
59		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
60		ffvelcdm 7115	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ (0[,)+∞))
61	7, 59, 60	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ (0[,)+∞))
62	58, 61	sselid 4006	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ ℝ)
63		nnnn0 12560	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
64		nnexpcl 14125	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ0) → (2↑𝑚) ∈ ℕ)
65	12, 63, 64	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
66	65	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
67	66	nnred 12308	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
68	62, 67	remulcld 11320	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ)
69		reflcl 13847	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
71	70, 66	nndivred 12347	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
72	71	ralrimivva 3208	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
73	8	fmpo 8109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
74	72, 73	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶ℝ)
75		fovcdm 7620	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
76	74, 75	syl3an1 1163	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
77	76	3expa 1118	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
78	77	adantlr 714	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
79	78	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛𝐽𝑥) ∈ ℝ)
80		lemin 13254	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
81	57, 79, 57, 80	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
82	79, 57	ifcld 4594	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
83	82, 57	letri3d 11432	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛 ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
84		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
85	84	eqeq2d 2751	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛))
86		min2 13252	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
87	79, 57, 86	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
88	87	biantrurd 532	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
89	83, 85, 88	3bitr4d 311	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ 𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛)))
90	57	leidd 11856	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ≤ 𝑛)
91	90	biantrud 531	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
92	81, 89, 91	3bitr4d 311	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
93		breq1 5169	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (𝑘 ≤ (𝐹‘𝑥) ↔ 𝑛 ≤ (𝐹‘𝑥)))
94	7	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞))
95	94	ffvelcdmda 7118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
96		elrege0 13514	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
97	95, 96	sylib 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
98	97	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
99	98	adantlr 714	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
100	55, 15	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℕ)
101	100	nnred 12308	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℝ)
102	99, 101	remulcld 11320	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ)
103		reflcl 13847	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ)
104	102, 103	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ)
105	100	nngt0d 12342	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝑛))
106		lemuldiv 12175	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℝ ∧ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
107	56, 104, 101, 105, 106	syl112anc 1374	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
108		lemul1 12146	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
109	56, 99, 101, 105, 108	syl112anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
110		nnmulcl 12317	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ (2↑𝑛) ∈ ℕ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
111	55, 15, 110	syl2anc2 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
112	111	nnzd 12666	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℤ)
113		flge 13856	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑛 · (2↑𝑛)) ∈ ℤ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛)))))
114	102, 112, 113	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛)))))
115	109, 114	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛)))))
116		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
117		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
118	117	fveq2d 6924	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
119		simpl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → 𝑚 = 𝑛)
120	119	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑛))
121	118, 120	oveq12d 7466	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝑛)))
122	121	fveq2d 6924	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝑛))))
123	122, 120	oveq12d 7466	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
124		ovex 7481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) ∈ V
125	123, 8, 124	ovmpoa 7605	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
126	55, 116, 125	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
127	126	breq2d 5178	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
128	107, 115, 127	3bitr4d 311	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹‘𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
129	93, 128	sylan9bbr 510	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹‘𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
130	116	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ ℝ)
131		iftrue 4554	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
132	131	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
133	130, 132	eleqtrrd 2847	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
134	133	biantrurd 532	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
135	92, 129, 134	3bitr2d 307	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
136	28	ssdifssd 4170	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran (𝐺‘𝑛) ∖ {0}) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
137	136	sselda 4008	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
138		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))
139	138	rnmpt 5980	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = {𝑘 ∣ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛))}
140	139	eqabri 2888	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ↔ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)))
141		elfzelz 13584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℤ)
142	141	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℤ)
143	142	zcnd 12748	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℂ)
144	15	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℕ)
145	144	nncnd 12309	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℂ)
146	144	nnne0d 12343	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ≠ 0)
147	143, 145, 146	divcan1d 12071	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) = 𝑚)
148	147, 142	eqeltrd 2844	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ)
149		oveq1 7455	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) = ((𝑚 / (2↑𝑛)) · (2↑𝑛)))
150	149	eleq1d 2829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑚 / (2↑𝑛)) → ((𝑘 · (2↑𝑛)) ∈ ℤ ↔ ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ))
151	148, 150	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
152	151	rexlimdva 3161	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
153	140, 152	biimtrid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) → (𝑘 · (2↑𝑛)) ∈ ℤ))
154	153	imp 406	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → (𝑘 · (2↑𝑛)) ∈ ℤ)
155	137, 154	syldan 590	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑘 · (2↑𝑛)) ∈ ℤ)
156	155	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 · (2↑𝑛)) ∈ ℤ)
157		flbi 13867	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑘 · (2↑𝑛)) ∈ ℤ) → ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
158	102, 156, 157	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
159	158	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
160		neeq1 3009	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 ↔ 𝑘 ≠ 𝑛))
161	160	biimparc 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛)
162		iffalse 4557	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑛𝐽𝑥) ≤ 𝑛 → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛)
163	162	necon1ai 2974	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 → (𝑛𝐽𝑥) ≤ 𝑛)
164	161, 163	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
165	164	iftrued 4556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
166		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
167	165, 166	eqtr3d 2782	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
168	167, 164	eqbrtrrd 5190	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → 𝑘 ≤ 𝑛)
169	168, 167	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘))
170	169	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ≠ 𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
171		breq1 5169	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛𝐽𝑥) = 𝑘 → ((𝑛𝐽𝑥) ≤ 𝑛 ↔ 𝑘 ≤ 𝑛))
172	171	biimparc 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
173	172	iftrued 4556	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
174		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
175	173, 174	eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
176	170, 175	impbid1 225	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ≠ 𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
177	176	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
178		eldifi 4154	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0}) → 𝑘 ∈ ran (𝐺‘𝑛))
179		nnre 12300	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
180	179	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
181	77, 180, 86	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
182	13	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ0)
183	182	nn0ge0d 12616	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝑛)
184		breq1 5169	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
185		breq1 5169	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (0 ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
186	184, 185	ifboth 4587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 0 ≤ 𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
187	181, 183, 186	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
188	42, 187	eqbrtrd 5188	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) ≤ 𝑛)
189	188	ralrimiva 3152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛)
190	9	ffnd 6748	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) Fn ℝ)
191		breq1 5169	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = ((𝐺‘𝑛)‘𝑥) → (𝑘 ≤ 𝑛 ↔ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
192	191	ralrn 7122	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺‘𝑛) Fn ℝ → (∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
193	190, 192	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
194	189, 193	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛)
195	194	r19.21bi 3257	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝐺‘𝑛)) → 𝑘 ≤ 𝑛)
196	178, 195	sylan2 592	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ≤ 𝑛)
197	196	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → 𝑘 ≤ 𝑛)
198	197	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
199	126	eqeq1d 2742	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘))
200	104	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℂ)
201	28, 20	sstrd 4019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ⊆ ℝ)
202	201	ssdifssd 4170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran (𝐺‘𝑛) ∖ {0}) ⊆ ℝ)
203	202	sselda 4008	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ∈ ℝ)
204	203	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ)
205	204	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℂ)
206	100	nncnd 12309	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℂ)
207	100	nnne0d 12343	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ≠ 0)
208	200, 205, 206, 207	divmul3d 12104	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
209	199, 208	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
210	209	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
211	177, 198, 210	3bitr2d 307	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
212		ifnefalse 4560	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ≠ 𝑛 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
213	212	eleq2d 2830	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ≠ 𝑛 → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ 𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
214	100	nnrecred 12344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℝ)
215	204, 214	readdcld 11319	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ)
216	215	rexrd 11340	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ*)
217		elioomnf 13504	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 + (1 / (2↑𝑛))) ∈ ℝ* → ((𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
218	216, 217	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
219	94	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶(0[,)+∞))
220	219	ffnd 6748	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
221		elpreima 7091	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
222	220, 221	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
223	116, 222	mpbirand 706	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
224	99	biantrurd 532	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
225	218, 223, 224	3bitr4d 311	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛)))))
226		ltmul1 12144	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘𝑥) ∈ ℝ ∧ (𝑘 + (1 / (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
227	99, 215, 101, 105, 226	syl112anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
228	214	recnd 11318	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℂ)
229	206, 207	recid2d 12066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((1 / (2↑𝑛)) · (2↑𝑛)) = 1)
230	229	oveq2d 7464	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 · (2↑𝑛)) + ((1 / (2↑𝑛)) · (2↑𝑛))) = ((𝑘 · (2↑𝑛)) + 1))
231	205, 206, 228, 230	joinlmuladdmuld 11317	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) = ((𝑘 · (2↑𝑛)) + 1))
232	231	breq2d 5178	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
233	225, 227, 232	3bitrd 305	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
234	213, 233	sylan9bbr 510	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
235		lemul1 12146	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
236	204, 99, 101, 105, 235	syl112anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
237	236	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
238	234, 237	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥)) ↔ (((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1) ∧ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)))))
239	238	biancomd 463	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
240	159, 211, 239	3bitr4d 311	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
241	135, 240	pm2.61dane 3035	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
242		eldif 3986	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘))))
243	204	rexrd 11340	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ*)
244		elioomnf 13504	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ* → ((𝐹‘𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
245	243, 244	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
246		elpreima 7091	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)𝑘))))
247	220, 246	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)𝑘))))
248	116, 247	mpbirand 706	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝐹‘𝑥) ∈ (-∞(,)𝑘)))
249	99	biantrurd 532	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) < 𝑘 ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
250	245, 248, 249	3bitr4d 311	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝐹‘𝑥) < 𝑘))
251	250	notbid 318	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ ¬ (𝐹‘𝑥) < 𝑘))
252	204, 99	lenltd 11436	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑥) < 𝑘))
253	251, 252	bitr4d 282	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ 𝑘 ≤ (𝐹‘𝑥)))
254	253	anbi2d 629	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
255	242, 254	bitrid 283	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
256	241, 255	bitr4d 282	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
257	54, 256	sylan9bbr 510	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ (-𝑛[,]𝑛)) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
258	257	pm5.32da 578	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))))))
259	44, 52, 258	3bitrd 305	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))))))
260	259	pm5.32da 578	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))))
261	21	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛):ℝ⟶ℝ)
262	261	ffnd 6748	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛) Fn ℝ)
263		fniniseg 7093	. . . . . . . 8 ⊢ ((𝐺‘𝑛) Fn ℝ → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
264	262, 263	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
265		elin 3992	. . . . . . . 8 ⊢ (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
266	179	ad2antlr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑛 ∈ ℝ)
267	266	renegcld 11717	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → -𝑛 ∈ ℝ)
268		iccmbl 25620	. . . . . . . . . . . . 13 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol)
269	267, 266, 268	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (-𝑛[,]𝑛) ∈ dom vol)
270		mblss 25585	. . . . . . . . . . . 12 ⊢ ((-𝑛[,]𝑛) ∈ dom vol → (-𝑛[,]𝑛) ⊆ ℝ)
271	269, 270	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
272	271	sseld 4007	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (-𝑛[,]𝑛) → 𝑥 ∈ ℝ))
273	272	adantrd 491	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) → 𝑥 ∈ ℝ))
274	273	pm4.71rd 562	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))))
275	265, 274	bitrid 283	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))))
276	260, 264, 275	3bitr4d 311	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ 𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))))))
277	276	eqrdv 2738	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) = ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
278		rembl 25594	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
279		fss 6763	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
280	7, 58, 279	sylancl 585	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
281		mbfima 25684	. . . . . . . . . 10 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
282	6, 280, 281	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
283		ifcl 4593	. . . . . . . . 9 ⊢ ((ℝ ∈ dom vol ∧ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol) → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
284	278, 282, 283	sylancr 586	. . . . . . . 8 ⊢ (𝜑 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
285		mbfima 25684	. . . . . . . . 9 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
286	6, 280, 285	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
287		difmbl 25597	. . . . . . . 8 ⊢ ((if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol ∧ (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol) → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
288	284, 286, 287	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
289	288	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
290		inmbl 25596	. . . . . 6 ⊢ (((-𝑛[,]𝑛) ∈ dom vol ∧ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
291	269, 289, 290	syl2anc 583	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
292	277, 291	eqeltrd 2844	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) ∈ dom vol)
293		mblvol 25584	. . . . . 6 ⊢ ((◡(𝐺‘𝑛) “ {𝑘}) ∈ dom vol → (vol‘(◡(𝐺‘𝑛) “ {𝑘})) = (vol*‘(◡(𝐺‘𝑛) “ {𝑘})))
294	292, 293	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(◡(𝐺‘𝑛) “ {𝑘})) = (vol*‘(◡(𝐺‘𝑛) “ {𝑘})))
295	190	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛) Fn ℝ)
296	295, 263	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
297	77, 180	ifcld 4594	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
298		0re 11292	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
299		ifcl 4593	. . . . . . . . . . . . . . 15 ⊢ ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
300	297, 298, 299	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
301	39	fvmpt2 7040	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
302	33, 300, 301	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
303	32, 302	eqtrd 2780	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
304	303	adantlr 714	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
305	304	eqeq1d 2742	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
306	305, 51	sylbid 240	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 → 𝑥 ∈ (-𝑛[,]𝑛)))
307	306	expimpd 453	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘) → 𝑥 ∈ (-𝑛[,]𝑛)))
308	296, 307	sylbid 240	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) → 𝑥 ∈ (-𝑛[,]𝑛)))
309	308	ssrdv 4014	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛))
310		iccssre 13489	. . . . . . 7 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ⊆ ℝ)
311	267, 266, 310	syl2anc 583	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
312		mblvol 25584	. . . . . . . 8 ⊢ ((-𝑛[,]𝑛) ∈ dom vol → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
313	269, 312	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
314		iccvolcl 25621	. . . . . . . 8 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
315	267, 266, 314	syl2anc 583	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
316	313, 315	eqeltrrd 2845	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol*‘(-𝑛[,]𝑛)) ∈ ℝ)
317		ovolsscl 25540	. . . . . 6 ⊢ (((◡(𝐺‘𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛) ∧ (-𝑛[,]𝑛) ⊆ ℝ ∧ (vol*‘(-𝑛[,]𝑛)) ∈ ℝ) → (vol*‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
318	309, 311, 316, 317	syl3anc 1371	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol*‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
319	294, 318	eqeltrd 2844	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
320	21, 29, 292, 319	i1fd 25735	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ dom ∫1)
321	320	ralrimiva 3152	. 2 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ dom ∫1)
322		ffnfv 7153	. 2 ⊢ (𝐺:ℕ⟶dom ∫1 ↔ (𝐺 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ dom ∫1))
323	5, 321, 322	sylanbrc 582	1 ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫1)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  Vcvv 3488   ∖ cdif 3973   ∩ cin 3975   ⊆ wss 3976  ifcif 4548  {csn 4648   class class class wbr 5166   ↦ cmpt 5249   × cxp 5698  ^◡ccnv 5699  dom cdm 5700  ran crn 5701   “ cima 5703   Fn wfn 6568  ⟶wf 6569  –onto→wfo 6571  ‘cfv 6573  (class class class)co 7448   ∈ cmpo 7450  Fincfn 9003  ℝcr 11183  0cc0 11184  1c1 11185   + caddc 11187   · cmul 11189  +∞cpnf 11321  -∞cmnf 11322  ℝ^*cxr 11323   < clt 11324   ≤ cle 11325  -cneg 11521   / cdiv 11947  ℕcn 12293  2c2 12348  ℕ₀cn0 12553  ℤcz 12639  (,)cioo 13407  [,)cico 13409  [,]cicc 13410  ...cfz 13567  ⌊cfl 13841  ↑cexp 14112  vol*covol 25516  volcvol 25517  MblFncmbf 25668  ∫₁citg1 25669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-of 7714  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-er 8763  df-map 8886  df-pm 8887  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-fi 9480  df-sup 9511  df-inf 9512  df-oi 9579  df-dju 9970  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-n0 12554  df-z 12640  df-uz 12904  df-q 13014  df-rp 13058  df-xneg 13175  df-xadd 13176  df-xmul 13177  df-ioo 13411  df-ico 13413  df-icc 13414  df-fz 13568  df-fzo 13712  df-fl 13843  df-seq 14053  df-exp 14113  df-hash 14380  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-clim 15534  df-rlim 15535  df-sum 15735  df-rest 17482  df-topgen 17503  df-psmet 21379  df-xmet 21380  df-met 21381  df-bl 21382  df-mopn 21383  df-top 22921  df-topon 22938  df-bases 22974  df-cmp 23416  df-ovol 25518  df-vol 25519  df-mbf 25673  df-itg1 25674

This theorem is referenced by:  mbfi1fseqlem5  25774  mbfi1fseqlem6  25775