Description: Indirect strong induction on the upper integers. (Contributed by Stefan O'Rear, 25-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | uzindi.a | |
|
uzindi.b | |
||
uzindi.c | |
||
uzindi.d | |
||
uzindi.e | |
||
uzindi.f | |
||
uzindi.g | |
||
Assertion | uzindi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uzindi.a | |
|
2 | uzindi.b | |
|
3 | uzindi.c | |
|
4 | uzindi.d | |
|
5 | uzindi.e | |
|
6 | uzindi.f | |
|
7 | uzindi.g | |
|
8 | eluzfz2 | |
|
9 | 2 8 | syl | |
10 | fzofi | |
|
11 | finnum | |
|
12 | 10 11 | mp1i | |
13 | simpll | |
|
14 | simpr | |
|
15 | elfzuz3 | |
|
16 | 15 | adantl | |
17 | fzoss2 | |
|
18 | fzossfz | |
|
19 | 17 18 | sstrdi | |
20 | 16 19 | syl | |
21 | 20 | sselda | |
22 | fzofi | |
|
23 | elfzofz | |
|
24 | 23 | adantl | |
25 | elfzuz3 | |
|
26 | fzoss2 | |
|
27 | 24 25 26 | 3syl | |
28 | fzonel | |
|
29 | 28 | jctr | |
30 | 29 | adantl | |
31 | ssnelpss | |
|
32 | 27 30 31 | sylc | |
33 | php3 | |
|
34 | 22 32 33 | sylancr | |
35 | id | |
|
36 | 35 | com13 | |
37 | 21 34 36 | sylc | |
38 | 37 | ex | |
39 | 38 | com23 | |
40 | 39 | alimdv | |
41 | 40 | ex | |
42 | 41 | com23 | |
43 | 42 | imp31 | |
44 | 13 14 43 3 | syl3anc | |
45 | 44 | ex | |
46 | 45 | 3adant2 | |
47 | 6 | eleq1d | |
48 | 47 4 | imbi12d | |
49 | 7 | eleq1d | |
50 | 49 5 | imbi12d | |
51 | 6 | oveq2d | |
52 | 7 | oveq2d | |
53 | 1 12 46 48 50 51 52 | indcardi | |
54 | 9 53 | mpd | |