Theorem ulm2 24430

Description: Simplify ulmval 24425 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 24425	. . 3 ⊢ (𝑆 ∈ 𝑉 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)))
4		3anan12 1117	. . . 4 ⊢ ((𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝐺:𝑆⟶ℂ ∧ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)))
5		ulm2.z	. . . . . . . . . 10 ⊢ 𝑍 = (ℤ≥‘𝑀)
6		ulm2.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
7	6	fdmd 6232	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝐹 = 𝑍)
8		fdm 6231	. . . . . . . . . . 11 ⊢ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) → dom 𝐹 = (ℤ≥‘𝑛))
9	7, 8	sylan9req 2820	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆)) → 𝑍 = (ℤ≥‘𝑛))
10	5, 9	syl5eqr 2813	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆)) → (ℤ≥‘𝑀) = (ℤ≥‘𝑛))
11		ulm2.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℤ)
12	11	adantr 472	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆)) → 𝑀 ∈ ℤ)
13		uz11 11909	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℤ → ((ℤ≥‘𝑀) = (ℤ≥‘𝑛) ↔ 𝑀 = 𝑛))
14	12, 13	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆)) → ((ℤ≥‘𝑀) = (ℤ≥‘𝑛) ↔ 𝑀 = 𝑛))
15	10, 14	mpbid 223	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆)) → 𝑀 = 𝑛)
16	15	eqcomd 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆)) → 𝑛 = 𝑀)
17		fveq2 6375	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑀 → (ℤ≥‘𝑛) = (ℤ≥‘𝑀))
18	17, 5	syl6eqr 2817	. . . . . . . . . 10 ⊢ (𝑛 = 𝑀 → (ℤ≥‘𝑛) = 𝑍)
19	18	feq2d 6209	. . . . . . . . 9 ⊢ (𝑛 = 𝑀 → (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ↔ 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆)))
20	19	biimparc 471	. . . . . . . 8 ⊢ ((𝐹:𝑍⟶(ℂ ↑𝑚 𝑆) ∧ 𝑛 = 𝑀) → 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆))
21	6, 20	sylan 575	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆))
22	16, 21	impbida 835	. . . . . 6 ⊢ (𝜑 → (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ↔ 𝑛 = 𝑀))
23	22	anbi1d 623	. . . . 5 ⊢ (𝜑 → ((𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)))
24		ulm2.g	. . . . . 6 ⊢ (𝜑 → 𝐺:𝑆⟶ℂ)
25	24	biantrurd 528	. . . . 5 ⊢ (𝜑 → ((𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝐺:𝑆⟶ℂ ∧ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))))
26		simp-4l 801	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → 𝜑)
27		simpr 477	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝑛 = 𝑀)
28		uzid 11901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
29	11, 28	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀))
30	29, 5	syl6eleqr 2855	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ 𝑍)
31	30	adantr 472	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝑀 ∈ 𝑍)
32	27, 31	eqeltrd 2844	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → 𝑛 ∈ 𝑍)
33	5	uztrn2 11904	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ 𝑍)
34	32, 33	sylan 575	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → 𝑗 ∈ 𝑍)
35	5	uztrn2 11904	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍)
36	34, 35	sylan 575	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍)
37	36	adantr 472	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → 𝑘 ∈ 𝑍)
38		simpr 477	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆)
39		ulm2.b	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = 𝐵)
40	26, 37, 38, 39	syl12anc 865	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑘)‘𝑧) = 𝐵)
41		ulm2.a	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴)
42	26, 41	sylancom 582	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = 𝐴)
43	40, 42	oveq12d 6860	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧)) = (𝐵 − 𝐴))
44	43	fveq2d 6379	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) = (abs‘(𝐵 − 𝐴)))
45	44	breq1d 4819	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → ((abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ (abs‘(𝐵 − 𝐴)) < 𝑥))
46	45	ralbidva 3132	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
47	46	ralbidva 3132	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 = 𝑀) ∧ 𝑗 ∈ (ℤ≥‘𝑛)) → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
48	47	rexbidva 3196	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
49	48	ralbidv 3133	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
50	49	pm5.32da 574	. . . . 5 ⊢ (𝜑 → ((𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)))
51	23, 25, 50	3bitr3d 300	. . . 4 ⊢ (𝜑 → ((𝐺:𝑆⟶ℂ ∧ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)))
52	4, 51	syl5bb 274	. . 3 ⊢ (𝜑 → ((𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)))
53	52	rexbidv 3199	. 2 ⊢ (𝜑 → (∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) ↔ ∃𝑛 ∈ ℤ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥)))
54	18	rexeqdv 3293	. . . . 5 ⊢ (𝑛 = 𝑀 → (∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
55	54	ralbidv 3133	. . . 4 ⊢ (𝑛 = 𝑀 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
56	55	ceqsrexv 3489	. . 3 ⊢ (𝑀 ∈ ℤ → (∃𝑛 ∈ ℤ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
57	11, 56	syl 17	. 2 ⊢ (𝜑 → (∃𝑛 ∈ ℤ (𝑛 = 𝑀 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))
58	3, 53, 57	3bitrd 296	1 ⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(𝐵 − 𝐴)) < 𝑥))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   ∧ w3a 1107   = wceq 1652   ∈ wcel 2155  ∀wral 3055  ∃wrex 3056   class class class wbr 4809  dom cdm 5277  ⟶wf 6064  ‘cfv 6068  (class class class)co 6842   ↑_𝑚 cmap 8060  ℂcc 10187   < clt 10328   − cmin 10520  ℤcz 11624  ℤ_≥cuz 11886  ℝ⁺crp 12028  abscabs 14261  ⇝_𝑢culm 24421

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-pre-lttri 10263  ax-pre-lttrn 10264

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-po 5198  df-so 5199  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-er 7947  df-map 8062  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-neg 10523  df-z 11625  df-uz 11887  df-ulm 24422

This theorem is referenced by:  ulmi  24431  ulmclm  24432  ulmres  24433  ulmshftlem  24434  ulm0  24436  ulmcau  24440  ulmss  24442