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

Theorem lgsdilem2 21054
 Description: Lemma for lgsdi 21055. (Contributed by Mario Carneiro, 4-Feb-2015.)
Hypotheses
Ref Expression
lgsdilem2.1
lgsdilem2.2
lgsdilem2.3
lgsdilem2.4
lgsdilem2.5
lgsdilem2.6
Assertion
Ref Expression
lgsdilem2
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem lgsdilem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mulid1 9035 . . 3
3 lgsdilem2.2 . . . 4
4 lgsdilem2.4 . . . 4
5 nnabscl 12070 . . . 4
63, 4, 5syl2anc 643 . . 3
7 nnuz 10467 . . 3
86, 7syl6eleq 2491 . 2
96nnzd 10320 . . 3
10 lgsdilem2.3 . . . . . 6
113, 10zmulcld 10327 . . . . 5
123zcnd 10322 . . . . . 6
1310zcnd 10322 . . . . . 6
14 lgsdilem2.5 . . . . . 6
1512, 13, 4, 14mulne0d 9620 . . . . 5
16 nnabscl 12070 . . . . 5
1711, 15, 16syl2anc 643 . . . 4
1817nnzd 10320 . . 3
1912abscld 12179 . . . . 5
2013abscld 12179 . . . . 5
2112absge0d 12187 . . . . 5
22 nnabscl 12070 . . . . . . 7
2310, 14, 22syl2anc 643 . . . . . 6
2423nnge1d 9988 . . . . 5
2519, 20, 21, 24lemulge11d 9894 . . . 4
2612, 13absmuld 12197 . . . 4
2725, 26breqtrrd 4193 . . 3
28 eluz2 10440 . . 3
299, 18, 27, 28syl3anbrc 1138 . 2
30 lgsdilem2.1 . . . . . 6
31 lgsdilem2.6 . . . . . . 7
3231lgsfcl3 21040 . . . . . 6
3330, 3, 4, 32syl3anc 1184 . . . . 5
34 elfznn 11026 . . . . 5
35 ffvelrn 5821 . . . . 5
3633, 34, 35syl2an 464 . . . 4
3736zcnd 10322 . . 3
38 mulcl 9021 . . . 4
408, 37, 39seqcl 11284 . 2
416peano2nnd 9963 . . . . 5
42 elfzuz 11001 . . . . 5
437uztrn2 10449 . . . . 5
4441, 42, 43syl2an 464 . . . 4
45 eleq1 2461 . . . . . 6
46 oveq2 6042 . . . . . . 7
47 oveq1 6041 . . . . . . 7
4846, 47oveq12d 6052 . . . . . 6
49 eqidd 2402 . . . . . 6
5045, 48, 49ifbieq12d 3718 . . . . 5
51 ovex 6059 . . . . . 6
52 1ex 9033 . . . . . 6
5351, 52ifex 3754 . . . . 5
5450, 31, 53fvmpt 5759 . . . 4
5544, 54syl 16 . . 3
56 simpr 448 . . . . . . . . 9
573ad2antrr 707 . . . . . . . . . 10
58 zq 10526 . . . . . . . . . 10
5957, 58syl 16 . . . . . . . . 9
60 pcabs 13189 . . . . . . . . 9
6156, 59, 60syl2anc 643 . . . . . . . 8
62 elfzle1 11006 . . . . . . . . . . . . . 14
6362adantl 453 . . . . . . . . . . . . 13
64 elfzelz 11005 . . . . . . . . . . . . . 14
65 zltp1le 10271 . . . . . . . . . . . . . 14
669, 64, 65syl2an 464 . . . . . . . . . . . . 13
6763, 66mpbird 224 . . . . . . . . . . . 12
6819adantr 452 . . . . . . . . . . . . 13
6964adantl 453 . . . . . . . . . . . . . 14
7069zred 10321 . . . . . . . . . . . . 13
7168, 70ltnled 9166 . . . . . . . . . . . 12
7267, 71mpbid 202 . . . . . . . . . . 11
7372adantr 452 . . . . . . . . . 10
74 prmz 13024 . . . . . . . . . . . 12
7574adantl 453 . . . . . . . . . . 11
764ad2antrr 707 . . . . . . . . . . . 12
7757, 76, 5syl2anc 643 . . . . . . . . . . 11
78 dvdsle 12836 . . . . . . . . . . 11
7975, 77, 78syl2anc 643 . . . . . . . . . 10
8073, 79mtod 170 . . . . . . . . 9
81 pceq0 13185 . . . . . . . . . 10
8256, 77, 81syl2anc 643 . . . . . . . . 9
8380, 82mpbird 224 . . . . . . . 8
8461, 83eqtr3d 2435 . . . . . . 7
8584oveq2d 6050 . . . . . 6
8630ad2antrr 707 . . . . . . . . 9
87 lgscl 21033 . . . . . . . . 9
8886, 75, 87syl2anc 643 . . . . . . . 8
8988zcnd 10322 . . . . . . 7
9089exp0d 11458 . . . . . 6
9185, 90eqtrd 2433 . . . . 5
9291ifeq1da 3721 . . . 4
93 ifid 3728 . . . 4
9492, 93syl6eq 2449 . . 3
9555, 94eqtrd 2433 . 2
962, 8, 29, 40, 95seqid2 11310 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   wceq 1649   wcel 1721   wne 2564  cif 3696   class class class wbr 4167   cmpt 4221  wf 5404  cfv 5408  (class class class)co 6034  cc 8935  cr 8936  cc0 8937  c1 8938   caddc 8940   cmul 8942   clt 9067   cle 9068  cn 9946  cz 10228  cuz 10434  cq 10520  cfz 10989   cseq 11264  cexp 11323  cabs 11980   cdivides 12793  cprime 13020   cpc 13151   clgs 21017 This theorem is referenced by:  lgsdi  21055 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-cnex 8993  ax-resscn 8994  ax-1cn 8995  ax-icn 8996  ax-addcl 8997  ax-addrcl 8998  ax-mulcl 8999  ax-mulrcl 9000  ax-mulcom 9001  ax-addass 9002  ax-mulass 9003  ax-distr 9004  ax-i2m1 9005  ax-1ne0 9006  ax-1rid 9007  ax-rnegex 9008  ax-rrecex 9009  ax-cnre 9010  ax-pre-lttri 9011  ax-pre-lttrn 9012  ax-pre-ltadd 9013  ax-pre-mulgt0 9014  ax-pre-sup 9015 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-int 4007  df-iun 4051  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-1st 6302  df-2nd 6303  df-riota 6499  df-recs 6583  df-rdg 6618  df-1o 6674  df-2o 6675  df-oadd 6678  df-er 6855  df-map 6970  df-en 7060  df-dom 7061  df-sdom 7062  df-fin 7063  df-sup 7395  df-card 7773  df-cda 7995  df-pnf 9069  df-mnf 9070  df-xr 9071  df-ltxr 9072  df-le 9073  df-sub 9239  df-neg 9240  df-div 9624  df-nn 9947  df-2 10004  df-3 10005  df-n0 10168  df-z 10229  df-uz 10435  df-q 10521  df-rp 10559  df-fz 10990  df-fzo 11080  df-fl 11143  df-mod 11192  df-seq 11265  df-exp 11324  df-hash 11560  df-cj 11845  df-re 11846  df-im 11847  df-sqr 11981  df-abs 11982  df-dvds 12794  df-gcd 12948  df-prm 13021  df-phi 13096  df-pc 13152  df-lgs 21018
 Copyright terms: Public domain W3C validator