Metamath Proof Explorer

Theorem zmax

Description: There is a unique largest integer less than or equal to a given real number. (Contributed by NM, 15-Nov-2004)

Ref Expression
Assertion zmax ⊢A∈ℝ→∃!x∈ℤx≤A∧∀y∈ℤy≤A→y≤x

Proof

Step Hyp Ref Expression
1 renegcl ⊢A∈ℝ→−A∈ℝ
2 zmin ⊢−A∈ℝ→∃!z∈ℤ−A≤z∧∀w∈ℤ−A≤w→z≤w
3 1 2 syl ⊢A∈ℝ→∃!z∈ℤ−A≤z∧∀w∈ℤ−A≤w→z≤w
4 znegcl ⊢x∈ℤ→−x∈ℤ
5 znegcl ⊢z∈ℤ→−z∈ℤ
6 zcn ⊢z∈ℤ→z∈ℂ
7 zcn ⊢x∈ℤ→x∈ℂ
8 negcon2 ⊢z∈ℂ∧x∈ℂ→z=−x↔x=−z
9 6 7 8 syl2an ⊢z∈ℤ∧x∈ℤ→z=−x↔x=−z
10 5 9 reuhyp ⊢z∈ℤ→∃!x∈ℤz=−x
11 breq2 ⊢z=−x→−A≤z↔−A≤−x
12 breq1 ⊢z=−x→z≤w↔−x≤w
13 12 imbi2d ⊢z=−x→−A≤w→z≤w↔−A≤w→−x≤w
14 13 ralbidv ⊢z=−x→∀w∈ℤ−A≤w→z≤w↔∀w∈ℤ−A≤w→−x≤w
15 11 14 anbi12d ⊢z=−x→−A≤z∧∀w∈ℤ−A≤w→z≤w↔−A≤−x∧∀w∈ℤ−A≤w→−x≤w
16 4 10 15 reuxfr1 ⊢∃!z∈ℤ−A≤z∧∀w∈ℤ−A≤w→z≤w↔∃!x∈ℤ−A≤−x∧∀w∈ℤ−A≤w→−x≤w
17 zre ⊢x∈ℤ→x∈ℝ
18 leneg ⊢x∈ℝ∧A∈ℝ→x≤A↔−A≤−x
19 17 18 sylan ⊢x∈ℤ∧A∈ℝ→x≤A↔−A≤−x
20 19 ancoms ⊢A∈ℝ∧x∈ℤ→x≤A↔−A≤−x
21 znegcl ⊢w∈ℤ→−w∈ℤ
22 breq1 ⊢y=−w→y≤A↔−w≤A
23 breq1 ⊢y=−w→y≤x↔−w≤x
24 22 23 imbi12d ⊢y=−w→y≤A→y≤x↔−w≤A→−w≤x
25 24 rspcv ⊢−w∈ℤ→∀y∈ℤy≤A→y≤x→−w≤A→−w≤x
26 21 25 syl ⊢w∈ℤ→∀y∈ℤy≤A→y≤x→−w≤A→−w≤x
27 zre ⊢w∈ℤ→w∈ℝ
28 lenegcon1 ⊢w∈ℝ∧A∈ℝ→−w≤A↔−A≤w
29 28 adantrr ⊢w∈ℝ∧A∈ℝ∧x∈ℤ→−w≤A↔−A≤w
30 lenegcon1 ⊢w∈ℝ∧x∈ℝ→−w≤x↔−x≤w
31 17 30 sylan2 ⊢w∈ℝ∧x∈ℤ→−w≤x↔−x≤w
32 31 adantrl ⊢w∈ℝ∧A∈ℝ∧x∈ℤ→−w≤x↔−x≤w
33 29 32 imbi12d ⊢w∈ℝ∧A∈ℝ∧x∈ℤ→−w≤A→−w≤x↔−A≤w→−x≤w
34 27 33 sylan ⊢w∈ℤ∧A∈ℝ∧x∈ℤ→−w≤A→−w≤x↔−A≤w→−x≤w
35 34 biimpd ⊢w∈ℤ∧A∈ℝ∧x∈ℤ→−w≤A→−w≤x→−A≤w→−x≤w
36 35 ex ⊢w∈ℤ→A∈ℝ∧x∈ℤ→−w≤A→−w≤x→−A≤w→−x≤w
37 36 com23 ⊢w∈ℤ→−w≤A→−w≤x→A∈ℝ∧x∈ℤ→−A≤w→−x≤w
38 26 37 syld ⊢w∈ℤ→∀y∈ℤy≤A→y≤x→A∈ℝ∧x∈ℤ→−A≤w→−x≤w
39 38 com13 ⊢A∈ℝ∧x∈ℤ→∀y∈ℤy≤A→y≤x→w∈ℤ→−A≤w→−x≤w
40 39 ralrimdv ⊢A∈ℝ∧x∈ℤ→∀y∈ℤy≤A→y≤x→∀w∈ℤ−A≤w→−x≤w
41 znegcl ⊢y∈ℤ→−y∈ℤ
42 breq2 ⊢w=−y→−A≤w↔−A≤−y
43 breq2 ⊢w=−y→−x≤w↔−x≤−y
44 42 43 imbi12d ⊢w=−y→−A≤w→−x≤w↔−A≤−y→−x≤−y
45 44 rspcv ⊢−y∈ℤ→∀w∈ℤ−A≤w→−x≤w→−A≤−y→−x≤−y
46 41 45 syl ⊢y∈ℤ→∀w∈ℤ−A≤w→−x≤w→−A≤−y→−x≤−y
47 zre ⊢y∈ℤ→y∈ℝ
48 leneg ⊢y∈ℝ∧A∈ℝ→y≤A↔−A≤−y
49 48 adantrr ⊢y∈ℝ∧A∈ℝ∧x∈ℤ→y≤A↔−A≤−y
50 leneg ⊢y∈ℝ∧x∈ℝ→y≤x↔−x≤−y
51 17 50 sylan2 ⊢y∈ℝ∧x∈ℤ→y≤x↔−x≤−y
52 51 adantrl ⊢y∈ℝ∧A∈ℝ∧x∈ℤ→y≤x↔−x≤−y
53 49 52 imbi12d ⊢y∈ℝ∧A∈ℝ∧x∈ℤ→y≤A→y≤x↔−A≤−y→−x≤−y
54 47 53 sylan ⊢y∈ℤ∧A∈ℝ∧x∈ℤ→y≤A→y≤x↔−A≤−y→−x≤−y
55 54 exbiri ⊢y∈ℤ→A∈ℝ∧x∈ℤ→−A≤−y→−x≤−y→y≤A→y≤x
56 55 com23 ⊢y∈ℤ→−A≤−y→−x≤−y→A∈ℝ∧x∈ℤ→y≤A→y≤x
57 46 56 syld ⊢y∈ℤ→∀w∈ℤ−A≤w→−x≤w→A∈ℝ∧x∈ℤ→y≤A→y≤x
58 57 com13 ⊢A∈ℝ∧x∈ℤ→∀w∈ℤ−A≤w→−x≤w→y∈ℤ→y≤A→y≤x
59 58 ralrimdv ⊢A∈ℝ∧x∈ℤ→∀w∈ℤ−A≤w→−x≤w→∀y∈ℤy≤A→y≤x
60 40 59 impbid ⊢A∈ℝ∧x∈ℤ→∀y∈ℤy≤A→y≤x↔∀w∈ℤ−A≤w→−x≤w
61 20 60 anbi12d ⊢A∈ℝ∧x∈ℤ→x≤A∧∀y∈ℤy≤A→y≤x↔−A≤−x∧∀w∈ℤ−A≤w→−x≤w
62 61 reubidva ⊢A∈ℝ→∃!x∈ℤx≤A∧∀y∈ℤy≤A→y≤x↔∃!x∈ℤ−A≤−x∧∀w∈ℤ−A≤w→−x≤w
63 16 62 bitr4id ⊢A∈ℝ→∃!z∈ℤ−A≤z∧∀w∈ℤ−A≤w→z≤w↔∃!x∈ℤx≤A∧∀y∈ℤy≤A→y≤x
64 3 63 mpbid ⊢A∈ℝ→∃!x∈ℤx≤A∧∀y∈ℤy≤A→y≤x