HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem indpi 5006
Description: Principle of Finite Induction on positive integers.
Hypotheses
Ref Expression
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
Ref Expression
indpi |- (A e. N. -> ta)
Distinct variable groups:   x,y   x,A   ps,x   ch,x   th,x   ta,x   ph,y
Proof of Theorem indpi
StepHypRef Expression
1 nlt1pi 5005 . . . 4 |- -. A <N 1o
2 1pi 4983 . . . . 5 |- 1o e. N.
3 ltsopi 4988 . . . . . 6 |- <N Or N.
4 sotric 2851 . . . . . 6 |- (( <N Or N. /\ (A e. N. /\ 1o e. N.)) -> (A <N 1o <-> -. (A = 1o \/ 1o <N A)))
53, 4mpan 693 . . . . 5 |- ((A e. N. /\ 1o e. N.) -> (A <N 1o <-> -. (A = 1o \/ 1o <N A)))
62, 5mpan2 694 . . . 4 |- (A e. N. -> (A <N 1o <-> -. (A = 1o \/ 1o <N A)))
71, 6mtbii 714 . . 3 |- (A e. N. -> -. -. (A = 1o \/ 1o <N A))
8 nega 84 . . 3 |- (-. -. (A = 1o \/ 1o <N A) -> (A = 1o \/ 1o <N A))
97, 8syl 10 . 2 |- (A e. N. -> (A = 1o \/ 1o <N A))
102elisseti 1809 . . . . . . 7 |- 1o e. V
1110eqvinc 1874 . . . . . 6 |- (1o = A <-> E.x(x = 1o /\ x = A))
12 indpi.4 . . . . . 6 |- (x = A -> (ph <-> ta))
13 indpi.5 . . . . . . 7 |- ps
14 indpi.1 . . . . . . 7 |- (x = 1o -> (ph <-> ps))
1513, 14mpbiri 194 . . . . . 6 |- (x = 1o -> ph)
1611, 12, 15gencl 1819 . . . . 5 |- (1o = A -> ta)
1716eqcoms 1470 . . . 4 |- (A = 1o -> ta)
1817a1i 8 . . 3 |- (A e. N. -> (A = 1o -> ta))
19 1onn 4237 . . . . . . 7 |- 1o e. om
20 eleq1 1526 . . . . . . . . . 10 |- (x = 1o -> (x e. N. <-> 1o e. N.))
21 breq2 2613 . . . . . . . . . 10 |- (x = 1o -> (1o <N x <-> 1o <N 1o))
2220, 21anbi12d 626 . . . . . . . . 9 |- (x = 1o -> ((x e. N. /\ 1o <N x) <-> (1o e. N. /\ 1o <N 1o)))
2322, 14imbi12d 624 . . . . . . . 8 |- (x = 1o -> (((x e. N. /\ 1o <N x) -> ph) <-> ((1o e. N. /\ 1o <N 1o) -> ps)))
24 eleq1 1526 . . . . . . . . . 10 |- (x = y -> (x e. N. <-> y e. N.))
25 breq2 2613 . . . . . . . . . 10 |- (x = y -> (1o <N x <-> 1o <N y))
2624, 25anbi12d 626 . . . . . . . . 9 |- (x = y -> ((x e. N. /\ 1o <N x) <-> (y e. N. /\ 1o <N y)))
27 indpi.2 . . . . . . . . 9 |- (x = y -> (ph <-> ch))
2826, 27imbi12d 624 . . . . . . . 8 |- (x = y -> (((x e. N. /\ 1o <N x) -> ph) <-> ((y e. N. /\ 1o <N y) -> ch)))
29 eleq1 1526 . . . . . . . . . . . . . . . . 17 |- (x = suc y -> (x e. om <-> suc y e. om))
30 peano2b 3137 . . . . . . . . . . . . . . . . 17 |- (y e. om <-> suc y e. om)
3129, 30syl6bbr 536 . . . . . . . . . . . . . . . 16 |- (x = suc y -> (x e. om <-> y e. om))
32 pinn 4978 . . . . . . . . . . . . . . . 16 |- (x e. N. -> x e. om)
3331, 32syl5bi 208 . . . . . . . . . . . . . . 15 |- (x = suc y -> (x e. N. -> y e. om))
3433adantrd 391 . . . . . . . . . . . . . 14 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> y e. om))
35 eleq2 1527 . . . . . . . . . . . . . . . 16 |- (x = suc y -> (1o e. x <-> 1o e. suc y))
36 elsuci 3025 . . . . . . . . . . . . . . . . 17 |- (1o e. suc y -> (1o e. y \/ 1o = y))
37 ne0i 2276 . . . . . . . . . . . . . . . . . 18 |- (1o e. y -> y =/= (/))
38 0lt1o 4131 . . . . . . . . . . . . . . . . . . . 20 |- (/) e. 1o
39 eleq2 1527 . . . . . . . . . . . . . . . . . . . 20 |- (1o = y -> ((/) e. 1o <-> (/) e. y))
4038, 39mpbii 193 . . . . . . . . . . . . . . . . . . 19 |- (1o = y -> (/) e. y)
41 ne0i 2276 . . . . . . . . . . . . . . . . . . 19 |- ((/) e. y -> y =/= (/))
4240, 41syl 10 . . . . . . . . . . . . . . . . . 18 |- (1o = y -> y =/= (/))
4337, 42jaoi 341 . . . . . . . . . . . . . . . . 17 |- ((1o e. y \/ 1o = y) -> y =/= (/))
4436, 43syl 10 . . . . . . . . . . . . . . . 16 |- (1o e. suc y -> y =/= (/))
4535, 44syl6bi 214 . . . . . . . . . . . . . . 15 |- (x = suc y -> (1o e. x -> y =/= (/)))
46 ltpiord 4987 . . . . . . . . . . . . . . . . 17 |- ((1o e. N. /\ x e. N.) -> (1o <N x <-> 1o e. x))
472, 46mpan 693 . . . . . . . . . . . . . . . 16 |- (x e. N. -> (1o <N x <-> 1o e. x))
4847biimpa 416 . . . . . . . . . . . . . . 15 |- ((x e. N. /\ 1o <N x) -> 1o e. x)
4945, 48syl5 21 . . . . . . . . . . . . . 14 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> y =/= (/)))
5034, 49jcad 598 . . . . . . . . . . . . 13 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> (y e. om /\ y =/= (/))))
51 elni 4976 . . . . . . . . . . . . 13 |- (y e. N. <-> (y e. om /\ y =/= (/)))
5250, 51syl6ibr 213 . . . . . . . . . . . 12 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> y e. N.))
53 breq2 2613 . . . . . . . . . . . . 13 |- (x = suc y -> (1o <N x <-> 1o <N suc y))
54 pm3.27 323 . . . . . . . . . . . . 13 |- ((x e. N. /\ 1o <N x) -> 1o <N x)
5553, 54syl5bi 208 . . . . . . . . . . . 12 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> 1o <N suc y))
5652, 55jcad 598 . . . . . . . . . . 11 |- (x = suc y -> ((x e. N. /\ 1o <N x) -> (y e. N. /\ 1o <N suc y)))
57 addpiord 4984 . . . . . . . . . . . . . . . . . . . 20 |- ((y e. N. /\ 1o e. N.) -> (y +N 1o) = (y +o 1o))
582, 57mpan2 694 . . . . . . . . . . . . . . . . . . 19 |- (y e. N. -> (y +N 1o) = (y +o 1o))
59 pion 4979 . . . . . . . . . . . . . . . . . . . 20 |- (y e. N. -> y e. On)
60 oa1suc 4148 . . . . . . . . . . . . . . . . . . . 20 |- (y e. On -> (y +o 1o) = suc y)
6159, 60syl 10 . . . . . . . . . . . . . . . . . . 19 |- (y e. N. -> (y +o 1o) = suc y)
6258, 61eqtrd 1499 . . . . . . . . . . . . . . . . . 18 |- (y e. N. -> (y +N 1o) = suc y)
6362eqeq2d 1478 . . . . . . . . . . . . . . . . 17 |- (y e. N. -> (x = (y +N 1o) <-> x = suc y))
6463biimparc 419 . . . . . . . . . . . . . . . 16 |- ((x = suc y /\ y e. N.) -> x = (y +N 1o))
6564eleq1d 1532 . . . . . . . . . . . . . . 15 |- ((x = suc y /\ y e. N.) -> (x e. N. <-> (y +N 1o) e. N.))
66 addclpi 4992 . . . . . . . . . . . . . . . 16 |- ((y e. N. /\ 1o e. N.) -> (y +N 1o) e. N.)
672, 66mpan2 694 . . . . . . . . . . . . . . 15 |- (y e. N. -> (y +N 1o) e. N.)
6865, 67syl5bir 210 . . . . . . . . . . . . . 14 |- ((x = suc y /\ y e. N.) -> (y e. N. -> x e. N.))
6968ex 373 . . . . . . . . . . . . 13 |- (x = suc y -> (y e. N. -> (y e. N. -> x e. N.)))
7069pm2.43d 65 . . . . . . . . . . . 12 |- (x = suc y -> (y e. N. -> x e. N.))
7153biimprd 154 . . . . . . . . . . . 12 |- (x = suc y -> (1o <N suc y -> 1o <N x))
7270, 71anim12d 556 . . . . . . . . . . 11 |- (x = suc y -> ((y e. N. /\ 1o <N suc y) -> (x e. N. /\ 1o <N x)))
7356, 72impbid 514 . . . . . . . . . 10 |- (x = suc y -> ((x e. N. /\ 1o <N x) <-> (y e. N. /\ 1o <N suc y)))
7473imbi1d 611 . . . . . . . . 9 |- (x = suc y -> (((x e. N. /\ 1o <N x) -> ph) <-> ((y e. N. /\ 1o <N suc y) -> ph)))
75 indpi.3 . . . . . . . . . . . . 13 |- (x = (y +N 1o) -> (ph <-> th))
7663, 75syl6bir 215 . . . . . . . . . . . 12 |- (y e. N. -> (x = suc y -> (ph <-> th)))
7776adantr 389 . . . . . . . . . . 11 |- ((y e. N. /\ 1o <N suc y) -> (x = suc y -> (ph <-> th)))
7877com12 11 . . . . . . . . . 10 |- (x = suc y -> ((y e. N. /\ 1o <N suc y) -> (ph <-> th)))
7978pm5.74d 583 . . . . . . . . 9 |- (x = suc y -> (((y e. N. /\ 1o <N suc y) -> ph) <-> ((y e. N. /\ 1o <N suc y) -> th)))
8074, 79bitrd 526 . . . . . . . 8 |- (x = suc y -> (((x e. N. /\ 1o <N x) -> ph) <-> ((y e. N. /\ 1o <N suc y) -> th)))
81 eleq1 1526 . . . . . . . . . 10 |- (x = A -> (x e. N. <-> A e. N.))
82 breq2 2613 . . . . . . . . . 10 |- (x = A -> (1o <N x <-> 1o <N A))
8381, 82anbi12d 626 . . . . . . . . 9 |- (x = A -> ((x e. N. /\ 1o <N x) <-> (A e. N. /\ 1o <N A)))
8483, 12imbi12d 624 . . . . . . . 8 |- (x = A -> (((x e. N. /\ 1o <N x) -> ph) <-> ((A e. N. /\ 1o <N A) -> ta)))
8513a1i 8 . . . . . . . . 9 |- ((1o e. N. /\ 1o <N 1o) -> ps)
8685a1i 8 . . . . . . . 8 |- (1o e. om -> ((1o e. N. /\ 1o <N 1o) -> ps))
87 pm3.2 283 . . . . . . . . . . . . . 14 |- (y e. N. -> (1o e. y -> (y e. N. /\ 1o e. y)))
88 ltpiord 4987 . . . . . . . . . . . . . . . 16 |- ((1o e. N. /\ y e. N.) -> (1o <N y <-> 1o e. y))
892, 88mpan 693 . . . . . . . . . . . . . . 15 |- (y e. N. -> (1o <N y <-> 1o e. y))
9089pm5.32i 643 . . . . . . . . . . . . . 14 |- ((y e. N. /\ 1o <N y) <-> (y e. N. /\ 1o e. y))
9187, 90syl6ibr 213 . . . . . . . . . . . . 13 |- (y e. N. -> (1o e. y -> (y e. N. /\ 1o <N y)))
9291imim1d 28 . . . . . . . . . . . 12 |- (y e. N. -> (((y e. N. /\ 1o <N y) -> ch) -> (1o e. y -> ch)))
9310eqvinc 1874 . . . . . . . . . . . . . . . 16 |- (1o = y <-> E.x(