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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion rexuzre ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 rexuz3.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 eluzelre ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℝ )
3 2 1 eleq2s ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℝ )
4 3 adantr ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) → 𝑗 ∈ ℝ )
5 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ )
6 5 1 eleq2s ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ )
7 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
8 7 1 eleq2s ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
9 eluz ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ↔ 𝑗 ≤ 𝑘 ) )
10 6 8 9 syl2an ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ↔ 𝑗 ≤ 𝑘 ) )
11 10 biimprd ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑗 ≤ 𝑘 → 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) )
12 11 expimpd ⊢ ( 𝑗 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ≤ 𝑘 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) )
13 12 imim1d ⊢ ( 𝑗 ∈ 𝑍 → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → 𝜑 ) → ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ≤ 𝑘 ) → 𝜑 ) ) )
14 13 exp4a ⊢ ( 𝑗 ∈ 𝑍 → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → 𝜑 ) → ( 𝑘 ∈ 𝑍 → ( 𝑗 ≤ 𝑘 → 𝜑 ) ) ) )
15 14 ralimdv2 ⊢ ( 𝑗 ∈ 𝑍 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → 𝜑 ) ) )
16 15 imp ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) → ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → 𝜑 ) )
17 4 16 jca ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) → ( 𝑗 ∈ ℝ ∧ ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → 𝜑 ) ) )
18 17 reximi2 ⊢ ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 → ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → 𝜑 ) )
19 simpl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → 𝑀 ∈ ℤ )
20 flcl ⊢ ( 𝑗 ∈ ℝ → ( ⌊ ‘ 𝑗 ) ∈ ℤ )
21 20 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → ( ⌊ ‘ 𝑗 ) ∈ ℤ )
22 21 peano2zd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → ( ( ⌊ ‘ 𝑗 ) + 1 ) ∈ ℤ )
23 22 19 ifcld ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ∈ ℤ )
24 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
25 reflcl ⊢ ( 𝑗 ∈ ℝ → ( ⌊ ‘ 𝑗 ) ∈ ℝ )
26 peano2re ⊢ ( ( ⌊ ‘ 𝑗 ) ∈ ℝ → ( ( ⌊ ‘ 𝑗 ) + 1 ) ∈ ℝ )
27 25 26 syl ⊢ ( 𝑗 ∈ ℝ → ( ( ⌊ ‘ 𝑗 ) + 1 ) ∈ ℝ )
28 max1 ⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑗 ) + 1 ) ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) )
29 24 27 28 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) )
30 eluz2 ⊢ ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ∈ ℤ ∧ 𝑀 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) )
31 19 23 29 30 syl3anbrc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
32 31 1 eleqtrrdi ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ∈ 𝑍 )
33 impexp ⊢ ( ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ≤ 𝑘 ) → 𝜑 ) ↔ ( 𝑘 ∈ 𝑍 → ( 𝑗 ≤ 𝑘 → 𝜑 ) ) )
34 uzss ⊢ ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
35 31 34 syl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
36 35 1 sseqtrrdi ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) ⊆ 𝑍 )
37 36 sselda ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) ) → 𝑘 ∈ 𝑍 )
38 simplr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) ) → 𝑗 ∈ ℝ )
39 23 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ∈ ℤ )
40 39 zred ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ∈ ℝ )
41 eluzelre ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) → 𝑘 ∈ ℝ )
42 41 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) ) → 𝑘 ∈ ℝ )
43 simpr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → 𝑗 ∈ ℝ )
44 27 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → ( ( ⌊ ‘ 𝑗 ) + 1 ) ∈ ℝ )
45 23 zred ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ∈ ℝ )
46 fllep1 ⊢ ( 𝑗 ∈ ℝ → 𝑗 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) )
47 46 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → 𝑗 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) )
48 max2 ⊢ ( ( 𝑀 ∈ ℝ ∧ ( ( ⌊ ‘ 𝑗 ) + 1 ) ∈ ℝ ) → ( ( ⌊ ‘ 𝑗 ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) )
49 24 27 48 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → ( ( ⌊ ‘ 𝑗 ) + 1 ) ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) )
50 43 44 45 47 49 letrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → 𝑗 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) )
51 50 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) ) → 𝑗 ≤ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) )
52 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ≤ 𝑘 )
53 52 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) ) → if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ≤ 𝑘 )
54 38 40 42 51 53 letrd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) ) → 𝑗 ≤ 𝑘 )
55 37 54 jca ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) ) → ( 𝑘 ∈ 𝑍 ∧ 𝑗 ≤ 𝑘 ) )
56 55 ex ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) → ( 𝑘 ∈ 𝑍 ∧ 𝑗 ≤ 𝑘 ) ) )
57 56 imim1d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → ( ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ≤ 𝑘 ) → 𝜑 ) → ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) → 𝜑 ) ) )
58 33 57 biimtrrid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → ( ( 𝑘 ∈ 𝑍 → ( 𝑗 ≤ 𝑘 → 𝜑 ) ) → ( 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) → 𝜑 ) ) )
59 58 ralimdv2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → ( ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → 𝜑 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) 𝜑 ) )
60 fveq2 ⊢ ( 𝑚 = if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) → ( ℤ≥ ‘ 𝑚 ) = ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) )
61 60 raleqdv ⊢ ( 𝑚 = if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) 𝜑 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) 𝜑 ) )
62 61 rspcev ⊢ ( ( if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ if ( 𝑀 ≤ ( ( ⌊ ‘ 𝑗 ) + 1 ) , ( ( ⌊ ‘ 𝑗 ) + 1 ) , 𝑀 ) ) 𝜑 ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) 𝜑 )
63 32 59 62 syl6an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℝ ) → ( ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → 𝜑 ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) 𝜑 ) )
64 63 rexlimdva ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → 𝜑 ) → ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) 𝜑 ) )
65 fveq2 ⊢ ( 𝑚 = 𝑗 → ( ℤ≥ ‘ 𝑚 ) = ( ℤ≥ ‘ 𝑗 ) )
66 65 raleqdv ⊢ ( 𝑚 = 𝑗 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) 𝜑 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) )
67 66 cbvrexvw ⊢ ( ∃ 𝑚 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) 𝜑 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 )
68 64 67 imbitrdi ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → 𝜑 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ) )
69 18 68 impbid2 ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝜑 ↔ ∃ 𝑗 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ( 𝑗 ≤ 𝑘 → 𝜑 ) ) )