Metamath Proof Explorer

Theorem indpi

Description: Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996) (New usage is discouraged.)

Ref Expression
Hypotheses indpi.1 
|- ( x = 1o -> ( ph <-> ps ) )
indpi.2 
|- ( x = y -> ( ph <-> ch ) )
indpi.3 
|- ( x = ( y +N 1o ) -> ( ph <-> th ) )
indpi.4 
|- ( x = A -> ( ph <-> ta ) )
indpi.5 
|- ps
indpi.6 
|- ( y e. N. -> ( ch -> th ) )
Assertion indpi 
|- ( A e. N. -> ta )

Proof

Step Hyp Ref Expression
1 indpi.1 
 |-  ( x = 1o -> ( ph <-> ps ) )
2 indpi.2 
 |-  ( x = y -> ( ph <-> ch ) )
3 indpi.3 
 |-  ( x = ( y +N 1o ) -> ( ph <-> th ) )
4 indpi.4 
 |-  ( x = A -> ( ph <-> ta ) )
5 indpi.5 
 |-  ps
6 indpi.6 
 |-  ( y e. N. -> ( ch -> th ) )
7 1oex 
 |-  1o e. _V
8 7 eqvinc 
 |-  ( 1o = A <-> E. x ( x = 1o /\ x = A ) )
9 5 1 mpbiri 
 |-  ( x = 1o -> ph )
10 8 4 9 gencl 
 |-  ( 1o = A -> ta )
11 10 eqcoms 
 |-  ( A = 1o -> ta )
12 11 a1i 
 |-  ( A e. N. -> ( A = 1o -> ta ) )
13 pinn 
 |-  ( A e. N. -> A e. _om )
14 elni2 
 |-  ( A e. N. <-> ( A e. _om /\ (/) e. A ) )
15 nnord 
 |-  ( A e. _om -> Ord A )
16 ordsucss 
 |-  ( Ord A -> ( (/) e. A -> suc (/) C_ A ) )
17 15 16 syl 
 |-  ( A e. _om -> ( (/) e. A -> suc (/) C_ A ) )
18 df-1o 
 |-  1o = suc (/)
19 18 sseq1i 
 |-  ( 1o C_ A <-> suc (/) C_ A )
20 17 19 syl6ibr 
 |-  ( A e. _om -> ( (/) e. A -> 1o C_ A ) )
21 20 imp 
 |-  ( ( A e. _om /\ (/) e. A ) -> 1o C_ A )
22 14 21 sylbi 
 |-  ( A e. N. -> 1o C_ A )
23 1onn 
 |-  1o e. _om
24 eleq1 
 |-  ( x = 1o -> ( x e. N. <-> 1o e. N. ) )
