Metamath Proof Explorer


Theorem isercolllem1

Description: Lemma for isercoll . (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses isercoll.z
|- Z = ( ZZ>= ` M )
isercoll.m
|- ( ph -> M e. ZZ )
isercoll.g
|- ( ph -> G : NN --> Z )
isercoll.i
|- ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )
Assertion isercolllem1
|- ( ( ph /\ S C_ NN ) -> ( G |` S ) Isom < , < ( S , ( G " S ) ) )

Proof

Step Hyp Ref Expression
1 isercoll.z
 |-  Z = ( ZZ>= ` M )
2 isercoll.m
 |-  ( ph -> M e. ZZ )
3 isercoll.g
 |-  ( ph -> G : NN --> Z )
4 isercoll.i
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )
5 uzssz
 |-  ( ZZ>= ` M ) C_ ZZ
6 1 5 eqsstri
 |-  Z C_ ZZ
7 zssre
 |-  ZZ C_ RR
8 6 7 sstri
 |-  Z C_ RR
9 3 ad2antrr
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> G : NN --> Z )
10 simplrl
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> x e. NN )
11 9 10 ffvelrnd
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( G ` x ) e. Z )
12 8 11 sselid
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( G ` x ) e. RR )
13 simplrr
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> y e. NN )
14 13 nnred
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> y e. RR )
15 12 14 resubcld
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( ( G ` x ) - y ) e. RR )
16 10 nnred
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> x e. RR )
17 12 16 resubcld
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( ( G ` x ) - x ) e. RR )
18 9 13 ffvelrnd
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( G ` y ) e. Z )
19 8 18 sselid
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( G ` y ) e. RR )
20 19 14 resubcld
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( ( G ` y ) - y ) e. RR )
21 simpr
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> x < y )
22 16 14 12 21 ltsub2dd
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( ( G ` x ) - y ) < ( ( G ` x ) - x ) )
23 10 nnzd
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> x e. ZZ )
24 13 nnzd
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> y e. ZZ )
25 16 14 21 ltled
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> x <_ y )
26 eluz2
 |-  ( y e. ( ZZ>= ` x ) <-> ( x e. ZZ /\ y e. ZZ /\ x <_ y ) )
27 23 24 25 26 syl3anbrc
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> y e. ( ZZ>= ` x ) )
28 elfzuz
 |-  ( k e. ( x ... y ) -> k e. ( ZZ>= ` x ) )
29 eluznn
 |-  ( ( x e. NN /\ k e. ( ZZ>= ` x ) ) -> k e. NN )
30 10 29 sylan
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. ( ZZ>= ` x ) ) -> k e. NN )
31 fveq2
 |-  ( n = k -> ( G ` n ) = ( G ` k ) )
32 id
 |-  ( n = k -> n = k )
33 31 32 oveq12d
 |-  ( n = k -> ( ( G ` n ) - n ) = ( ( G ` k ) - k ) )
34 eqid
 |-  ( n e. NN |-> ( ( G ` n ) - n ) ) = ( n e. NN |-> ( ( G ` n ) - n ) )
35 ovex
 |-  ( ( G ` k ) - k ) e. _V
36 33 34 35 fvmpt
 |-  ( k e. NN -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` k ) = ( ( G ` k ) - k ) )
37 36 adantl
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` k ) = ( ( G ` k ) - k ) )
38 9 ffvelrnda
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( G ` k ) e. Z )
39 8 38 sselid
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( G ` k ) e. RR )
40 nnre
 |-  ( k e. NN -> k e. RR )
41 40 adantl
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> k e. RR )
42 39 41 resubcld
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( ( G ` k ) - k ) e. RR )
43 37 42 eqeltrd
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` k ) e. RR )
44 30 43 syldan
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. ( ZZ>= ` x ) ) -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` k ) e. RR )
45 28 44 sylan2
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. ( x ... y ) ) -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` k ) e. RR )
46 elfzuz
 |-  ( k e. ( x ... ( y - 1 ) ) -> k e. ( ZZ>= ` x ) )
47 peano2nn
 |-  ( k e. NN -> ( k + 1 ) e. NN )
48 ffvelrn
 |-  ( ( G : NN --> Z /\ ( k + 1 ) e. NN ) -> ( G ` ( k + 1 ) ) e. Z )
