Metamath Proof Explorer

Theorem sn-1ne2

Description: A proof of 1ne2 without using ax-mulcom , ax-mulass , ax-pre-mulgt0 . Based on mul02lem2 . (Contributed by SN, 13-Dec-2023)

Ref Expression
Assertion sn-1ne2 
|- 1 =/= 2

Proof

Step Hyp Ref Expression
1 0ne1 
 |-  0 =/= 1
2 ax-icn 
 |-  _i e. CC
3 2 2 mulcli 
 |-  ( _i x. _i ) e. CC
4 ax-1cn 
 |-  1 e. CC
5 3 4 4 addassi 
 |-  ( ( ( _i x. _i ) + 1 ) + 1 ) = ( ( _i x. _i ) + ( 1 + 1 ) )
6 5 a1i 
 |-  ( ( 0 = ( 0 + 0 ) /\ 1 = ( 1 + 1 ) ) -> ( ( ( _i x. _i ) + 1 ) + 1 ) = ( ( _i x. _i ) + ( 1 + 1 ) ) )
7 simpr 
 |-  ( ( 0 = ( 0 + 0 ) /\ 1 = ( 1 + 1 ) ) -> 1 = ( 1 + 1 ) )
8 7 oveq2d 
 |-  ( ( 0 = ( 0 + 0 ) /\ 1 = ( 1 + 1 ) ) -> ( ( _i x. _i ) + 1 ) = ( ( _i x. _i ) + ( 1 + 1 ) ) )
9 ax-i2m1 
 |-  ( ( _i x. _i ) + 1 ) = 0
10 9 a1i 
 |-  ( ( 0 = ( 0 + 0 ) /\ 1 = ( 1 + 1 ) ) -> ( ( _i x. _i ) + 1 ) = 0 )
11 6 8 10 3eqtr2rd 
 |-  ( ( 0 = ( 0 + 0 ) /\ 1 = ( 1 + 1 ) ) -> 0 = ( ( ( _i x. _i ) + 1 ) + 1 ) )
12 simpl 
 |-  ( ( 0 = ( 0 + 0 ) /\ 1 = ( 1 + 1 ) ) -> 0 = ( 0 + 0 ) )
13 10 oveq1d 
 |-  ( ( 0 = ( 0 + 0 ) /\ 1 = ( 1 + 1 ) ) -> ( ( ( _i x. _i ) + 1 ) + 1 ) = ( 0 + 1 ) )
14 11 12 13 3eqtr3d 
 |-  ( ( 0 = ( 0 + 0 ) /\ 1 = ( 1 + 1 ) ) -> ( 0 + 0 ) = ( 0 + 1 ) )
15 0red 
 |-  ( ( 0 = ( 0 + 0 ) /\ 1 = ( 1 + 1 ) ) -> 0 e. RR )
16 1red 
 |-  ( ( 0 = ( 0 + 0 ) /\ 1 = ( 1 + 1 ) ) -> 1 e. RR )
17 readdcan 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ 0 e. RR ) -> ( ( 0 + 0 ) = ( 0 + 1 ) <-> 0 = 1 ) )
18 15 16 15 17 syl3anc 
 |-  ( ( 0 = ( 0 + 0 ) /\ 1 = ( 1 + 1 ) ) -> ( ( 0 + 0 ) = ( 0 + 1 ) <-> 0 = 1 ) )
19 14 18 mpbid 
 |-  ( ( 0 = ( 0 + 0 ) /\ 1 = ( 1 + 1 ) ) -> 0 = 1 )
20 19 ex 
 |-  ( 0 = ( 0 + 0 ) -> ( 1 = ( 1 + 1 ) -> 0 = 1 ) )
21 20 necon3d 
 |-  ( 0 = ( 0 + 0 ) -> ( 0 =/= 1 -> 1 =/= ( 1 + 1 ) ) )
22 1 21 mpi 
 |-  ( 0 = ( 0 + 0 ) -> 1 =/= ( 1 + 1 ) )
23 oveq2 
 |-  ( 1 = ( 1 + 1 ) -> ( 0 x. 1 ) = ( 0 x. ( 1 + 1 ) ) )
24 0re 
 |-  0 e. RR
25 ax-1rid 
 |-  ( 0 e. RR -> ( 0 x. 1 ) = 0 )
26 24 25 ax-mp 
 |-  ( 0 x. 1 ) = 0
27 0cn 
 |-  0 e. CC
28 27 4 4 adddii 
 |-  ( 0 x. ( 1 + 1 ) ) = ( ( 0 x. 1 ) + ( 0 x. 1 ) )
29 26 26 oveq12i 
 |-  ( ( 0 x. 1 ) + ( 0 x. 1 ) ) = ( 0 + 0 )
30 28 29 eqtri 
 |-  ( 0 x. ( 1 + 1 ) ) = ( 0 + 0 )
31 23 26 30 3eqtr3g 
 |-  ( 1 = ( 1 + 1 ) -> 0 = ( 0 + 0 ) )
32 31 necon3i 
 |-  ( 0 =/= ( 0 + 0 ) -> 1 =/= ( 1 + 1 ) )
33 22 32 pm2.61ine 
 |-  1 =/= ( 1 + 1 )
34 df-2 
 |-  2 = ( 1 + 1 )
35 33 34 neeqtrri 
 |-  1 =/= 2