Theorem 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	⊢ ( 𝑛 = 0 → ( 𝜓 ↔ 𝜒 ) )
	nn0min.1	⊢ ( 𝑛 = 𝑚 → ( 𝜓 ↔ 𝜃 ) )
	nn0min.2	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝜓 ↔ 𝜏 ) )
	nn0min.3	⊢ ( 𝜑 → ¬ 𝜒 )
	nn0min.4	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ 𝜓 )
Assertion	nn0min	⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ0 ( ¬ 𝜃 ∧ 𝜏 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0min.0	⊢ ( 𝑛 = 0 → ( 𝜓 ↔ 𝜒 ) )
2		nn0min.1	⊢ ( 𝑛 = 𝑚 → ( 𝜓 ↔ 𝜃 ) )
3		nn0min.2	⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝜓 ↔ 𝜏 ) )
4		nn0min.3	⊢ ( 𝜑 → ¬ 𝜒 )
5		nn0min.4	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ 𝜓 )
6	5	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ∃ 𝑛 ∈ ℕ 𝜓 )
7		nfv	⊢ Ⅎ 𝑚 𝜑
8		nfra1	⊢ Ⅎ 𝑚 ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 )
9	7 8	nfan	⊢ Ⅎ 𝑚 ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) )
10		nfv	⊢ Ⅎ 𝑚 ¬ [ 𝑘 / 𝑛 ] 𝜓
11	9 10	nfim	⊢ Ⅎ 𝑚 ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ [ 𝑘 / 𝑛 ] 𝜓 )
12		dfsbcq2	⊢ ( 𝑘 = 1 → ( [ 𝑘 / 𝑛 ] 𝜓 ↔ [ 1 / 𝑛 ] 𝜓 ) )
13	12	notbid	⊢ ( 𝑘 = 1 → ( ¬ [ 𝑘 / 𝑛 ] 𝜓 ↔ ¬ [ 1 / 𝑛 ] 𝜓 ) )
14	13	imbi2d	⊢ ( 𝑘 = 1 → ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ [ 𝑘 / 𝑛 ] 𝜓 ) ↔ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ [ 1 / 𝑛 ] 𝜓 ) ) )
15		nfv	⊢ Ⅎ 𝑛 𝜃
16	15 2	sbhypf	⊢ ( 𝑘 = 𝑚 → ( [ 𝑘 / 𝑛 ] 𝜓 ↔ 𝜃 ) )
17	16	notbid	⊢ ( 𝑘 = 𝑚 → ( ¬ [ 𝑘 / 𝑛 ] 𝜓 ↔ ¬ 𝜃 ) )
18	17	imbi2d	⊢ ( 𝑘 = 𝑚 → ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ [ 𝑘 / 𝑛 ] 𝜓 ) ↔ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ 𝜃 ) ) )
19		nfv	⊢ Ⅎ 𝑛 𝜏
20	19 3	sbhypf	⊢ ( 𝑘 = ( 𝑚 + 1 ) → ( [ 𝑘 / 𝑛 ] 𝜓 ↔ 𝜏 ) )
21	20	notbid	⊢ ( 𝑘 = ( 𝑚 + 1 ) → ( ¬ [ 𝑘 / 𝑛 ] 𝜓 ↔ ¬ 𝜏 ) )
22	21	imbi2d	⊢ ( 𝑘 = ( 𝑚 + 1 ) → ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ [ 𝑘 / 𝑛 ] 𝜓 ) ↔ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ 𝜏 ) ) )
23		sbequ12r	⊢ ( 𝑘 = 𝑛 → ( [ 𝑘 / 𝑛 ] 𝜓 ↔ 𝜓 ) )
24	23	notbid	⊢ ( 𝑘 = 𝑛 → ( ¬ [ 𝑘 / 𝑛 ] 𝜓 ↔ ¬ 𝜓 ) )
25	24	imbi2d	⊢ ( 𝑘 = 𝑛 → ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ [ 𝑘 / 𝑛 ] 𝜓 ) ↔ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ 𝜓 ) ) )
26		0nn0	⊢ 0 ∈ ℕ0
27	15 2	sbiev	⊢ ( [ 𝑚 / 𝑛 ] 𝜓 ↔ 𝜃 )
28		nfv	⊢ Ⅎ 𝑛 𝜒
29	28 1	sbhypf	⊢ ( 𝑚 = 0 → ( [ 𝑚 / 𝑛 ] 𝜓 ↔ 𝜒 ) )
30	27 29	bitr3id	⊢ ( 𝑚 = 0 → ( 𝜃 ↔ 𝜒 ) )
31	30	notbid	⊢ ( 𝑚 = 0 → ( ¬ 𝜃 ↔ ¬ 𝜒 ) )
32		oveq1	⊢ ( 𝑚 = 0 → ( 𝑚 + 1 ) = ( 0 + 1 ) )
33		0p1e1	⊢ ( 0 + 1 ) = 1
34	32 33	eqtrdi	⊢ ( 𝑚 = 0 → ( 𝑚 + 1 ) = 1 )
35		1nn	⊢ 1 ∈ ℕ
36		eleq1	⊢ ( ( 𝑚 + 1 ) = 1 → ( ( 𝑚 + 1 ) ∈ ℕ ↔ 1 ∈ ℕ ) )
37	35 36	mpbiri	⊢ ( ( 𝑚 + 1 ) = 1 → ( 𝑚 + 1 ) ∈ ℕ )
38	3	sbcieg	⊢ ( ( 𝑚 + 1 ) ∈ ℕ → ( [ ( 𝑚 + 1 ) / 𝑛 ] 𝜓 ↔ 𝜏 ) )
39	34 37 38	3syl	⊢ ( 𝑚 = 0 → ( [ ( 𝑚 + 1 ) / 𝑛 ] 𝜓 ↔ 𝜏 ) )
40	34	sbceq1d	⊢ ( 𝑚 = 0 → ( [ ( 𝑚 + 1 ) / 𝑛 ] 𝜓 ↔ [ 1 / 𝑛 ] 𝜓 ) )
41	39 40	bitr3d	⊢ ( 𝑚 = 0 → ( 𝜏 ↔ [ 1 / 𝑛 ] 𝜓 ) )
42	41	notbid	⊢ ( 𝑚 = 0 → ( ¬ 𝜏 ↔ ¬ [ 1 / 𝑛 ] 𝜓 ) )
43	31 42	imbi12d	⊢ ( 𝑚 = 0 → ( ( ¬ 𝜃 → ¬ 𝜏 ) ↔ ( ¬ 𝜒 → ¬ [ 1 / 𝑛 ] 𝜓 ) ) )
44	43	rspcv	⊢ ( 0 ∈ ℕ0 → ( ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) → ( ¬ 𝜒 → ¬ [ 1 / 𝑛 ] 𝜓 ) ) )
45	26 44	ax-mp	⊢ ( ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) → ( ¬ 𝜒 → ¬ [ 1 / 𝑛 ] 𝜓 ) )
46	4 45	mpan9	⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ [ 1 / 𝑛 ] 𝜓 )
47		cbvralsvw	⊢ ( ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ↔ ∀ 𝑘 ∈ ℕ0 [ 𝑘 / 𝑚 ] ( ¬ 𝜃 → ¬ 𝜏 ) )
48		nnnn0	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ0 )
49		sbequ12r	⊢ ( 𝑘 = 𝑚 → ( [ 𝑘 / 𝑚 ] ( ¬ 𝜃 → ¬ 𝜏 ) ↔ ( ¬ 𝜃 → ¬ 𝜏 ) ) )
50	49	rspcv	⊢ ( 𝑚 ∈ ℕ0 → ( ∀ 𝑘 ∈ ℕ0 [ 𝑘 / 𝑚 ] ( ¬ 𝜃 → ¬ 𝜏 ) → ( ¬ 𝜃 → ¬ 𝜏 ) ) )
51	48 50	syl	⊢ ( 𝑚 ∈ ℕ → ( ∀ 𝑘 ∈ ℕ0 [ 𝑘 / 𝑚 ] ( ¬ 𝜃 → ¬ 𝜏 ) → ( ¬ 𝜃 → ¬ 𝜏 ) ) )
52	47 51	biimtrid	⊢ ( 𝑚 ∈ ℕ → ( ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) → ( ¬ 𝜃 → ¬ 𝜏 ) ) )
53	52	adantld	⊢ ( 𝑚 ∈ ℕ → ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ( ¬ 𝜃 → ¬ 𝜏 ) ) )
54	53	a2d	⊢ ( 𝑚 ∈ ℕ → ( ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ 𝜃 ) → ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ 𝜏 ) ) )
55	11 14 18 22 25 46 54	nnindf	⊢ ( 𝑛 ∈ ℕ → ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ 𝜓 ) )
56	55	rgen	⊢ ∀ 𝑛 ∈ ℕ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ 𝜓 )
57		r19.21v	⊢ ( ∀ 𝑛 ∈ ℕ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ 𝜓 ) ↔ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ∀ 𝑛 ∈ ℕ ¬ 𝜓 ) )
58	56 57	mpbi	⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ∀ 𝑛 ∈ ℕ ¬ 𝜓 )
59		ralnex	⊢ ( ∀ 𝑛 ∈ ℕ ¬ 𝜓 ↔ ¬ ∃ 𝑛 ∈ ℕ 𝜓 )
60	58 59	sylib	⊢ ( ( 𝜑 ∧ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ) → ¬ ∃ 𝑛 ∈ ℕ 𝜓 )
61	6 60	pm2.65da	⊢ ( 𝜑 → ¬ ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) )
62		imnan	⊢ ( ( ¬ 𝜃 → ¬ 𝜏 ) ↔ ¬ ( ¬ 𝜃 ∧ 𝜏 ) )
63	62	ralbii	⊢ ( ∀ 𝑚 ∈ ℕ0 ( ¬ 𝜃 → ¬ 𝜏 ) ↔ ∀ 𝑚 ∈ ℕ0 ¬ ( ¬ 𝜃 ∧ 𝜏 ) )
64	61 63	sylnib	⊢ ( 𝜑 → ¬ ∀ 𝑚 ∈ ℕ0 ¬ ( ¬ 𝜃 ∧ 𝜏 ) )
65		dfrex2	⊢ ( ∃ 𝑚 ∈ ℕ0 ( ¬ 𝜃 ∧ 𝜏 ) ↔ ¬ ∀ 𝑚 ∈ ℕ0 ¬ ( ¬ 𝜃 ∧ 𝜏 ) )
66	64 65	sylibr	⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ0 ( ¬ 𝜃 ∧ 𝜏 ) )