49 9 47 48 syl2an
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( G ` ( k + 1 ) ) e. Z )
50 8 49 sselid
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( G ` ( k + 1 ) ) e. RR )
51 peano2rem
 |-  ( ( G ` ( k + 1 ) ) e. RR -> ( ( G ` ( k + 1 ) ) - 1 ) e. RR )
52 50 51 syl
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( ( G ` ( k + 1 ) ) - 1 ) e. RR )
53 4 ad4ant14
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )
54 6 38 sselid
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( G ` k ) e. ZZ )
55 6 49 sselid
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( G ` ( k + 1 ) ) e. ZZ )
56 zltlem1
 |-  ( ( ( G ` k ) e. ZZ /\ ( G ` ( k + 1 ) ) e. ZZ ) -> ( ( G ` k ) < ( G ` ( k + 1 ) ) <-> ( G ` k ) <_ ( ( G ` ( k + 1 ) ) - 1 ) ) )
57 54 55 56 syl2anc
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( ( G ` k ) < ( G ` ( k + 1 ) ) <-> ( G ` k ) <_ ( ( G ` ( k + 1 ) ) - 1 ) ) )
58 53 57 mpbid
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( G ` k ) <_ ( ( G ` ( k + 1 ) ) - 1 ) )
59 39 52 41 58 lesub1dd
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( ( G ` k ) - k ) <_ ( ( ( G ` ( k + 1 ) ) - 1 ) - k ) )
60 50 recnd
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( G ` ( k + 1 ) ) e. CC )
61 1cnd
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> 1 e. CC )
62 41 recnd
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> k e. CC )
63 60 61 62 sub32d
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( ( ( G ` ( k + 1 ) ) - 1 ) - k ) = ( ( ( G ` ( k + 1 ) ) - k ) - 1 ) )
64 60 62 61 subsub4d
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( ( ( G ` ( k + 1 ) ) - k ) - 1 ) = ( ( G ` ( k + 1 ) ) - ( k + 1 ) ) )
65 63 64 eqtrd
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( ( ( G ` ( k + 1 ) ) - 1 ) - k ) = ( ( G ` ( k + 1 ) ) - ( k + 1 ) ) )
66 59 65 breqtrd
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( ( G ` k ) - k ) <_ ( ( G ` ( k + 1 ) ) - ( k + 1 ) ) )
67 47 adantl
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( k + 1 ) e. NN )
68 fveq2
 |-  ( n = ( k + 1 ) -> ( G ` n ) = ( G ` ( k + 1 ) ) )
69 id
 |-  ( n = ( k + 1 ) -> n = ( k + 1 ) )
70 68 69 oveq12d
 |-  ( n = ( k + 1 ) -> ( ( G ` n ) - n ) = ( ( G ` ( k + 1 ) ) - ( k + 1 ) ) )
71 ovex
 |-  ( ( G ` ( k + 1 ) ) - ( k + 1 ) ) e. _V
72 70 34 71 fvmpt
 |-  ( ( k + 1 ) e. NN -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` ( k + 1 ) ) = ( ( G ` ( k + 1 ) ) - ( k + 1 ) ) )
73 67 72 syl
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` ( k + 1 ) ) = ( ( G ` ( k + 1 ) ) - ( k + 1 ) ) )
74 66 37 73 3brtr4d
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` k ) <_ ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` ( k + 1 ) ) )
75 30 74 syldan
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. ( ZZ>= ` x ) ) -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` k ) <_ ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` ( k + 1 ) ) )
76 46 75 sylan2
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. ( x ... ( y - 1 ) ) ) -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` k ) <_ ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` ( k + 1 ) ) )
77 27 45 76 monoord
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` x ) <_ ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` y ) )
78 fveq2
 |-  ( n = x -> ( G ` n ) = ( G ` x ) )
