Metamath Proof Explorer

Theorem monotuz

Description: A function defined on an upper set of integers which increases at every adjacent pair is globally strictly monotonic by induction. (Contributed by Stefan O'Rear, 24-Sep-2014)

Ref Expression
Hypotheses monotuz.1 
|- ( ( ph /\ y e. H ) -> F < G )
monotuz.2 
|- ( ( ph /\ x e. H ) -> C e. RR )
monotuz.3 
|- H = ( ZZ>= ` I )
monotuz.4 
|- ( x = ( y + 1 ) -> C = G )
monotuz.5 
|- ( x = y -> C = F )
monotuz.6 
|- ( x = A -> C = D )
monotuz.7 
|- ( x = B -> C = E )
Assertion monotuz 
|- ( ( ph /\ ( A e. H /\ B e. H ) ) -> ( A < B <-> D < E ) )

Proof

Step Hyp Ref Expression
1 monotuz.1 
 |-  ( ( ph /\ y e. H ) -> F < G )
2 monotuz.2 
 |-  ( ( ph /\ x e. H ) -> C e. RR )
3 monotuz.3 
 |-  H = ( ZZ>= ` I )
4 monotuz.4 
 |-  ( x = ( y + 1 ) -> C = G )
5 monotuz.5 
 |-  ( x = y -> C = F )
6 monotuz.6 
 |-  ( x = A -> C = D )
7 monotuz.7 
 |-  ( x = B -> C = E )
8 csbeq1 
 |-  ( a = b -> [_ a / x ]_ C = [_ b / x ]_ C )
9 csbeq1 
 |-  ( a = A -> [_ a / x ]_ C = [_ A / x ]_ C )
10 csbeq1 
 |-  ( a = B -> [_ a / x ]_ C = [_ B / x ]_ C )
11 uzssz 
 |-  ( ZZ>= ` I ) C_ ZZ
12 zssre 
 |-  ZZ C_ RR
13 11 12 sstri 
 |-  ( ZZ>= ` I ) C_ RR
14 3 13 eqsstri 
 |-  H C_ RR
15 nfv 
 |-  F/ x ( ph /\ a e. H )
16 nfcsb1v 
 |-  F/_ x [_ a / x ]_ C
17 16 nfel1 
 |-  F/ x [_ a / x ]_ C e. RR
18 15 17 nfim 
 |-  F/ x ( ( ph /\ a e. H ) -> [_ a / x ]_ C e. RR )
19 eleq1 
 |-  ( x = a -> ( x e. H <-> a e. H ) )
20 19 anbi2d 
 |-  ( x = a -> ( ( ph /\ x e. H ) <-> ( ph /\ a e. H ) ) )
21 csbeq1a 
 |-  ( x = a -> C = [_ a / x ]_ C )
22 21 eleq1d 
 |-  ( x = a -> ( C e. RR <-> [_ a / x ]_ C e. RR ) )
23 20 22 imbi12d 
 |-  ( x = a -> ( ( ( ph /\ x e. H ) -> C e. RR ) <-> ( ( ph /\ a e. H ) -> [_ a / x ]_ C e. RR ) ) )
24 18 23 2 chvarfv 
 |-  ( ( ph /\ a e. H ) -> [_ a / x ]_ C e. RR )
25 simpl 
 |-  ( ( ( ph /\ a e. H ) /\ a < b ) -> ( ph /\ a e. H ) )
26 25 adantlrr 
 |-  ( ( ( ph /\ ( a e. H /\ b e. H ) ) /\ a < b ) -> ( ph /\ a e. H ) )
27 3 11 eqsstri 
 |-  H C_ ZZ
28 simplrl 
 |-  ( ( ( ph /\ ( a e. H /\ b e. H ) ) /\ a < b ) -> a e. H )
29 27 28 sselid 
 |-  ( ( ( ph /\ ( a e. H /\ b e. H ) ) /\ a < b ) -> a e. ZZ )
30 simplrr 
 |-  ( ( ( ph /\ ( a e. H /\ b e. H ) ) /\ a < b ) -> b e. H )
31 27 30 sselid 
 |-  ( ( ( ph /\ ( a e. H /\ b e. H ) ) /\ a < b ) -> b e. ZZ )
32 simpr 
 |-  ( ( ( ph /\ ( a e. H /\ b e. H ) ) /\ a < b ) -> a < b )
33 csbeq1 
 |-  ( c = ( a + 1 ) -> [_ c / x ]_ C = [_ ( a + 1 ) / x ]_ C )
34 33 breq2d 
 |-  ( c = ( a + 1 ) -> ( [_ a / x ]_ C < [_ c / x ]_ C <-> [_ a / x ]_ C < [_ ( a + 1 ) / x ]_ C ) )
35 34 imbi2d 
 |-  ( c = ( a + 1 ) -> ( ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ c / x ]_ C ) <-> ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ ( a + 1 ) / x ]_ C ) ) )
