zmin - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem zmin 6177

Description: There is a unique smallest integer greater than or equal to a given real number.

**Assertion**
Ref	Expression
zmin	⊢ (A ∈ ℝ → ∃!x ∈ ℤ (A ≤ x ⋀ ∀y ∈ ℤ (A ≤ y → x ≤ y)))

Distinct variable group: x,y,A

**Proof of Theorem zmin**
Step	Hyp	Ref	Expression
1		eqid 1474	. . 3 ⊢ {z ∈ ℤ∣A ≤ z} = {z ∈ ℤ∣A ≤ z}
2	1	uzwo3lem1 6174	. 2 ⊢ (A ∈ ℝ → ∃!x ∈ {z ∈ ℤ∣A ≤ z}∀y ∈ {z ∈ ℤ∣A ≤ z}x ≤ y)
3		breq2 2619	. . . . . . 7 ⊢ (z = x → (A ≤ z ↔ A ≤ x))
4	3	elrab 1902	. . . . . 6 ⊢ (x ∈ {z ∈ ℤ∣A ≤ z} ↔ (x ∈ ℤ ⋀ A ≤ x))
5		breq2 2619	. . . . . . . . . 10 ⊢ (z = y → (A ≤ z ↔ A ≤ y))
6	5	elrab 1902	. . . . . . . . 9 ⊢ (y ∈ {z ∈ ℤ∣A ≤ z} ↔ (y ∈ ℤ ⋀ A ≤ y))
7	6	imbi1i 186	. . . . . . . 8 ⊢ ((y ∈ {z ∈ ℤ∣A ≤ z} → x ≤ y) ↔ ((y ∈ ℤ ⋀ A ≤ y) → x ≤ y))
8		impexp 347	. . . . . . . 8 ⊢ (((y ∈ ℤ ⋀ A ≤ y) → x ≤ y) ↔ (y ∈ ℤ → (A ≤ y → x ≤ y)))
9	7, 8	bitr 173	. . . . . . 7 ⊢ ((y ∈ {z ∈ ℤ∣A ≤ z} → x ≤ y) ↔ (y ∈ ℤ → (A ≤ y → x ≤ y)))
10	9	ralbii2 1669	. . . . . 6 ⊢ (∀y ∈ {z ∈ ℤ∣A ≤ z}x ≤ y ↔ ∀y ∈ ℤ (A ≤ y → x ≤ y))
11	4, 10	anbi12i 482	. . . . 5 ⊢ ((x ∈ {z ∈ ℤ∣A ≤ z} ⋀ ∀y ∈ {z ∈ ℤ∣A ≤ z}x ≤ y) ↔ ((x ∈ ℤ ⋀ A ≤ x) ⋀ ∀y ∈ ℤ (A ≤ y → x ≤ y)))
12		anass 439	. . . . 5 ⊢ (((x ∈ ℤ ⋀ A ≤ x) ⋀ ∀y ∈ ℤ (A ≤ y → x ≤ y)) ↔ (x ∈ ℤ ⋀ (A ≤ x ⋀ ∀y ∈ ℤ (A ≤ y → x ≤ y))))
13	11, 12	bitr 173	. . . 4 ⊢ ((x ∈ {z ∈ ℤ∣A ≤ z} ⋀ ∀y ∈ {z ∈ ℤ∣A ≤ z}x ≤ y) ↔ (x ∈ ℤ ⋀ (A ≤ x ⋀ ∀y ∈ ℤ (A ≤ y → x ≤ y))))
14	13	eubii 1386	. . 3 ⊢ (∃!x(x ∈ {z ∈ ℤ∣A ≤ z} ⋀ ∀y ∈ {z ∈ ℤ∣A ≤ z}x ≤ y) ↔ ∃!x(x ∈ ℤ ⋀ (A ≤ x ⋀ ∀y ∈ ℤ (A ≤ y → x ≤ y))))
15		df-reu 1649	. . 3 ⊢ (∃!x ∈ {z ∈ ℤ∣A ≤ z}∀y ∈ {z ∈ ℤ∣A ≤ z}x ≤ y ↔ ∃!x(x ∈ {z ∈ ℤ∣A ≤ z} ⋀ ∀y ∈ {z ∈ ℤ∣A ≤ z}x ≤ y))
16		df-reu 1649	. . 3 ⊢ (∃!x ∈ ℤ (A ≤ x ⋀ ∀y ∈ ℤ (A ≤ y → x ≤ y)) ↔ ∃!x(x ∈ ℤ ⋀ (A ≤ x ⋀ ∀y ∈ ℤ (A ≤ y → x ≤ y))))
17	14, 15, 16	3bitr4r 184	. 2 ⊢ (∃!x ∈ ℤ (A ≤ x ⋀ ∀y ∈ ℤ (A ≤ y → x ≤ y)) ↔ ∃!x ∈ {z ∈ ℤ∣A ≤ z}∀y ∈ {z ∈ ℤ∣A ≤ z}x ≤ y)
18	2, 17	sylibr 200	1 ⊢ (A ∈ ℝ → ∃!x ∈ ℤ (A ≤ x ⋀ ∀y ∈ ℤ (A ≤ y → x ≤ y)))

