This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ( ¬ 𝜃 ∧ 𝜏 ) )