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

Theorem isercolllem1 12928
Description: Lemma for isercoll 12931. (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 10687 . . . . . . . . . . 11
31, 2eqsstri 3411 . . . . . . . . . 10
4 zssre 10460 . . . . . . . . . 10
53, 4sstri 3390 . . . . . . . . 9
6 isercoll.g . . . . . . . . . . 11
76ad2antrr 708 . . . . . . . . . 10
8 simplrl 738 . . . . . . . . . 10
97, 8ffvelrnd 5833 . . . . . . . . 9
105, 9sseldi 3379 . . . . . . . 8
11 simplrr 739 . . . . . . . . 9
1211nnred 10146 . . . . . . . 8
1310, 12resubcld 9593 . . . . . . 7
148nnred 10146 . . . . . . . 8
1510, 14resubcld 9593 . . . . . . 7
167, 11ffvelrnd 5833 . . . . . . . . 9
175, 16sseldi 3379 . . . . . . . 8
1817, 12resubcld 9593 . . . . . . 7
19 simpr 449 . . . . . . . 8
2014, 12, 10, 19ltsub2dd 9768 . . . . . . 7
218nnzd 10553 . . . . . . . . . 10
2211nnzd 10553 . . . . . . . . . 10
2314, 12, 19ltled 9344 . . . . . . . . . 10
24 eluz2 10674 . . . . . . . . . 10
2521, 22, 23, 24syl3anbrc 1146 . . . . . . . . 9
26 elfzuz 11248 . . . . . . . . . 10
27 eluznn 10732 . . . . . . . . . . . 12
288, 27sylan 459 . . . . . . . . . . 11
29 fveq2 5685 . . . . . . . . . . . . . . 15
30 id 21 . . . . . . . . . . . . . . 15
3129, 30oveq12d 6085 . . . . . . . . . . . . . 14
32 eqid 2481 . . . . . . . . . . . . . 14
33 ovex 6092 . . . . . . . . . . . . . 14
3431, 32, 33fvmpt 5767 . . . . . . . . . . . . 13
3534adantl 454 . . . . . . . . . . . 12
367ffvelrnda 5832 . . . . . . . . . . . . . 14
375, 36sseldi 3379 . . . . . . . . . . . . 13
38 nnre 10138 . . . . . . . . . . . . . 14
3938adantl 454 . . . . . . . . . . . . 13
4037, 39resubcld 9593 . . . . . . . . . . . 12
4135, 40eqeltrd 2555 . . . . . . . . . . 11
4228, 41syldan 458 . . . . . . . . . 10
4326, 42sylan2 462 . . . . . . . . 9
44 elfzuz 11248 . . . . . . . . . 10
45 peano2nn 10143 . . . . . . . . . . . . . . . . 17
46 ffvelrn 5830 . . . . . . . . . . . . . . . . 17
477, 45, 46syl2an 465 . . . . . . . . . . . . . . . 16
485, 47sseldi 3379 . . . . . . . . . . . . . . 15
49 peano2rem 9493 . . . . . . . . . . . . . . 15
5048, 49syl 16 . . . . . . . . . . . . . 14
51 simpll 732 . . . . . . . . . . . . . . . 16
52 isercoll.i . . . . . . . . . . . . . . . 16
5351, 52sylan 459 . . . . . . . . . . . . . . 15
543, 36sseldi 3379 . . . . . . . . . . . . . . . 16
553, 47sseldi 3379 . . . . . . . . . . . . . . . 16
56 zltlem1 10504 . . . . . . . . . . . . . . . 16
5754, 55, 56syl2anc 644 . . . . . . . . . . . . . . 15
5853, 57mpbid 203 . . . . . . . . . . . . . 14
5937, 50, 39, 58lesub1dd 9771 . . . . . . . . . . . . 13
6048recnd 9234 . . . . . . . . . . . . . . 15
61 ax-1cn 9162 . . . . . . . . . . . . . . . 16
6261a1i 11 . . . . . . . . . . . . . . 15
6339recnd 9234 . . . . . . . . . . . . . . 15
6460, 62, 63sub32d 9569 . . . . . . . . . . . . . 14
6560, 63, 62subsub4d 9568 . . . . . . . . . . . . . 14
6664, 65eqtrd 2513 . . . . . . . . . . . . 13
6759, 66breqtrd 4326 . . . . . . . . . . . 12
6845adantl 454 . . . . . . . . . . . . 13
69 fveq2 5685 . . . . . . . . . . . . . . 15
70 id 21 . . . . . . . . . . . . . . 15
7169, 70oveq12d 6085 . . . . . . . . . . . . . 14
72 ovex 6092 . . . . . . . . . . . . . 14
7371, 32, 72fvmpt 5767 . . . . . . . . . . . . 13
7468, 73syl 16 . . . . . . . . . . . 12
7567, 35, 743brtr4d 4332 . . . . . . . . . . 11
7628, 75syldan 458 . . . . . . . . . 10
7744, 76sylan2 462 . . . . . . . . 9
7825, 43, 77monoord 11628 . . . . . . . 8
79 fveq2 5685 . . . . . . . . . . 11
80 id 21 . . . . . . . . . . 11
8179, 80oveq12d 6085 . . . . . . . . . 10
82 ovex 6092 . . . . . . . . . 10
8381, 32, 82fvmpt 5767 . . . . . . . . 9
848, 83syl 16 . . . . . . . 8
85 fveq2 5685 . . . . . . . . . . 11
86 id 21 . . . . . . . . . . 11
8785, 86oveq12d 6085 . . . . . . . . . 10
88 ovex 6092 . . . . . . . . . 10
8987, 32, 88fvmpt 5767 . . . . . . . . 9
9011, 89syl 16 . . . . . . . 8
9178, 84, 903brtr3d 4331 . . . . . . 7
9213, 15, 18, 20, 91ltletrd 9353 . . . . . 6
9310, 17, 12ltsub1d 9764 . . . . . 6
9492, 93mpbird 225 . . . . 5
9594ex 425 . . . 4
9695ralrimivva 2844 . . 3
97 ssralv 3440 . . . . 5
9897ralimdv 2831 . . . 4
99 ssralv 3440 . . . 4
10098, 99syld 43 . . 3
10196, 100mpan9 457 . 2
102 nnssre 10135 . . . . 5
103 ltso 9277 . . . . 5
104 soss 4662 . . . . 5
105102, 103, 104mp2 9 . . . 4
106105a1i 11 . . 3
107 soss 4662 . . . . 5
1085, 103, 107mp2 9 . . . 4
109108a1i 11 . . 3
1106adantr 453 . . 3
111 simpr 449 . . 3
112 soisores 5992 . . 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 1662  e.wcel 1724  A.wral 2751  C_wss 3353   class class class wbr 4302  e.cmpt 4360  Orwor 4643  |`cres 4846  "cima 4847  -->wf 5413  `cfv 5417  Isomwiso 5418  (class class class)co 6067   cc 9102   cr 9103  1c1 9105   caddc 9107   clt 9240   cle 9241   cmin 9415   cn 10131   cz 10453   cuz 10668   cfz 11236
This theorem is referenced by:  isercolllem2  12929  isercolllem3  12930  isercoll  12931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-8 1726  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pow 4477  ax-pr 4538  ax-un 6338  ax-cnex 9160  ax-resscn 9161  ax-1cn 9162  ax-icn 9163  ax-addcl 9164  ax-addrcl 9165  ax-mulcl 9166  ax-mulrcl 9167  ax-mulcom 9168  ax-addass 9169  ax-mulass 9170  ax-distr 9171  ax-i2m1 9172  ax-1ne0 9173  ax-1rid 9174  ax-rnegex 9175  ax-rrecex 9176  ax-cnre 9177  ax-pre-lttri 9178  ax-pre-lttrn 9179  ax-pre-ltadd 9180  ax-pre-mulgt0 9181
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-nel 2647  df-ral 2756  df-rex 2757  df-reu 2758  df-rab 2760  df-v 3008  df-sbc 3213  df-csb 3314  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-pss 3369  df-nul 3661  df-if 3813  df-pw 3880  df-sn 3900  df-pr 3901  df-tp 3902  df-op 3903  df-uni 4102  df-iun 4183  df-br 4303  df-opab 4361  df-mpt 4362  df-tr 4396  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4850  df-rel 4851  df-cnv 4852  df-co 4853  df-dm 4854  df-rn 4855  df-res 4856  df-ima 4857  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-isom 5426  df-riota 6026  df-ov 6070  df-oprab 6071  df-mpt2 6072  df-om 6442  df-1st 6538  df-2nd 6539  df-recs 6745  df-rdg 6780  df-er 7017  df-en 7222  df-dom 7223  df-sdom 7224  df-pnf 9242  df-mnf 9243  df-xr 9244  df-ltxr 9245  df-le 9246  df-sub 9417  df-neg 9418  df-nn 10132  df-n0 10389  df-z 10454  df-uz 10669  df-fz 11237
  Copyright terms: Public domain W3C validator