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={\mathbb{N}}_0$$
	rexanuz2nf.2	$$⊢\phi \leftrightarrow \left(j=0\wedge j\le k\right)$$
	rexanuz2nf.3	$$⊢\psi \leftrightarrow 0<k$$
Assertion	rexanuz2nf	$$⊢\neg \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		rexanuz2nf.1	$$⊢Z={\mathbb{N}}_0$$
2		rexanuz2nf.2	$$⊢\phi \leftrightarrow \left(j=0\wedge j\le k\right)$$
3		rexanuz2nf.3	$$⊢\psi \leftrightarrow 0<k$$
4		0nn0	$$⊢0\in {\mathbb{N}}_0$$
5		nn0ge0	$$⊢k\in {\mathbb{N}}_0\to 0\le k$$
6	5	rgen	$$⊢\forall k\in {\mathbb{N}}_{0}0\le k$$
7		fveq2	$$⊢j=0\to {\mathbb{Z}}_{\ge j}={\mathbb{Z}}_{\ge 0}$$
8		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
9	7 8	eqtr4di	$$⊢j=0\to {\mathbb{Z}}_{\ge j}={\mathbb{N}}_0$$
10	9	raleqdv	$$⊢j=0\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left(j=0\wedge j\le k\right)\leftrightarrow \forall k\in {\mathbb{N}}_0\left(j=0\wedge j\le k\right)\right)$$
11	5	ad2antlr	$$⊢\left(\left(j=0\wedge k\in {\mathbb{N}}_0\right)\wedge \left(j=0\wedge j\le k\right)\right)\to 0\le k$$
12		simpll	$$⊢\left(\left(j=0\wedge k\in {\mathbb{N}}_0\right)\wedge 0\le k\right)\to j=0$$
13		simpr	$$⊢\left(\left(j=0\wedge k\in {\mathbb{N}}_0\right)\wedge 0\le k\right)\to 0\le k$$
14	12 13	eqbrtrd	$$⊢\left(\left(j=0\wedge k\in {\mathbb{N}}_0\right)\wedge 0\le k\right)\to j\le k$$
15	12 14	jca	$$⊢\left(\left(j=0\wedge k\in {\mathbb{N}}_0\right)\wedge 0\le k\right)\to \left(j=0\wedge j\le k\right)$$
16	11 15	impbida	$$⊢\left(j=0\wedge k\in {\mathbb{N}}_0\right)\to \left(\left(j=0\wedge j\le k\right)\leftrightarrow 0\le k\right)$$
17	16	ralbidva	$$⊢j=0\to \left(\forall k\in {\mathbb{N}}_0\left(j=0\wedge j\le k\right)\leftrightarrow \forall k\in {\mathbb{N}}_{0}0\le k\right)$$
18	10 17	bitrd	$$⊢j=0\to \left(\forall k\in {\mathbb{Z}}_{\ge j}\left(j=0\wedge j\le k\right)\leftrightarrow \forall k\in {\mathbb{N}}_{0}0\le k\right)$$
19	18	rspcev	$$⊢\left(0\in {\mathbb{N}}_0\wedge \forall k\in {\mathbb{N}}_{0}0\le k\right)\to \exists j\in {\mathbb{N}}_0\forall k\in {\mathbb{Z}}_{\ge j}\left(j=0\wedge j\le k\right)$$
20	4 6 19	mp2an	$$⊢\exists j\in {\mathbb{N}}_0\forall k\in {\mathbb{Z}}_{\ge j}\left(j=0\wedge j\le k\right)$$
21		nfcv	$$⊢\underset{\_}{Ⅎ}j{\mathbb{N}}_0$$
22	1 21	nfcxfr	$$⊢\underset{\_}{Ⅎ}jZ$$
23	22 21 1	rexeqif	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(j=0\wedge j\le k\right)\leftrightarrow \exists j\in {\mathbb{N}}_0\forall k\in {\mathbb{Z}}_{\ge j}\left(j=0\wedge j\le k\right)$$
24	20 23	mpbir	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(j=0\wedge j\le k\right)$$
25	2	ralbii	$$⊢\forall k\in {\mathbb{Z}}_{\ge j}\phi \leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}\left(j=0\wedge j\le k\right)$$
26	25	rexbii	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(j=0\wedge j\le k\right)$$
27	24 26	mpbir	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi$$
28		1nn0	$$⊢1\in {\mathbb{N}}_0$$
29		nngt0	$$⊢k\in \mathbb{N}\to 0<k$$
30	29	rgen	$$⊢\forall k\in \mathbb{N}0<k$$
31		fveq2	$$⊢j=1\to {\mathbb{Z}}_{\ge j}={\mathbb{Z}}_{\ge 1}$$
32		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
33	31 32	eqtr4di	$$⊢j=1\to {\mathbb{Z}}_{\ge j}=\mathbb{N}$$
34	33	raleqdv	$$⊢j=1\to \left(\forall k\in {\mathbb{Z}}_{\ge j}0<k\leftrightarrow \forall k\in \mathbb{N}0<k\right)$$
35	34	rspcev	$$⊢\left(1\in {\mathbb{N}}_0\wedge \forall k\in \mathbb{N}0<k\right)\to \exists j\in {\mathbb{N}}_0\forall k\in {\mathbb{Z}}_{\ge j}0<k$$
36	28 30 35	mp2an	$$⊢\exists j\in {\mathbb{N}}_0\forall k\in {\mathbb{Z}}_{\ge j}0<k$$
37	22 21 1	rexeqif	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}0<k\leftrightarrow \exists j\in {\mathbb{N}}_0\forall k\in {\mathbb{Z}}_{\ge j}0<k$$
38	36 37	mpbir	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}0<k$$
39	3	ralbii	$$⊢\forall k\in {\mathbb{Z}}_{\ge j}\psi \leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}0<k$$
40	39	rexbii	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}0<k$$
41	38 40	mpbir	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi$$
42	27 41	pm3.2i	$$⊢\left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)$$
43		nfv	$$⊢Ⅎk\neg \left(\left(j=0\wedge j\le j\right)\wedge 0<j\right)$$
44		nfcv	$$⊢\underset{\_}{Ⅎ}kj$$
45		nfcv	$$⊢\underset{\_}{Ⅎ}k{\mathbb{Z}}_{\ge j}$$
46	8	uzid3	$$⊢j\in {\mathbb{N}}_0\to j\in {\mathbb{Z}}_{\ge j}$$
47	46	adantr	$$⊢\left(j\in {\mathbb{N}}_0\wedge j=0\right)\to j\in {\mathbb{Z}}_{\ge j}$$
48		0re	$$⊢0\in ℝ$$
49	48	ltnri	$$⊢\neg 0<0$$
50	49	a1i	$$⊢j=0\to \neg 0<0$$
51		eqcom	$$⊢j=0\leftrightarrow 0=j$$
52	51	biimpi	$$⊢j=0\to 0=j$$
53	50 52	brneqtrd	$$⊢j=0\to \neg 0<j$$
54	53	intnand	$$⊢j=0\to \neg \left(\left(j=0\wedge j\le j\right)\wedge 0<j\right)$$
55	54	adantl	$$⊢\left(j\in {\mathbb{N}}_0\wedge j=0\right)\to \neg \left(\left(j=0\wedge j\le j\right)\wedge 0<j\right)$$
56		breq2	$$⊢k=j\to \left(j\le k\leftrightarrow j\le j\right)$$
57	56	anbi2d	$$⊢k=j\to \left(\left(j=0\wedge j\le k\right)\leftrightarrow \left(j=0\wedge j\le j\right)\right)$$
58	2 57	bitrid	$$⊢k=j\to \left(\phi \leftrightarrow \left(j=0\wedge j\le j\right)\right)$$
59		breq2	$$⊢k=j\to \left(0<k\leftrightarrow 0<j\right)$$
60	3 59	bitrid	$$⊢k=j\to \left(\psi \leftrightarrow 0<j\right)$$
61	58 60	anbi12d	$$⊢k=j\to \left(\left(\phi \wedge \psi \right)\leftrightarrow \left(\left(j=0\wedge j\le j\right)\wedge 0<j\right)\right)$$
62	61	notbid	$$⊢k=j\to \left(\neg \left(\phi \wedge \psi \right)\leftrightarrow \neg \left(\left(j=0\wedge j\le j\right)\wedge 0<j\right)\right)$$
63	43 44 45 47 55 62	rspced	$$⊢\left(j\in {\mathbb{N}}_0\wedge j=0\right)\to \exists k\in {\mathbb{Z}}_{\ge j}\neg \left(\phi \wedge \psi \right)$$
64	46	adantr	$$⊢\left(j\in {\mathbb{N}}_0\wedge \neg j=0\right)\to j\in {\mathbb{Z}}_{\ge j}$$
65		id	$$⊢\neg j=0\to \neg j=0$$
66	65	intnanrd	$$⊢\neg j=0\to \neg \left(j=0\wedge j\le j\right)$$
67	66	intnanrd	$$⊢\neg j=0\to \neg \left(\left(j=0\wedge j\le j\right)\wedge 0<j\right)$$
68	67	adantl	$$⊢\left(j\in {\mathbb{N}}_0\wedge \neg j=0\right)\to \neg \left(\left(j=0\wedge j\le j\right)\wedge 0<j\right)$$
69	43 44 45 64 68 62	rspced	$$⊢\left(j\in {\mathbb{N}}_0\wedge \neg j=0\right)\to \exists k\in {\mathbb{Z}}_{\ge j}\neg \left(\phi \wedge \psi \right)$$
70	63 69	pm2.61dan	$$⊢j\in {\mathbb{N}}_0\to \exists k\in {\mathbb{Z}}_{\ge j}\neg \left(\phi \wedge \psi \right)$$
71		rexnal	$$⊢\exists k\in {\mathbb{Z}}_{\ge j}\neg \left(\phi \wedge \psi \right)\leftrightarrow \neg \forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)$$
72	70 71	sylib	$$⊢j\in {\mathbb{N}}_0\to \neg \forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)$$
73	72	nrex	$$⊢\neg \exists j\in {\mathbb{N}}_0\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)$$
74	22 21 1	rexeqif	$$⊢\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\leftrightarrow \exists j\in {\mathbb{N}}_0\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)$$
75	73 74	mtbir	$$⊢\neg \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)$$
76	42 75	pm3.2i	$$⊢\left(\left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)\wedge \neg \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\right)$$
77		annim	$$⊢\left(\left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)\wedge \neg \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\right)\leftrightarrow \neg \left(\left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\right)$$
78	76 77	mpbi	$$⊢\neg \left(\left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\right)$$
79	78	nimnbi2	$$⊢\neg \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(\phi \wedge \psi \right)\leftrightarrow \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\phi \wedge \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\psi \right)\right)$$