Colors of
variables: wff set class |
Syntax hints:
→ wi 4 ∈ wcel 2158
(class class class)co 5888 1c1 7825
+ caddc 7827 ℕ0cn0 9189 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710
ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 ax-sep 4133 ax-cnex 7915 ax-resscn 7916 ax-1cn 7917 ax-1re 7918 ax-icn 7919 ax-addcl 7920 ax-addrcl 7921 ax-mulcl 7922 ax-addcom 7924 ax-addass 7926 ax-i2m1 7929 ax-0id 7932 |
This theorem depends on definitions:
df-bi 117 df-3an 981 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ral 2470 df-rex 2471 df-rab 2474 df-v 2751 df-un 3145 df-in 3147 df-ss 3154 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-int 3857 df-br 4016 df-iota 5190 df-fv 5236 df-ov 5891 df-inn 8933 df-n0 9190 |
This theorem is referenced by: peano2z
9302 nn0split
10149 fzonn0p1p1
10226 elfzom1p1elfzo
10227 frecfzennn
10439 leexp2r
10587 facdiv
10731 facwordi
10733 faclbnd
10734 faclbnd2
10735 faclbnd3
10736 faclbnd6
10737 bcnp1n
10752 bcp1m1
10758 bcpasc
10759 hashfz
10814 bcxmas
11510 geolim
11532 geo2sum
11535 mertenslemub
11555 mertenslemi1
11556 mertenslem2
11557 mertensabs
11558 efcllemp
11679 eftlub
11711 efsep
11712 effsumlt
11713 nn0ob
11926 nn0oddm1d2
11927 nn0seqcvgd
12054 algcvg
12061 pw2dvdseulemle
12180 2sqpwodd
12189 nonsq
12220 pcprendvds
12303 pcpremul
12306 pcdvdsb
12332 ennnfonelemp1
12420 ennnfonelemkh
12426 ennnfonelemim
12438 |