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 = ( ZZ>= ` M )
Assertion rexuzre 
|- ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <-> E. j e. RR A. k e. Z ( j <_ k -> ph ) ) )

Proof

Step Hyp Ref Expression
1 rexuz3.1 
 |-  Z = ( ZZ>= ` M )
2 eluzelre 
 |-  ( j e. ( ZZ>= ` M ) -> j e. RR )
3 2 1 eleq2s 
 |-  ( j e. Z -> j e. RR )
4 3 adantr 
 |-  ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ph ) -> j e. RR )
5 eluzelz 
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
6 5 1 eleq2s 
 |-  ( j e. Z -> j e. ZZ )
7 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
8 7 1 eleq2s 
 |-  ( k e. Z -> k e. ZZ )
9 eluz 
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( k e. ( ZZ>= ` j ) <-> j <_ k ) )
10 6 8 9 syl2an 
 |-  ( ( j e. Z /\ k e. Z ) -> ( k e. ( ZZ>= ` j ) <-> j <_ k ) )
11 10 biimprd 
 |-  ( ( j e. Z /\ k e. Z ) -> ( j <_ k -> k e. ( ZZ>= ` j ) ) )
12 11 expimpd 
 |-  ( j e. Z -> ( ( k e. Z /\ j <_ k ) -> k e. ( ZZ>= ` j ) ) )
13 12 imim1d 
 |-  ( j e. Z -> ( ( k e. ( ZZ>= ` j ) -> ph ) -> ( ( k e. Z /\ j <_ k ) -> ph ) ) )
14 13 exp4a 
 |-  ( j e. Z -> ( ( k e. ( ZZ>= ` j ) -> ph ) -> ( k e. Z -> ( j <_ k -> ph ) ) ) )
15 14 ralimdv2 
 |-  ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ph -> A. k e. Z ( j <_ k -> ph ) ) )
16 15 imp 
 |-  ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ph ) -> A. k e. Z ( j <_ k -> ph ) )
17 4 16 jca 
 |-  ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ph ) -> ( j e. RR /\ A. k e. Z ( j <_ k -> ph ) ) )
18 17 reximi2 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ph -> E. j e. RR A. k e. Z ( j <_ k -> ph ) )
19 simpl 
 |-  ( ( M e. ZZ /\ j e. RR ) -> M e. ZZ )
20 flcl 
 |-  ( j e. RR -> ( |_ ` j ) e. ZZ )
21 20 adantl 
 |-  ( ( M e. ZZ /\ j e. RR ) -> ( |_ ` j ) e. ZZ )
22 21 peano2zd 
 |-  ( ( M e. ZZ /\ j e. RR ) -> ( ( |_ ` j ) + 1 ) e. ZZ )
23 22 19 ifcld 
 |-  ( ( M e. ZZ /\ j e. RR ) -> if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) e. ZZ )
24 zre 
 |-  ( M e. ZZ -> M e. RR )
25 reflcl 
 |-  ( j e. RR -> ( |_ ` j ) e. RR )
26 peano2re 
 |-  ( ( |_ ` j ) e. RR -> ( ( |_ ` j ) + 1 ) e. RR )
27 25 26 syl 
 |-  ( j e. RR -> ( ( |_ ` j ) + 1 ) e. RR )
28 max1 
 |-  ( ( M e. RR /\ ( ( |_ ` j ) + 1 ) e. RR ) -> M <_ if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) )
29 24 27 28 syl2an 
 |-  ( ( M e. ZZ /\ j e. RR ) -> M <_ if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) )
30 eluz2 
 |-  ( if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) e. ZZ /\ M <_ if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) )
31 19 23 29 30 syl3anbrc 
 |-  ( ( M e. ZZ /\ j e. RR ) -> if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) e. ( ZZ>= ` M ) )
32 31 1 eleqtrrdi 
 |-  ( ( M e. ZZ /\ j e. RR ) -> if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) e. Z )
33 impexp 
 |-  ( ( ( k e. Z /\ j <_ k ) -> ph ) <-> ( k e. Z -> ( j <_ k -> ph ) ) )
34 uzss 
 |-  ( if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) e. ( ZZ>= ` M ) -> ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) C_ ( ZZ>= ` M ) )
