Metamath Proof Explorer

Theorem zindd

Description: Principle of Mathematical Induction on all integers, deduction version. The first five hypotheses give the substitutions; the last three are the basis, the induction, and the extension to negative numbers. (Contributed by Paul Chapman, 17-Apr-2009) (Proof shortened by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses zindd.1 
|- ( x = 0 -> ( ph <-> ps ) )
zindd.2 
|- ( x = y -> ( ph <-> ch ) )
zindd.3 
|- ( x = ( y + 1 ) -> ( ph <-> ta ) )
zindd.4 
|- ( x = -u y -> ( ph <-> th ) )
zindd.5 
|- ( x = A -> ( ph <-> et ) )
zindd.6 
|- ( ze -> ps )
zindd.7 
|- ( ze -> ( y e. NN0 -> ( ch -> ta ) ) )
zindd.8 
|- ( ze -> ( y e. NN -> ( ch -> th ) ) )
Assertion zindd 
|- ( ze -> ( A e. ZZ -> et ) )

Proof

Step Hyp Ref Expression
1 zindd.1 
 |-  ( x = 0 -> ( ph <-> ps ) )
2 zindd.2 
 |-  ( x = y -> ( ph <-> ch ) )
3 zindd.3 
 |-  ( x = ( y + 1 ) -> ( ph <-> ta ) )
4 zindd.4 
 |-  ( x = -u y -> ( ph <-> th ) )
5 zindd.5 
 |-  ( x = A -> ( ph <-> et ) )
6 zindd.6 
 |-  ( ze -> ps )
7 zindd.7 
 |-  ( ze -> ( y e. NN0 -> ( ch -> ta ) ) )
8 zindd.8 
 |-  ( ze -> ( y e. NN -> ( ch -> th ) ) )
9 znegcl 
 |-  ( y e. ZZ -> -u y e. ZZ )
10 elznn0nn 
 |-  ( -u y e. ZZ <-> ( -u y e. NN0 \/ ( -u y e. RR /\ -u -u y e. NN ) ) )
11 9 10 sylib 
 |-  ( y e. ZZ -> ( -u y e. NN0 \/ ( -u y e. RR /\ -u -u y e. NN ) ) )
12 simpr 
 |-  ( ( -u y e. RR /\ -u -u y e. NN ) -> -u -u y e. NN )
13 12 orim2i 
 |-  ( ( -u y e. NN0 \/ ( -u y e. RR /\ -u -u y e. NN ) ) -> ( -u y e. NN0 \/ -u -u y e. NN ) )
14 11 13 syl 
 |-  ( y e. ZZ -> ( -u y e. NN0 \/ -u -u y e. NN ) )
15 zcn 
 |-  ( y e. ZZ -> y e. CC )
16 15 negnegd 
 |-  ( y e. ZZ -> -u -u y = y )
17 16 eleq1d 
 |-  ( y e. ZZ -> ( -u -u y e. NN <-> y e. NN ) )
18 17 orbi2d 
 |-  ( y e. ZZ -> ( ( -u y e. NN0 \/ -u -u y e. NN ) <-> ( -u y e. NN0 \/ y e. NN ) ) )
19 14 18 mpbid 
 |-  ( y e. ZZ -> ( -u y e. NN0 \/ y e. NN ) )
20 1 imbi2d 
 |-  ( x = 0 -> ( ( ze -> ph ) <-> ( ze -> ps ) ) )
21 2 imbi2d 
 |-  ( x = y -> ( ( ze -> ph ) <-> ( ze -> ch ) ) )
22 3 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( ze -> ph ) <-> ( ze -> ta ) ) )
23 4 imbi2d 
 |-  ( x = -u y -> ( ( ze -> ph ) <-> ( ze -> th ) ) )
24 7 com12 
 |-  ( y e. NN0 -> ( ze -> ( ch -> ta ) ) )
25 24 a2d 
 |-  ( y e. NN0 -> ( ( ze -> ch ) -> ( ze -> ta ) ) )
26 20 21 22 23 6 25 nn0ind 
 |-  ( -u y e. NN0 -> ( ze -> th ) )
27 26 com12 
 |-  ( ze -> ( -u y e. NN0 -> th ) )
28 20 21 22 21 6 25 nn0ind 
 |-  ( y e. NN0 -> ( ze -> ch ) )
29 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
30 28 29 syl11 
 |-  ( ze -> ( y e. NN -> ch ) )
31 30 8 mpdd 
 |-  ( ze -> ( y e. NN -> th ) )
32 27 31 jaod 
 |-  ( ze -> ( ( -u y e. NN0 \/ y e. NN ) -> th ) )
33 19 32 syl5 
 |-  ( ze -> ( y e. ZZ -> th ) )
34 33 ralrimiv 
 |-  ( ze -> A. y e. ZZ th )
35 znegcl 
 |-  ( x e. ZZ -> -u x e. ZZ )
36 negeq 
 |-  ( y = -u x -> -u y = -u -u x )
37 zcn 
 |-  ( x e. ZZ -> x e. CC )
38 37 negnegd 
 |-  ( x e. ZZ -> -u -u x = x )
39 36 38 sylan9eqr 
 |-  ( ( x e. ZZ /\ y = -u x ) -> -u y = x )
40 39 eqcomd 
 |-  ( ( x e. ZZ /\ y = -u x ) -> x = -u y )
41 40 4 syl 
 |-  ( ( x e. ZZ /\ y = -u x ) -> ( ph <-> th ) )
42 41 bicomd 
 |-  ( ( x e. ZZ /\ y = -u x ) -> ( th <-> ph ) )
43 35 42 rspcdv 
 |-  ( x e. ZZ -> ( A. y e. ZZ th -> ph ) )
44 43 com12 
 |-  ( A. y e. ZZ th -> ( x e. ZZ -> ph ) )
45 44 ralrimiv 
 |-  ( A. y e. ZZ th -> A. x e. ZZ ph )
46 5 rspccv 
 |-  ( A. x e. ZZ ph -> ( A e. ZZ -> et ) )
47 34 45 46 3syl 
 |-  ( ze -> ( A e. ZZ -> et ) )