36 csbeq1 
 |-  ( c = d -> [_ c / x ]_ C = [_ d / x ]_ C )
37 36 breq2d 
 |-  ( c = d -> ( [_ a / x ]_ C < [_ c / x ]_ C <-> [_ a / x ]_ C < [_ d / x ]_ C ) )
38 37 imbi2d 
 |-  ( c = d -> ( ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ c / x ]_ C ) <-> ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ d / x ]_ C ) ) )
39 csbeq1 
 |-  ( c = ( d + 1 ) -> [_ c / x ]_ C = [_ ( d + 1 ) / x ]_ C )
40 39 breq2d 
 |-  ( c = ( d + 1 ) -> ( [_ a / x ]_ C < [_ c / x ]_ C <-> [_ a / x ]_ C < [_ ( d + 1 ) / x ]_ C ) )
41 40 imbi2d 
 |-  ( c = ( d + 1 ) -> ( ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ c / x ]_ C ) <-> ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ ( d + 1 ) / x ]_ C ) ) )
42 csbeq1 
 |-  ( c = b -> [_ c / x ]_ C = [_ b / x ]_ C )
43 42 breq2d 
 |-  ( c = b -> ( [_ a / x ]_ C < [_ c / x ]_ C <-> [_ a / x ]_ C < [_ b / x ]_ C ) )
44 43 imbi2d 
 |-  ( c = b -> ( ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ c / x ]_ C ) <-> ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ b / x ]_ C ) ) )
45 eleq1 
 |-  ( y = a -> ( y e. H <-> a e. H ) )
46 45 anbi2d 
 |-  ( y = a -> ( ( ph /\ y e. H ) <-> ( ph /\ a e. H ) ) )
47 vex 
 |-  y e. _V
48 47 5 csbie 
 |-  [_ y / x ]_ C = F
49 csbeq1 
 |-  ( y = a -> [_ y / x ]_ C = [_ a / x ]_ C )
50 48 49 eqtr3id 
 |-  ( y = a -> F = [_ a / x ]_ C )
51 ovex 
 |-  ( y + 1 ) e. _V
52 51 4 csbie 
 |-  [_ ( y + 1 ) / x ]_ C = G
53 oveq1 
 |-  ( y = a -> ( y + 1 ) = ( a + 1 ) )
54 53 csbeq1d 
 |-  ( y = a -> [_ ( y + 1 ) / x ]_ C = [_ ( a + 1 ) / x ]_ C )
55 52 54 eqtr3id 
 |-  ( y = a -> G = [_ ( a + 1 ) / x ]_ C )
56 50 55 breq12d 
 |-  ( y = a -> ( F < G <-> [_ a / x ]_ C < [_ ( a + 1 ) / x ]_ C ) )
57 46 56 imbi12d 
 |-  ( y = a -> ( ( ( ph /\ y e. H ) -> F < G ) <-> ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ ( a + 1 ) / x ]_ C ) ) )
58 57 1 vtoclg 
 |-  ( a e. ZZ -> ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ ( a + 1 ) / x ]_ C ) )
59 24 3ad2ant2 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> [_ a / x ]_ C e. RR )
60 simp2l 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> ph )
61 zre 
 |-  ( a e. ZZ -> a e. RR )
62 61 3ad2ant1 
 |-  ( ( a e. ZZ /\ d e. ZZ /\ a < d ) -> a e. RR )
63 zre 
 |-  ( d e. ZZ -> d e. RR )
64 63 3ad2ant2 
 |-  ( ( a e. ZZ /\ d e. ZZ /\ a < d ) -> d e. RR )
65 simp3 
 |-  ( ( a e. ZZ /\ d e. ZZ /\ a < d ) -> a < d )
66 62 64 65 ltled 
 |-  ( ( a e. ZZ /\ d e. ZZ /\ a < d ) -> a <_ d )
