Metamath Proof Explorer


Theorem fzind

Description: Induction on the integers from M to N inclusive . The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Hypotheses fzind.1 x = M φ ψ
fzind.2 x = y φ χ
fzind.3 x = y + 1 φ θ
fzind.4 x = K φ τ
fzind.5 M N M N ψ
fzind.6 M N y M y y < N χ θ
Assertion fzind M N K M K K N τ

Proof

Step Hyp Ref Expression
1 fzind.1 x = M φ ψ
2 fzind.2 x = y φ χ
3 fzind.3 x = y + 1 φ θ
4 fzind.4 x = K φ τ
5 fzind.5 M N M N ψ
6 fzind.6 M N y M y y < N χ θ
7 breq1 x = M x N M N
8 7 anbi2d x = M N x N N M N
9 8 1 imbi12d x = M N x N φ N M N ψ
10 breq1 x = y x N y N
11 10 anbi2d x = y N x N N y N
12 11 2 imbi12d x = y N x N φ N y N χ
13 breq1 x = y + 1 x N y + 1 N
14 13 anbi2d x = y + 1 N x N N y + 1 N
15 14 3 imbi12d x = y + 1 N x N φ N y + 1 N θ
16 breq1 x = K x N K N
17 16 anbi2d x = K N x N N K N
18 17 4 imbi12d x = K N x N φ N K N τ
19 5 3expib M N M N ψ
20 zre y y
21 zre N N
22 p1le y N y + 1 N y N
23 22 3expia y N y + 1 N y N
24 20 21 23 syl2an y N y + 1 N y N
25 24 imdistanda y N y + 1 N N y N
26 25 imim1d y N y N χ N y + 1 N χ
27 26 3ad2ant2 M y M y N y N χ N y + 1 N χ
28 zltp1le y N y < N y + 1 N
29 28 adantlr y M y N y < N y + 1 N
30 29 expcom N y M y y < N y + 1 N
31 30 pm5.32d N y M y y < N y M y y + 1 N
32 31 adantl M N y M y y < N y M y y + 1 N
33 6 expcom y M y y < N M N χ θ
34 33 3expa y M y y < N M N χ θ
35 34 com12 M N y M y y < N χ θ
36 32 35 sylbird M N y M y y + 1 N χ θ
37 36 ex M N y M y y + 1 N χ θ
38 37 com23 M y M y y + 1 N N χ θ
39 38 expd M y M y y + 1 N N χ θ
40 39 3impib M y M y y + 1 N N χ θ
41 40 impcomd M y M y N y + 1 N χ θ
42 41 a2d M y M y N y + 1 N χ N y + 1 N θ
43 27 42 syld M y M y N y N χ N y + 1 N θ
44 9 12 15 18 19 43 uzind M K M K N K N τ
45 44 expcomd M K M K K N N τ
46 45 3expb M K M K K N N τ
47 46 expcom K M K M K N N τ
48 47 com23 K M K K N M N τ
49 48 3impia K M K K N M N τ
50 49 impd K M K K N M N τ
51 50 impcom M N K M K K N τ