25 breq2 
 |-  ( x = 1o -> ( 1o  1o
26 24 25 anbi12d 
 |-  ( x = 1o -> ( ( x e. N. /\ 1o  ( 1o e. N. /\ 1o
27 26 1 imbi12d 
 |-  ( x = 1o -> ( ( ( x e. N. /\ 1o  ph ) <-> ( ( 1o e. N. /\ 1o  ps ) ) )
28 eleq1 
 |-  ( x = y -> ( x e. N. <-> y e. N. ) )
29 breq2 
 |-  ( x = y -> ( 1o  1o
30 28 29 anbi12d 
 |-  ( x = y -> ( ( x e. N. /\ 1o  ( y e. N. /\ 1o
31 30 2 imbi12d 
 |-  ( x = y -> ( ( ( x e. N. /\ 1o  ph ) <-> ( ( y e. N. /\ 1o  ch ) ) )
32 pinn 
 |-  ( x e. N. -> x e. _om )
33 eleq1 
 |-  ( x = suc y -> ( x e. _om <-> suc y e. _om ) )
34 peano2b 
 |-  ( y e. _om <-> suc y e. _om )
35 33 34 bitr4di 
 |-  ( x = suc y -> ( x e. _om <-> y e. _om ) )
36 32 35 syl5ib 
 |-  ( x = suc y -> ( x e. N. -> y e. _om ) )
37 36 adantrd 
 |-  ( x = suc y -> ( ( x e. N. /\ 1o  y e. _om ) )
38 1pi 
 |-  1o e. N.
39 ltpiord 
 |-  ( ( 1o e. N. /\ x e. N. ) -> ( 1o  1o e. x ) )
40 38 39 mpan 
 |-  ( x e. N. -> ( 1o  1o e. x ) )
41 40 biimpa 
 |-  ( ( x e. N. /\ 1o  1o e. x )
42 eleq2 
 |-  ( x = suc y -> ( 1o e. x <-> 1o e. suc y ) )
43 elsuci 
 |-  ( 1o e. suc y -> ( 1o e. y \/ 1o = y ) )
44 ne0i 
 |-  ( 1o e. y -> y =/= (/) )
45 0lt1o 
 |-  (/) e. 1o
46 eleq2 
 |-  ( 1o = y -> ( (/) e. 1o <-> (/) e. y ) )
47 45 46 mpbii 
 |-  ( 1o = y -> (/) e. y )
48 47 ne0d 
 |-  ( 1o = y -> y =/= (/) )
49 44 48 jaoi 
 |-  ( ( 1o e. y \/ 1o = y ) -> y =/= (/) )
50 43 49 syl 
 |-  ( 1o e. suc y -> y =/= (/) )
51 42 50 syl6bi 
 |-  ( x = suc y -> ( 1o e. x -> y =/= (/) ) )
52 41 51 syl5 
 |-  ( x = suc y -> ( ( x e. N. /\ 1o  y =/= (/) ) )
53 37 52 jcad 
 |-  ( x = suc y -> ( ( x e. N. /\ 1o  ( y e. _om /\ y =/= (/) ) ) )
54 elni 
 |-  ( y e. N. <-> ( y e. _om /\ y =/= (/) ) )
55 53 54 syl6ibr 
 |-  ( x = suc y -> ( ( x e. N. /\ 1o  y e. N. ) )
56 simpr 
 |-  ( ( x e. N. /\ 1o  1o
57 breq2 
 |-  ( x = suc y -> ( 1o  1o
58 56 57 syl5ib 
 |-  ( x = suc y -> ( ( x e. N. /\ 1o  1o
59 55 58 jcad 
 |-  ( x = suc y -> ( ( x e. N. /\ 1o  ( y e. N. /\ 1o
60 addclpi 
 |-  ( ( y e. N. /\ 1o e. N. ) -> ( y +N 1o ) e. N. )
61 38 60 mpan2 
 |-  ( y e. N. -> ( y +N 1o ) e. N. )
62 addpiord 
 |-  ( ( y e. N. /\ 1o e. N. ) -> ( y +N 1o ) = ( y +o 1o ) )
63 38 62 mpan2 
 |-  ( y e. N. -> ( y +N 1o ) = ( y +o 1o ) )
64 pion 
 |-  ( y e. N. -> y e. On )
65 oa1suc 
 |-  ( y e. On -> ( y +o 1o ) = suc y )
66 64 65 syl 
 |-  ( y e. N. -> ( y +o 1o ) = suc y )
67 63 66 eqtrd 
 |-  ( y e. N. -> ( y +N 1o ) = suc y )
68 67 eqeq2d 
 |-  ( y e. N. -> ( x = ( y +N 1o ) <-> x = suc y ) )
69 68 biimparc 
 |-  ( ( x = suc y /\ y e. N. ) -> x = ( y +N 1o ) )
70 69 eleq1d 
 |-  ( ( x = suc y /\ y e. N. ) -> ( x e. N. <-> ( y +N 1o ) e. N. ) )
71 61 70 syl5ibr 
 |-  ( ( x = suc y /\ y e. N. ) -> ( y e. N. -> x e. N. ) )
72 71 ex 
 |-  ( x = suc y -> ( y e. N. -> ( y e. N. -> x e. N. ) ) )
73 72 pm2.43d 
 |-  ( x = suc y -> ( y e. N. -> x e. N. ) )
74 57 biimprd 
 |-  ( x = suc y -> ( 1o  1o
75 73 74 anim12d 
 |-  ( x = suc y -> ( ( y e. N. /\ 1o  ( x e. N. /\ 1o
76 59 75 impbid 
 |-  ( x = suc y -> ( ( x e. N. /\ 1o  ( y e. N. /\ 1o
77 76 imbi1d 
 |-  ( x = suc y -> ( ( ( x e. N. /\ 1o  ph ) <-> ( ( y e. N. /\ 1o  ph ) ) )
78 68 3 syl6bir 
 |-  ( y e. N. -> ( x = suc y -> ( ph <-> th ) ) )
79 78 adantr 
 |-  ( ( y e. N. /\ 1o  ( x = suc y -> ( ph <-> th ) ) )
80 79 com12 
 |-  ( x = suc y -> ( ( y e. N. /\ 1o  ( ph <-> th ) ) )
81 80 pm5.74d 
 |-  ( x = suc y -> ( ( ( y e. N. /\ 1o  ph ) <-> ( ( y e. N. /\ 1o  th ) ) )
82 77 81 bitrd 
 |-  ( x = suc y -> ( ( ( x e. N. /\ 1o  ph ) <-> ( ( y e. N. /\ 1o  th ) ) )
83 eleq1 
 |-  ( x = A -> ( x e. N. <-> A e. N. ) )
84 breq2 
 |-  ( x = A -> ( 1o  1o
85 83 84 anbi12d 
 |-  ( x = A -> ( ( x e. N. /\ 1o  ( A e. N. /\ 1o
86 85 4 imbi12d 
 |-  ( x = A -> ( ( ( x e. N. /\ 1o  ph ) <-> ( ( A e. N. /\ 1o  ta ) ) )
87 5 2a1i 
 |-  ( 1o e. _om -> ( ( 1o e. N. /\ 1o  ps ) )
88 ltpiord 
 |-  ( ( 1o e. N. /\ y e. N. ) -> ( 1o  1o e. y ) )
89 38 88 mpan 
 |-  ( y e. N. -> ( 1o  1o e. y ) )
90 89 pm5.32i 
 |-  ( ( y e. N. /\ 1o  ( y e. N. /\ 1o e. y ) )
91 90 simplbi2 
 |-  ( y e. N. -> ( 1o e. y -> ( y e. N. /\ 1o
92 91 imim1d 
 |-  ( y e. N. -> ( ( ( y e. N. /\ 1o  ch ) -> ( 1o e. y -> ch ) ) )
93 ltrelpi 
 |-
94 93 brel 
 |-  ( 1o  ( 1o e. N. /\ suc y e. N. ) )
95 ltpiord 
 |-  ( ( 1o e. N. /\ suc y e. N. ) -> ( 1o  1o e. suc y ) )
96 94 95 syl 
 |-  ( 1o  ( 1o  1o e. suc y ) )
97 96 ibi 
 |-  ( 1o  1o e. suc y )
98 7 eqvinc 
 |-  ( 1o = y <-> E. x ( x = 1o /\ x = y ) )
99 98 2 9 gencl 
 |-  ( 1o = y -> ch )
100 jao 
 |-  ( ( 1o e. y -> ch ) -> ( ( 1o = y -> ch ) -> ( ( 1o e. y \/ 1o = y ) -> ch ) ) )
101 99 100 mpi 
 |-  ( ( 1o e. y -> ch ) -> ( ( 1o e. y \/ 1o = y ) -> ch ) )
102 43 101 syl5 
 |-  ( ( 1o e. y -> ch ) -> ( 1o e. suc y -> ch ) )
103 97 102 syl5 
 |-  ( ( 1o e. y -> ch ) -> ( 1o  ch ) )
104 92 103 syl6com 
 |-  ( ( ( y e. N. /\ 1o  ch ) -> ( y e. N. -> ( 1o  ch ) ) )
105 104 impd 
 |-  ( ( ( y e. N. /\ 1o  ch ) -> ( ( y e. N. /\ 1o  ch ) )
106 18 sseq1i 
 |-  ( 1o C_ y <-> suc (/) C_ y )
107 0ex 
 |-  (/) e. _V
108 sucssel 
 |-  ( (/) e. _V -> ( suc (/) C_ y -> (/) e. y ) )
109 107 108 ax-mp 
 |-  ( suc (/) C_ y -> (/) e. y )
110 106 109 sylbi 
 |-  ( 1o C_ y -> (/) e. y )
111 elni2 
 |-  ( y e. N. <-> ( y e. _om /\ (/) e. y ) )
112 111 6 sylbir 
 |-  ( ( y e. _om /\ (/) e. y ) -> ( ch -> th ) )
113 110 112 sylan2 
 |-  ( ( y e. _om /\ 1o C_ y ) -> ( ch -> th ) )
114 105 113 syl9r 
 |-  ( ( y e. _om /\ 1o C_ y ) -> ( ( ( y e. N. /\ 1o  ch ) -> ( ( y e. N. /\ 1o  th ) ) )
115 114 adantlr 
 |-  ( ( ( y e. _om /\ 1o e. _om ) /\ 1o C_ y ) -> ( ( ( y e. N. /\ 1o  ch ) -> ( ( y e. N. /\ 1o  th ) ) )
116 27 31 82 86 87 115 findsg 
 |-  ( ( ( A e. _om /\ 1o e. _om ) /\ 1o C_ A ) -> ( ( A e. N. /\ 1o  ta ) )
117 23 116 mpanl2 
 |-  ( ( A e. _om /\ 1o C_ A ) -> ( ( A e. N. /\ 1o  ta ) )
118 13 22 117 syl2anc 
 |-  ( A e. N. -> ( ( A e. N. /\ 1o  ta ) )
119 118 expd 
 |-  ( A e. N. -> ( A e. N. -> ( 1o  ta ) ) )
120 119 pm2.43i 
 |-  ( A e. N. -> ( 1o  ta ) )
121 nlt1pi 
 |-  -. A
122 ltsopi 
 |-
123 sotric 
 |-  ( (  ( A  -. ( A = 1o \/ 1o
124 122 123 mpan 
 |-  ( ( A e. N. /\ 1o e. N. ) -> ( A  -. ( A = 1o \/ 1o
125 38 124 mpan2 
 |-  ( A e. N. -> ( A  -. ( A = 1o \/ 1o
126 121 125 mtbii 
 |-  ( A e. N. -> -. -. ( A = 1o \/ 1o
127 126 notnotrd 
 |-  ( A e. N. -> ( A = 1o \/ 1o
128 12 120 127 mpjaod 
 |-  ( A e. N. -> ta )