35 31 34 syl 
 |-  ( ( M e. ZZ /\ j e. RR ) -> ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) C_ ( ZZ>= ` M ) )
36 35 1 sseqtrrdi 
 |-  ( ( M e. ZZ /\ j e. RR ) -> ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) C_ Z )
37 36 sselda 
 |-  ( ( ( M e. ZZ /\ j e. RR ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) ) -> k e. Z )
38 simplr 
 |-  ( ( ( M e. ZZ /\ j e. RR ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) ) -> j e. RR )
39 23 adantr 
 |-  ( ( ( M e. ZZ /\ j e. RR ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) ) -> if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) e. ZZ )
40 39 zred 
 |-  ( ( ( M e. ZZ /\ j e. RR ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) ) -> if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) e. RR )
41 eluzelre 
 |-  ( k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) -> k e. RR )
42 41 adantl 
 |-  ( ( ( M e. ZZ /\ j e. RR ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) ) -> k e. RR )
43 simpr 
 |-  ( ( M e. ZZ /\ j e. RR ) -> j e. RR )
44 27 adantl 
 |-  ( ( M e. ZZ /\ j e. RR ) -> ( ( |_ ` j ) + 1 ) e. RR )
45 23 zred 
 |-  ( ( M e. ZZ /\ j e. RR ) -> if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) e. RR )
46 fllep1 
 |-  ( j e. RR -> j <_ ( ( |_ ` j ) + 1 ) )
47 46 adantl 
 |-  ( ( M e. ZZ /\ j e. RR ) -> j <_ ( ( |_ ` j ) + 1 ) )
48 max2 
 |-  ( ( M e. RR /\ ( ( |_ ` j ) + 1 ) e. RR ) -> ( ( |_ ` j ) + 1 ) <_ if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) )
49 24 27 48 syl2an 
 |-  ( ( M e. ZZ /\ j e. RR ) -> ( ( |_ ` j ) + 1 ) <_ if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) )
50 43 44 45 47 49 letrd 
 |-  ( ( M e. ZZ /\ j e. RR ) -> j <_ if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) )
51 50 adantr 
 |-  ( ( ( M e. ZZ /\ j e. RR ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) ) -> j <_ if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) )
52 eluzle 
 |-  ( k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) -> if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) <_ k )
53 52 adantl 
 |-  ( ( ( M e. ZZ /\ j e. RR ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) ) -> if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) <_ k )
54 38 40 42 51 53 letrd 
 |-  ( ( ( M e. ZZ /\ j e. RR ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) ) -> j <_ k )
55 37 54 jca 
 |-  ( ( ( M e. ZZ /\ j e. RR ) /\ k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) ) -> ( k e. Z /\ j <_ k ) )
56 55 ex 
 |-  ( ( M e. ZZ /\ j e. RR ) -> ( k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) -> ( k e. Z /\ j <_ k ) ) )
57 56 imim1d 
 |-  ( ( M e. ZZ /\ j e. RR ) -> ( ( ( k e. Z /\ j <_ k ) -> ph ) -> ( k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) -> ph ) ) )
58 33 57 biimtrrid 
 |-  ( ( M e. ZZ /\ j e. RR ) -> ( ( k e. Z -> ( j <_ k -> ph ) ) -> ( k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) -> ph ) ) )
59 58 ralimdv2 
 |-  ( ( M e. ZZ /\ j e. RR ) -> ( A. k e. Z ( j <_ k -> ph ) -> A. k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) ph ) )
60 fveq2 
 |-  ( m = if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) -> ( ZZ>= ` m ) = ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) )
61 60 raleqdv 
 |-  ( m = if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) -> ( A. k e. ( ZZ>= ` m ) ph <-> A. k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) ph ) )
62 61 rspcev 
 |-  ( ( if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) e. Z /\ A. k e. ( ZZ>= ` if ( M <_ ( ( |_ ` j ) + 1 ) , ( ( |_ ` j ) + 1 ) , M ) ) ph ) -> E. m e. Z A. k e. ( ZZ>= ` m ) ph )
63 32 59 62 syl6an 
 |-  ( ( M e. ZZ /\ j e. RR ) -> ( A. k e. Z ( j <_ k -> ph ) -> E. m e. Z A. k e. ( ZZ>= ` m ) ph ) )
64 63 rexlimdva 
 |-  ( M e. ZZ -> ( E. j e. RR A. k e. Z ( j <_ k -> ph ) -> E. m e. Z A. k e. ( ZZ>= ` m ) ph ) )
65 fveq2 
 |-  ( m = j -> ( ZZ>= ` m ) = ( ZZ>= ` j ) )
66 65 raleqdv 
 |-  ( m = j -> ( A. k e. ( ZZ>= ` m ) ph <-> A. k e. ( ZZ>= ` j ) ph ) )
67 66 cbvrexvw 
 |-  ( E. m e. Z A. k e. ( ZZ>= ` m ) ph <-> E. j e. Z A. k e. ( ZZ>= ` j ) ph )
68 64 67 imbitrdi 
 |-  ( M e. ZZ -> ( E. j e. RR A. k e. Z ( j <_ k -> ph ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ph ) )
69 18 68 impbid2 
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <-> E. j e. RR A. k e. Z ( j <_ k -> ph ) ) )