Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pmodl42N Structured version   Unicode version

Theorem pmodl42N 30710
 Description: Lemma derived from modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
pmodl42.s
pmodl42.p
Assertion
Ref Expression
pmodl42N

Proof of Theorem pmodl42N
StepHypRef Expression
1 incom 3535 . . . 4
2 simpl1 961 . . . . 5
3 simpl3 963 . . . . . 6
4 eqid 2438 . . . . . . 7
5 pmodl42.s . . . . . . 7
64, 5psubssat 30613 . . . . . 6
72, 3, 6syl2anc 644 . . . . 5
8 simpl2 962 . . . . . . 7
94, 5psubssat 30613 . . . . . . 7
102, 8, 9syl2anc 644 . . . . . 6
11 simprl 734 . . . . . . 7
124, 5psubssat 30613 . . . . . . 7
132, 11, 12syl2anc 644 . . . . . 6
14 pmodl42.p . . . . . . 7
154, 14paddssat 30673 . . . . . 6
162, 10, 13, 15syl3anc 1185 . . . . 5
17 simprr 735 . . . . . 6
185, 14paddclN 30701 . . . . . 6
192, 3, 17, 18syl3anc 1185 . . . . 5
204, 5psubssat 30613 . . . . . . 7
212, 17, 20syl2anc 644 . . . . . 6
224, 14sspadd1 30674 . . . . . 6
232, 7, 21, 22syl3anc 1185 . . . . 5
244, 5, 14pmod1i 30707 . . . . . 6
25243impia 1151 . . . . 5
262, 7, 16, 19, 23, 25syl131anc 1198 . . . 4
271, 26syl5reqr 2485 . . 3
2827oveq2d 6099 . 2
29 ssinss1 3571 . . . 4
3016, 29syl 16 . . 3
314, 14paddass 30697 . . 3
322, 10, 7, 30, 31syl13anc 1187 . 2
334, 14paddass 30697 . . . . . . 7
342, 10, 7, 13, 33syl13anc 1187 . . . . . 6
354, 14padd12N 30698 . . . . . . 7
362, 10, 7, 13, 35syl13anc 1187 . . . . . 6
3734, 36eqtrd 2470 . . . . 5
384, 14paddass 30697 . . . . . 6
392, 10, 7, 21, 38syl13anc 1187 . . . . 5
4037, 39ineq12d 3545 . . . 4
41 incom 3535 . . . 4
4240, 41syl6eq 2486 . . 3
434, 5psubssat 30613 . . . . 5
442, 19, 43syl2anc 644 . . . 4
455, 14paddclN 30701 . . . . . 6
462, 8, 11, 45syl3anc 1185 . . . . 5
475, 14paddclN 30701 . . . . 5
482, 3, 46, 47syl3anc 1185 . . . 4
494, 14sspadd1 30674 . . . . . 6
502, 10, 13, 49syl3anc 1185 . . . . 5
514, 14sspadd2 30675 . . . . . 6
522, 16, 7, 51syl3anc 1185 . . . . 5
5350, 52sstrd 3360 . . . 4
544, 5, 14pmod1i 30707 . . . . 5
55543impia 1151 . . . 4
562, 10, 44, 48, 53, 55syl131anc 1198 . . 3
5742, 56eqtrd 2470 . 2
5828, 32, 573eqtr4rd 2481 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 360   w3a 937   wceq 1653   wcel 1726   cin 3321   wss 3322  cfv 5456  (class class class)co 6083  catm 30123  chlt 30210  cpsubsp 30355  cpadd 30654 This theorem is referenced by:  pl42lem4N  30841 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4322  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-iun 4097  df-br 4215  df-opab 4269  df-mpt 4270  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-1st 6351  df-2nd 6352  df-undef 6545  df-riota 6551  df-poset 14405  df-plt 14417  df-lub 14433  df-glb 14434  df-join 14435  df-meet 14436  df-p0 14470  df-lat 14477  df-clat 14539  df-oposet 30036  df-ol 30038  df-oml 30039  df-covers 30126  df-ats 30127  df-atl 30158  df-cvlat 30182  df-hlat 30211  df-psubsp 30362  df-padd 30655
 Copyright terms: Public domain W3C validator