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

Theorem addrid 11425
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 11245 . 2 1 โˆˆ โ„
2 ax-rnegex 11210 . 2 (1 โˆˆ โ„ โ†’ โˆƒ๐‘ โˆˆ โ„ (1 + ๐‘) = 0)
3 ax-1ne0 11208 . . . . . 6 1 โ‰  0
4 oveq2 7428 . . . . . . . . . 10 (๐‘ = 0 โ†’ (1 + ๐‘) = (1 + 0))
54eqeq1d 2730 . . . . . . . . 9 (๐‘ = 0 โ†’ ((1 + ๐‘) = 0 โ†” (1 + 0) = 0))
65biimpcd 248 . . . . . . . 8 ((1 + ๐‘) = 0 โ†’ (๐‘ = 0 โ†’ (1 + 0) = 0))
7 oveq2 7428 . . . . . . . . 9 ((1 + 0) = 0 โ†’ (((i ยท i) ยท (i ยท i)) ยท (1 + 0)) = (((i ยท i) ยท (i ยท i)) ยท 0))
8 ax-icn 11198 . . . . . . . . . . . . . . 15 i โˆˆ โ„‚
98, 8mulcli 11252 . . . . . . . . . . . . . 14 (i ยท i) โˆˆ โ„‚
109, 9mulcli 11252 . . . . . . . . . . . . 13 ((i ยท i) ยท (i ยท i)) โˆˆ โ„‚
11 ax-1cn 11197 . . . . . . . . . . . . 13 1 โˆˆ โ„‚
12 0cn 11237 . . . . . . . . . . . . 13 0 โˆˆ โ„‚
1310, 11, 12adddii 11257 . . . . . . . . . . . 12 (((i ยท i) ยท (i ยท i)) ยท (1 + 0)) = ((((i ยท i) ยท (i ยท i)) ยท 1) + (((i ยท i) ยท (i ยท i)) ยท 0))
1410mulridi 11249 . . . . . . . . . . . . 13 (((i ยท i) ยท (i ยท i)) ยท 1) = ((i ยท i) ยท (i ยท i))
15 mul01 11424 . . . . . . . . . . . . . . 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 11207 . . . . . . . . . . . . . 14 ((i ยท i) + 1) = 0
1816, 17eqtr4i 2759 . . . . . . . . . . . . 13 (((i ยท i) ยท (i ยท i)) ยท 0) = ((i ยท i) + 1)
1914, 18oveq12i 7432 . . . . . . . . . . . 12 ((((i ยท i) ยท (i ยท i)) ยท 1) + (((i ยท i) ยท (i ยท i)) ยท 0)) = (((i ยท i) ยท (i ยท i)) + ((i ยท i) + 1))
2013, 19eqtri 2756 . . . . . . . . . . 11 (((i ยท i) ยท (i ยท i)) ยท (1 + 0)) = (((i ยท i) ยท (i ยท i)) + ((i ยท i) + 1))
2120, 16eqeq12i 2746 . . . . . . . . . 10 ((((i ยท i) ยท (i ยท i)) ยท (1 + 0)) = (((i ยท i) ยท (i ยท i)) ยท 0) โ†” (((i ยท i) ยท (i ยท i)) + ((i ยท i) + 1)) = 0)
2210, 9, 11addassi 11255 . . . . . . . . . . . 12 ((((i ยท i) ยท (i ยท i)) + (i ยท i)) + 1) = (((i ยท i) ยท (i ยท i)) + ((i ยท i) + 1))
239mulridi 11249 . . . . . . . . . . . . . . 15 ((i ยท i) ยท 1) = (i ยท i)
2423oveq2i 7431 . . . . . . . . . . . . . 14 (((i ยท i) ยท (i ยท i)) + ((i ยท i) ยท 1)) = (((i ยท i) ยท (i ยท i)) + (i ยท i))
259, 9, 11adddii 11257 . . . . . . . . . . . . . . 15 ((i ยท i) ยท ((i ยท i) + 1)) = (((i ยท i) ยท (i ยท i)) + ((i ยท i) ยท 1))
2617oveq2i 7431 . . . . . . . . . . . . . . . 16 ((i ยท i) ยท ((i ยท i) + 1)) = ((i ยท i) ยท 0)
27 mul01 11424 . . . . . . . . . . . . . . . . 17 ((i ยท i) โˆˆ โ„‚ โ†’ ((i ยท i) ยท 0) = 0)
289, 27ax-mp 5 . . . . . . . . . . . . . . . 16 ((i ยท i) ยท 0) = 0
2926, 28eqtri 2756 . . . . . . . . . . . . . . 15 ((i ยท i) ยท ((i ยท i) + 1)) = 0
3025, 29eqtr3i 2758 . . . . . . . . . . . . . 14 (((i ยท i) ยท (i ยท i)) + ((i ยท i) ยท 1)) = 0
3124, 30eqtr3i 2758 . . . . . . . . . . . . 13 (((i ยท i) ยท (i ยท i)) + (i ยท i)) = 0
3231oveq1i 7430 . . . . . . . . . . . 12 ((((i ยท i) ยท (i ยท i)) + (i ยท i)) + 1) = (0 + 1)
3322, 32eqtr3i 2758 . . . . . . . . . . 11 (((i ยท i) ยท (i ยท i)) + ((i ยท i) + 1)) = (0 + 1)
34 00id 11420 . . . . . . . . . . . 12 (0 + 0) = 0
3534eqcomi 2737 . . . . . . . . . . 11 0 = (0 + 0)
3633, 35eqeq12i 2746 . . . . . . . . . 10 ((((i ยท i) ยท (i ยท i)) + ((i ยท i) + 1)) = 0 โ†” (0 + 1) = (0 + 0))
37 0re 11247 . . . . . . . . . . 11 0 โˆˆ โ„
38 readdcan 11419 . . . . . . . . . . 11 ((1 โˆˆ โ„ โˆง 0 โˆˆ โ„ โˆง 0 โˆˆ โ„) โ†’ ((0 + 1) = (0 + 0) โ†” 1 = 0))
391, 37, 37, 38mp3an 1458 . . . . . . . . . 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 2958 . . . . . 6 ((1 + ๐‘) = 0 โ†’ (1 โ‰  0 โ†’ ๐‘ โ‰  0))
443, 43mpi 20 . . . . 5 ((1 + ๐‘) = 0 โ†’ ๐‘ โ‰  0)
45 ax-rrecex 11211 . . . . 5 ((๐‘ โˆˆ โ„ โˆง ๐‘ โ‰  0) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ (๐‘ ยท ๐‘ฅ) = 1)
4644, 45sylan2 592 . . . 4 ((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โ†’ โˆƒ๐‘ฅ โˆˆ โ„ (๐‘ ยท ๐‘ฅ) = 1)
47 simpr 484 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ๐ด โˆˆ โ„‚)
48 simplrl 776 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ๐‘ฅ โˆˆ โ„)
4948recnd 11273 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ๐‘ฅ โˆˆ โ„‚)
5047, 49mulcld 11265 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (๐ด ยท ๐‘ฅ) โˆˆ โ„‚)
51 simplll 774 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ๐‘ โˆˆ โ„)
5251recnd 11273 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ๐‘ โˆˆ โ„‚)
5312a1i 11 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ 0 โˆˆ โ„‚)
5450, 52, 53adddid 11269 . . . . . . . 8 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((๐ด ยท ๐‘ฅ) ยท (๐‘ + 0)) = (((๐ด ยท ๐‘ฅ) ยท ๐‘) + ((๐ด ยท ๐‘ฅ) ยท 0)))
5511a1i 11 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ 1 โˆˆ โ„‚)
5655, 52, 53addassd 11267 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((1 + ๐‘) + 0) = (1 + (๐‘ + 0)))
57 simpllr 775 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (1 + ๐‘) = 0)
5857oveq1d 7435 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((1 + ๐‘) + 0) = (0 + 0))
5956, 58eqtr3d 2770 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (1 + (๐‘ + 0)) = (0 + 0))
6034, 59, 573eqtr4a 2794 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (1 + (๐‘ + 0)) = (1 + ๐‘))
6137a1i 11 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ 0 โˆˆ โ„)
6251, 61readdcld 11274 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (๐‘ + 0) โˆˆ โ„)
631a1i 11 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ 1 โˆˆ โ„)
64 readdcan 11419 . . . . . . . . . . 11 (((๐‘ + 0) โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ โˆง 1 โˆˆ โ„) โ†’ ((1 + (๐‘ + 0)) = (1 + ๐‘) โ†” (๐‘ + 0) = ๐‘))
6562, 51, 63, 64syl3anc 1369 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((1 + (๐‘ + 0)) = (1 + ๐‘) โ†” (๐‘ + 0) = ๐‘))
6660, 65mpbid 231 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (๐‘ + 0) = ๐‘)
6766oveq2d 7436 . . . . . . . 8 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((๐ด ยท ๐‘ฅ) ยท (๐‘ + 0)) = ((๐ด ยท ๐‘ฅ) ยท ๐‘))
6854, 67eqtr3d 2770 . . . . . . 7 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (((๐ด ยท ๐‘ฅ) ยท ๐‘) + ((๐ด ยท ๐‘ฅ) ยท 0)) = ((๐ด ยท ๐‘ฅ) ยท ๐‘))
69 mul31 11412 . . . . . . . . . 10 ((๐ด โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ ((๐ด ยท ๐‘ฅ) ยท ๐‘) = ((๐‘ ยท ๐‘ฅ) ยท ๐ด))
7047, 49, 52, 69syl3anc 1369 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((๐ด ยท ๐‘ฅ) ยท ๐‘) = ((๐‘ ยท ๐‘ฅ) ยท ๐ด))
71 simplrr 777 . . . . . . . . . 10 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (๐‘ ยท ๐‘ฅ) = 1)
7271oveq1d 7435 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((๐‘ ยท ๐‘ฅ) ยท ๐ด) = (1 ยท ๐ด))
7347mullidd 11263 . . . . . . . . 9 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (1 ยท ๐ด) = ๐ด)
7470, 72, 733eqtrd 2772 . . . . . . . 8 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((๐ด ยท ๐‘ฅ) ยท ๐‘) = ๐ด)
75 mul01 11424 . . . . . . . . 9 ((๐ด ยท ๐‘ฅ) โˆˆ โ„‚ โ†’ ((๐ด ยท ๐‘ฅ) ยท 0) = 0)
7650, 75syl 17 . . . . . . . 8 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ ((๐ด ยท ๐‘ฅ) ยท 0) = 0)
7774, 76oveq12d 7438 . . . . . . 7 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (((๐ด ยท ๐‘ฅ) ยท ๐‘) + ((๐ด ยท ๐‘ฅ) ยท 0)) = (๐ด + 0))
7868, 77, 743eqtr3d 2776 . . . . . 6 ((((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โˆง (๐‘ฅ โˆˆ โ„ โˆง (๐‘ ยท ๐‘ฅ) = 1)) โˆง ๐ด โˆˆ โ„‚) โ†’ (๐ด + 0) = ๐ด)
7978exp42 435 . . . . 5 ((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โ†’ (๐‘ฅ โˆˆ โ„ โ†’ ((๐‘ ยท ๐‘ฅ) = 1 โ†’ (๐ด โˆˆ โ„‚ โ†’ (๐ด + 0) = ๐ด))))
8079rexlimdv 3150 . . . 4 ((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โ†’ (โˆƒ๐‘ฅ โˆˆ โ„ (๐‘ ยท ๐‘ฅ) = 1 โ†’ (๐ด โˆˆ โ„‚ โ†’ (๐ด + 0) = ๐ด)))
8146, 80mpd 15 . . 3 ((๐‘ โˆˆ โ„ โˆง (1 + ๐‘) = 0) โ†’ (๐ด โˆˆ โ„‚ โ†’ (๐ด + 0) = ๐ด))
8281rexlimiva 3144 . 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 1534   โˆˆ wcel 2099   โ‰  wne 2937  โˆƒwrex 3067  (class class class)co 7420  โ„‚cc 11137  โ„cr 11138  0cc0 11139  1c1 11140  ici 11141   + caddc 11142   ยท cmul 11144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-resscn 11196  ax-1cn 11197  ax-icn 11198  ax-addcl 11199  ax-addrcl 11200  ax-mulcl 11201  ax-mulrcl 11202  ax-mulcom 11203  ax-addass 11204  ax-mulass 11205  ax-distr 11206  ax-i2m1 11207  ax-1ne0 11208  ax-1rid 11209  ax-rnegex 11210  ax-rrecex 11211  ax-cnre 11212  ax-pre-lttri 11213  ax-pre-lttrn 11214  ax-pre-ltadd 11215
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11281  df-mnf 11282  df-ltxr 11284
This theorem is referenced by:  cnegex  11426  addlid  11428  addcan2  11430  addridi  11432  addridd  11445  subid  11510  subid1  11511  addid0  11664  swrdccat3blem  14722  shftval3  15056  reim0  15098  isercolllem3  15646  fsumcvg  15691  summolem2a  15694  risefac1  16010  cnaddid  19825  ovolicc1  25458  addsqnreup  27389  brbtwn2  28729  axsegconlem1  28741  ax5seglem4  28756  axeuclid  28787  axcontlem2  28789  axcontlem4  28791  2xp3dxp2ge1d  41693  factwoffsmonot  41694  stoweidlem26  45414  2zrngamnd  47309  aacllem  48234
  Copyright terms: Public domain W3C validator