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 ∈ ℂ
3 2 2 mulcli ⊢ ( i · i ) ∈ ℂ
4 ax-1cn ⊢ 1 ∈ ℂ
5 3 4 4 addassi ⊢ ( ( ( i · i ) + 1 ) + 1 ) = ( ( i · i ) + ( 1 + 1 ) )
6 5 a1i ⊢ ( ( 0 = ( 0 + 0 ) ∧ 1 = ( 1 + 1 ) ) → ( ( ( i · i ) + 1 ) + 1 ) = ( ( i · i ) + ( 1 + 1 ) ) )
7 simpr ⊢ ( ( 0 = ( 0 + 0 ) ∧ 1 = ( 1 + 1 ) ) → 1 = ( 1 + 1 ) )
8 7 oveq2d ⊢ ( ( 0 = ( 0 + 0 ) ∧ 1 = ( 1 + 1 ) ) → ( ( i · i ) + 1 ) = ( ( i · i ) + ( 1 + 1 ) ) )
9 ax-i2m1 ⊢ ( ( i · i ) + 1 ) = 0
10 9 a1i ⊢ ( ( 0 = ( 0 + 0 ) ∧ 1 = ( 1 + 1 ) ) → ( ( i · i ) + 1 ) = 0 )
11 6 8 10 3eqtr2rd ⊢ ( ( 0 = ( 0 + 0 ) ∧ 1 = ( 1 + 1 ) ) → 0 = ( ( ( i · i ) + 1 ) + 1 ) )
12 simpl ⊢ ( ( 0 = ( 0 + 0 ) ∧ 1 = ( 1 + 1 ) ) → 0 = ( 0 + 0 ) )
13 10 oveq1d ⊢ ( ( 0 = ( 0 + 0 ) ∧ 1 = ( 1 + 1 ) ) → ( ( ( i · 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 ∈ ℝ )
16 1red ⊢ ( ( 0 = ( 0 + 0 ) ∧ 1 = ( 1 + 1 ) ) → 1 ∈ ℝ )
17 readdcan ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 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 · 1 ) = ( 0 · ( 1 + 1 ) ) )
24 0re ⊢ 0 ∈ ℝ
25 ax-1rid ⊢ ( 0 ∈ ℝ → ( 0 · 1 ) = 0 )
26 24 25 ax-mp ⊢ ( 0 · 1 ) = 0
27 0cn ⊢ 0 ∈ ℂ
28 27 4 4 adddii ⊢ ( 0 · ( 1 + 1 ) ) = ( ( 0 · 1 ) + ( 0 · 1 ) )
29 26 26 oveq12i ⊢ ( ( 0 · 1 ) + ( 0 · 1 ) ) = ( 0 + 0 )
30 28 29 eqtri ⊢ ( 0 · ( 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