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 sseldi 
 |-  ( ( ( 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 sseldi 
 |-  ( ( ( 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 sseldi 
 |-  ( ( ( ( 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 sseldi 
 |-  ( ( ( ( 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 sseldi 
 |-  ( ( ( ( ph /\ ( x e. NN /\ y e. NN ) ) /\ x < y ) /\ k e. NN ) -> ( G ` k ) e. ZZ )
55 6 49 sseldi 
 |-  ( ( ( ( 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 ) ) )