Metamath Proof Explorer


Theorem uzind

Description: Induction on the upper integers that start at M . The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by NM, 5-Jul-2005)

Ref Expression
Hypotheses uzind.1 j = M φ ψ
uzind.2 j = k φ χ
uzind.3 j = k + 1 φ θ
uzind.4 j = N φ τ
uzind.5 M ψ
uzind.6 M k M k χ θ
Assertion uzind M N M N τ

Proof

Step Hyp Ref Expression
1 uzind.1 j = M φ ψ
2 uzind.2 j = k φ χ
3 uzind.3 j = k + 1 φ θ
4 uzind.4 j = N φ τ
5 uzind.5 M ψ
6 uzind.6 M k M k χ θ
7 zre M M
8 7 leidd M M M
9 8 5 jca M M M ψ
10 9 ancli M M M M ψ
11 breq2 j = M M j M M
12 11 1 anbi12d j = M M j φ M M ψ
13 12 elrab M j | M j φ M M M ψ
14 10 13 sylibr M M j | M j φ
15 peano2z k k + 1
16 15 a1i M k k + 1
17 16 adantrd M k M k χ k + 1
18 zre k k
19 ltp1 k k < k + 1
20 19 adantl M k k < k + 1
21 peano2re k k + 1
22 21 ancli k k k + 1
23 lelttr M k k + 1 M k k < k + 1 M < k + 1
24 23 3expb M k k + 1 M k k < k + 1 M < k + 1
25 22 24 sylan2 M k M k k < k + 1 M < k + 1
26 20 25 mpan2d M k M k M < k + 1
27 ltle M k + 1 M < k + 1 M k + 1
28 21 27 sylan2 M k M < k + 1 M k + 1
29 26 28 syld M k M k M k + 1
30 7 18 29 syl2an M k M k M k + 1
31 30 adantrd M k M k χ M k + 1
32 31 expimpd M k M k χ M k + 1
33 6 3exp M k M k χ θ
34 33 imp4d M k M k χ θ
35 32 34 jcad M k M k χ M k + 1 θ
36 17 35 jcad M k M k χ k + 1 M k + 1 θ
37 breq2 j = k M j M k
38 37 2 anbi12d j = k M j φ M k χ
39 38 elrab k j | M j φ k M k χ
40 breq2 j = k + 1 M j M k + 1
41 40 3 anbi12d j = k + 1 M j φ M k + 1 θ
42 41 elrab k + 1 j | M j φ k + 1 M k + 1 θ
43 36 39 42 3imtr4g M k j | M j φ k + 1 j | M j φ
44 43 ralrimiv M k j | M j φ k + 1 j | M j φ
45 peano5uzti M M j | M j φ k j | M j φ k + 1 j | M j φ w | M w j | M j φ
46 14 44 45 mp2and M w | M w j | M j φ
47 46 sseld M N w | M w N j | M j φ
48 breq2 w = N M w M N
49 48 elrab N w | M w N M N
50 breq2 j = N M j M N
51 50 4 anbi12d j = N M j φ M N τ
52 51 elrab N j | M j φ N M N τ
53 47 49 52 3imtr3g M N M N N M N τ
54 53 3impib M N M N N M N τ
55 54 simprrd M N M N τ