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=1𝑜φψ
indpi.2 x=yφχ
indpi.3 x=y+𝑵1𝑜φθ
indpi.4 x=Aφτ
indpi.5 ψ
indpi.6 y𝑵χθ
Assertion indpi A𝑵τ

Proof

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