MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addrid Structured version   Visualization version   GIF version

Theorem addrid 11393
Description: 0 is an additive identity. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Proof shortened by Mario Carneiro, 27-May-2016.)
Assertion
Ref Expression
addrid (๐ด โˆˆ โ„‚ โ†’ (๐ด + 0) = ๐ด)

Proof of Theorem addrid
Dummy variables ๐‘ ๐‘ฅ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1re 11213 . 2 1 โˆˆ โ„
2 ax-rnegex 11178 . 2 (1 โˆˆ โ„ โ†’ โˆƒ๐‘ โˆˆ โ„ (1 + ๐‘) = 0)
3 ax-1ne0 11176 . . . . . 6 1 โ‰  0
4 oveq2 7410 . . . . . . . . . 10 (๐‘ = 0 โ†’ (1 + ๐‘) = (1 + 0))
54eqeq1d 2726 . . . . . . . . 9 (๐‘ = 0 โ†’ ((1 + ๐‘) = 0 โ†” (1 + 0) = 0))
65biimpcd 248 . . . . . . . 8 ((1 + ๐‘) = 0 โ†’ (๐‘ = 0 โ†’ (1 + 0) = 0))
7 oveq2 7410 . . . . . . . . 9 ((1 + 0) = 0 โ†’ (((i ยท i) ยท (i ยท i)) ยท (1 + 0)) = (((i ยท i) ยท (i ยท i)) ยท 0))
8 ax-icn 11166 . . . . . . . . . . . . . . 15 i โˆˆ โ„‚
98, 8mulcli 11220 . . . . . . . . . . . . . 14 (i ยท i) โˆˆ โ„‚
109, 9mulcli 11220 . . . . . . . . . . . . 13 ((i ยท i) ยท (i ยท i)) โˆˆ โ„‚
11 ax-1cn 11165 . . . . . . . . . . . . 13 1 โˆˆ โ„‚
12 0cn 11205 . . . . . . . . . . . . 13 0 โˆˆ โ„‚
1310, 11, 12adddii 11225 . . . . . . . . . . . 12 (((i ยท i) ยท (i ยท i)) ยท (1 + 0)) = ((((i ยท i) ยท (i ยท i)) ยท 1) + (((i ยท i) ยท (i ยท i)) ยท 0))
1410mulridi 11217 . . . . . . . . . . . . 13 (((i ยท i) ยท (i ยท i)) ยท 1) = ((i ยท i) ยท (i ยท i))
15 mul01 11392 . . . . . . . . . . . . . . 15 (((i ยท i) ยท (i ยท i)) โˆˆ โ„‚ โ†’ (((i ยท i) ยท (i ยท i)) ยท 0) = 0)
1610, 15ax-mp 5 . . . . . . . . . . . . . 14 (((i ยท i) ยท (i ยท i)) ยท 0) = 0
17 ax-i2m1 11175 . . . . . . . . . . . . . 14 ((i ยท i) + 1) = 0
1816, 17eqtr4i 2755 . . . . . . . . . . . . 13 (((i ยท i) ยท (i ยท i)) ยท 0) = ((i ยท i) + 1)
1914, 18oveq12i 7414 . . . . . . . . . . . 12 ((((i ยท i) ยท (i ยท i)) ยท 1) + (((i ยท i) ยท (i ยท i)) ยท 0)) = (((i ยท i) ยท (i ยท i)) + ((i ยท i) + 1))
2013, 19eqtri 2752 . . . . . . . . . . 11 (((i ยท i) ยท (i ยท i)) ยท (1 + 0)) = (((i ยท i) ยท (i ยท i)) + ((i ยท i) + 1))
2120, 16eqeq12i 2742 . . . . . . . . . 10 ((((i ยท i) ยท (i ยท i)) ยท (1 + 0)) = (((i ยท i) ยท (i ยท i)) ยท 0) โ†” (((i ยท i) ยท (i ยท i)) + ((i ยท i) + 1)) = 0)
2210, 9, 11addassi 11223 . . . . . . . . . . . 12 ((((i ยท i) ยท (i ยท i)) + (i ยท i)) + 1) = (((i ยท i) ยท (i ยท i)) + ((i ยท i) + 1))
239mulridi 11217 . . . . . . . . . . . . . . 15 ((i ยท i) ยท 1) = (i ยท i)
2423oveq2i 7413 . . . . . . . . . . . . . 14 (((i ยท i) ยท (i ยท i)) + ((i ยท i) ยท 1)) = (((i ยท i) ยท (i ยท i)) + (i ยท i))
259, 9, 11adddii 11225 . . . . . . . . . . . . . . 15 ((i ยท i) ยท ((i ยท i) + 1)) = (((i ยท i) ยท (i ยท i)) + ((i ยท i) ยท 1))
2617oveq2i 7413 . . . . . . . . . . . . . . . 16 ((i ยท i) ยท ((i ยท i) + 1)) = ((i ยท i) ยท 0)
27 mul01 11392 . . . . . . . . . . . . . . . . 17 ((i ยท i) โˆˆ โ„‚ โ†’ ((i ยท i) ยท 0) = 0)
289, 27ax-mp 5 . . . . . . . . . . . . . . . 16 ((i ยท i) ยท 0) = 0
2926, 28eqtri 2752 . . . . . . . . . . . . . . 15 ((i ยท i) ยท ((i ยท i) + 1)) = 0
3025, 29eqtr3i 2754 . . . . . . . . . . . . . 14 (((i ยท i) ยท (i ยท i)) + ((i ยท i) ยท 1)) = 0
3124, 30eqtr3i 2754 . . . . . . . . . . . . 13 (((i ยท i) ยท (i ยท i)) + (i ยท i)) = 0
3231oveq1i 7412 . . . . . . . . . . . 12 ((((i ยท i) ยท (i ยท i)) + (i ยท i)) + 1) = (0 + 1)
3322, 32eqtr3i 2754 . . . . . . . . . . 11 (((i ยท i) ยท (i ยท i)) + ((i ยท i) + 1)) = (0 + 1)
34 00id 11388 . . . . . . . . . . . 12 (0 + 0) = 0
3534eqcomi 2733 . . . . . . . . . . 11 0 = (0 + 0)
3633, 35eqeq12i 2742 . . . . . . . . . 10 ((((i ยท i) ยท (i ยท i)) + ((i ยท i) + 1)) = 0 โ†” (0 + 1) = (0 + 0))
37 0re 11215 . . . . . . . . . . 11 0 โˆˆ โ„
38 readdcan 11387 . . . . . . . . . . 11 ((1 โˆˆ โ„ โˆง 0 โˆˆ โ„ โˆง 0 โˆˆ โ„) โ†’ ((0 + 1) = (0 + 0) โ†” 1 = 0))
391, 37, 37, 38mp3an 1457 . . . . . . . . . 10 ((0 + 1) = (0 + 0) โ†” 1 = 0)
4021, 36, 393bitri 297 . . . . . . . . 9 ((((i ยท i) ยท (i ยท i)) ยท (1 + 0)) = (((i ยท i) ยท (i ยท i)) ยท 0) โ†” 1 = 0)
417, 40sylib 217 . . . . . . . 8 ((1 + 0) = 0 โ†’ 1 = 0)
426, 41syl6 35 . . . . . . 7 ((1 + ๐‘) = 0 โ†’ (๐‘ = 0 โ†’ 1 = 0))
4342necon3d 2953 . . . . . 6 ((1 + ๐‘) = 0 โ†’ (1 โ‰  0 โ†’ ๐‘ โ‰  0))
443, 43mpi 20 . . . . 5 ((1 + ๐‘) = 0 โ†’ ๐‘ โ‰  0)
45 ax-rrecex 11179 . . . . 5 ((๐‘ โˆˆ โ„ โˆง ๐‘ โ‰  0) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ (๐‘ ยท ๐‘ฅ) = 1)
4644, 45sylan2 592 . . . 4 ((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ (๐‘ ยท ๐‘ฅ) = 1)
47 simpr 484 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ๐ด โˆˆ โ„‚)
48 simplrl 774 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ๐‘ฅ โˆˆ โ„)
4948recnd 11241 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ๐‘ฅ โˆˆ โ„‚)
5047, 49mulcld 11233 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (๐ด ยท ๐‘ฅ) โˆˆ โ„‚)
51 simplll 772 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ๐‘ โˆˆ โ„)
5251recnd 11241 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ๐‘ โˆˆ โ„‚)
5312a1i 11 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ 0 โˆˆ โ„‚)
5450, 52, 53adddid 11237 . . . . . . . 8 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((๐ด ยท ๐‘ฅ) ยท (๐‘ + 0)) = (((๐ด ยท ๐‘ฅ) ยท ๐‘) + ((๐ด ยท ๐‘ฅ) ยท 0)))
5511a1i 11 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ 1 โˆˆ โ„‚)
5655, 52, 53addassd 11235 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((1 + ๐‘) + 0) = (1 + (๐‘ + 0)))
57 simpllr 773 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (1 + ๐‘) = 0)
5857oveq1d 7417 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((1 + ๐‘) + 0) = (0 + 0))
5956, 58eqtr3d 2766 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (1 + (๐‘ + 0)) = (0 + 0))
6034, 59, 573eqtr4a 2790 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (1 + (๐‘ + 0)) = (1 + ๐‘))
6137a1i 11 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ 0 โˆˆ โ„)
6251, 61readdcld 11242 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (๐‘ + 0) โˆˆ โ„)
631a1i 11 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ 1 โˆˆ โ„)
64 readdcan 11387 . . . . . . . . . . 11 (((๐‘ + 0) โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง 1 โˆˆ โ„) โ†’ ((1 + (๐‘ + 0)) = (1 + ๐‘) โ†” (๐‘ + 0) = ๐‘))
6562, 51, 63, 64syl3anc 1368 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((1 + (๐‘ + 0)) = (1 + ๐‘) โ†” (๐‘ + 0) = ๐‘))
6660, 65mpbid 231 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (๐‘ + 0) = ๐‘)
6766oveq2d 7418 . . . . . . . 8 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((๐ด ยท ๐‘ฅ) ยท (๐‘ + 0)) = ((๐ด ยท ๐‘ฅ) ยท ๐‘))
6854, 67eqtr3d 2766 . . . . . . 7 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (((๐ด ยท ๐‘ฅ) ยท ๐‘) + ((๐ด ยท ๐‘ฅ) ยท 0)) = ((๐ด ยท ๐‘ฅ) ยท ๐‘))
69 mul31 11380 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ ((๐ด ยท ๐‘ฅ) ยท ๐‘) = ((๐‘ ยท ๐‘ฅ) ยท ๐ด))
7047, 49, 52, 69syl3anc 1368 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((๐ด ยท ๐‘ฅ) ยท ๐‘) = ((๐‘ ยท ๐‘ฅ) ยท ๐ด))
71 simplrr 775 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (๐‘ ยท ๐‘ฅ) = 1)
7271oveq1d 7417 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((๐‘ ยท ๐‘ฅ) ยท ๐ด) = (1 ยท ๐ด))
7347mullidd 11231 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (1 ยท ๐ด) = ๐ด)
7470, 72, 733eqtrd 2768 . . . . . . . 8 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((๐ด ยท ๐‘ฅ) ยท ๐‘) = ๐ด)
75 mul01 11392 . . . . . . . . 9 ((๐ด ยท ๐‘ฅ) โˆˆ โ„‚ โ†’ ((๐ด ยท ๐‘ฅ) ยท 0) = 0)
7650, 75syl 17 . . . . . . . 8 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((๐ด ยท ๐‘ฅ) ยท 0) = 0)
7774, 76oveq12d 7420 . . . . . . 7 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (((๐ด ยท ๐‘ฅ) ยท ๐‘) + ((๐ด ยท ๐‘ฅ) ยท 0)) = (๐ด + 0))
7868, 77, 743eqtr3d 2772 . . . . . 6 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (๐ด + 0) = ๐ด)
7978exp42 435 . . . . 5 ((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โ†’ (๐‘ฅ โˆˆ โ„ โ†’ ((๐‘ ยท ๐‘ฅ) = 1 โ†’ (๐ด โˆˆ โ„‚ โ†’ (๐ด + 0) = ๐ด))))
8079rexlimdv 3145 . . . 4 ((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โ†’ (โˆƒ๐‘ฅ โˆˆ โ„ (๐‘ ยท ๐‘ฅ) = 1 โ†’ (๐ด โˆˆ โ„‚ โ†’ (๐ด + 0) = ๐ด)))
8146, 80mpd 15 . . 3 ((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โ†’ (๐ด โˆˆ โ„‚ โ†’ (๐ด + 0) = ๐ด))
8281rexlimiva 3139 . 2 (โˆƒ๐‘ โˆˆ โ„ (1 + ๐‘) = 0 โ†’ (๐ด โˆˆ โ„‚ โ†’ (๐ด + 0) = ๐ด))
831, 2, 82mp2b 10 1 (๐ด โˆˆ โ„‚ โ†’ (๐ด + 0) = ๐ด)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2932  โˆƒwrex 3062  (class class class)co 7402  โ„‚cc 11105  โ„cr 11106  0cc0 11107  1c1 11108  ici 11109   + caddc 11110   ยท cmul 11112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-po 5579  df-so 5580  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-ov 7405  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11249  df-mnf 11250  df-ltxr 11252
This theorem is referenced by:  cnegex  11394  addlid  11396  addcan2  11398  addridi  11400  addridd  11413  subid  11478  subid1  11479  addid0  11632  swrdccat3blem  14691  shftval3  15025  reim0  15067  isercolllem3  15615  fsumcvg  15660  summolem2a  15663  risefac1  15979  cnaddid  19786  ovolicc1  25389  addsqnreup  27317  brbtwn2  28657  axsegconlem1  28669  ax5seglem4  28684  axeuclid  28715  axcontlem2  28717  axcontlem4  28719  2xp3dxp2ge1d  41557  factwoffsmonot  41558  stoweidlem26  45288  2zrngamnd  47171  aacllem  48096
  Copyright terms: Public domain W3C validator