Theorem ax0id 7872

Description: 0 is an identity element for real addition. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0id 7914.

In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.)

Assertion

Ref	Expression
ax0id	|- ( A e. CC -> ( A + 0 ) = A )

Proof of Theorem ax0id

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-c 7812	. 2 |- CC = ( R. X. R. )
2		oveq1 5877	. . 3 |- ( <. x , y >. = A -> ( <. x , y >. + 0 ) = ( A + 0 ) )
3		id 19	. . 3 |- ( <. x , y >. = A -> <. x , y >. = A )
4	2, 3	eqeq12d 2192	. 2 |- ( <. x , y >. = A -> ( ( <. x , y >. + 0 ) = <. x , y >. <-> ( A + 0 ) = A ) )
5		0r 7744	. . . 4 |- 0R e. R.
6		addcnsr 7828	. . . 4 |- ( ( ( x e. R. /\ y e. R. ) /\ ( 0R e. R. /\ 0R e. R. ) ) -> ( <. x , y >. + <. 0R , 0R >. ) = <. ( x +R 0R ) , ( y +R 0R ) >. )
7	5, 5, 6	mpanr12 439	. . 3 |- ( ( x e. R. /\ y e. R. ) -> ( <. x , y >. + <. 0R , 0R >. ) = <. ( x +R 0R ) , ( y +R 0R ) >. )
8		df-0 7813	. . . . . 6 |- 0 = <. 0R , 0R >.
9	8	eqcomi 2181	. . . . 5 |- <. 0R , 0R >. = 0
10	9	a1i 9	. . . 4 |- ( ( x e. R. /\ y e. R. ) -> <. 0R , 0R >. = 0 )
11	10	oveq2d 5886	. . 3 |- ( ( x e. R. /\ y e. R. ) -> ( <. x , y >. + <. 0R , 0R >. ) = ( <. x , y >. + 0 ) )
12		0idsr 7761	. . . . 5 |- ( x e. R. -> ( x +R 0R ) = x )
13	12	adantr 276	. . . 4 |- ( ( x e. R. /\ y e. R. ) -> ( x +R 0R ) = x )
14		0idsr 7761	. . . . 5 |- ( y e. R. -> ( y +R 0R ) = y )
15	14	adantl 277	. . . 4 |- ( ( x e. R. /\ y e. R. ) -> ( y +R 0R ) = y )
16	13, 15	opeq12d 3785	. . 3 |- ( ( x e. R. /\ y e. R. ) -> <. ( x +R 0R ) , ( y +R 0R ) >. = <. x , y >. )
17	7, 11, 16	3eqtr3d 2218	. 2 |- ( ( x e. R. /\ y e. R. ) -> ( <. x , y >. + 0 ) = <. x , y >. )
18	1, 4, 17	optocl 4700	1 |- ( A e. CC -> ( A + 0 ) = A )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1353   e. wcel 2148   <.cop 3595  (class class class)co 5870   R.cnr 7291   0Rc0r 7292   +R cplr 7295   CCcc 7804   0cc0 7806   + caddc 7809

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-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4116  ax-sep 4119  ax-nul 4127  ax-pow 4172  ax-pr 4207  ax-un 4431  ax-setind 4534  ax-iinf 4585

This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-int 3844  df-iun 3887  df-br 4002  df-opab 4063  df-mpt 4064  df-tr 4100  df-eprel 4287  df-id 4291  df-po 4294  df-iso 4295  df-iord 4364  df-on 4366  df-suc 4369  df-iom 4588  df-xp 4630  df-rel 4631  df-cnv 4632  df-co 4633  df-dm 4634  df-rn 4635  df-res 4636  df-ima 4637  df-iota 5175  df-fun 5215  df-fn 5216  df-f 5217  df-f1 5218  df-fo 5219  df-f1o 5220  df-fv 5221  df-ov 5873  df-oprab 5874  df-mpo 5875  df-1st 6136  df-2nd 6137  df-recs 6301  df-irdg 6366  df-1o 6412  df-2o 6413  df-oadd 6416  df-omul 6417  df-er 6530  df-ec 6532  df-qs 6536  df-ni 7298  df-pli 7299  df-mi 7300  df-lti 7301  df-plpq 7338  df-mpq 7339  df-enq 7341  df-nqqs 7342  df-plqqs 7343  df-mqqs 7344  df-1nqqs 7345  df-rq 7346  df-ltnqqs 7347  df-enq0 7418  df-nq0 7419  df-0nq0 7420  df-plq0 7421  df-mq0 7422  df-inp 7460  df-i1p 7461  df-iplp 7462  df-enr 7720  df-nr 7721  df-plr 7722  df-0r 7725  df-c 7812  df-0 7813  df-add 7817

This theorem is referenced by: (None)