MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isercolllem1 Unicode version

Theorem isercolllem1 12989
Description: Lemma for isercoll 12992. (Contributed by Mario Carneiro, 6-Apr-2015.)
Hypotheses
Ref Expression
isercoll.z
isercoll.m
isercoll.g
isercoll.i
Assertion
Ref Expression
isercolllem1
Distinct variable groups:   ,   ,   ,M
Allowed substitution hints:   S( )   ( )

Proof of Theorem isercolllem1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isercoll.z . . . . . . . . . . 11
2 uzssz 10744 . . . . . . . . . . 11
31, 2eqsstri 3423 . . . . . . . . . 10
4 zssre 10517 . . . . . . . . . 10
53, 4sstri 3402 . . . . . . . . 9
6 isercoll.g . . . . . . . . . . 11
76ad2antrr 708 . . . . . . . . . 10
8 simplrl 738 . . . . . . . . . 10
97, 8ffvelrnd 5860 . . . . . . . . 9
105, 9sseldi 3391 . . . . . . . 8
11 simplrr 739 . . . . . . . . 9
1211nnred 10203 . . . . . . . 8
1310, 12resubcld 9650 . . . . . . 7
148nnred 10203 . . . . . . . 8
1510, 14resubcld 9650 . . . . . . 7
167, 11ffvelrnd 5860 . . . . . . . . 9
175, 16sseldi 3391 . . . . . . . 8
1817, 12resubcld 9650 . . . . . . 7
19 simpr 449 . . . . . . . 8
2014, 12, 10, 19ltsub2dd 9825 . . . . . . 7
218nnzd 10610 . . . . . . . . . 10
2211nnzd 10610 . . . . . . . . . 10
2314, 12, 19ltled 9401 . . . . . . . . . 10
24 eluz2 10731 . . . . . . . . . 10
2521, 22, 23, 24syl3anbrc 1146 . . . . . . . . 9
26 elfzuz 11305 . . . . . . . . . 10
27 eluznn 10789 . . . . . . . . . . . 12
288, 27sylan 459 . . . . . . . . . . 11
29 fveq2 5708 . . . . . . . . . . . . . . 15
30 id 21 . . . . . . . . . . . . . . 15
3129, 30oveq12d 6121 . . . . . . . . . . . . . 14
32 eqid 2489 . . . . . . . . . . . . . 14
33 ovex 6128 . . . . . . . . . . . . . 14
3431, 32, 33fvmpt 5790 . . . . . . . . . . . . 13
3534adantl 454 . . . . . . . . . . . 12
367ffvelrnda 5859 . . . . . . . . . . . . . 14
375, 36sseldi 3391 . . . . . . . . . . . . 13
38 nnre 10195 . . . . . . . . . . . . . 14
3938adantl 454 . . . . . . . . . . . . 13
4037, 39resubcld 9650 . . . . . . . . . . . 12
4135, 40eqeltrd 2563 . . . . . . . . . . 11
4228, 41syldan 458 . . . . . . . . . 10
4326, 42sylan2 462 . . . . . . . . 9
44 elfzuz 11305 . . . . . . . . . 10
45 peano2nn 10200 . . . . . . . . . . . . . . . . 17
46 ffvelrn 5857 . . . . . . . . . . . . . . . . 17
477, 45, 46syl2an 465 . . . . . . . . . . . . . . . 16
485, 47sseldi 3391 . . . . . . . . . . . . . . 15
49 peano2rem 9550 . . . . . . . . . . . . . . 15
5048, 49syl 16 . . . . . . . . . . . . . 14
51 simpll 732 . . . . . . . . . . . . . . . 16
52 isercoll.i . . . . . . . . . . . . . . . 16
5351, 52sylan 459 . . . . . . . . . . . . . . 15
543, 36sseldi 3391 . . . . . . . . . . . . . . . 16
553, 47sseldi 3391 . . . . . . . . . . . . . . . 16
56 zltlem1 10561 . . . . . . . . . . . . . . . 16
5754, 55, 56syl2anc 644 . . . . . . . . . . . . . . 15
5853, 57mpbid 203 . . . . . . . . . . . . . 14
5937, 50, 39, 58lesub1dd 9828 . . . . . . . . . . . . 13
6048recnd 9291 . . . . . . . . . . . . . . 15
61 ax-1cn 9219 . . . . . . . . . . . . . . . 16
6261a1i 11 . . . . . . . . . . . . . . 15
6339recnd 9291 . . . . . . . . . . . . . . 15
6460, 62, 63sub32d 9626 . . . . . . . . . . . . . 14
6560, 63, 62subsub4d 9625 . . . . . . . . . . . . . 14
6664, 65eqtrd 2521 . . . . . . . . . . . . 13
6759, 66breqtrd 4342 . . . . . . . . . . . 12
6845adantl 454 . . . . . . . . . . . . 13
69 fveq2 5708 . . . . . . . . . . . . . . 15
70 id 21 . . . . . . . . . . . . . . 15
7169, 70oveq12d 6121 . . . . . . . . . . . . . 14
72 ovex 6128 . . . . . . . . . . . . . 14
7371, 32, 72fvmpt 5790 . . . . . . . . . . . . 13
7468, 73syl 16 . . . . . . . . . . . 12
7567, 35, 743brtr4d 4348 . . . . . . . . . . 11
7628, 75syldan 458 . . . . . . . . . 10
7744, 76sylan2 462 . . . . . . . . 9
7825, 43, 77monoord 11685 . . . . . . . 8
79 fveq2 5708 . . . . . . . . . . 11
80 id 21 . . . . . . . . . . 11
8179, 80oveq12d 6121 . . . . . . . . . 10
82 ovex 6128 . . . . . . . . . 10
8381, 32, 82fvmpt 5790 . . . . . . . . 9
848, 83syl 16 . . . . . . . 8
85 fveq2 5708 . . . . . . . . . . 11
86 id 21 . . . . . . . . . . 11
8785, 86oveq12d 6121 . . . . . . . . . 10
88 ovex 6128 . . . . . . . . . 10
8987, 32, 88fvmpt 5790 . . . . . . . . 9
9011, 89syl 16 . . . . . . . 8
9178, 84, 903brtr3d 4347 . . . . . . 7
9213, 15, 18, 20, 91ltletrd 9410 . . . . . 6
9310, 17, 12ltsub1d 9821 . . . . . 6
9492, 93mpbird 225 . . . . 5
9594ex 425 . . . 4
9695ralrimivva 2852 . . 3
97 ssralv 3453 . . . . 5
9897ralimdv 2839 . . . 4
99 ssralv 3453 . . . 4
10098, 99syld 43 . . 3
10196, 100mpan9 457 . 2
102 nnssre 10192 . . . . 5
103 ltso 9334 . . . . 5
104 soss 4680 . . . . 5
105102, 103, 104mp2 9 . . . 4
106105a1i 11 . . 3
107 soss 4680 . . . . 5
1085, 103, 107mp2 9 . . . 4
109108a1i 11 . . 3
1106adantr 453 . . 3
111 simpr 449 . . 3
112 soisores 6028 . . 3
113106, 109, 110, 111, 112syl22anc 1193 . 2
114101, 113mpbird 225 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  /\wa 360  =wceq 1670  e.wcel 1732  A.wral 2759  C_wss 3365   class class class wbr 4318  e.cmpt 4376  Orwor 4661  |`cres 4864  "cima 4865  -->wf 5434  `cfv 5438  Isomwiso 5439  (class class class)co 6103   cc 9159   cr 9160  1c1 9162   caddc 9164   clt 9297   cle 9298   cmin 9472   cn 10188   cz 10510   cuz 10725   cfz 11293
This theorem is referenced by:  isercolllem2  12990  isercolllem3  12991  isercoll  12992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382  ax-cnex 9217  ax-resscn 9218  ax-1cn 9219  ax-icn 9220  ax-addcl 9221  ax-addrcl 9222  ax-mulcl 9223  ax-mulrcl 9224  ax-mulcom 9225  ax-addass 9226  ax-mulass 9227  ax-distr 9228  ax-i2m1 9229  ax-1ne0 9230  ax-1rid 9231  ax-rnegex 9232  ax-rrecex 9233  ax-cnre 9234  ax-pre-lttri 9235  ax-pre-lttrn 9236  ax-pre-ltadd 9237  ax-pre-mulgt0 9238
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-nel 2655  df-ral 2764  df-rex 2765  df-reu 2766  df-rab 2768  df-v 3017  df-sbc 3225  df-csb 3326  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-pss 3381  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-tp 3917  df-op 3918  df-uni 4118  df-iun 4199  df-br 4319  df-opab 4377  df-mpt 4378  df-tr 4412  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-iota 5401  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445  df-fv 5446  df-isom 5447  df-riota 6062  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-om 6487  df-1st 6583  df-2nd 6584  df-recs 6795  df-rdg 6830  df-er 7067  df-en 7274  df-dom 7275  df-sdom 7276  df-pnf 9299  df-mnf 9300  df-xr 9301  df-ltxr 9302  df-le 9303  df-sub 9474  df-neg 9475  df-nn 10189  df-n0 10446  df-z 10511  df-uz 10726  df-fz 11294
  Copyright terms: Public domain W3C validator