Metamath Proof Explorer

Theorem rexanuz2nf

Description: A simple counterexample related to theorem rexanuz2 , demonstrating the necessity of its disjoint variable constraints. Here, j appears free in ph , showing that without these constraints, rexanuz2 and similar theorems would not hold (see rexanre and rexanuz ). (Contributed by Glauco Siliprandi, 15-Feb-2025)

Ref Expression
Hypotheses rexanuz2nf.1 
|- Z = NN0
rexanuz2nf.2 
|- ( ph <-> ( j = 0 /\ j <_ k ) )
rexanuz2nf.3 
|- ( ps <-> 0 < k )
Assertion rexanuz2nf 
|- -. ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) )

Proof

Step Hyp Ref Expression
1 rexanuz2nf.1 
 |-  Z = NN0
2 rexanuz2nf.2 
 |-  ( ph <-> ( j = 0 /\ j <_ k ) )
3 rexanuz2nf.3 
 |-  ( ps <-> 0 < k )
4 0nn0 
 |-  0 e. NN0
5 nn0ge0 
 |-  ( k e. NN0 -> 0 <_ k )
6 5 rgen 
 |-  A. k e. NN0 0 <_ k
7 fveq2 
 |-  ( j = 0 -> ( ZZ>= ` j ) = ( ZZ>= ` 0 ) )
8 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
9 7 8 eqtr4di 
 |-  ( j = 0 -> ( ZZ>= ` j ) = NN0 )
10 9 raleqdv 
 |-  ( j = 0 -> ( A. k e. ( ZZ>= ` j ) ( j = 0 /\ j <_ k ) <-> A. k e. NN0 ( j = 0 /\ j <_ k ) ) )
11 5 ad2antlr 
 |-  ( ( ( j = 0 /\ k e. NN0 ) /\ ( j = 0 /\ j <_ k ) ) -> 0 <_ k )
12 simpll 
 |-  ( ( ( j = 0 /\ k e. NN0 ) /\ 0 <_ k ) -> j = 0 )
13 simpr 
 |-  ( ( ( j = 0 /\ k e. NN0 ) /\ 0 <_ k ) -> 0 <_ k )
14 12 13 eqbrtrd 
 |-  ( ( ( j = 0 /\ k e. NN0 ) /\ 0 <_ k ) -> j <_ k )
15 12 14 jca 
 |-  ( ( ( j = 0 /\ k e. NN0 ) /\ 0 <_ k ) -> ( j = 0 /\ j <_ k ) )
16 11 15 impbida 
 |-  ( ( j = 0 /\ k e. NN0 ) -> ( ( j = 0 /\ j <_ k ) <-> 0 <_ k ) )
17 16 ralbidva 
 |-  ( j = 0 -> ( A. k e. NN0 ( j = 0 /\ j <_ k ) <-> A. k e. NN0 0 <_ k ) )
18 10 17 bitrd 
 |-  ( j = 0 -> ( A. k e. ( ZZ>= ` j ) ( j = 0 /\ j <_ k ) <-> A. k e. NN0 0 <_ k ) )
19 18 rspcev 
 |-  ( ( 0 e. NN0 /\ A. k e. NN0 0 <_ k ) -> E. j e. NN0 A. k e. ( ZZ>= ` j ) ( j = 0 /\ j <_ k ) )
20 4 6 19 mp2an 
 |-  E. j e. NN0 A. k e. ( ZZ>= ` j ) ( j = 0 /\ j <_ k )
21 nfcv 
 |-  F/_ j NN0
22 1 21 nfcxfr 
 |-  F/_ j Z
23 22 21 1 rexeqif 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( j = 0 /\ j <_ k ) <-> E. j e. NN0 A. k e. ( ZZ>= ` j ) ( j = 0 /\ j <_ k ) )
24 20 23 mpbir 
 |-  E. j e. Z A. k e. ( ZZ>= ` j ) ( j = 0 /\ j <_ k )
25 2 ralbii 
 |-  ( A. k e. ( ZZ>= ` j ) ph <-> A. k e. ( ZZ>= ` j ) ( j = 0 /\ j <_ k ) )
26 25 rexbii 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ph <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( j = 0 /\ j <_ k ) )
27 24 26 mpbir 
 |-  E. j e. Z A. k e. ( ZZ>= ` j ) ph
28 1nn0 
 |-  1 e. NN0
29 nngt0 
 |-  ( k e. NN -> 0 < k )
30 29 rgen 
 |-  A. k e. NN 0 < k
31 fveq2 
 |-  ( j = 1 -> ( ZZ>= ` j ) = ( ZZ>= ` 1 ) )
32 nnuz 
 |-  NN = ( ZZ>= ` 1 )
33 31 32 eqtr4di 
 |-  ( j = 1 -> ( ZZ>= ` j ) = NN )
