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	⊢ ( ( i · i ) + 1 ) = 0

Proof

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