Theorem ulm2 24139

Description: Simplify ulmval 24134 when 𝐹 and 𝐺 are known to be functions. (Contributed by Mario Carneiro, 26-Feb-2015.)

Hypotheses

Ref	Expression
ulm2.z	⊢ 𝑍 = (ℤ≥‘𝑀)
ulm2.m	⊢ (𝜑 → 𝑀 ∈ ℤ)
ulm2.f	⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
ulm2.b	⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵)
ulm2.a	⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴)
ulm2.g	⊢ (𝜑 → 𝐺:𝑆⟶ℂ)
ulm2.s	⊢ (𝜑 → 𝑆 ∈ 𝑉)

Assertion

Ref	Expression
ulm2	⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))

Distinct variable groups:   𝑗,𝑘,𝑥,𝑧,𝐹   𝑗,𝐺,𝑘,𝑥,𝑧   𝑗,𝑀,𝑘,𝑥,𝑧   𝜑,𝑗,𝑘,𝑥,𝑧   𝐴,𝑗,𝑘,𝑥   𝑥,𝐵   𝑆,𝑗,𝑘,𝑥,𝑧   𝑗,𝑍,𝑥

Allowed substitution hints:   𝐴(𝑧)   𝐵(𝑧,𝑗,𝑘)   𝑉(𝑥,𝑧,𝑗,𝑘)   𝑍(𝑧,𝑘)

Proof of Theorem ulm2

Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ulm2.s	. . 3 ⊢ (𝜑 → 𝑆 ∈ 𝑉)
2		ulmval 24134	. . 3 ⊢ (𝑆 ∈ 𝑉 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)))
4		3anan12 1051	. . . 4 ⊢ ((𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝐺:𝑆⟶ℂ ∧ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)))
5		ulm2.z	. . . . . . . . . 10 ⊢ 𝑍 = (ℤ≥‘𝑀)
6		ulm2.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
7		fdm 6051	. . . . . . . . . . . 12 ⊢ (𝐹:𝑍⟶(ℂ ↑𝑚 𝑆) → dom 𝐹 = 𝑍)
8	6, 7	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = 𝑍)
9		fdm 6051	. . . . . . . . . . 11 ⊢ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) → dom 𝐹 = (ℤ≥‘𝑛))
10	8, 9	sylan9req 2677	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆)) → 𝑍 = (ℤ≥‘𝑛))
11	5, 10	syl5eqr 2670	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆)) → (ℤ≥‘𝑀) = (ℤ≥‘𝑛))
12		ulm2.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℤ)
13	12	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆)) → 𝑀 ∈ ℤ)
14		uz11 11710	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℤ → ((ℤ≥‘𝑀) = (ℤ≥‘𝑛) ↔ 𝑀 = 𝑛))
15	13, 14	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆)) → ((ℤ≥‘𝑀) = (ℤ≥‘𝑛) ↔ 𝑀 = 𝑛))
16	11, 15	mpbid 222	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆)) → 𝑀 = 𝑛)
17	16	eqcomd 2628	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆)) → 𝑛 = 𝑀)
18		fveq2 6191	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑀 → (ℤ≥‘𝑛) = (ℤ≥‘𝑀))
19	18, 5	syl6eqr 2674	. . . . . . . . . 10 ⊢ (𝑛 = 𝑀 → (ℤ≥‘𝑛) = 𝑍)
20	19	feq2d 6031	. . . . . . . . 9 ⊢ (𝑛 = 𝑀 → (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ↔ 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)))
21	20	biimparc 504	. . . . . . . 8 ⊢ ((𝐹:𝑍⟶(ℂ ↑𝑚 𝑆) ∧ 𝑛 = 𝑀) → 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆))
22	6, 21	sylan 488	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆))
23	17, 22	impbida 877	. . . . . 6 ⊢ (𝜑 → (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ↔ 𝑛 = 𝑀))
24	23	anbi1d 741	. . . . 5 ⊢ (𝜑 → ((𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)))
25		ulm2.g	. . . . . 6 ⊢ (𝜑 → 𝐺:𝑆⟶ℂ)
26	25	biantrurd 529	. . . . 5 ⊢ (𝜑 → ((𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝐺:𝑆⟶ℂ ∧ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))))
27		simp-4l 806	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → 𝜑)
28		simpr 477	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝑛 = 𝑀)
29		uzid 11702	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
30	12, 29	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀))
31	30, 5	syl6eleqr 2712	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ 𝑍)
32	31	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝑀 ∈ 𝑍)
33	28, 32	eqeltrd 2701	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝑛 ∈ 𝑍)
34	5	uztrn2 11705	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ 𝑍)
35	33, 34	sylan 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ 𝑍)
36	5	uztrn2 11705	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍)
37	35, 36	sylan 488	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍)
38	37	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → 𝑘 ∈ 𝑍)
39		simpr 477	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆)
40		ulm2.b	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵)
41	27, 38, 39, 40	syl12anc 1324	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑘)‘𝑧) = 𝐵)
42		ulm2.a	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴)
43	27, 42	sylancom 701	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴)
44	41, 43	oveq12d 6668	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)) = (𝐵 − 𝐴))
45	44	fveq2d 6195	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) = (abs‘(𝐵 − 𝐴)))
46	45	breq1d 4663	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → ((abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ (abs‘(𝐵 − 𝐴)) < 𝑥))
47	46	ralbidva 2985	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
48	47	ralbidva 2985	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
49	48	rexbidva 3049	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
50	49	ralbidv 2986	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
51	50	pm5.32da 673	. . . . 5 ⊢ (𝜑 → ((𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)))
52	24, 26, 51	3bitr3d 298	. . . 4 ⊢ (𝜑 → ((𝐺:𝑆⟶ℂ ∧ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)))
53	4, 52	syl5bb 272	. . 3 ⊢ (𝜑 → ((𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)))
54	53	rexbidv 3052	. 2 ⊢ (𝜑 → (∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ ∃𝑛 ∈ ℤ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)))
55	19	rexeqdv 3145	. . . . 5 ⊢ (𝑛 = 𝑀 → (∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
56	55	ralbidv 2986	. . . 4 ⊢ (𝑛 = 𝑀 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
57	56	ceqsrexv 3336	. . 3 ⊢ (𝑀 ∈ ℤ → (∃𝑛 ∈ ℤ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
58	12, 57	syl 17	. 2 ⊢ (𝜑 → (∃𝑛 ∈ ℤ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
59	3, 54, 58	3bitrd 294	1 ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913   class class class wbr 4653  dom cdm 5114  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650   ↑_𝑚 cmap 7857  ℂcc 9934   < clt 10074   − cmin 10266  ℤcz 11377  ℤ_≥cuz 11687  ℝ⁺crp 11832  abscabs 13974  ⇝_𝑢culm 24130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-pre-lttri 10010  ax-pre-lttrn 10011

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-neg 10269  df-z 11378  df-uz 11688  df-ulm 24131

This theorem is referenced by:  ulmi  24140  ulmclm  24141  ulmres  24142  ulmshftlem  24143  ulm0  24145  ulmcau  24149  ulmss  24151