MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexuzre Structured version   Visualization version   GIF version

Theorem rexuzre 14377
Description: Convert an upper real quantifier to an upper integer quantifier. (Contributed by Mario Carneiro, 7-May-2016.)
Hypothesis
Ref Expression
rexuz3.1 𝑍 = (ℤ𝑀)
Assertion
Ref Expression
rexuzre (𝑀 ∈ ℤ → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)𝜑 ↔ ∃𝑗 ∈ ℝ ∀𝑘𝑍 (𝑗𝑘𝜑)))
Distinct variable groups:   𝑗,𝑀   𝜑,𝑗   𝑗,𝑘,𝑍   𝑘,𝑀
Allowed substitution hint:   𝜑(𝑘)

Proof of Theorem rexuzre
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 eluzelre 11897 . . . . . 6 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℝ)
2 rexuz3.1 . . . . . 6 𝑍 = (ℤ𝑀)
31, 2eleq2s 2862 . . . . 5 (𝑗𝑍𝑗 ∈ ℝ)
43adantr 472 . . . 4 ((𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)𝜑) → 𝑗 ∈ ℝ)
5 eluzelz 11896 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℤ)
65, 2eleq2s 2862 . . . . . . . . . . 11 (𝑗𝑍𝑗 ∈ ℤ)
7 eluzelz 11896 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℤ)
87, 2eleq2s 2862 . . . . . . . . . . 11 (𝑘𝑍𝑘 ∈ ℤ)
9 eluz 11900 . . . . . . . . . . 11 ((𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ𝑗) ↔ 𝑗𝑘))
106, 8, 9syl2an 589 . . . . . . . . . 10 ((𝑗𝑍𝑘𝑍) → (𝑘 ∈ (ℤ𝑗) ↔ 𝑗𝑘))
1110biimprd 239 . . . . . . . . 9 ((𝑗𝑍𝑘𝑍) → (𝑗𝑘𝑘 ∈ (ℤ𝑗)))
1211expimpd 445 . . . . . . . 8 (𝑗𝑍 → ((𝑘𝑍𝑗𝑘) → 𝑘 ∈ (ℤ𝑗)))
1312imim1d 82 . . . . . . 7 (𝑗𝑍 → ((𝑘 ∈ (ℤ𝑗) → 𝜑) → ((𝑘𝑍𝑗𝑘) → 𝜑)))
1413exp4a 422 . . . . . 6 (𝑗𝑍 → ((𝑘 ∈ (ℤ𝑗) → 𝜑) → (𝑘𝑍 → (𝑗𝑘𝜑))))
1514ralimdv2 3108 . . . . 5 (𝑗𝑍 → (∀𝑘 ∈ (ℤ𝑗)𝜑 → ∀𝑘𝑍 (𝑗𝑘𝜑)))
1615imp 395 . . . 4 ((𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)𝜑) → ∀𝑘𝑍 (𝑗𝑘𝜑))
174, 16jca 507 . . 3 ((𝑗𝑍 ∧ ∀𝑘 ∈ (ℤ𝑗)𝜑) → (𝑗 ∈ ℝ ∧ ∀𝑘𝑍 (𝑗𝑘𝜑)))
1817reximi2 3156 . 2 (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)𝜑 → ∃𝑗 ∈ ℝ ∀𝑘𝑍 (𝑗𝑘𝜑))
19 simpl 474 . . . . . . 7 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → 𝑀 ∈ ℤ)
20 flcl 12804 . . . . . . . . . 10 (𝑗 ∈ ℝ → (⌊‘𝑗) ∈ ℤ)
2120adantl 473 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → (⌊‘𝑗) ∈ ℤ)
2221peano2zd 11732 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → ((⌊‘𝑗) + 1) ∈ ℤ)
2322, 19ifcld 4288 . . . . . . 7 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ ℤ)
24 zre 11628 . . . . . . . 8 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
25 reflcl 12805 . . . . . . . . 9 (𝑗 ∈ ℝ → (⌊‘𝑗) ∈ ℝ)
26 peano2re 10463 . . . . . . . . 9 ((⌊‘𝑗) ∈ ℝ → ((⌊‘𝑗) + 1) ∈ ℝ)
2725, 26syl 17 . . . . . . . 8 (𝑗 ∈ ℝ → ((⌊‘𝑗) + 1) ∈ ℝ)
28 max1 12218 . . . . . . . 8 ((𝑀 ∈ ℝ ∧ ((⌊‘𝑗) + 1) ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))
2924, 27, 28syl2an 589 . . . . . . 7 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))
30 eluz2 11892 . . . . . . 7 (if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ ℤ ∧ 𝑀 ≤ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)))
3119, 23, 29, 30syl3anbrc 1443 . . . . . 6 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ (ℤ𝑀))
3231, 2syl6eleqr 2855 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ 𝑍)
33 impexp 441 . . . . . . 7 (((𝑘𝑍𝑗𝑘) → 𝜑) ↔ (𝑘𝑍 → (𝑗𝑘𝜑)))
34 uzss 11907 . . . . . . . . . . . . 13 (if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ (ℤ𝑀) → (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) ⊆ (ℤ𝑀))
3531, 34syl 17 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) ⊆ (ℤ𝑀))
3635, 2syl6sseqr 3812 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) ⊆ 𝑍)
3736sselda 3761 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → 𝑘𝑍)
38 simplr 785 . . . . . . . . . . 11 (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → 𝑗 ∈ ℝ)
3923adantr 472 . . . . . . . . . . . 12 (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ ℤ)
4039zred 11729 . . . . . . . . . . 11 (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ ℝ)
41 eluzelre 11897 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) → 𝑘 ∈ ℝ)
4241adantl 473 . . . . . . . . . . 11 (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → 𝑘 ∈ ℝ)
43 simpr 477 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → 𝑗 ∈ ℝ)
4427adantl 473 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → ((⌊‘𝑗) + 1) ∈ ℝ)
4523zred 11729 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ ℝ)
46 fllep1 12810 . . . . . . . . . . . . . 14 (𝑗 ∈ ℝ → 𝑗 ≤ ((⌊‘𝑗) + 1))
4746adantl 473 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → 𝑗 ≤ ((⌊‘𝑗) + 1))
48 max2 12220 . . . . . . . . . . . . . 14 ((𝑀 ∈ ℝ ∧ ((⌊‘𝑗) + 1) ∈ ℝ) → ((⌊‘𝑗) + 1) ≤ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))
4924, 27, 48syl2an 589 . . . . . . . . . . . . 13 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → ((⌊‘𝑗) + 1) ≤ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))
5043, 44, 45, 47, 49letrd 10448 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → 𝑗 ≤ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))
5150adantr 472 . . . . . . . . . . 11 (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → 𝑗 ≤ if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))
52 eluzle 11899 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ≤ 𝑘)
5352adantl 473 . . . . . . . . . . 11 (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ≤ 𝑘)
5438, 40, 42, 51, 53letrd 10448 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → 𝑗𝑘)
5537, 54jca 507 . . . . . . . . 9 (((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) ∧ 𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))) → (𝑘𝑍𝑗𝑘))
5655ex 401 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → (𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) → (𝑘𝑍𝑗𝑘)))
5756imim1d 82 . . . . . . 7 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → (((𝑘𝑍𝑗𝑘) → 𝜑) → (𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) → 𝜑)))
5833, 57syl5bir 234 . . . . . 6 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → ((𝑘𝑍 → (𝑗𝑘𝜑)) → (𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)) → 𝜑)))
5958ralimdv2 3108 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → (∀𝑘𝑍 (𝑗𝑘𝜑) → ∀𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))𝜑))
60 fveq2 6375 . . . . . . 7 (𝑚 = if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) → (ℤ𝑚) = (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀)))
6160raleqdv 3292 . . . . . 6 (𝑚 = if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) → (∀𝑘 ∈ (ℤ𝑚)𝜑 ↔ ∀𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))𝜑))
6261rspcev 3461 . . . . 5 ((if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀) ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ‘if(𝑀 ≤ ((⌊‘𝑗) + 1), ((⌊‘𝑗) + 1), 𝑀))𝜑) → ∃𝑚𝑍𝑘 ∈ (ℤ𝑚)𝜑)
6332, 59, 62syl6an 674 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ) → (∀𝑘𝑍 (𝑗𝑘𝜑) → ∃𝑚𝑍𝑘 ∈ (ℤ𝑚)𝜑))
6463rexlimdva 3178 . . 3 (𝑀 ∈ ℤ → (∃𝑗 ∈ ℝ ∀𝑘𝑍 (𝑗𝑘𝜑) → ∃𝑚𝑍𝑘 ∈ (ℤ𝑚)𝜑))
65 fveq2 6375 . . . . 5 (𝑚 = 𝑗 → (ℤ𝑚) = (ℤ𝑗))
6665raleqdv 3292 . . . 4 (𝑚 = 𝑗 → (∀𝑘 ∈ (ℤ𝑚)𝜑 ↔ ∀𝑘 ∈ (ℤ𝑗)𝜑))
6766cbvrexv 3320 . . 3 (∃𝑚𝑍𝑘 ∈ (ℤ𝑚)𝜑 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)𝜑)
6864, 67syl6ib 242 . 2 (𝑀 ∈ ℤ → (∃𝑗 ∈ ℝ ∀𝑘𝑍 (𝑗𝑘𝜑) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)𝜑))
6918, 68impbid2 217 1 (𝑀 ∈ ℤ → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)𝜑 ↔ ∃𝑗 ∈ ℝ ∀𝑘𝑍 (𝑗𝑘𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3055  wrex 3056  wss 3732  ifcif 4243   class class class wbr 4809  cfv 6068  (class class class)co 6842  cr 10188  1c1 10190   + caddc 10192  cle 10329  cz 11624  cuz 11886  cfl 12799
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-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
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-rmo 3063  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-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  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-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  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-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-sup 8555  df-inf 8556  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-n0 11539  df-z 11625  df-uz 11887  df-fl 12801
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator