Theorem axi2m1

Description: i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom 12 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-i2m1 . (Contributed by NM, 5-May-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	axi2m1	$$⊢\mathrm{i}\mathrm{i}+1=0$$

Proof

Step	Hyp	Ref	Expression
1		0r	$$⊢0_{𝑹}\in 𝑹$$
2		1sr	$$⊢1_{𝑹}\in 𝑹$$
3		mulcnsr	$$⊢\left(\left(0_{𝑹}\in 𝑹\wedge 1_{𝑹}\in 𝑹\right)\wedge \left(0_{𝑹}\in 𝑹\wedge 1_{𝑹}\in 𝑹\right)\right)\to ⟨0_{𝑹},1_{𝑹}⟩⟨0_{𝑹},1_{𝑹}⟩=⟨\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}\right)\right),\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right){+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}\right)⟩$$
4	1 2 1 2 3	mp4an	$$⊢⟨0_{𝑹},1_{𝑹}⟩⟨0_{𝑹},1_{𝑹}⟩=⟨\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}\right)\right),\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right){+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}\right)⟩$$
5		00sr	$$⊢0_{𝑹}\in 𝑹\to 0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}=0_{𝑹}$$
6	1 5	ax-mp	$$⊢0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}=0_{𝑹}$$
7		1idsr	$$⊢1_{𝑹}\in 𝑹\to 1_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}=1_{𝑹}$$
8	2 7	ax-mp	$$⊢1_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}=1_{𝑹}$$
9	8	oveq2i	$$⊢{-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}\right)={-1}_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}$$
10		m1r	$$⊢{-1}_{𝑹}\in 𝑹$$
11		1idsr	$$⊢{-1}_{𝑹}\in 𝑹\to {-1}_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}={-1}_{𝑹}$$
12	10 11	ax-mp	$$⊢{-1}_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}={-1}_{𝑹}$$
13	9 12	eqtri	$$⊢{-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}\right)={-1}_{𝑹}$$
14	6 13	oveq12i	$$⊢\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}\right)\right)=0_{𝑹}{+}_{𝑹}{-1}_{𝑹}$$
15		addcomsr	$$⊢0_{𝑹}{+}_{𝑹}{-1}_{𝑹}={-1}_{𝑹}{+}_{𝑹}{0}_{𝑹}$$
16		0idsr	$$⊢{-1}_{𝑹}\in 𝑹\to {-1}_{𝑹}{+}_{𝑹}{0}_{𝑹}={-1}_{𝑹}$$
17	10 16	ax-mp	$$⊢{-1}_{𝑹}{+}_{𝑹}{0}_{𝑹}={-1}_{𝑹}$$
18	14 15 17	3eqtri	$$⊢\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}\right)\right)={-1}_{𝑹}$$
19		00sr	$$⊢1_{𝑹}\in 𝑹\to 1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}=0_{𝑹}$$
20	2 19	ax-mp	$$⊢1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}=0_{𝑹}$$
21		1idsr	$$⊢0_{𝑹}\in 𝑹\to 0_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}=0_{𝑹}$$
22	1 21	ax-mp	$$⊢0_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}=0_{𝑹}$$
23	20 22	oveq12i	$$⊢\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right){+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}\right)=0_{𝑹}{+}_{𝑹}{0}_{𝑹}$$
24		0idsr	$$⊢0_{𝑹}\in 𝑹\to 0_{𝑹}{+}_{𝑹}{0}_{𝑹}=0_{𝑹}$$
25	1 24	ax-mp	$$⊢0_{𝑹}{+}_{𝑹}{0}_{𝑹}=0_{𝑹}$$
26	23 25	eqtri	$$⊢\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right){+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}\right)=0_{𝑹}$$
27	18 26	opeq12i	$$⊢⟨\left(0_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(1_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}\right)\right),\left(1_{𝑹}{\cdot }_{𝑹}{0}_{𝑹}\right){+}_{𝑹}\left(0_{𝑹}{\cdot }_{𝑹}{1}_{𝑹}\right)⟩=⟨{-1}_{𝑹},0_{𝑹}⟩$$
28	4 27	eqtri	$$⊢⟨0_{𝑹},1_{𝑹}⟩⟨0_{𝑹},1_{𝑹}⟩=⟨{-1}_{𝑹},0_{𝑹}⟩$$
29	28	oveq1i	$$⊢⟨0_{𝑹},1_{𝑹}⟩⟨0_{𝑹},1_{𝑹}⟩+⟨1_{𝑹},0_{𝑹}⟩=⟨{-1}_{𝑹},0_{𝑹}⟩+⟨1_{𝑹},0_{𝑹}⟩$$
30		addresr	$$⊢\left({-1}_{𝑹}\in 𝑹\wedge 1_{𝑹}\in 𝑹\right)\to ⟨{-1}_{𝑹},0_{𝑹}⟩+⟨1_{𝑹},0_{𝑹}⟩=⟨{-1}_{𝑹}{+}_{𝑹}{1}_{𝑹},0_{𝑹}⟩$$
31	10 2 30	mp2an	$$⊢⟨{-1}_{𝑹},0_{𝑹}⟩+⟨1_{𝑹},0_{𝑹}⟩=⟨{-1}_{𝑹}{+}_{𝑹}{1}_{𝑹},0_{𝑹}⟩$$
32		m1p1sr	$$⊢{-1}_{𝑹}{+}_{𝑹}{1}_{𝑹}=0_{𝑹}$$
33	32	opeq1i	$$⊢⟨{-1}_{𝑹}{+}_{𝑹}{1}_{𝑹},0_{𝑹}⟩=⟨0_{𝑹},0_{𝑹}⟩$$
34	29 31 33	3eqtri	$$⊢⟨0_{𝑹},1_{𝑹}⟩⟨0_{𝑹},1_{𝑹}⟩+⟨1_{𝑹},0_{𝑹}⟩=⟨0_{𝑹},0_{𝑹}⟩$$
35		df-i	$$⊢\mathrm{i}=⟨0_{𝑹},1_{𝑹}⟩$$
36	35 35	oveq12i	$$⊢\mathrm{i}\mathrm{i}=⟨0_{𝑹},1_{𝑹}⟩⟨0_{𝑹},1_{𝑹}⟩$$
37		df-1	$$⊢1=⟨1_{𝑹},0_{𝑹}⟩$$
38	36 37	oveq12i	$$⊢\mathrm{i}\mathrm{i}+1=⟨0_{𝑹},1_{𝑹}⟩⟨0_{𝑹},1_{𝑹}⟩+⟨1_{𝑹},0_{𝑹}⟩$$
39		df-0	$$⊢0=⟨0_{𝑹},0_{𝑹}⟩$$
40	34 38 39	3eqtr4i	$$⊢\mathrm{i}\mathrm{i}+1=0$$