Metamath Proof Explorer

Theorem rexanuz3

Description: Combine two different upper integer properties into one, for a single integer. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses rexanuz3.1 
|- F/ j ph
rexanuz3.2 
|- Z = ( ZZ>= ` M )
rexanuz3.3 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ch )
rexanuz3.4 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ps )
rexanuz3.5 
|- ( k = j -> ( ch <-> th ) )
rexanuz3.6 
|- ( k = j -> ( ps <-> ta ) )
Assertion rexanuz3 
|- ( ph -> E. j e. Z ( th /\ ta ) )

Proof

Step Hyp Ref Expression
1 rexanuz3.1 
 |-  F/ j ph
2 rexanuz3.2 
 |-  Z = ( ZZ>= ` M )
3 rexanuz3.3 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ch )
4 rexanuz3.4 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ps )
5 rexanuz3.5 
 |-  ( k = j -> ( ch <-> th ) )
6 rexanuz3.6 
 |-  ( k = j -> ( ps <-> ta ) )
7 3 4 jca 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ch /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) )
8 2 rexanuz2 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ch /\ ps ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ch /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) )
9 7 8 sylibr 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ch /\ ps ) )
10 2 eleq2i 
 |-  ( j e. Z <-> j e. ( ZZ>= ` M ) )
11 10 biimpi 
 |-  ( j e. Z -> j e. ( ZZ>= ` M ) )
12 eluzelz 
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
13 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
14 11 12 13 3syl 
 |-  ( j e. Z -> j e. ( ZZ>= ` j ) )
15 14 adantr 
 |-  ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ch /\ ps ) ) -> j e. ( ZZ>= ` j ) )
16 simpr 
 |-  ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ch /\ ps ) ) -> A. k e. ( ZZ>= ` j ) ( ch /\ ps ) )
17 5 6 anbi12d 
 |-  ( k = j -> ( ( ch /\ ps ) <-> ( th /\ ta ) ) )
18 17 rspcva 
 |-  ( ( j e. ( ZZ>= ` j ) /\ A. k e. ( ZZ>= ` j ) ( ch /\ ps ) ) -> ( th /\ ta ) )
19 15 16 18 syl2anc 
 |-  ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ch /\ ps ) ) -> ( th /\ ta ) )
20 19 adantll 
 |-  ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ch /\ ps ) ) -> ( th /\ ta ) )
21 20 ex 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ch /\ ps ) -> ( th /\ ta ) ) )
22 21 ex 
 |-  ( ph -> ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ( ch /\ ps ) -> ( th /\ ta ) ) ) )
23 1 22 reximdai 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ch /\ ps ) -> E. j e. Z ( th /\ ta ) ) )
24 9 23 mpd 
 |-  ( ph -> E. j e. Z ( th /\ ta ) )