34 33 raleqdv 
 |-  ( j = 1 -> ( A. k e. ( ZZ>= ` j ) 0 < k <-> A. k e. NN 0 < k ) )
35 34 rspcev 
 |-  ( ( 1 e. NN0 /\ A. k e. NN 0 < k ) -> E. j e. NN0 A. k e. ( ZZ>= ` j ) 0 < k )
36 28 30 35 mp2an 
 |-  E. j e. NN0 A. k e. ( ZZ>= ` j ) 0 < k
37 22 21 1 rexeqif 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) 0 < k <-> E. j e. NN0 A. k e. ( ZZ>= ` j ) 0 < k )
38 36 37 mpbir 
 |-  E. j e. Z A. k e. ( ZZ>= ` j ) 0 < k
39 3 ralbii 
 |-  ( A. k e. ( ZZ>= ` j ) ps <-> A. k e. ( ZZ>= ` j ) 0 < k )
40 39 rexbii 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ps <-> E. j e. Z A. k e. ( ZZ>= ` j ) 0 < k )
41 38 40 mpbir 
 |-  E. j e. Z A. k e. ( ZZ>= ` j ) ps
42 27 41 pm3.2i 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps )
43 nfv 
 |-  F/ k -. ( ( j = 0 /\ j <_ j ) /\ 0 < j )
44 nfcv 
 |-  F/_ k j
45 nfcv 
 |-  F/_ k ( ZZ>= ` j )
46 8 uzid3 
 |-  ( j e. NN0 -> j e. ( ZZ>= ` j ) )
47 46 adantr 
 |-  ( ( j e. NN0 /\ j = 0 ) -> j e. ( ZZ>= ` j ) )
48 0re 
 |-  0 e. RR
49 48 ltnri 
 |-  -. 0 < 0
50 49 a1i 
 |-  ( j = 0 -> -. 0 < 0 )
51 eqcom 
 |-  ( j = 0 <-> 0 = j )
52 51 biimpi 
 |-  ( j = 0 -> 0 = j )
53 50 52 brneqtrd 
 |-  ( j = 0 -> -. 0 < j )
54 53 intnand 
 |-  ( j = 0 -> -. ( ( j = 0 /\ j <_ j ) /\ 0 < j ) )
55 54 adantl 
 |-  ( ( j e. NN0 /\ j = 0 ) -> -. ( ( j = 0 /\ j <_ j ) /\ 0 < j ) )
56 breq2 
 |-  ( k = j -> ( j <_ k <-> j <_ j ) )
57 56 anbi2d 
 |-  ( k = j -> ( ( j = 0 /\ j <_ k ) <-> ( j = 0 /\ j <_ j ) ) )
58 2 57 bitrid 
 |-  ( k = j -> ( ph <-> ( j = 0 /\ j <_ j ) ) )
59 breq2 
 |-  ( k = j -> ( 0 < k <-> 0 < j ) )
60 3 59 bitrid 
 |-  ( k = j -> ( ps <-> 0 < j ) )
61 58 60 anbi12d 
 |-  ( k = j -> ( ( ph /\ ps ) <-> ( ( j = 0 /\ j <_ j ) /\ 0 < j ) ) )
62 61 notbid 
 |-  ( k = j -> ( -. ( ph /\ ps ) <-> -. ( ( j = 0 /\ j <_ j ) /\ 0 < j ) ) )
63 43 44 45 47 55 62 rspced 
 |-  ( ( j e. NN0 /\ j = 0 ) -> E. k e. ( ZZ>= ` j ) -. ( ph /\ ps ) )
64 46 adantr 
 |-  ( ( j e. NN0 /\ -. j = 0 ) -> j e. ( ZZ>= ` j ) )
65 id 
 |-  ( -. j = 0 -> -. j = 0 )
66 65 intnanrd 
 |-  ( -. j = 0 -> -. ( j = 0 /\ j <_ j ) )
67 66 intnanrd 
 |-  ( -. j = 0 -> -. ( ( j = 0 /\ j <_ j ) /\ 0 < j ) )
68 67 adantl 
 |-  ( ( j e. NN0 /\ -. j = 0 ) -> -. ( ( j = 0 /\ j <_ j ) /\ 0 < j ) )
69 43 44 45 64 68 62 rspced 
 |-  ( ( j e. NN0 /\ -. j = 0 ) -> E. k e. ( ZZ>= ` j ) -. ( ph /\ ps ) )
70 63 69 pm2.61dan 
 |-  ( j e. NN0 -> E. k e. ( ZZ>= ` j ) -. ( ph /\ ps ) )
71 rexnal 
 |-  ( E. k e. ( ZZ>= ` j ) -. ( ph /\ ps ) <-> -. A. k e. ( ZZ>= ` j ) ( ph /\ ps ) )
72 70 71 sylib 
 |-  ( j e. NN0 -> -. A. k e. ( ZZ>= ` j ) ( ph /\ ps ) )
73 72 nrex 
 |-  -. E. j e. NN0 A. k e. ( ZZ>= ` j ) ( ph /\ ps )
74 22 21 1 rexeqif 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <-> E. j e. NN0 A. k e. ( ZZ>= ` j ) ( ph /\ ps ) )
75 73 74 mtbir 
 |-  -. E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps )
76 42 75 pm3.2i 
 |-  ( ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) /\ -. E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) )
77 annim 
 |-  ( ( ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) /\ -. E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) ) <-> -. ( ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) ) )
78 76 77 mpbi 
 |-  -. ( ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) )
79 78 nimnbi2 
 |-  -. ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ph /\ ps ) <-> ( E. j e. Z A. k e. ( ZZ>= ` j ) ph /\ E. j e. Z A. k e. ( ZZ>= ` j ) ps ) )