67 66 3ad2ant1 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> a <_ d )
68 simp11 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> a e. ZZ )
69 simp12 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> d e. ZZ )
70 eluz 
 |-  ( ( a e. ZZ /\ d e. ZZ ) -> ( d e. ( ZZ>= ` a ) <-> a <_ d ) )
71 68 69 70 syl2anc 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> ( d e. ( ZZ>= ` a ) <-> a <_ d ) )
72 67 71 mpbird 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> d e. ( ZZ>= ` a ) )
73 simp2r 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> a e. H )
74 73 3 eleqtrdi 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> a e. ( ZZ>= ` I ) )
75 uztrn 
 |-  ( ( d e. ( ZZ>= ` a ) /\ a e. ( ZZ>= ` I ) ) -> d e. ( ZZ>= ` I ) )
76 72 74 75 syl2anc 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> d e. ( ZZ>= ` I ) )
77 76 3 eleqtrrdi 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> d e. H )
78 nfv 
 |-  F/ x ( ph /\ d e. H )
79 nfcsb1v 
 |-  F/_ x [_ d / x ]_ C
80 79 nfel1 
 |-  F/ x [_ d / x ]_ C e. RR
81 78 80 nfim 
 |-  F/ x ( ( ph /\ d e. H ) -> [_ d / x ]_ C e. RR )
82 eleq1 
 |-  ( x = d -> ( x e. H <-> d e. H ) )
83 82 anbi2d 
 |-  ( x = d -> ( ( ph /\ x e. H ) <-> ( ph /\ d e. H ) ) )
84 csbeq1a 
 |-  ( x = d -> C = [_ d / x ]_ C )
85 84 eleq1d 
 |-  ( x = d -> ( C e. RR <-> [_ d / x ]_ C e. RR ) )
86 83 85 imbi12d 
 |-  ( x = d -> ( ( ( ph /\ x e. H ) -> C e. RR ) <-> ( ( ph /\ d e. H ) -> [_ d / x ]_ C e. RR ) ) )
87 81 86 2 chvarfv 
 |-  ( ( ph /\ d e. H ) -> [_ d / x ]_ C e. RR )
88 60 77 87 syl2anc 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> [_ d / x ]_ C e. RR )
89 peano2uz 
 |-  ( d e. ( ZZ>= ` I ) -> ( d + 1 ) e. ( ZZ>= ` I ) )
