Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > lgsval4 | Unicode version |
Description: Restate lgsval 13784 for nonzero , where the function has been abbreviated into a self-referential expression taking the value of on the primes as given. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Ref | Expression |
---|---|
lgsval4.1 |
Ref | Expression |
---|---|
lgsval4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2171 | . . . 4 | |
2 | 1 | lgsval 13784 | . . 3 |
3 | 2 | 3adant3 1013 | . 2 |
4 | simp3 995 | . . . 4 | |
5 | 4 | neneqd 2362 | . . 3 |
6 | 5 | iffalsed 3537 | . 2 |
7 | 1 | lgsval4lem 13791 | . . . . . 6 |
8 | lgsval4.1 | . . . . . 6 | |
9 | 7, 8 | eqtr4di 2222 | . . . . 5 |
10 | 9 | seqeq3d 10413 | . . . 4 |
11 | 10 | fveq1d 5501 | . . 3 |
12 | 11 | oveq2d 5873 | . 2 |
13 | 3, 6, 12 | 3eqtrd 2208 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 974 wceq 1349 wcel 2142 wne 2341 cif 3527 cpr 3585 class class class wbr 3990 cmpt 4051 cfv 5200 (class class class)co 5857 cc0 7778 c1 7779 caddc 7781 cmul 7783 clt 7958 cmin 8094 cneg 8095 cdiv 8593 cn 8882 c2 8933 c7 8938 c8 8939 cz 9216 cmo 10282 cseq 10405 cexp 10479 cabs 10965 cdvds 11753 cprime 12065 cpc 12242 clgs 13777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 610 ax-in2 611 ax-io 705 ax-5 1441 ax-7 1442 ax-gen 1443 ax-ie1 1487 ax-ie2 1488 ax-8 1498 ax-10 1499 ax-11 1500 ax-i12 1501 ax-bndl 1503 ax-4 1504 ax-17 1520 ax-i9 1524 ax-ial 1528 ax-i5r 1529 ax-13 2144 ax-14 2145 ax-ext 2153 ax-coll 4105 ax-sep 4108 ax-nul 4116 ax-pow 4161 ax-pr 4195 ax-un 4419 ax-setind 4522 ax-iinf 4573 ax-cnex 7869 ax-resscn 7870 ax-1cn 7871 ax-1re 7872 ax-icn 7873 ax-addcl 7874 ax-addrcl 7875 ax-mulcl 7876 ax-mulrcl 7877 ax-addcom 7878 ax-mulcom 7879 ax-addass 7880 ax-mulass 7881 ax-distr 7882 ax-i2m1 7883 ax-0lt1 7884 ax-1rid 7885 ax-0id 7886 ax-rnegex 7887 ax-precex 7888 ax-cnre 7889 ax-pre-ltirr 7890 ax-pre-ltwlin 7891 ax-pre-lttrn 7892 ax-pre-apti 7893 ax-pre-ltadd 7894 ax-pre-mulgt0 7895 ax-pre-mulext 7896 ax-arch 7897 ax-caucvg 7898 |
This theorem depends on definitions: df-bi 116 df-stab 827 df-dc 831 df-3or 975 df-3an 976 df-tru 1352 df-fal 1355 df-xor 1372 df-nf 1455 df-sb 1757 df-eu 2023 df-mo 2024 df-clab 2158 df-cleq 2164 df-clel 2167 df-nfc 2302 df-ne 2342 df-nel 2437 df-ral 2454 df-rex 2455 df-reu 2456 df-rmo 2457 df-rab 2458 df-v 2733 df-sbc 2957 df-csb 3051 df-dif 3124 df-un 3126 df-in 3128 df-ss 3135 df-nul 3416 df-if 3528 df-pw 3569 df-sn 3590 df-pr 3591 df-op 3593 df-uni 3798 df-int 3833 df-iun 3876 df-br 3991 df-opab 4052 df-mpt 4053 df-tr 4089 df-id 4279 df-po 4282 df-iso 4283 df-iord 4352 df-on 4354 df-ilim 4355 df-suc 4357 df-iom 4576 df-xp 4618 df-rel 4619 df-cnv 4620 df-co 4621 df-dm 4622 df-rn 4623 df-res 4624 df-ima 4625 df-iota 5162 df-fun 5202 df-fn 5203 df-f 5204 df-f1 5205 df-fo 5206 df-f1o 5207 df-fv 5208 df-isom 5209 df-riota 5813 df-ov 5860 df-oprab 5861 df-mpo 5862 df-1st 6123 df-2nd 6124 df-recs 6288 df-irdg 6353 df-frec 6374 df-1o 6399 df-2o 6400 df-oadd 6403 df-er 6517 df-en 6723 df-dom 6724 df-fin 6725 df-sup 6965 df-inf 6966 df-pnf 7960 df-mnf 7961 df-xr 7962 df-ltxr 7963 df-le 7964 df-sub 8096 df-neg 8097 df-reap 8498 df-ap 8505 df-div 8594 df-inn 8883 df-2 8941 df-3 8942 df-4 8943 df-5 8944 df-6 8945 df-7 8946 df-8 8947 df-n0 9140 df-z 9217 df-uz 9492 df-q 9583 df-rp 9615 df-fz 9970 df-fzo 10103 df-fl 10230 df-mod 10283 df-seqfrec 10406 df-exp 10480 df-ihash 10714 df-cj 10810 df-re 10811 df-im 10812 df-rsqrt 10966 df-abs 10967 df-clim 11246 df-proddc 11518 df-dvds 11754 df-gcd 11902 df-prm 12066 df-phi 12169 df-pc 12243 df-lgs 13778 |
This theorem is referenced by: lgsval4a 13802 lgsneg 13804 lgsdir 13815 lgsdi 13817 lgsne0 13818 |
Copyright terms: Public domain | W3C validator |