Theorem mbfi1fseqlem4 26072

Description: Lemma for mbfi1fseq 26075. 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 11321	. . . . 5 ⊢ ℝ ∈ V
2	1	mptex 7255	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ( -𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)) ∈ V
3		mbfi1fseq.4	. . . 4 ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ( -𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))
4	2, 3	fnmpti 6707	. . 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 26071	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛):ℝ⟶ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
10		elfznn0 13784	. . . . . . . . 9 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℕ0)
11	10	nn0red 12698	. . . . . . . 8 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℝ)
12		2nn 12446	. . . . . . . . . 10 ⊢ 2 ∈ ℕ
13		nnnn0 12643	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
14		nnexpcl 14247	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
15	12, 13, 14	sylancr 599	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
16	15	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℕ)
17		nndivre 12409	. . . . . . . 8 ⊢ ((𝑚 ∈ ℝ ∧ (2↑𝑛) ∈ ℕ) → (𝑚 / (2↑𝑛)) ∈ ℝ)
18	11, 16, 17	syl2anr 609	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑚 / (2↑𝑛)) ∈ ℝ)
19	18	fmpttd 7142	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ℝ)
20	19	frnd 6743	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ⊆ ℝ)
21	9, 20	fssd 6752	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛):ℝ⟶ℝ)
22		fzfid 14146	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (0...(𝑛 · (2↑𝑛))) ∈ Fin)
23	19	ffnd 6735	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))))
24		dffn4 6827	. . . . . . 7 ⊢ ((𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) Fn (0...(𝑛 · (2↑𝑛))) ↔ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ontoran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
25	23, 24	sylib 221	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ontoran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
26		fofi 9336	. . . . . 6 ⊢ (((0...(𝑛 · (2↑𝑛))) ∈ Fin ∧ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))):(0...(𝑛 · (2↑𝑛)))⟶ontoran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
27	22, 25, 26	syl2anc 596	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ∈ Fin)
28	9	frnd 6743	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
29	27, 28	ssfid 9291	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ∈ Fin)
30	6, 7, 8, 3	mbfi1fseqlem2 26070	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)))
31	30	fveq1d 6913	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝐺‘𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
32	31	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥))
33		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
34		ovex 7479	. . . . . . . . . . . . . . 15 ⊢ (𝑛𝐽𝑥) ∈ V
35		vex 3458	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ∈ V
36	34, 35	ifex 4536	. . . . . . . . . . . . . 14 ⊢ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ V
37		c0ex 11330	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
38	36, 37	ifex 4536	. . . . . . . . . . . . 13 ⊢ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V
39		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
40	39	fvmpt2 7031	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
41	33, 38, 40	sylancl 598	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
42	32, 41	eqtrd 2798	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
43	42	adantlr 728	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
44	43	eqeq1d 2765	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
45		eldifsni 4753	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0}) → 𝑘 ≠ 0)
46	45	ad2antlr 740	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ≠ 0)
47		neeq1 3021	. . . . . . . . . . . 12 ⊢ (if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → (if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 ↔ 𝑘 ≠ 0))
48	46, 47	syl5ibrcom 250	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0))
49		iffalse 4494	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ ( -𝑛[,]𝑛) → if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 0)
50	49	necon1ai 2986	. . . . . . . . . . 11 ⊢ (if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≠ 0 → 𝑥 ∈ ( -𝑛[,]𝑛))
51	48, 50	syl6 36	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 → 𝑥 ∈ ( -𝑛[,]𝑛)))
52	51	pm4.71rd 572	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ (𝑥 ∈ ( -𝑛[,]𝑛) ∧ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘)))
53		iftrue 4491	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ( -𝑛[,]𝑛) → if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))
54	53	eqeq1d 2765	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ( -𝑛[,]𝑛) → (if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘))
55		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ)
56	55	nnred 12380	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
57	56	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ∈ ℝ)
58		rge0ssre 13617	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0[,)+∞) ⊆ ℝ
59		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
60		ffvelcdm 7108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ 𝑦 ∈ ℝ) → (𝐹‘𝑦) ∈ (0[,)+∞))
61	7, 59, 60	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ (0[,)+∞))
62	58, 61	sselid 3911	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (𝐹‘𝑦) ∈ ℝ)
63		nnnn0 12643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
64		nnexpcl 14247	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ0) → (2↑𝑚) ∈ ℕ)
65	12, 63, 64	sylancr 599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 ∈ ℕ → (2↑𝑚) ∈ ℕ)
66	65	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℕ)
67	66	nnred 12380	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (2↑𝑚) ∈ ℝ)
68	62, 67	remulcld 11369	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ)
69		reflcl 13966	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹‘𝑦) · (2↑𝑚)) ∈ ℝ → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
70	68, 69	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) ∈ ℝ)
71	70, 66	nndivred 12422	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑚 ∈ ℕ ∧ 𝑦 ∈ ℝ)) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
72	71	ralrimivva 3209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ)
73	8	fmpo 8107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑚 ∈ ℕ ∀𝑦 ∈ ℝ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) ∈ ℝ ↔ 𝐽:(ℕ × ℝ)⟶ℝ)
74	72, 73	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶ℝ)
75		fovcdm 7618	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽:(ℕ × ℝ)⟶ℝ ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
76	74, 75	syl3an1 1181	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
77	76	3expa 1136	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
78	77	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) ∈ ℝ)
79	78	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛𝐽𝑥) ∈ ℝ)
80		lemin 13352	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
81	57, 79, 57, 80	syl3anc 1399	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
82	79, 57	ifcld 4532	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
83	82, 57	letri3d 11482	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛 ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
84		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
85	84	eqeq2d 2774	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛))
86		min2 13350	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑛𝐽𝑥) ∈ ℝ ∧ 𝑛 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
87	79, 57, 86	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
88	87	biantrurd 542	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ↔ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛))))
89	83, 85, 88	3bitr4d 314	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ 𝑛 ≤ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛)))
90	57	leidd 11912	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑛 ≤ 𝑛)
91	90	biantrud 541	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ (𝑛 ≤ (𝑛𝐽𝑥) ∧ 𝑛 ≤ 𝑛)))
92	81, 89, 91	3bitr4d 314	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
93		breq1 5109	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑛 → (𝑘 ≤ (𝐹‘𝑥) ↔ 𝑛 ≤ (𝐹‘𝑥)))
94	7	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℝ⟶(0[,)+∞))
95	94	ffvelcdmda 7111	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
96		elrege0 13615	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
97	95, 96	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
98	97	simpld 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
99	98	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
100	55, 15	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℕ)
101	100	nnred 12380	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℝ)
102	99, 101	remulcld 11369	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ)
103		reflcl 13966	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ)
104	102, 103	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ)
105	100	nngt0d 12417	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 0 < (2↑𝑛))
106		lemuldiv 12227	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℝ ∧ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
107	56, 104, 101, 105, 106	syl112anc 1402	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
108		lemul1 12199	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
109	56, 99, 101, 105, 108	syl112anc 1402	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
110		nnmulcl 12389	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ (2↑𝑛) ∈ ℕ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
111	55, 15, 110	syl2anc2 597	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℕ)
112	111	nnzd 12749	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 · (2↑𝑛)) ∈ ℤ)
113		flge 13975	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑛 · (2↑𝑛)) ∈ ℤ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛)))))
114	102, 112, 113	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛)))))
115	109, 114	bitrd 282	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹‘𝑥) ↔ (𝑛 · (2↑𝑛)) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑛)))))
116		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
117		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
118	117	fveq2d 6915	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥))
119		simpl 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → 𝑚 = 𝑛)
120	119	oveq2d 7462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑛))
121	118, 120	oveq12d 7464	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝑛)))
122	121	fveq2d 6915	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝑛))))
123	122, 120	oveq12d 7464	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑚 = 𝑛 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
124		ovex 7479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) ∈ V
125	123, 8, 124	ovmpoa 7602	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
126	55, 116, 125	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)))
127	126	breq2d 5118	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝑛𝐽𝑥) ↔ 𝑛 ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛))))
128	107, 115, 127	3bitr4d 314	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑛 ≤ (𝐹‘𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
129	93, 128	sylan9bbr 520	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹‘𝑥) ↔ 𝑛 ≤ (𝑛𝐽𝑥)))
130	116	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ ℝ)
131		iftrue 4491	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
132	131	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = ℝ)
133	130, 132	eleqtrrd 2867	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → 𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
134	133	biantrurd 542	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
135	92, 129, 134	3bitr2d 310	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 = 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
136	28	ssdifssd 4086	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran (𝐺‘𝑛) ∖ {0}) ⊆ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
137	136	sselda 3913	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))))
138		eqid 2763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))
139	138	rnmpt 5947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) = {𝑘 ∣ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛))}
140	139	eqabri 2906	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) ↔ ∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)))
141		elfzelz 13686	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) → 𝑚 ∈ ℤ)
142	141	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℤ)
143	142	zcnd 12834	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → 𝑚 ∈ ℂ)
144	15	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℕ)
145	144	nncnd 12381	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ∈ ℂ)
146	144	nnne0d 12418	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (2↑𝑛) ≠ 0)
147	143, 145, 146	divcan1d 12124	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) = 𝑚)
148	147, 142	eqeltrd 2864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ)
149		oveq1 7453	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) = ((𝑚 / (2↑𝑛)) · (2↑𝑛)))
150	149	eleq1d 2849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = (𝑚 / (2↑𝑛)) → ((𝑘 · (2↑𝑛)) ∈ ℤ ↔ ((𝑚 / (2↑𝑛)) · (2↑𝑛)) ∈ ℤ))
151	148, 150	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 · (2↑𝑛)))) → (𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
152	151	rexlimdva 3167	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑚 ∈ (0...(𝑛 · (2↑𝑛)))𝑘 = (𝑚 / (2↑𝑛)) → (𝑘 · (2↑𝑛)) ∈ ℤ))
153	140, 152	biimtrid 245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛))) → (𝑘 · (2↑𝑛)) ∈ ℤ))
154	153	imp 412	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝑚 ∈ (0...(𝑛 · (2↑𝑛))) ↦ (𝑚 / (2↑𝑛)))) → (𝑘 · (2↑𝑛)) ∈ ℤ)
155	137, 154	syldan 603	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑘 · (2↑𝑛)) ∈ ℤ)
156	155	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 · (2↑𝑛)) ∈ ℤ)
157		flbi 13986	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑥) · (2↑𝑛)) ∈ ℝ ∧ (𝑘 · (2↑𝑛)) ∈ ℤ) → ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
158	102, 156, 157	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
159	158	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
160		neeq1 3021	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 ↔ 𝑘 ≠ 𝑛))
161	160	biimparc 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛)
162		iffalse 4494	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ (𝑛𝐽𝑥) ≤ 𝑛 → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑛)
163	162	necon1ai 2986	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≠ 𝑛 → (𝑛𝐽𝑥) ≤ 𝑛)
164	161, 163	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
165	164	iftrued 4493	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
166		simpr 490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
167	165, 166	eqtr3d 2800	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
168	167, 164	eqbrtrrd 5133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → 𝑘 ≤ 𝑛)
169	168, 167	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≠ 𝑛 ∧ if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘) → (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘))
170	169	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ≠ 𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 → (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
171		breq1 5109	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛𝐽𝑥) = 𝑘 → ((𝑛𝐽𝑥) ≤ 𝑛 ↔ 𝑘 ≤ 𝑛))
172	171	biimparc 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) ≤ 𝑛)
173	172	iftrued 4493	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = (𝑛𝐽𝑥))
174		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → (𝑛𝐽𝑥) = 𝑘)
175	173, 174	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘)
176	170, 175	impbid1 228	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ≠ 𝑛 → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
177	176	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
178		eldifi 4070	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0}) → 𝑘 ∈ ran (𝐺‘𝑛))
179		nnre 12372	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
180	179	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℝ)
181	77, 180, 86	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛)
182	13	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 𝑛 ∈ ℕ0)
183	182	nn0ge0d 12700	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝑛)
184		breq1 5109	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ↔ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
185		breq1 5109	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 = if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) → (0 ≤ 𝑛 ↔ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛))
186	184, 185	ifboth 4525	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ≤ 𝑛 ∧ 0 ≤ 𝑛) → if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
187	181, 183, 186	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ≤ 𝑛)
188	42, 187	eqbrtrd 5131	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) ≤ 𝑛)
189	188	ralrimiva 3158	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛)
190	9	ffnd 6735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) Fn ℝ)
191		breq1 5109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = ((𝐺‘𝑛)‘𝑥) → (𝑘 ≤ 𝑛 ↔ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
192	191	ralrn 7115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺‘𝑛) Fn ℝ → (∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
193	190, 192	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛 ↔ ∀𝑥 ∈ ℝ ((𝐺‘𝑛)‘𝑥) ≤ 𝑛))
194	189, 193	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ ran (𝐺‘𝑛)𝑘 ≤ 𝑛)
195	194	r19.21bi 3258	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ ran (𝐺‘𝑛)) → 𝑘 ≤ 𝑛)
196	178, 195	sylan2 605	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ≤ 𝑛)
197	196	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → 𝑘 ≤ 𝑛)
198	197	biantrurd 542	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (𝑘 ≤ 𝑛 ∧ (𝑛𝐽𝑥) = 𝑘)))
199	126	eqeq1d 2765	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ ((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘))
200	104	recnd 11367	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹‘𝑥) · (2↑𝑛))) ∈ ℂ)
201	28, 20	sstrd 3923	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝐺‘𝑛) ⊆ ℝ)
202	201	ssdifssd 4086	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (ran (𝐺‘𝑛) ∖ {0}) ⊆ ℝ)
203	202	sselda 3913	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑘 ∈ ℝ)
204	203	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ)
205	204	recnd 11367	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℂ)
206	100	nncnd 12381	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ∈ ℂ)
207	100	nnne0d 12418	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (2↑𝑛) ≠ 0)
208	200, 205, 206, 207	divmul3d 12157	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹‘𝑥) · (2↑𝑛))) / (2↑𝑛)) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
209	199, 208	bitrd 282	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
210	209	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑛𝐽𝑥) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
211	177, 198, 210	3bitr2d 310	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑛))) = (𝑘 · (2↑𝑛))))
212		ifnefalse 4497	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ≠ 𝑛 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) = (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
213	212	eleq2d 2850	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ≠ 𝑛 → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ 𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
214	100	nnrecred 12419	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℝ)
215	204, 214	readdcld 11368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ)
216	215	rexrd 11389	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 + (1 / (2↑𝑛))) ∈ ℝ*)
217		elioomnf 13605	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 + (1 / (2↑𝑛))) ∈ ℝ* → ((𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
218	216, 217	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
219	94	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹:ℝ⟶(0[,)+∞))
220	219	ffnd 6735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
221		elpreima 7083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
222	220, 221	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))))
223	116, 222	mpbirand 720	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹‘𝑥) ∈ (-∞(,)(𝑘 + (1 / (2↑𝑛))))))
224	99	biantrurd 542	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))))))
225	218, 223, 224	3bitr4d 314	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ (𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛)))))
226		ltmul1 12197	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘𝑥) ∈ ℝ ∧ (𝑘 + (1 / (2↑𝑛))) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
227	99, 215, 101, 105, 226	syl112anc 1402	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) < (𝑘 + (1 / (2↑𝑛))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛))))
228	214	recnd 11367	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (1 / (2↑𝑛)) ∈ ℂ)
229	206, 207	recid2d 12119	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((1 / (2↑𝑛)) · (2↑𝑛)) = 1)
230	229	oveq2d 7462	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 · (2↑𝑛)) + ((1 / (2↑𝑛)) · (2↑𝑛))) = ((𝑘 · (2↑𝑛)) + 1))
231	205, 206, 228, 230	joinlmuladdmuld 11366	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) = ((𝑘 · (2↑𝑛)) + 1))
232	231	breq2d 5118	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 + (1 / (2↑𝑛))) · (2↑𝑛)) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
233	225, 227, 232	3bitrd 308	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
234	213, 233	sylan9bbr 520	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ↔ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1)))
235		lemul1 12199	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
236	204, 99, 101, 105, 235	syl112anc 1402	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
237	236	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (𝑘 ≤ (𝐹‘𝑥) ↔ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛))))
238	234, 237	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥)) ↔ (((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1) ∧ (𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)))))
239	238	biancomd 469	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥)) ↔ ((𝑘 · (2↑𝑛)) ≤ ((𝐹‘𝑥) · (2↑𝑛)) ∧ ((𝐹‘𝑥) · (2↑𝑛)) < ((𝑘 · (2↑𝑛)) + 1))))
240	159, 211, 239	3bitr4d 314	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑘 ≠ 𝑛) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
241	135, 240	pm2.61dane 3046	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
242		eldif 4052	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘))))
243	204	rexrd 11389	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → 𝑘 ∈ ℝ*)
244		elioomnf 13605	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℝ* → ((𝐹‘𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
245	243, 244	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (-∞(,)𝑘) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
246		elpreima 7083	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)𝑘))))
247	220, 246	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (-∞(,)𝑘))))
248	116, 247	mpbirand 720	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝐹‘𝑥) ∈ (-∞(,)𝑘)))
249	99	biantrurd 542	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) < 𝑘 ↔ ((𝐹‘𝑥) ∈ ℝ ∧ (𝐹‘𝑥) < 𝑘)))
250	245, 248, 249	3bitr4d 314	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ (𝐹‘𝑥) < 𝑘))
251	250	notbid 321	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ ¬ (𝐹‘𝑥) < 𝑘))
252	204, 99	lenltd 11486	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑘 ≤ (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑥) < 𝑘))
253	251, 252	bitr4d 285	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘)) ↔ 𝑘 ≤ (𝐹‘𝑥)))
254	253	anbi2d 642	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ ¬ 𝑥 ∈ (◡𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
255	242, 254	bitrid 286	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ↔ (𝑥 ∈ if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∧ 𝑘 ≤ (𝐹‘𝑥))))
256	241, 255	bitr4d 285	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) = 𝑘 ↔ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
257	54, 256	sylan9bbr 520	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) ∧ 𝑥 ∈ ( -𝑛[,]𝑛)) → (if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘 ↔ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
258	257	pm5.32da 590	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ( -𝑛[,]𝑛) ∧ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘) ↔ (𝑥 ∈ ( -𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))))))
259	44, 52, 258	3bitrd 308	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 ↔ (𝑥 ∈ ( -𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))))))
260	259	pm5.32da 590	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ ( -𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))))
261	21	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛):ℝ⟶ℝ)
262	261	ffnd 6735	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛) Fn ℝ)
263		fniniseg 7086	. . . . . . . 8 ⊢ ((𝐺‘𝑛) Fn ℝ → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
264	262, 263	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
265		elin 4096	. . . . . . . 8 ⊢ (𝑥 ∈ (( -𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ( -𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
266	179	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → 𝑛 ∈ ℝ)
267	266	renegcld 11773	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → -𝑛 ∈ ℝ)
268		iccmbl 25920	. . . . . . . . . . . . 13 ⊢ (( -𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ( -𝑛[,]𝑛) ∈ dom vol)
269	267, 266, 268	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ( -𝑛[,]𝑛) ∈ dom vol)
270		mblss 25885	. . . . . . . . . . . 12 ⊢ (( -𝑛[,]𝑛) ∈ dom vol → ( -𝑛[,]𝑛) ⊆ ℝ)
271	269, 270	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ( -𝑛[,]𝑛) ⊆ ℝ)
272	271	sseld 3912	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ ( -𝑛[,]𝑛) → 𝑥 ∈ ℝ))
273	272	adantrd 497	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ ( -𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) → 𝑥 ∈ ℝ))
274	273	pm4.71rd 572	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ ( -𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ ( -𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))))
275	265, 274	bitrid 286	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (( -𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ↔ (𝑥 ∈ ℝ ∧ (𝑥 ∈ ( -𝑛[,]𝑛) ∧ 𝑥 ∈ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))))
276	260, 264, 275	3bitr4d 314	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ 𝑥 ∈ (( -𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))))))
277	276	eqrdv 2761	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) = (( -𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))))
278		rembl 25894	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
279		fss 6751	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
280	7, 58, 279	sylancl 598	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
281		mbfima 25984	. . . . . . . . . 10 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
282	6, 280, 281	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol)
283		ifcl 4531	. . . . . . . . 9 ⊢ ((ℝ ∈ dom vol ∧ (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛))))) ∈ dom vol) → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
284	278, 282, 283	sylancr 599	. . . . . . . 8 ⊢ (𝜑 → if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol)
285		mbfima 25984	. . . . . . . . 9 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
286	6, 280, 285	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol)
287		difmbl 25897	. . . . . . . 8 ⊢ ((if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∈ dom vol ∧ (◡𝐹 “ (-∞(,)𝑘)) ∈ dom vol) → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
288	284, 286, 287	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
289	288	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol)
290		inmbl 25896	. . . . . 6 ⊢ ((( -𝑛[,]𝑛) ∈ dom vol ∧ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘))) ∈ dom vol) → (( -𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
291	269, 289, 290	syl2anc 596	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (( -𝑛[,]𝑛) ∩ (if(𝑘 = 𝑛, ℝ, (◡𝐹 “ (-∞(,)(𝑘 + (1 / (2↑𝑛)))))) ∖ (◡𝐹 “ (-∞(,)𝑘)))) ∈ dom vol)
292	277, 291	eqeltrd 2864	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) ∈ dom vol)
293		mblvol 25884	. . . . . 6 ⊢ ((◡(𝐺‘𝑛) “ {𝑘}) ∈ dom vol → (vol‘(◡(𝐺‘𝑛) “ {𝑘})) = (vol*‘(◡(𝐺‘𝑛) “ {𝑘})))
294	292, 293	syl 18	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(◡(𝐺‘𝑛) “ {𝑘})) = (vol*‘(◡(𝐺‘𝑛) “ {𝑘})))
295	190	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝐺‘𝑛) Fn ℝ)
296	295, 263	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) ↔ (𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘)))
297	77, 180	ifcld 4532	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ)
298		0re 11340	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℝ
299		ifcl 4531	. . . . . . . . . . . . . . 15 ⊢ ((if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
300	297, 298, 299	sylancl 598	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ)
301	39	fvmpt2 7031	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
302	33, 300, 301	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))‘𝑥) = if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
303	32, 302	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
304	303	adantlr 728	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → ((𝐺‘𝑛)‘𝑥) = if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0))
305	304	eqeq1d 2765	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 ↔ if(𝑥 ∈ ( -𝑛[,]𝑛), if((𝑛𝐽𝑥) ≤ 𝑛, (𝑛𝐽𝑥), 𝑛), 0) = 𝑘))
306	305, 51	sylbid 243	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) ∧ 𝑥 ∈ ℝ) → (((𝐺‘𝑛)‘𝑥) = 𝑘 → 𝑥 ∈ ( -𝑛[,]𝑛)))
307	306	expimpd 459	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ((𝑥 ∈ ℝ ∧ ((𝐺‘𝑛)‘𝑥) = 𝑘) → 𝑥 ∈ ( -𝑛[,]𝑛)))
308	296, 307	sylbid 243	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (𝑥 ∈ (◡(𝐺‘𝑛) “ {𝑘}) → 𝑥 ∈ ( -𝑛[,]𝑛)))
309	308	ssrdv 3919	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (◡(𝐺‘𝑛) “ {𝑘}) ⊆ ( -𝑛[,]𝑛))
310		iccssre 13590	. . . . . . 7 ⊢ (( -𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ( -𝑛[,]𝑛) ⊆ ℝ)
311	267, 266, 310	syl2anc 596	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → ( -𝑛[,]𝑛) ⊆ ℝ)
312		mblvol 25884	. . . . . . . 8 ⊢ (( -𝑛[,]𝑛) ∈ dom vol → (vol‘( -𝑛[,]𝑛)) = (vol*‘( -𝑛[,]𝑛)))
313	269, 312	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘( -𝑛[,]𝑛)) = (vol*‘( -𝑛[,]𝑛)))
314		iccvolcl 25921	. . . . . . . 8 ⊢ (( -𝑛 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (vol‘( -𝑛[,]𝑛)) ∈ ℝ)
315	267, 266, 314	syl2anc 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘( -𝑛[,]𝑛)) ∈ ℝ)
316	313, 315	eqeltrrd 2865	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol*‘( -𝑛[,]𝑛)) ∈ ℝ)
317		ovolsscl 25840	. . . . . 6 ⊢ (((◡(𝐺‘𝑛) “ {𝑘}) ⊆ ( -𝑛[,]𝑛) ∧ ( -𝑛[,]𝑛) ⊆ ℝ ∧ (vol*‘( -𝑛[,]𝑛)) ∈ ℝ) → (vol*‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
318	309, 311, 316, 317	syl3anc 1399	. . . . 5 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol*‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
319	294, 318	eqeltrd 2864	. . . 4 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ran (𝐺‘𝑛) ∖ {0})) → (vol‘(◡(𝐺‘𝑛) “ {𝑘})) ∈ ℝ)
320	21, 29, 292, 319	i1fd 26035	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ dom ∫1)
321	320	ralrimiva 3158	. 2 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ dom ∫1)
322		ffnfv 7146	. 2 ⊢ (𝐺:ℕ⟶dom ∫1 ↔ (𝐺 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝐺‘𝑛) ∈ dom ∫1))
323	5, 321, 322	sylanbrc 595	1 ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫1)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092  ifcif 4485  {csn 4588   class class class wbr 5106   ↦ cmpt 5190   × cxp 5654  ^◡ccnv 5655  dom cdm 5656  ran crn 5657   “ cima 5659   Fn wfn 6556  ⟶wf 6557  ⟶ontowfo 6559  ‘cfv 6561  (class class class)co 7446   ∈ cmpo 7448  Fincfn 9004  ℝcr 11229  0cc0 11230  1c1 11231   + caddc 11233   · cmul 11235  +∞cpnf 11370  -∞cmnf 11371  ℝ^*cxr 11372   < clt 11373   ≤ cle 11374   -cneg 11572   / cdiv 12003  ℕcn 12365  2c2 12427  ℕ₀cn0 12636  ℤcz 12723  (,)cioo 13506  [,)cico 13508  [,]cicc 13509  ...cfz 13669  ⌊cfl 13960  ↑cexp 14234  vol*covol 25816  volcvol 25817  MblFncmbf 25968  ∫₁citg1 25969

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5236  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-inf2 9672  ax-cnex 11286  ax-resscn 11287  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-addrcl 11291  ax-mulcl 11292  ax-mulrcl 11293  ax-mulcom 11294  ax-addass 11295  ax-mulass 11296  ax-distr 11297  ax-i2m1 11298  ax-1ne0 11299  ax-1rid 11300  ax-rnegex 11301  ax-rrecex 11302  ax-cnre 11303  ax-pre-lttri 11304  ax-pre-lttrn 11305  ax-pre-ltadd 11306  ax-pre-mulgt0 11307  ax-pre-sup 11308

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-se 5610  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7403  df-ov 7449  df-oprab 7450  df-mpo 7451  df-of 7720  df-om 7905  df-1st 8028  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-1o 8507  df-2o 8508  df-er 8748  df-map 8880  df-pm 8881  df-en 9005  df-dom 9006  df-sdom 9007  df-fin 9008  df-fi 9433  df-sup 9464  df-inf 9465  df-oi 9534  df-dju 10012  df-card 10050  df-pnf 11375  df-mnf 11376  df-xr 11377  df-ltxr 11378  df-le 11379  df-sub 11573  df-neg 11574  df-div 12004  df-nn 12366  df-2 12435  df-3 12436  df-n0 12637  df-z 12724  df-uz 12996  df-q 13106  df-rp 13151  df-xneg 13271  df-xadd 13272  df-xmul 13273  df-ioo 13510  df-ico 13512  df-icc 13513  df-fz 13670  df-fzo 13819  df-fl 13962  df-seq 14175  df-exp 14235  df-hash 14505  df-cj 15298  df-re 15299  df-im 15300  df-sqrt 15434  df-abs 15435  df-clim 15687  df-rlim 15688  df-sum 15886  df-rest 17625  df-topgen 17646  df-psmet 21703  df-xmet 21704  df-met 21705  df-bl 21706  df-mopn 21707  df-top 23245  df-topon 23262  df-bases 23297  df-cmp 23738  df-ovol 25818  df-vol 25819  df-mbf 25973  df-itg1 25974

This theorem is used by:  mbfi1fseqlem5  26073  mbfi1fseqlem6  26074