# Metamath Proof Explorer

## Theorem rexuzre

Description: Convert an upper real quantifier to an upper integer quantifier. (Contributed by Mario Carneiro, 7-May-2016)

Ref Expression
Hypothesis rexuz3.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
Assertion rexuzre ${⊢}{M}\in ℤ\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {j}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({j}\le {k}\to {\phi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 rexuz3.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 eluzelre ${⊢}{j}\in {ℤ}_{\ge {M}}\to {j}\in ℝ$
3 2 1 eleq2s ${⊢}{j}\in {Z}\to {j}\in ℝ$
4 3 adantr ${⊢}\left({j}\in {Z}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to {j}\in ℝ$
5 eluzelz ${⊢}{j}\in {ℤ}_{\ge {M}}\to {j}\in ℤ$
6 5 1 eleq2s ${⊢}{j}\in {Z}\to {j}\in ℤ$
7 eluzelz ${⊢}{k}\in {ℤ}_{\ge {M}}\to {k}\in ℤ$
8 7 1 eleq2s ${⊢}{k}\in {Z}\to {k}\in ℤ$
9 eluz ${⊢}\left({j}\in ℤ\wedge {k}\in ℤ\right)\to \left({k}\in {ℤ}_{\ge {j}}↔{j}\le {k}\right)$
10 6 8 9 syl2an ${⊢}\left({j}\in {Z}\wedge {k}\in {Z}\right)\to \left({k}\in {ℤ}_{\ge {j}}↔{j}\le {k}\right)$
11 10 biimprd ${⊢}\left({j}\in {Z}\wedge {k}\in {Z}\right)\to \left({j}\le {k}\to {k}\in {ℤ}_{\ge {j}}\right)$
12 11 expimpd ${⊢}{j}\in {Z}\to \left(\left({k}\in {Z}\wedge {j}\le {k}\right)\to {k}\in {ℤ}_{\ge {j}}\right)$
13 12 imim1d ${⊢}{j}\in {Z}\to \left(\left({k}\in {ℤ}_{\ge {j}}\to {\phi }\right)\to \left(\left({k}\in {Z}\wedge {j}\le {k}\right)\to {\phi }\right)\right)$
14 13 exp4a ${⊢}{j}\in {Z}\to \left(\left({k}\in {ℤ}_{\ge {j}}\to {\phi }\right)\to \left({k}\in {Z}\to \left({j}\le {k}\to {\phi }\right)\right)\right)$
15 14 ralimdv2 ${⊢}{j}\in {Z}\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({j}\le {k}\to {\phi }\right)\right)$
16 15 imp ${⊢}\left({j}\in {Z}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({j}\le {k}\to {\phi }\right)$
17 4 16 jca ${⊢}\left({j}\in {Z}\wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left({j}\in ℝ\wedge \forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({j}\le {k}\to {\phi }\right)\right)$
18 17 reximi2 ${⊢}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {j}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({j}\le {k}\to {\phi }\right)$
19 simpl ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to {M}\in ℤ$
20 flcl ${⊢}{j}\in ℝ\to ⌊{j}⌋\in ℤ$
21 20 adantl ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to ⌊{j}⌋\in ℤ$
22 21 peano2zd ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to ⌊{j}⌋+1\in ℤ$
23 22 19 ifcld ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\in ℤ$
24 zre ${⊢}{M}\in ℤ\to {M}\in ℝ$
25 reflcl ${⊢}{j}\in ℝ\to ⌊{j}⌋\in ℝ$
26 peano2re ${⊢}⌊{j}⌋\in ℝ\to ⌊{j}⌋+1\in ℝ$
27 25 26 syl ${⊢}{j}\in ℝ\to ⌊{j}⌋+1\in ℝ$
28 max1 ${⊢}\left({M}\in ℝ\wedge ⌊{j}⌋+1\in ℝ\right)\to {M}\le if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)$
29 24 27 28 syl2an ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to {M}\le if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)$
30 eluz2 ${⊢}if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\in ℤ\wedge {M}\le if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\right)$
31 19 23 29 30 syl3anbrc ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\in {ℤ}_{\ge {M}}$
32 31 1 eleqtrrdi ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\in {Z}$
33 impexp ${⊢}\left(\left({k}\in {Z}\wedge {j}\le {k}\right)\to {\phi }\right)↔\left({k}\in {Z}\to \left({j}\le {k}\to {\phi }\right)\right)$
34 uzss ${⊢}if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\in {ℤ}_{\ge {M}}\to {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\subseteq {ℤ}_{\ge {M}}$
35 31 34 syl ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\subseteq {ℤ}_{\ge {M}}$
36 35 1 sseqtrrdi ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\subseteq {Z}$
37 36 sselda ${⊢}\left(\left({M}\in ℤ\wedge {j}\in ℝ\right)\wedge {k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\right)\to {k}\in {Z}$
38 simplr ${⊢}\left(\left({M}\in ℤ\wedge {j}\in ℝ\right)\wedge {k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\right)\to {j}\in ℝ$
39 23 adantr ${⊢}\left(\left({M}\in ℤ\wedge {j}\in ℝ\right)\wedge {k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\right)\to if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\in ℤ$
40 39 zred ${⊢}\left(\left({M}\in ℤ\wedge {j}\in ℝ\right)\wedge {k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\right)\to if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\in ℝ$
41 eluzelre ${⊢}{k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\to {k}\in ℝ$
42 41 adantl ${⊢}\left(\left({M}\in ℤ\wedge {j}\in ℝ\right)\wedge {k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\right)\to {k}\in ℝ$
43 simpr ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to {j}\in ℝ$
44 27 adantl ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to ⌊{j}⌋+1\in ℝ$
45 23 zred ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\in ℝ$
46 fllep1 ${⊢}{j}\in ℝ\to {j}\le ⌊{j}⌋+1$
47 46 adantl ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to {j}\le ⌊{j}⌋+1$
48 max2 ${⊢}\left({M}\in ℝ\wedge ⌊{j}⌋+1\in ℝ\right)\to ⌊{j}⌋+1\le if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)$
49 24 27 48 syl2an ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to ⌊{j}⌋+1\le if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)$
50 43 44 45 47 49 letrd ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to {j}\le if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)$
51 50 adantr ${⊢}\left(\left({M}\in ℤ\wedge {j}\in ℝ\right)\wedge {k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\right)\to {j}\le if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)$
52 eluzle ${⊢}{k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\to if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\le {k}$
53 52 adantl ${⊢}\left(\left({M}\in ℤ\wedge {j}\in ℝ\right)\wedge {k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\right)\to if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\le {k}$
54 38 40 42 51 53 letrd ${⊢}\left(\left({M}\in ℤ\wedge {j}\in ℝ\right)\wedge {k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\right)\to {j}\le {k}$
55 37 54 jca ${⊢}\left(\left({M}\in ℤ\wedge {j}\in ℝ\right)\wedge {k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\right)\to \left({k}\in {Z}\wedge {j}\le {k}\right)$
56 55 ex ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to \left({k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\to \left({k}\in {Z}\wedge {j}\le {k}\right)\right)$
57 56 imim1d ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to \left(\left(\left({k}\in {Z}\wedge {j}\le {k}\right)\to {\phi }\right)\to \left({k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\to {\phi }\right)\right)$
58 33 57 syl5bir ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to \left(\left({k}\in {Z}\to \left({j}\le {k}\to {\phi }\right)\right)\to \left({k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\to {\phi }\right)\right)$
59 58 ralimdv2 ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to \left(\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({j}\le {k}\to {\phi }\right)\to \forall {k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
60 fveq2 ${⊢}{m}=if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\to {ℤ}_{\ge {m}}={ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}$
61 60 raleqdv ${⊢}{m}=if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\to \left(\forall {k}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
62 61 rspcev ${⊢}\left(if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)\in {Z}\wedge \forall {k}\in {ℤ}_{\ge if\left({M}\le ⌊{j}⌋+1,⌊{j}⌋+1,{M}\right)}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}{\phi }$
63 32 59 62 syl6an ${⊢}\left({M}\in ℤ\wedge {j}\in ℝ\right)\to \left(\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({j}\le {k}\to {\phi }\right)\to \exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
64 63 rexlimdva ${⊢}{M}\in ℤ\to \left(\exists {j}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({j}\le {k}\to {\phi }\right)\to \exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
65 fveq2 ${⊢}{m}={j}\to {ℤ}_{\ge {m}}={ℤ}_{\ge {j}}$
66 65 raleqdv ${⊢}{m}={j}\to \left(\forall {k}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
67 66 cbvrexvw ${⊢}\exists {m}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {m}}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{\phi }$
68 64 67 syl6ib ${⊢}{M}\in ℤ\to \left(\exists {j}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({j}\le {k}\to {\phi }\right)\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
69 18 68 impbid2 ${⊢}{M}\in ℤ\to \left(\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {j}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({j}\le {k}\to {\phi }\right)\right)$