Colors of
variables: wff set class |
Syntax hints:
→ wi 4 ∈ wcel 2160
(class class class)co 5891 1c1 7831
+ caddc 7833 ℕ0cn0 9195 |
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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 ax-sep 4136 ax-cnex 7921 ax-resscn 7922 ax-1cn 7923 ax-1re 7924 ax-icn 7925 ax-addcl 7926 ax-addrcl 7927 ax-mulcl 7928 ax-addcom 7930 ax-addass 7932 ax-i2m1 7935 ax-0id 7938 |
This theorem depends on definitions:
df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-rex 2474 df-rab 2477 df-v 2754 df-un 3148 df-in 3150 df-ss 3157 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-br 4019 df-iota 5193 df-fv 5239 df-ov 5894 df-inn 8939 df-n0 9196 |
This theorem is referenced by: peano2z
9308 nn0split
10155 fzonn0p1p1
10232 elfzom1p1elfzo
10233 frecfzennn
10445 leexp2r
10593 facdiv
10737 facwordi
10739 faclbnd
10740 faclbnd2
10741 faclbnd3
10742 faclbnd6
10743 bcnp1n
10758 bcp1m1
10764 bcpasc
10765 hashfz
10820 bcxmas
11516 geolim
11538 geo2sum
11541 mertenslemub
11561 mertenslemi1
11562 mertenslem2
11563 mertensabs
11564 efcllemp
11685 eftlub
11717 efsep
11718 effsumlt
11719 nn0ob
11932 nn0oddm1d2
11933 nn0seqcvgd
12060 algcvg
12067 pw2dvdseulemle
12186 2sqpwodd
12195 nonsq
12226 pcprendvds
12309 pcpremul
12312 pcdvdsb
12338 4sqlem11
12415 ennnfonelemp1
12431 ennnfonelemkh
12437 ennnfonelemim
12449 |