79 id
 |-  ( n = x -> n = x )
80 78 79 oveq12d
 |-  ( n = x -> ( ( G ` n ) - n ) = ( ( G ` x ) - x ) )
81 ovex
 |-  ( ( G ` x ) - x ) e. _V
82 80 34 81 fvmpt
 |-  ( x e. NN -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` x ) = ( ( G ` x ) - x ) )
83 10 82 syl
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` x ) = ( ( G ` x ) - x ) )
84 fveq2
 |-  ( n = y -> ( G ` n ) = ( G ` y ) )
85 id
 |-  ( n = y -> n = y )
86 84 85 oveq12d
 |-  ( n = y -> ( ( G ` n ) - n ) = ( ( G ` y ) - y ) )
87 ovex
 |-  ( ( G ` y ) - y ) e. _V
88 86 34 87 fvmpt
 |-  ( y e. NN -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` y ) = ( ( G ` y ) - y ) )
89 13 88 syl
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( ( n e. NN |-> ( ( G ` n ) - n ) ) ` y ) = ( ( G ` y ) - y ) )
90 77 83 89 3brtr3d
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( ( G ` x ) - x ) <_ ( ( G ` y ) - y ) )
91 15 17 20 22 90 ltletrd
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( ( G ` x ) - y ) < ( ( G ` y ) - y ) )
92 12 19 14 ltsub1d
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( ( G ` x ) < ( G ` y ) <-> ( ( G ` x ) - y ) < ( ( G ` y ) - y ) ) )
93 91 92 mpbird
 |-  ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) -> ( G ` x ) < ( G ` y ) )
94 93 ex
 |-  ( ( ph /\ ( x e. NN /\ y e. NN ) ) -> ( x < y -> ( G ` x ) < ( G ` y ) ) )
95 94 ralrimivva
 |-  ( ph -> A. x e. NN A. y e. NN ( x < y -> ( G ` x ) < ( G ` y ) ) )
96 ss2ralv
 |-  ( S C_ NN -> ( A. x e. NN A. y e. NN ( x < y -> ( G ` x ) < ( G ` y ) ) -> A. x e. S A. y e. S ( x < y -> ( G ` x ) < ( G ` y ) ) ) )
97 95 96 mpan9
 |-  ( ( ph /\ S C_ NN ) -> A. x e. S A. y e. S ( x < y -> ( G ` x ) < ( G ` y ) ) )
98 nnssre
 |-  NN C_ RR
99 ltso
 |-  < Or RR
100 soss
 |-  ( NN C_ RR -> ( < Or RR -> < Or NN ) )
101 98 99 100 mp2
 |-  < Or NN
102 101 a1i
 |-  ( ( ph /\ S C_ NN ) -> < Or NN )
103 soss
 |-  ( Z C_ RR -> ( < Or RR -> < Or Z ) )
104 8 99 103 mp2
 |-  < Or Z
105 104 a1i
 |-  ( ( ph /\ S C_ NN ) -> < Or Z )
106 3 adantr
 |-  ( ( ph /\ S C_ NN ) -> G : NN --> Z )
107 simpr
 |-  ( ( ph /\ S C_ NN ) -> S C_ NN )
108 soisores
 |-  ( ( ( < Or NN /\ < Or Z ) /\ ( G : NN --> Z /\ S C_ NN ) ) -> ( ( G |` S ) Isom < , < ( S , ( G " S ) ) <-> A. x e. S A. y e. S ( x < y -> ( G ` x ) < ( G ` y ) ) ) )
109 102 105 106 107 108 syl22anc
 |-  ( ( ph /\ S C_ NN ) -> ( ( G |` S ) Isom < , < ( S , ( G " S ) ) <-> A. x e. S A. y e. S ( x < y -> ( G ` x ) < ( G ` y ) ) ) )
110 97 109 mpbird
 |-  ( ( ph /\ S C_ NN ) -> ( G |` S ) Isom < , < ( S , ( G " S ) ) )