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 x. _i ) + 1 ) = 0

Proof

Step Hyp Ref Expression
1 0r 
 |-  0R e. R.
2 1sr 
 |-  1R e. R.
3 mulcnsr 
 |-  ( ( ( 0R e. R. /\ 1R e. R. ) /\ ( 0R e. R. /\ 1R e. R. ) ) -> ( <. 0R , 1R >. x. <. 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 >. x. <. 0R , 1R >. ) = <. ( ( 0R .R 0R ) +R ( -1R .R ( 1R .R 1R ) ) ) , ( ( 1R .R 0R ) +R ( 0R .R 1R ) ) >.
5 00sr 
 |-  ( 0R e. R. -> ( 0R .R 0R ) = 0R )
6 1 5 ax-mp 
 |-  ( 0R .R 0R ) = 0R
7 1idsr 
 |-  ( 1R e. 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 e. R.
11 1idsr 
 |-  ( -1R e. 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 e. 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 e. R. -> ( 1R .R 0R ) = 0R )
20 2 19 ax-mp 
 |-  ( 1R .R 0R ) = 0R
21 1idsr 
 |-  ( 0R e. 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 e. 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 >. x. <. 0R , 1R >. ) = <. -1R , 0R >.
29 28 oveq1i 
 |-  ( ( <. 0R , 1R >. x. <. 0R , 1R >. ) + <. 1R , 0R >. ) = ( <. -1R , 0R >. + <. 1R , 0R >. )
30 addresr 
 |-  ( ( -1R e. R. /\ 1R e. 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 >. x. <. 0R , 1R >. ) + <. 1R , 0R >. ) = <. 0R , 0R >.
35 df-i 
 |-  _i = <. 0R , 1R >.
36 35 35 oveq12i 
 |-  ( _i x. _i ) = ( <. 0R , 1R >. x. <. 0R , 1R >. )
37 df-1 
 |-  1 = <. 1R , 0R >.
38 36 37 oveq12i 
 |-  ( ( _i x. _i ) + 1 ) = ( ( <. 0R , 1R >. x. <. 0R , 1R >. ) + <. 1R , 0R >. )
39 df-0 
 |-  0 = <. 0R , 0R >.
40 34 38 39 3eqtr4i 
 |-  ( ( _i x. _i ) + 1 ) = 0