90 76 89 syl 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> ( d + 1 ) e. ( ZZ>= ` I ) )
91 90 3 eleqtrrdi 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> ( d + 1 ) e. H )
92 nfv 
 |-  F/ x ( ph /\ ( d + 1 ) e. H )
93 nfcsb1v 
 |-  F/_ x [_ ( d + 1 ) / x ]_ C
94 93 nfel1 
 |-  F/ x [_ ( d + 1 ) / x ]_ C e. RR
95 92 94 nfim 
 |-  F/ x ( ( ph /\ ( d + 1 ) e. H ) -> [_ ( d + 1 ) / x ]_ C e. RR )
96 ovex 
 |-  ( d + 1 ) e. _V
97 eleq1 
 |-  ( x = ( d + 1 ) -> ( x e. H <-> ( d + 1 ) e. H ) )
98 97 anbi2d 
 |-  ( x = ( d + 1 ) -> ( ( ph /\ x e. H ) <-> ( ph /\ ( d + 1 ) e. H ) ) )
99 csbeq1a 
 |-  ( x = ( d + 1 ) -> C = [_ ( d + 1 ) / x ]_ C )
100 99 eleq1d 
 |-  ( x = ( d + 1 ) -> ( C e. RR <-> [_ ( d + 1 ) / x ]_ C e. RR ) )
101 98 100 imbi12d 
 |-  ( x = ( d + 1 ) -> ( ( ( ph /\ x e. H ) -> C e. RR ) <-> ( ( ph /\ ( d + 1 ) e. H ) -> [_ ( d + 1 ) / x ]_ C e. RR ) ) )
102 95 96 101 2 vtoclf 
 |-  ( ( ph /\ ( d + 1 ) e. H ) -> [_ ( d + 1 ) / x ]_ C e. RR )
103 60 91 102 syl2anc 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> [_ ( d + 1 ) / x ]_ C e. RR )
104 simp3 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> [_ a / x ]_ C < [_ d / x ]_ C )
105 nfv 
 |-  F/ y ( ( ph /\ d e. H ) -> [_ d / x ]_ C < [_ ( d + 1 ) / x ]_ C )
106 eleq1 
 |-  ( y = d -> ( y e. H <-> d e. H ) )
107 106 anbi2d 
 |-  ( y = d -> ( ( ph /\ y e. H ) <-> ( ph /\ d e. H ) ) )
108 csbeq1 
 |-  ( y = d -> [_ y / x ]_ C = [_ d / x ]_ C )
109 48 108 eqtr3id 
 |-  ( y = d -> F = [_ d / x ]_ C )
110 oveq1 
 |-  ( y = d -> ( y + 1 ) = ( d + 1 ) )
111 110 csbeq1d 
 |-  ( y = d -> [_ ( y + 1 ) / x ]_ C = [_ ( d + 1 ) / x ]_ C )
112 52 111 eqtr3id 
 |-  ( y = d -> G = [_ ( d + 1 ) / x ]_ C )
113 109 112 breq12d 
 |-  ( y = d -> ( F < G <-> [_ d / x ]_ C < [_ ( d + 1 ) / x ]_ C ) )
114 107 113 imbi12d 
 |-  ( y = d -> ( ( ( ph /\ y e. H ) -> F < G ) <-> ( ( ph /\ d e. H ) -> [_ d / x ]_ C < [_ ( d + 1 ) / x ]_ C ) ) )
115 105 114 1 chvarfv 
 |-  ( ( ph /\ d e. H ) -> [_ d / x ]_ C < [_ ( d + 1 ) / x ]_ C )
116 60 77 115 syl2anc 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> [_ d / x ]_ C < [_ ( d + 1 ) / x ]_ C )
117 59 88 103 104 116 lttrd 
 |-  ( ( ( a e. ZZ /\ d e. ZZ /\ a < d ) /\ ( ph /\ a e. H ) /\ [_ a / x ]_ C < [_ d / x ]_ C ) -> [_ a / x ]_ C < [_ ( d + 1 ) / x ]_ C )
118 117 3exp 
 |-  ( ( a e. ZZ /\ d e. ZZ /\ a < d ) -> ( ( ph /\ a e. H ) -> ( [_ a / x ]_ C < [_ d / x ]_ C -> [_ a / x ]_ C < [_ ( d + 1 ) / x ]_ C ) ) )
119 118 a2d 
 |-  ( ( a e. ZZ /\ d e. ZZ /\ a < d ) -> ( ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ d / x ]_ C ) -> ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ ( d + 1 ) / x ]_ C ) ) )
120 35 38 41 44 58 119 uzind2 
 |-  ( ( a e. ZZ /\ b e. ZZ /\ a < b ) -> ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ b / x ]_ C ) )
121 29 31 32 120 syl3anc 
 |-  ( ( ( ph /\ ( a e. H /\ b e. H ) ) /\ a < b ) -> ( ( ph /\ a e. H ) -> [_ a / x ]_ C < [_ b / x ]_ C ) )
122 26 121 mpd 
 |-  ( ( ( ph /\ ( a e. H /\ b e. H ) ) /\ a < b ) -> [_ a / x ]_ C < [_ b / x ]_ C )
123 122 ex 
 |-  ( ( ph /\ ( a e. H /\ b e. H ) ) -> ( a < b -> [_ a / x ]_ C < [_ b / x ]_ C ) )
124 8 9 10 14 24 123 ltord1 
 |-  ( ( ph /\ ( A e. H /\ B e. H ) ) -> ( A < B <-> [_ A / x ]_ C < [_ B / x ]_ C ) )
125 nfcvd 
 |-  ( A e. H -> F/_ x D )
126 125 6 csbiegf 
 |-  ( A e. H -> [_ A / x ]_ C = D )
127 nfcvd 
 |-  ( B e. H -> F/_ x E )
128 127 7 csbiegf 
 |-  ( B e. H -> [_ B / x ]_ C = E )
129 126 128 breqan12d 
 |-  ( ( A e. H /\ B e. H ) -> ( [_ A / x ]_ C < [_ B / x ]_ C <-> D < E ) )
130 129 adantl 
 |-  ( ( ph /\ ( A e. H /\ B e. H ) ) -> ( [_ A / x ]_ C < [_ B / x ]_ C <-> D < E ) )
131 124 130 bitrd 
 |-  ( ( ph /\ ( A e. H /\ B e. H ) ) -> ( A < B <-> D < E ) )