This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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