Colors of variables: wff set class

Syntax hints: → wi 3 ⋀ wa 223 ∈ wcel 957 ∃!weu 1379 ∀wral 1643 ∃!wreu 1645 {crab 1646 class class class wbr 2615 ℝcr 5216 ≤ cle 5278 ℤcz 5281

This theorem is referenced by: zmax 6178 zbtwnre 6179

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 961 ax-gen 962 ax-8 963 ax-9 964 ax-10 965 ax-11 966 ax-12 967 ax-13 968 ax-14 969 ax-17 970 ax-4 972 ax-5o 974 ax-6o 977 ax-9o 1122 ax-10o 1139 ax-16 1209 ax-11o 1217 ax-ext 1458 ax-rep 2689 ax-sep 2699 ax-nul 2706 ax-pow 2738 ax-pr 2775 ax-un 2862 ax-inf2 4608

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 980 df-sb 1171 df-eu 1381 df-mo 1382 df-clab 1463 df-cleq 1468 df-clel 1471 df-ne 1585 df-nel 1586 df-ral 1647 df-rex 1648 df-reu 1649 df-rab 1650 df-v 1809 df-sbc 1939 df-csb 1999 df-dif 2046 df-un 2047 df-in 2048 df-ss 2050 df-pss 2052 df-nul 2278 df-if 2359 df-pw 2399 df-sn 2409 df-pr 2410 df-tp 2412 df-op 2413 df-uni 2500 df-int 2530 df-iun 2564 df-br 2616 df-opab 2663 df-tr 2677 df-eprel 2828 df-id 2831 df-po 2836 df-so 2846 df-fr 2913 df-we 2930 df-ord 2947 df-on 2948 df-lim 2949 df-suc 2950 df-om 3128 df-xp 3180 df-rel 3181 df-cnv 3182 df-co 3183 df-dm 3184 df-rn 3185 df-res 3186 df-ima 3187 df-fun 3188 df-fn 3189 df-f 3190 df-f1 3191 df-fo 3192 df-f1o 3193 df-fv 3194 df-rdg 3927 df-opr 3960 df-oprab 3961 df-1st 4072 df-2nd 4073 df-1o 4126 df-oadd 4128 df-omul 4129 df-er 4254 df-ec 4256 df-qs 4259 df-en 4360 df-dom 4361 df-sdom 4362 df-ni 4983 df-pli 4984 df-mi 4985 df-lti 4986 df-plpq 5018 df-mpq 5019 df-enq 5020 df-nq 5021 df-plq 5022 df-mq 5023 df-rq 5024 df-ltq 5025 df-1q 5026 df-np 5069 df-1p 5070 df-plp 5071 df-mp 5072 df-ltp 5073 df-plpr 5147 df-mpr 5148 df-enr 5149 df-nr 5150 df-plr 5151 df-mr 5152 df-ltr 5153 df-0r 5154 df-1r 5155 df-m1r 5156 df-c 5223 df-0 5224 df-1 5225 df-i 5226 df-r 5227 df-plus 5228 df-mul 5229 df-lt 5230 df-sub 5339 df-neg 5341 df-pnf 5470 df-mnf 5471 df-xr 5472 df-ltxr 5473 df-le 5474 df-n 5883 df-n0 6057 df-z 6093