nn0min

Description: Extracting the minimum positive integer for which a property ch does not hold. This uses substitutions similar to nn0ind . (Contributed by Thierry Arnoux, 6-May-2018)

	Ref	Expression
Hypotheses	nn0min.0	$⊢ n = 0 \to (ψ \leftrightarrow χ)$
	nn0min.1	$⊢ n = m \to (ψ \leftrightarrow θ)$
	nn0min.2	$⊢ n = m + 1 \to (ψ \leftrightarrow τ)$
	nn0min.3	$⊢ φ \to \neg χ$
	nn0min.4	$⊢ φ \to \exists n \in ℕ ψ$
Assertion	nn0min	$⊢ φ \to \exists m \in ℕ_{0} (\neg θ \land τ)$

Proof

Step	Hyp	Ref	Expression
1		nn0min.0	$⊢ n = 0 \to (ψ \leftrightarrow χ)$
2		nn0min.1	$⊢ n = m \to (ψ \leftrightarrow θ)$
3		nn0min.2	$⊢ n = m + 1 \to (ψ \leftrightarrow τ)$
4		nn0min.3	$⊢ φ \to \neg χ$
5		nn0min.4	$⊢ φ \to \exists n \in ℕ ψ$
6	5	adantr	$⊢ (φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \exists n \in ℕ ψ$
7		nfv	$⊢ Ⅎ m φ$
8		nfra1	$⊢ Ⅎ m \forall m \in ℕ_{0} (\neg θ \to \neg τ)$
9	7 8	nfan	$⊢ Ⅎ m (φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ))$
10		nfv	$⊢ Ⅎ m \neg [k/ n] ψ$
11	9 10	nfim	$⊢ Ⅎ m ((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg [k/ n] ψ)$
12		dfsbcq2	$⊢ k = 1 \to ([k/ n] ψ \leftrightarrow \underset{˙}{[} 1 / n \underset{˙}{]} ψ)$
13	12	notbid	$⊢ k = 1 \to (\neg [k/ n] ψ \leftrightarrow \neg \underset{˙}{[} 1 / n \underset{˙}{]} ψ)$
14	13	imbi2d	$⊢ k = 1 \to (((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg [k/ n] ψ) \leftrightarrow ((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg \underset{˙}{[} 1 / n \underset{˙}{]} ψ))$
15		nfv	$⊢ Ⅎ n θ$
16	15 2	sbhypf	$⊢ k = m \to ([k/ n] ψ \leftrightarrow θ)$
17	16	notbid	$⊢ k = m \to (\neg [k/ n] ψ \leftrightarrow \neg θ)$
18	17	imbi2d	$⊢ k = m \to (((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg [k/ n] ψ) \leftrightarrow ((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg θ))$
19		nfv	$⊢ Ⅎ n τ$
20	19 3	sbhypf	$⊢ k = m + 1 \to ([k/ n] ψ \leftrightarrow τ)$
21	20	notbid	$⊢ k = m + 1 \to (\neg [k/ n] ψ \leftrightarrow \neg τ)$
22	21	imbi2d	$⊢ k = m + 1 \to (((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg [k/ n] ψ) \leftrightarrow ((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg τ))$
23		sbequ12r	$⊢ k = n \to ([k/ n] ψ \leftrightarrow ψ)$
24	23	notbid	$⊢ k = n \to (\neg [k/ n] ψ \leftrightarrow \neg ψ)$
25	24	imbi2d	$⊢ k = n \to (((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg [k/ n] ψ) \leftrightarrow ((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg ψ))$
26		0nn0	$⊢ 0 \in ℕ_{0}$
27	15 2	sbiev	$⊢ [m/ n] ψ \leftrightarrow θ$
28		nfv	$⊢ Ⅎ n χ$
29	28 1	sbhypf	$⊢ m = 0 \to ([m/ n] ψ \leftrightarrow χ)$
30	27 29	bitr3id	$⊢ m = 0 \to (θ \leftrightarrow χ)$
31	30	notbid	$⊢ m = 0 \to (\neg θ \leftrightarrow \neg χ)$
32		oveq1	$⊢ m = 0 \to m + 1 = 0 + 1$
33		0p1e1	$⊢ 0 + 1 = 1$
34	32 33	eqtrdi	$⊢ m = 0 \to m + 1 = 1$
35		1nn	$⊢ 1 \in ℕ$
36		eleq1	$⊢ m + 1 = 1 \to (m + 1 \in ℕ \leftrightarrow 1 \in ℕ)$
37	35 36	mpbiri	$⊢ m + 1 = 1 \to m + 1 \in ℕ$
38	3	sbcieg	$⊢ m + 1 \in ℕ \to (\underset{˙}{[} (m + 1) / n \underset{˙}{]} ψ \leftrightarrow τ)$
39	34 37 38	3syl	$⊢ m = 0 \to (\underset{˙}{[} (m + 1) / n \underset{˙}{]} ψ \leftrightarrow τ)$
40	34	sbceq1d	$⊢ m = 0 \to (\underset{˙}{[} (m + 1) / n \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} 1 / n \underset{˙}{]} ψ)$
41	39 40	bitr3d	$⊢ m = 0 \to (τ \leftrightarrow \underset{˙}{[} 1 / n \underset{˙}{]} ψ)$
42	41	notbid	$⊢ m = 0 \to (\neg τ \leftrightarrow \neg \underset{˙}{[} 1 / n \underset{˙}{]} ψ)$
43	31 42	imbi12d	$⊢ m = 0 \to ((\neg θ \to \neg τ) \leftrightarrow (\neg χ \to \neg \underset{˙}{[} 1 / n \underset{˙}{]} ψ))$
44	43	rspcv	$⊢ 0 \in ℕ_{0} \to (\forall m \in ℕ_{0} (\neg θ \to \neg τ) \to (\neg χ \to \neg \underset{˙}{[} 1 / n \underset{˙}{]} ψ))$
45	26 44	ax-mp	$⊢ \forall m \in ℕ_{0} (\neg θ \to \neg τ) \to (\neg χ \to \neg \underset{˙}{[} 1 / n \underset{˙}{]} ψ)$
46	4 45	mpan9	$⊢ (φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg \underset{˙}{[} 1 / n \underset{˙}{]} ψ$
47		cbvralsvw	$⊢ \forall m \in ℕ_{0} (\neg θ \to \neg τ) \leftrightarrow \forall k \in ℕ_{0} [k/ m] (\neg θ \to \neg τ)$
48		nnnn0	$⊢ m \in ℕ \to m \in ℕ_{0}$
49		sbequ12r	$⊢ k = m \to ([k/ m] (\neg θ \to \neg τ) \leftrightarrow (\neg θ \to \neg τ))$
50	49	rspcv	$⊢ m \in ℕ_{0} \to (\forall k \in ℕ_{0} [k/ m] (\neg θ \to \neg τ) \to (\neg θ \to \neg τ))$
51	48 50	syl	$⊢ m \in ℕ \to (\forall k \in ℕ_{0} [k/ m] (\neg θ \to \neg τ) \to (\neg θ \to \neg τ))$
52	47 51	biimtrid	$⊢ m \in ℕ \to (\forall m \in ℕ_{0} (\neg θ \to \neg τ) \to (\neg θ \to \neg τ))$
53	52	adantld	$⊢ m \in ℕ \to ((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to (\neg θ \to \neg τ))$
54	53	a2d	$⊢ m \in ℕ \to (((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg θ) \to ((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg τ))$
55	11 14 18 22 25 46 54	nnindf	$⊢ n \in ℕ \to ((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg ψ)$
56	55	rgen	$⊢ \forall n \in ℕ ((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg ψ)$
57		r19.21v	$⊢ \forall n \in ℕ ((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg ψ) \leftrightarrow ((φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \forall n \in ℕ \neg ψ)$
58	56 57	mpbi	$⊢ (φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \forall n \in ℕ \neg ψ$
59		ralnex	$⊢ \forall n \in ℕ \neg ψ \leftrightarrow \neg \exists n \in ℕ ψ$
60	58 59	sylib	$⊢ (φ \land \forall m \in ℕ_{0} (\neg θ \to \neg τ)) \to \neg \exists n \in ℕ ψ$
61	6 60	pm2.65da	$⊢ φ \to \neg \forall m \in ℕ_{0} (\neg θ \to \neg τ)$
62		imnan	$⊢ (\neg θ \to \neg τ) \leftrightarrow \neg (\neg θ \land τ)$
63	62	ralbii	$⊢ \forall m \in ℕ_{0} (\neg θ \to \neg τ) \leftrightarrow \forall m \in ℕ_{0} \neg (\neg θ \land τ)$
64	61 63	sylnib	$⊢ φ \to \neg \forall m \in ℕ_{0} \neg (\neg θ \land τ)$
65		dfrex2	$⊢ \exists m \in ℕ_{0} (\neg θ \land τ) \leftrightarrow \neg \forall m \in ℕ_{0} \neg (\neg θ \land τ)$
66	64 65	sylibr	$⊢ φ \to \exists m \in ℕ_{0} (\neg θ \land τ)$

Metamath Proof Explorer

Theorem nn0min

Proof