Metamath Proof Explorer

Theorem zindbi

Description: Inductively transfer a property to the integers if it holds for zero and passes between adjacent integers in either direction. (Contributed by Stefan O'Rear, 1-Oct-2014)

Ref Expression
Hypotheses zindbi.1 
|- ( y e. ZZ -> ( ps <-> ch ) )
zindbi.2 
|- ( x = y -> ( ph <-> ps ) )
zindbi.3 
|- ( x = ( y + 1 ) -> ( ph <-> ch ) )
zindbi.4 
|- ( x = 0 -> ( ph <-> th ) )
zindbi.5 
|- ( x = A -> ( ph <-> ta ) )
Assertion zindbi 
|- ( A e. ZZ -> ( th <-> ta ) )

Proof

Step Hyp Ref Expression
1 zindbi.1 
 |-  ( y e. ZZ -> ( ps <-> ch ) )
2 zindbi.2 
 |-  ( x = y -> ( ph <-> ps ) )
3 zindbi.3 
 |-  ( x = ( y + 1 ) -> ( ph <-> ch ) )
4 zindbi.4 
 |-  ( x = 0 -> ( ph <-> th ) )
5 zindbi.5 
 |-  ( x = A -> ( ph <-> ta ) )
6 c0ex 
 |-  0 e. _V
7 6 4 sbcie 
 |-  ( [. 0 / x ]. ph <-> th )
8 0z 
 |-  0 e. ZZ
9 eleq1 
 |-  ( y = 0 -> ( y e. ZZ <-> 0 e. ZZ ) )
10 breq1 
 |-  ( y = 0 -> ( y <_ b <-> 0 <_ b ) )
11 9 10 3anbi13d 
 |-  ( y = 0 -> ( ( y e. ZZ /\ b e. ZZ /\ y <_ b ) <-> ( 0 e. ZZ /\ b e. ZZ /\ 0 <_ b ) ) )
12 dfsbcq 
 |-  ( y = 0 -> ( [. y / x ]. ph <-> [. 0 / x ]. ph ) )
13 12 bibi1d 
 |-  ( y = 0 -> ( ( [. y / x ]. ph <-> [. b / x ]. ph ) <-> ( [. 0 / x ]. ph <-> [. b / x ]. ph ) ) )
14 11 13 imbi12d 
 |-  ( y = 0 -> ( ( ( y e. ZZ /\ b e. ZZ /\ y <_ b ) -> ( [. y / x ]. ph <-> [. b / x ]. ph ) ) <-> ( ( 0 e. ZZ /\ b e. ZZ /\ 0 <_ b ) -> ( [. 0 / x ]. ph <-> [. b / x ]. ph ) ) ) )
15 eleq1 
 |-  ( b = A -> ( b e. ZZ <-> A e. ZZ ) )
16 breq2 
 |-  ( b = A -> ( 0 <_ b <-> 0 <_ A ) )
17 15 16 3anbi23d 
 |-  ( b = A -> ( ( 0 e. ZZ /\ b e. ZZ /\ 0 <_ b ) <-> ( 0 e. ZZ /\ A e. ZZ /\ 0 <_ A ) ) )
18 dfsbcq 
 |-  ( b = A -> ( [. b / x ]. ph <-> [. A / x ]. ph ) )
19 18 bibi2d 
 |-  ( b = A -> ( ( [. 0 / x ]. ph <-> [. b / x ]. ph ) <-> ( [. 0 / x ]. ph <-> [. A / x ]. ph ) ) )
20 17 19 imbi12d 
 |-  ( b = A -> ( ( ( 0 e. ZZ /\ b e. ZZ /\ 0 <_ b ) -> ( [. 0 / x ]. ph <-> [. b / x ]. ph ) ) <-> ( ( 0 e. ZZ /\ A e. ZZ /\ 0 <_ A ) -> ( [. 0 / x ]. ph <-> [. A / x ]. ph ) ) ) )
21 dfsbcq 
 |-  ( a = y -> ( [. a / x ]. ph <-> [. y / x ]. ph ) )
22 21 bibi2d 
 |-  ( a = y -> ( ( [. y / x ]. ph <-> [. a / x ]. ph ) <-> ( [. y / x ]. ph <-> [. y / x ]. ph ) ) )
23 dfsbcq 
 |-  ( a = b -> ( [. a / x ]. ph <-> [. b / x ]. ph ) )
24 23 bibi2d 
 |-  ( a = b -> ( ( [. y / x ]. ph <-> [. a / x ]. ph ) <-> ( [. y / x ]. ph <-> [. b / x ]. ph ) ) )
25 dfsbcq 
 |-  ( a = ( b + 1 ) -> ( [. a / x ]. ph <-> [. ( b + 1 ) / x ]. ph ) )
26 25 bibi2d 
 |-  ( a = ( b + 1 ) -> ( ( [. y / x ]. ph <-> [. a / x ]. ph ) <-> ( [. y / x ]. ph <-> [. ( b + 1 ) / x ]. ph ) ) )
27 biidd 
 |-  ( y e. ZZ -> ( [. y / x ]. ph <-> [. y / x ]. ph ) )
28 vex 
 |-  y e. _V
29 28 2 sbcie 
 |-  ( [. y / x ]. ph <-> ps )
30 dfsbcq 
 |-  ( y = b -> ( [. y / x ]. ph <-> [. b / x ]. ph ) )
31 29 30 bitr3id 
 |-  ( y = b -> ( ps <-> [. b / x ]. ph ) )
32 ovex 
 |-  ( y + 1 ) e. _V
33 32 3 sbcie 
 |-  ( [. ( y + 1 ) / x ]. ph <-> ch )
34 oveq1 
 |-  ( y = b -> ( y + 1 ) = ( b + 1 ) )
35 34 sbceq1d 
 |-  ( y = b -> ( [. ( y + 1 ) / x ]. ph <-> [. ( b + 1 ) / x ]. ph ) )
36 33 35 bitr3id 
 |-  ( y = b -> ( ch <-> [. ( b + 1 ) / x ]. ph ) )
37 31 36 bibi12d 
 |-  ( y = b -> ( ( ps <-> ch ) <-> ( [. b / x ]. ph <-> [. ( b + 1 ) / x ]. ph ) ) )
38 37 1 vtoclga 
 |-  ( b e. ZZ -> ( [. b / x ]. ph <-> [. ( b + 1 ) / x ]. ph ) )
39 38 3ad2ant2 
 |-  ( ( y e. ZZ /\ b e. ZZ /\ y <_ b ) -> ( [. b / x ]. ph <-> [. ( b + 1 ) / x ]. ph ) )
40 39 bibi2d 
 |-  ( ( y e. ZZ /\ b e. ZZ /\ y <_ b ) -> ( ( [. y / x ]. ph <-> [. b / x ]. ph ) <-> ( [. y / x ]. ph <-> [. ( b + 1 ) / x ]. ph ) ) )
41 40 biimpd 
 |-  ( ( y e. ZZ /\ b e. ZZ /\ y <_ b ) -> ( ( [. y / x ]. ph <-> [. b / x ]. ph ) -> ( [. y / x ]. ph <-> [. ( b + 1 ) / x ]. ph ) ) )
42 22 24 26 24 27 41 uzind 
 |-  ( ( y e. ZZ /\ b e. ZZ /\ y <_ b ) -> ( [. y / x ]. ph <-> [. b / x ]. ph ) )
43 14 20 42 vtocl2g 
 |-  ( ( 0 e. ZZ /\ A e. ZZ ) -> ( ( 0 e. ZZ /\ A e. ZZ /\ 0 <_ A ) -> ( [. 0 / x ]. ph <-> [. A / x ]. ph ) ) )
44 43 3adant3 
 |-  ( ( 0 e. ZZ /\ A e. ZZ /\ 0 <_ A ) -> ( ( 0 e. ZZ /\ A e. ZZ /\ 0 <_ A ) -> ( [. 0 / x ]. ph <-> [. A / x ]. ph ) ) )
45 44 pm2.43i 
 |-  ( ( 0 e. ZZ /\ A e. ZZ /\ 0 <_ A ) -> ( [. 0 / x ]. ph <-> [. A / x ]. ph ) )
46 8 45 mp3an1 
 |-  ( ( A e. ZZ /\ 0 <_ A ) -> ( [. 0 / x ]. ph <-> [. A / x ]. ph ) )
47 eleq1 
 |-  ( y = A -> ( y e. ZZ <-> A e. ZZ ) )
48 breq1 
 |-  ( y = A -> ( y <_ b <-> A <_ b ) )
49 47 48 3anbi13d 
 |-  ( y = A -> ( ( y e. ZZ /\ b e. ZZ /\ y <_ b ) <-> ( A e. ZZ /\ b e. ZZ /\ A <_ b ) ) )
50 dfsbcq 
 |-  ( y = A -> ( [. y / x ]. ph <-> [. A / x ]. ph ) )
51 50 bibi1d 
 |-  ( y = A -> ( ( [. y / x ]. ph <-> [. b / x ]. ph ) <-> ( [. A / x ]. ph <-> [. b / x ]. ph ) ) )
52 49 51 imbi12d 
 |-  ( y = A -> ( ( ( y e. ZZ /\ b e. ZZ /\ y <_ b ) -> ( [. y / x ]. ph <-> [. b / x ]. ph ) ) <-> ( ( A e. ZZ /\ b e. ZZ /\ A <_ b ) -> ( [. A / x ]. ph <-> [. b / x ]. ph ) ) ) )
53 eleq1 
 |-  ( b = 0 -> ( b e. ZZ <-> 0 e. ZZ ) )
54 breq2 
 |-  ( b = 0 -> ( A <_ b <-> A <_ 0 ) )
55 53 54 3anbi23d 
 |-  ( b = 0 -> ( ( A e. ZZ /\ b e. ZZ /\ A <_ b ) <-> ( A e. ZZ /\ 0 e. ZZ /\ A <_ 0 ) ) )
56 dfsbcq 
 |-  ( b = 0 -> ( [. b / x ]. ph <-> [. 0 / x ]. ph ) )
57 56 bibi2d 
 |-  ( b = 0 -> ( ( [. A / x ]. ph <-> [. b / x ]. ph ) <-> ( [. A / x ]. ph <-> [. 0 / x ]. ph ) ) )
58 55 57 imbi12d 
 |-  ( b = 0 -> ( ( ( A e. ZZ /\ b e. ZZ /\ A <_ b ) -> ( [. A / x ]. ph <-> [. b / x ]. ph ) ) <-> ( ( A e. ZZ /\ 0 e. ZZ /\ A <_ 0 ) -> ( [. A / x ]. ph <-> [. 0 / x ]. ph ) ) ) )
59 52 58 42 vtocl2g 
 |-  ( ( A e. ZZ /\ 0 e. ZZ ) -> ( ( A e. ZZ /\ 0 e. ZZ /\ A <_ 0 ) -> ( [. A / x ]. ph <-> [. 0 / x ]. ph ) ) )
60 59 3adant3 
 |-  ( ( A e. ZZ /\ 0 e. ZZ /\ A <_ 0 ) -> ( ( A e. ZZ /\ 0 e. ZZ /\ A <_ 0 ) -> ( [. A / x ]. ph <-> [. 0 / x ]. ph ) ) )
61 60 pm2.43i 
 |-  ( ( A e. ZZ /\ 0 e. ZZ /\ A <_ 0 ) -> ( [. A / x ]. ph <-> [. 0 / x ]. ph ) )
62 8 61 mp3an2 
 |-  ( ( A e. ZZ /\ A <_ 0 ) -> ( [. A / x ]. ph <-> [. 0 / x ]. ph ) )
63 62 bicomd 
 |-  ( ( A e. ZZ /\ A <_ 0 ) -> ( [. 0 / x ]. ph <-> [. A / x ]. ph ) )
64 0re 
 |-  0 e. RR
65 zre 
 |-  ( A e. ZZ -> A e. RR )
66 letric 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A \/ A <_ 0 ) )
67 64 65 66 sylancr 
 |-  ( A e. ZZ -> ( 0 <_ A \/ A <_ 0 ) )
68 46 63 67 mpjaodan 
 |-  ( A e. ZZ -> ( [. 0 / x ]. ph <-> [. A / x ]. ph ) )
69 7 68 bitr3id 
 |-  ( A e. ZZ -> ( th <-> [. A / x ]. ph ) )
70 5 sbcieg 
 |-  ( A e. ZZ -> ( [. A / x ]. ph <-> ta ) )
71 69 70 bitrd 
 |-  ( A e. ZZ -> ( th <-> ta ) )