Metamath Proof Explorer


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 syl5bi ( 𝑚 ∈ ℕ → ( ∀ 𝑚 ∈ ℕ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 ( ¬ 𝜃𝜏 ) )