Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
‘cfv 6544 ℂcc 11108 ℤ≥cuz 12822 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 ax-cnex 11166 ax-resscn 11167 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-fv 6552 df-ov 7412 df-neg 11447 df-z 12559
df-uz 12823 |
This theorem is referenced by: uzp1
12863 peano2uzr
12887 uzaddcl
12888 eluzgtdifelfzo
13694 fzosplitpr
13741 fldiv4lem1div2uz2
13801 mulp1mod1
13877 seqm1
13985 bcval5
14278 swrdfv2
14611 relexpaddg
15000 shftuz
15016 seqshft
15032 climshftlem
15518 climshft
15520 isumshft
15785 dvdsexp
16271 pclem
16771 efgtlen
19594 dvradcnv
25933 logbgcd1irr
26299 clwwlkext2edg
29309 clwwlknonex2lem1
29360 clwwlknonex2lem2
29361 clwwlknonex2
29362 2clwwlk2clwwlk
29603 numclwwlk1lem2foalem
29604 numclwwlk1lem2fo
29611 numclwwlk2
29634 nn0prpwlem
35207 aks4d1p1p1
40928 rmspecsqrtnq
41644 rmxm1
41673 rmym1
41674 rmxluc
41675 rmyluc
41676 rmyluc2
41677 jm2.17a
41699 relexpaddss
42469 trclfvdecomr
42479 binomcxplemnn0
43108 stoweidlem14
44730 fmtnorec3
46216 lighneallem4a
46276 lighneallem4b
46277 evengpop3
46466 evengpoap3
46467 nnsum4primeseven
46468 nnsum4primesevenALTV
46469 expnegico01
47199 dignn0ldlem
47288 dignnld
47289 digexp
47293 dig1
47294 nn0sumshdiglemB
47306 |