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 
|- ( n = 0 -> ( ps <-> ch ) )
nn0min.1 
|- ( n = m -> ( ps <-> th ) )
nn0min.2 
|- ( n = ( m + 1 ) -> ( ps <-> ta ) )
nn0min.3 
|- ( ph -> -. ch )
nn0min.4 
|- ( ph -> E. n e. NN ps )
Assertion nn0min 
|- ( ph -> E. m e. NN0 ( -. th /\ ta ) )

Proof

Step Hyp Ref Expression
1 nn0min.0 
 |-  ( n = 0 -> ( ps <-> ch ) )
2 nn0min.1 
 |-  ( n = m -> ( ps <-> th ) )
3 nn0min.2 
 |-  ( n = ( m + 1 ) -> ( ps <-> ta ) )
4 nn0min.3 
 |-  ( ph -> -. ch )
5 nn0min.4 
 |-  ( ph -> E. n e. NN ps )
6 5 adantr 
 |-  ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> E. n e. NN ps )
7 nfv 
 |-  F/ m ph
8 nfra1 
 |-  F/ m A. m e. NN0 ( -. th -> -. ta )
9 7 8 nfan 
 |-  F/ m ( ph /\ A. m e. NN0 ( -. th -> -. ta ) )
10 nfv 
 |-  F/ m -. [ k / n ] ps
11 9 10 nfim 
 |-  F/ m ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. [ k / n ] ps )
12 dfsbcq2 
 |-  ( k = 1 -> ( [ k / n ] ps <-> [. 1 / n ]. ps ) )
13 12 notbid 
 |-  ( k = 1 -> ( -. [ k / n ] ps <-> -. [. 1 / n ]. ps ) )
14 13 imbi2d 
 |-  ( k = 1 -> ( ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. [ k / n ] ps ) <-> ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. [. 1 / n ]. ps ) ) )
15 nfv 
 |-  F/ n th
16 15 2 sbhypf 
 |-  ( k = m -> ( [ k / n ] ps <-> th ) )
17 16 notbid 
 |-  ( k = m -> ( -. [ k / n ] ps <-> -. th ) )
18 17 imbi2d 
 |-  ( k = m -> ( ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. [ k / n ] ps ) <-> ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. th ) ) )
19 nfv 
 |-  F/ n ta
20 19 3 sbhypf 
 |-  ( k = ( m + 1 ) -> ( [ k / n ] ps <-> ta ) )
21 20 notbid 
 |-  ( k = ( m + 1 ) -> ( -. [ k / n ] ps <-> -. ta ) )
22 21 imbi2d 
 |-  ( k = ( m + 1 ) -> ( ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. [ k / n ] ps ) <-> ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. ta ) ) )
23 sbequ12r 
 |-  ( k = n -> ( [ k / n ] ps <-> ps ) )
24 23 notbid 
 |-  ( k = n -> ( -. [ k / n ] ps <-> -. ps ) )
25 24 imbi2d 
 |-  ( k = n -> ( ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. [ k / n ] ps ) <-> ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. ps ) ) )
26 0nn0 
 |-  0 e. NN0
27 15 2 sbiev 
 |-  ( [ m / n ] ps <-> th )
28 nfv 
 |-  F/ n ch
29 28 1 sbhypf 
 |-  ( m = 0 -> ( [ m / n ] ps <-> ch ) )
30 27 29 bitr3id 
 |-  ( m = 0 -> ( th <-> ch ) )
31 30 notbid 
 |-  ( m = 0 -> ( -. th <-> -. ch ) )
32 oveq1 
 |-  ( m = 0 -> ( m + 1 ) = ( 0 + 1 ) )
33 0p1e1 
 |-  ( 0 + 1 ) = 1
34 32 33 eqtrdi 
 |-  ( m = 0 -> ( m + 1 ) = 1 )
35 1nn 
 |-  1 e. NN
36 eleq1 
 |-  ( ( m + 1 ) = 1 -> ( ( m + 1 ) e. NN <-> 1 e. NN ) )
