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 ) )