Theorem mbfi1fseqlem4 25675

Description: Lemma for mbfi1fseq 25678. 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 11117	. . . . 5 ⊢ ℝ ∈ V
2	1	mptex 7169	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)) ∈ V
3		mbfi1fseq.4	. . . 4 ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
4	2, 3	fnmpti 6635	. . 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 25674	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛):ℝ⟶ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
10		elfznn0 13536	. . . . . . . . 9 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℕ0)
11	10	nn0red 12463	. . . . . . . 8 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℝ)
12		2nn 12218	. . . . . . . . . 10 ⊢ 2 ∈ ℕ
13		nnnn0 12408	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
14		nnexpcl 13997	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
15	12, 13, 14	sylancr 587	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
16	15	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℕ)
17		nndivre 12186	. . . . . . . 8 ⊢ ((𝑚 ∈ ℝ ∧ (2↑𝑛) ∈ ℕ) → (𝑚 / (2↑𝑛)) ∈ ℝ)
18	11, 16, 17	syl2anr 597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑚 / (2↑𝑛)) ∈ ℝ)
19	18	fmpttd 7060	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ℝ)
20	19	frnd 6670	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ⊆ ℝ)
21	9, 20	fssd 6679	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛):ℝ⟶ℝ)
22		fzfid 13896	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0...(𝑛 · (2↑𝑛))) ∈ Fin)
23	19	ffnd 6663	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))))
24		dffn4 6752	. . . . . . 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 9213	. . . . . 6 ⊢ (((0...(𝑛 · (2↑𝑛))) ∈ Fin ∧ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))–onto→ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
27	22, 25, 26	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
28	9	frnd 6670	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
29	27, 28	ssfid 9169	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ∈ Fin)
30	6, 7, 8, 3	mbfi1fseqlem2 25673	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)))
31	30	fveq1d 6836	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝐺‘𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
32	31	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
33		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
34		ovex 7391	. . . . . . . . . . . . . . 15 ⊢ (𝑛𝐽𝑥) ∈ V
35		vex 3444	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ∈ V
36	34, 35	ifex 4530	. . . . . . . . . . . . . 14 ⊢ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ V
37		c0ex 11126	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
38	36, 37	ifex 4530	. . . . . . . . . . . . 13 ⊢ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V
39		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
40	39	fvmpt2 6952	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
41	33, 38, 40	sylancl 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
42	32, 41	eqtrd 2771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
43	42	adantlr 715	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
44	43	eqeq1d 2738	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
45		eldifsni 4746	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0}) → 𝑘 ≠ 0)
46	45	ad2antlr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0)
47		neeq1 2994	. . . . . . . . . . . 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 4488	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 0)
50	49	necon1ai 2959	. . . . . . . . . . 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 4485	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (-𝑛[,]𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))
54	53	eqeq1d 2738	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-𝑛[,]𝑛) → (if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘))
55		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ)
56	55	nnred 12160	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
57	56	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ∈ ℝ)
58		rge0ssre 13372	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0[,)+∞) ⊆ ℝ
59		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
60		ffvelcdm 7026	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ (0[,)+∞))
61	7, 59, 60	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ (0[,)+∞))
62	58, 61	sselid 3931	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ ℝ)
63		nnnn0 12408	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
64		nnexpcl 13997	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ0) → (2↑𝑚) ∈ ℕ)
65	12, 63, 64	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
66	65	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
67	66	nnred 12160	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
68	62, 67	remulcld 11162	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ)
69		reflcl 13716	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
70	68, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
71	70, 66	nndivred 12199	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
72	71	ralrimivva 3179	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
73	8	fmpo 8012	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
74	72, 73	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶ℝ)
75		fovcdm 7528	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
76	74, 75	syl3an1 1163	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
77	76	3expa 1118	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
78	77	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
79	78	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛𝐽𝑥) ∈ ℝ)
80		lemin 13107	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
81	57, 79, 57, 80	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
82	79, 57	ifcld 4526	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
83	82, 57	letri3d 11275	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛 ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
84		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
85	84	eqeq2d 2747	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛))
86		min2 13105	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
87	79, 57, 86	syl2anc 584	. . . . . . . . . . . . . . . . 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 11703	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ≤ 𝑛)
91	90	biantrud 531	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
92	81, 89, 91	3bitr4d 311	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
93		breq1 5101	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (𝑘 ≤ (𝐹‘𝑥) ↔ 𝑛 ≤ (𝐹‘𝑥)))
94	7	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞))
95	94	ffvelcdmda 7029	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
96		elrege0 13370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
97	95, 96	sylib 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
98	97	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
99	98	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
100	55, 15	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℕ)
101	100	nnred 12160	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℝ)
102	99, 101	remulcld 11162	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ)
103		reflcl 13716	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ)
104	102, 103	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ)
105	100	nngt0d 12194	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝑛))
106		lemuldiv 12022	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℝ ∧ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
107	56, 104, 101, 105, 106	syl112anc 1376	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
108		lemul1 11993	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
109	56, 99, 101, 105, 108	syl112anc 1376	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
110		nnmulcl 12169	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ (2↑𝑛) ∈ ℕ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
111	55, 15, 110	syl2anc2 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
112	111	nnzd 12514	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℤ)
113		flge 13725	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑛 · (2↑𝑛)) ∈ ℤ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛)))))
114	102, 112, 113	syl2anc 584	. . . . . . . . . . . . . . . . 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 6838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
119		simpl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → 𝑚 = 𝑛)
120	119	oveq2d 7374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑛))
121	118, 120	oveq12d 7376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝑛)))
122	121	fveq2d 6838	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝑛))))
123	122, 120	oveq12d 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
124		ovex 7391	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) ∈ V
125	123, 8, 124	ovmpoa 7513	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
126	55, 116, 125	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
127	126	breq2d 5110	. . . . . . . . . . . . . . . 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 4485	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
132	131	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
133	130, 132	eleqtrrd 2839	. . . . . . . . . . . . . . 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 4099	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran (𝐺‘𝑛) ∖ {0}) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
137	136	sselda 3933	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
138		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))
139	138	rnmpt 5906	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = {𝑘 ∣ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛))}
140	139	eqabri 2878	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ↔ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)))
141		elfzelz 13440	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℤ)
142	141	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℤ)
143	142	zcnd 12597	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℂ)
144	15	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℕ)
145	144	nncnd 12161	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℂ)
146	144	nnne0d 12195	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ≠ 0)
147	143, 145, 146	divcan1d 11918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) = 𝑚)
148	147, 142	eqeltrd 2836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ)
149		oveq1 7365	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) = ((𝑚 / (2↑𝑛)) · (2↑𝑛)))
150	149	eleq1d 2821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑚 / (2↑𝑛)) → ((𝑘 · (2↑𝑛)) ∈ ℤ ↔ ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ))
151	148, 150	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
152	151	rexlimdva 3137	. . . . . . . . . . . . . . . . . . . 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 591	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑘 · (2↑𝑛)) ∈ ℤ)
156	155	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 · (2↑𝑛)) ∈ ℤ)
157		flbi 13736	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑘 · (2↑𝑛)) ∈ ℤ) → ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
158	102, 156, 157	syl2anc 584	. . . . . . . . . . . . . . 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 2994	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 ↔ 𝑘 ≠ 𝑛))
161	160	biimparc 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛)
162		iffalse 4488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑛𝐽𝑥) ≤ 𝑛 → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛)
163	162	necon1ai 2959	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 → (𝑛𝐽𝑥) ≤ 𝑛)
164	161, 163	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
165	164	iftrued 4487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
166		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
167	165, 166	eqtr3d 2773	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
168	167, 164	eqbrtrrd 5122	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → 𝑘 ≤ 𝑛)
169	168, 167	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘))
170	169	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ≠ 𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
171		breq1 5101	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛𝐽𝑥) = 𝑘 → ((𝑛𝐽𝑥) ≤ 𝑛 ↔ 𝑘 ≤ 𝑛))
172	171	biimparc 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
173	172	iftrued 4487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
174		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
175	173, 174	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
176	170, 175	impbid1 225	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ≠ 𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
177	176	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
178		eldifi 4083	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0}) → 𝑘 ∈ ran (𝐺‘𝑛))
179		nnre 12152	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
180	179	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
181	77, 180, 86	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
182	13	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ0)
183	182	nn0ge0d 12465	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝑛)
184		breq1 5101	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
185		breq1 5101	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (0 ≤ 𝑛 ↔ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
186	184, 185	ifboth 4519	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 0 ≤ 𝑛) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
187	181, 183, 186	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
188	42, 187	eqbrtrd 5120	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) ≤ 𝑛)
189	188	ralrimiva 3128	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛)
190	9	ffnd 6663	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) Fn ℝ)
191		breq1 5101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = ((𝐺‘𝑛)‘𝑥) → (𝑘 ≤ 𝑛 ↔ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
192	191	ralrn 7033	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺‘𝑛) Fn ℝ → (∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
193	190, 192	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
194	189, 193	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛)
195	194	r19.21bi 3228	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝐺‘𝑛)) → 𝑘 ≤ 𝑛)
196	178, 195	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ≤ 𝑛)
197	196	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → 𝑘 ≤ 𝑛)
198	197	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
199	126	eqeq1d 2738	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘))
200	104	recnd 11160	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℂ)
201	28, 20	sstrd 3944	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ⊆ ℝ)
202	201	ssdifssd 4099	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran (𝐺‘𝑛) ∖ {0}) ⊆ ℝ)
203	202	sselda 3933	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ∈ ℝ)
204	203	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ)
205	204	recnd 11160	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℂ)
206	100	nncnd 12161	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℂ)
207	100	nnne0d 12195	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ≠ 0)
208	200, 205, 206, 207	divmul3d 11951	. . . . . . . . . . . . . . . . 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 4491	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ≠ 𝑛 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
213	212	eleq2d 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ≠ 𝑛 → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ 𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
214	100	nnrecred 12196	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℝ)
215	204, 214	readdcld 11161	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ)
216	215	rexrd 11182	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ*)
217		elioomnf 13360	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 + (1 / (2↑𝑛))) ∈ ℝ* → ((𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
218	216, 217	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
219	94	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶(0[,)+∞))
220	219	ffnd 6663	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
221		elpreima 7003	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
222	220, 221	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
223	116, 222	mpbirand 707	. . . . . . . . . . . . . . . . . . 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 11991	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘𝑥) ∈ ℝ ∧ (𝑘 + (1 / (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
227	99, 215, 101, 105, 226	syl112anc 1376	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
228	214	recnd 11160	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℂ)
229	206, 207	recid2d 11913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((1 / (2↑𝑛)) · (2↑𝑛)) = 1)
230	229	oveq2d 7374	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 · (2↑𝑛)) + ((1 / (2↑𝑛)) · (2↑𝑛))) = ((𝑘 · (2↑𝑛)) + 1))
231	205, 206, 228, 230	joinlmuladdmuld 11159	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) = ((𝑘 · (2↑𝑛)) + 1))
232	231	breq2d 5110	. . . . . . . . . . . . . . . . . 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 11993	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
236	204, 99, 101, 105, 235	syl112anc 1376	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
237	236	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
238	234, 237	anbi12d 632	. . . . . . . . . . . . . . 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 3019	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
242		eldif 3911	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘))))
243	204	rexrd 11182	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ*)
244		elioomnf 13360	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ* → ((𝐹‘𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
245	243, 244	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
246		elpreima 7003	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)𝑘))))
247	220, 246	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)𝑘))))
248	116, 247	mpbirand 707	. . . . . . . . . . . . . . . . 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 11279	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑥) < 𝑘))
253	251, 252	bitr4d 282	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ 𝑘 ≤ (𝐹‘𝑥)))
254	253	anbi2d 630	. . . . . . . . . . . . 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 579	. . . . . . . . 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 579	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))))
261	21	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛):ℝ⟶ℝ)
262	261	ffnd 6663	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛) Fn ℝ)
263		fniniseg 7005	. . . . . . . 8 ⊢ ((𝐺‘𝑛) Fn ℝ → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
264	262, 263	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
265		elin 3917	. . . . . . . 8 ⊢ (𝑥 ∈ ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ (-𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
266	179	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑛 ∈ ℝ)
267	266	renegcld 11564	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → -𝑛 ∈ ℝ)
268		iccmbl 25523	. . . . . . . . . . . . 13 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ∈ dom vol)
269	267, 266, 268	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (-𝑛[,]𝑛) ∈ dom vol)
270		mblss 25488	. . . . . . . . . . . 12 ⊢ ((-𝑛[,]𝑛) ∈ dom vol → (-𝑛[,]𝑛) ⊆ ℝ)
271	269, 270	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
272	271	sseld 3932	. . . . . . . . . 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 2734	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) = ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
278		rembl 25497	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
279		fss 6678	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
280	7, 58, 279	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
281		mbfima 25587	. . . . . . . . . 10 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
282	6, 280, 281	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
283		ifcl 4525	. . . . . . . . 9 ⊢ ((ℝ ∈ dom vol ∧ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol) → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
284	278, 282, 283	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
285		mbfima 25587	. . . . . . . . 9 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
286	6, 280, 285	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
287		difmbl 25500	. . . . . . . 8 ⊢ ((if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol ∧ (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol) → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
288	284, 286, 287	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
289	288	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
290		inmbl 25499	. . . . . 6 ⊢ (((-𝑛[,]𝑛) ∈ dom vol ∧ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
291	269, 289, 290	syl2anc 584	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((-𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
292	277, 291	eqeltrd 2836	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) ∈ dom vol)
293		mblvol 25487	. . . . . 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 4526	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
298		0re 11134	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
299		ifcl 4525	. . . . . . . . . . . . . . 15 ⊢ ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
300	297, 298, 299	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
301	39	fvmpt2 6952	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
302	33, 300, 301	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
303	32, 302	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
304	303	adantlr 715	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ (-𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
305	304	eqeq1d 2738	. . . . . . . . . 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 3939	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛))
310		iccssre 13345	. . . . . . 7 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (-𝑛[,]𝑛) ⊆ ℝ)
311	267, 266, 310	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (-𝑛[,]𝑛) ⊆ ℝ)
312		mblvol 25487	. . . . . . . 8 ⊢ ((-𝑛[,]𝑛) ∈ dom vol → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
313	269, 312	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) = (vol*‘(-𝑛[,]𝑛)))
314		iccvolcl 25524	. . . . . . . 8 ⊢ ((-𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
315	267, 266, 314	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(-𝑛[,]𝑛)) ∈ ℝ)
316	313, 315	eqeltrrd 2837	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol*‘(-𝑛[,]𝑛)) ∈ ℝ)
317		ovolsscl 25443	. . . . . 6 ⊢ (((◡(𝐺‘𝑛) “ {𝑘}) ⊆ (-𝑛[,]𝑛) ∧ (-𝑛[,]𝑛) ⊆ ℝ ∧ (vol*‘(-𝑛[,]𝑛)) ∈ ℝ) → (vol*‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
318	309, 311, 316, 317	syl3anc 1373	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol*‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
319	294, 318	eqeltrd 2836	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
320	21, 29, 292, 319	i1fd 25638	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ dom ∫1)
321	320	ralrimiva 3128	. 2 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ dom ∫1)
322		ffnfv 7064	. 2 ⊢ (𝐺:ℕ⟶dom ∫1 ↔ (𝐺 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ dom ∫1))
323	5, 321, 322	sylanbrc 583	1 ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫1)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  Vcvv 3440   ∖ cdif 3898   ∩ cin 3900   ⊆ wss 3901  ifcif 4479  {csn 4580   class class class wbr 5098   ↦ cmpt 5179   × cxp 5622  ^◡ccnv 5623  dom cdm 5624  ran crn 5625   “ cima 5627   Fn wfn 6487  ⟶wf 6488  –onto→wfo 6490  ‘cfv 6492  (class class class)co 7358   ∈ cmpo 7360  Fincfn 8883  ℝcr 11025  0cc0 11026  1c1 11027   + caddc 11029   · cmul 11031  +∞cpnf 11163  -∞cmnf 11164  ℝ^*cxr 11165   < clt 11166   ≤ cle 11167  -cneg 11365   / cdiv 11794  ℕcn 12145  2c2 12200  ℕ₀cn0 12401  ℤcz 12488  (,)cioo 13261  [,)cico 13263  [,]cicc 13264  ...cfz 13423  ⌊cfl 13710  ↑cexp 13984  vol*covol 25419  volcvol 25420  MblFncmbf 25571  ∫₁citg1 25572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-inf2 9550  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103  ax-pre-sup 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7622  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-2o 8398  df-er 8635  df-map 8765  df-pm 8766  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fi 9314  df-sup 9345  df-inf 9346  df-oi 9415  df-dju 9813  df-card 9851  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-div 11795  df-nn 12146  df-2 12208  df-3 12209  df-n0 12402  df-z 12489  df-uz 12752  df-q 12862  df-rp 12906  df-xneg 13026  df-xadd 13027  df-xmul 13028  df-ioo 13265  df-ico 13267  df-icc 13268  df-fz 13424  df-fzo 13571  df-fl 13712  df-seq 13925  df-exp 13985  df-hash 14254  df-cj 15022  df-re 15023  df-im 15024  df-sqrt 15158  df-abs 15159  df-clim 15411  df-rlim 15412  df-sum 15610  df-rest 17342  df-topgen 17363  df-psmet 21301  df-xmet 21302  df-met 21303  df-bl 21304  df-mopn 21305  df-top 22838  df-topon 22855  df-bases 22890  df-cmp 23331  df-ovol 25421  df-vol 25422  df-mbf 25576  df-itg1 25577

This theorem is referenced by:  mbfi1fseqlem5  25676  mbfi1fseqlem6  25677