37 35 36 mpbiri 
 |-  ( ( m + 1 ) = 1 -> ( m + 1 ) e. NN )
38 3 sbcieg 
 |-  ( ( m + 1 ) e. NN -> ( [. ( m + 1 ) / n ]. ps <-> ta ) )
39 34 37 38 3syl 
 |-  ( m = 0 -> ( [. ( m + 1 ) / n ]. ps <-> ta ) )
40 34 sbceq1d 
 |-  ( m = 0 -> ( [. ( m + 1 ) / n ]. ps <-> [. 1 / n ]. ps ) )
41 39 40 bitr3d 
 |-  ( m = 0 -> ( ta <-> [. 1 / n ]. ps ) )
42 41 notbid 
 |-  ( m = 0 -> ( -. ta <-> -. [. 1 / n ]. ps ) )
43 31 42 imbi12d 
 |-  ( m = 0 -> ( ( -. th -> -. ta ) <-> ( -. ch -> -. [. 1 / n ]. ps ) ) )
44 43 rspcv 
 |-  ( 0 e. NN0 -> ( A. m e. NN0 ( -. th -> -. ta ) -> ( -. ch -> -. [. 1 / n ]. ps ) ) )
45 26 44 ax-mp 
 |-  ( A. m e. NN0 ( -. th -> -. ta ) -> ( -. ch -> -. [. 1 / n ]. ps ) )
46 4 45 mpan9 
 |-  ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. [. 1 / n ]. ps )
47 cbvralsvw 
 |-  ( A. m e. NN0 ( -. th -> -. ta ) <-> A. k e. NN0 [ k / m ] ( -. th -> -. ta ) )
48 nnnn0 
 |-  ( m e. NN -> m e. NN0 )
49 sbequ12r 
 |-  ( k = m -> ( [ k / m ] ( -. th -> -. ta ) <-> ( -. th -> -. ta ) ) )
50 49 rspcv 
 |-  ( m e. NN0 -> ( A. k e. NN0 [ k / m ] ( -. th -> -. ta ) -> ( -. th -> -. ta ) ) )
51 48 50 syl 
 |-  ( m e. NN -> ( A. k e. NN0 [ k / m ] ( -. th -> -. ta ) -> ( -. th -> -. ta ) ) )
52 47 51 syl5bi 
 |-  ( m e. NN -> ( A. m e. NN0 ( -. th -> -. ta ) -> ( -. th -> -. ta ) ) )
53 52 adantld 
 |-  ( m e. NN -> ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> ( -. th -> -. ta ) ) )
54 53 a2d 
 |-  ( m e. NN -> ( ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. th ) -> ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. ta ) ) )
55 11 14 18 22 25 46 54 nnindf 
 |-  ( n e. NN -> ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. ps ) )
56 55 rgen 
 |-  A. n e. NN ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. ps )
57 r19.21v 
 |-  ( A. n e. NN ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. ps ) <-> ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> A. n e. NN -. ps ) )
58 56 57 mpbi 
 |-  ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> A. n e. NN -. ps )
59 ralnex 
 |-  ( A. n e. NN -. ps <-> -. E. n e. NN ps )
60 58 59 sylib 
 |-  ( ( ph /\ A. m e. NN0 ( -. th -> -. ta ) ) -> -. E. n e. NN ps )
61 6 60 pm2.65da 
 |-  ( ph -> -. A. m e. NN0 ( -. th -> -. ta ) )
62 imnan 
 |-  ( ( -. th -> -. ta ) <-> -. ( -. th /\ ta ) )
63 62 ralbii 
 |-  ( A. m e. NN0 ( -. th -> -. ta ) <-> A. m e. NN0 -. ( -. th /\ ta ) )
64 61 63 sylnib 
 |-  ( ph -> -. A. m e. NN0 -. ( -. th /\ ta ) )
65 dfrex2 
 |-  ( E. m e. NN0 ( -. th /\ ta ) <-> -. A. m e. NN0 -. ( -. th /\ ta ) )
66 64 65 sylibr 
 |-  ( ph -> E. m e. NN0 ( -. th /\ ta ) )