Proof of Theorem usgrexmpldifpr
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0z 12624 | . . . . . 6
⊢ 0 ∈
ℤ | 
| 2 |  | 1z 12647 | . . . . . 6
⊢ 1 ∈
ℤ | 
| 3 | 1, 2 | pm3.2i 470 | . . . . 5
⊢ (0 ∈
ℤ ∧ 1 ∈ ℤ) | 
| 4 |  | 2z 12649 | . . . . . 6
⊢ 2 ∈
ℤ | 
| 5 | 2, 4 | pm3.2i 470 | . . . . 5
⊢ (1 ∈
ℤ ∧ 2 ∈ ℤ) | 
| 6 | 3, 5 | pm3.2i 470 | . . . 4
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) ∧ (1 ∈ ℤ ∧ 2 ∈
ℤ)) | 
| 7 |  | ax-1ne0 11224 | . . . . . . 7
⊢ 1 ≠
0 | 
| 8 | 7 | necomi 2995 | . . . . . 6
⊢ 0 ≠
1 | 
| 9 |  | 2ne0 12370 | . . . . . . 7
⊢ 2 ≠
0 | 
| 10 | 9 | necomi 2995 | . . . . . 6
⊢ 0 ≠
2 | 
| 11 | 8, 10 | pm3.2i 470 | . . . . 5
⊢ (0 ≠ 1
∧ 0 ≠ 2) | 
| 12 | 11 | orci 866 | . . . 4
⊢ ((0 ≠
1 ∧ 0 ≠ 2) ∨ (1 ≠ 1 ∧ 1 ≠ 2)) | 
| 13 |  | prneimg 4854 | . . . 4
⊢ (((0
∈ ℤ ∧ 1 ∈ ℤ) ∧ (1 ∈ ℤ ∧ 2 ∈
ℤ)) → (((0 ≠ 1 ∧ 0 ≠ 2) ∨ (1 ≠ 1 ∧ 1 ≠ 2))
→ {0, 1} ≠ {1, 2})) | 
| 14 | 6, 12, 13 | mp2 9 | . . 3
⊢ {0, 1}
≠ {1, 2} | 
| 15 | 4, 1 | pm3.2i 470 | . . . . 5
⊢ (2 ∈
ℤ ∧ 0 ∈ ℤ) | 
| 16 | 3, 15 | pm3.2i 470 | . . . 4
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) ∧ (2 ∈ ℤ ∧ 0 ∈
ℤ)) | 
| 17 |  | 1ne2 12474 | . . . . . 6
⊢ 1 ≠
2 | 
| 18 | 17, 7 | pm3.2i 470 | . . . . 5
⊢ (1 ≠ 2
∧ 1 ≠ 0) | 
| 19 | 18 | olci 867 | . . . 4
⊢ ((0 ≠
2 ∧ 0 ≠ 0) ∨ (1 ≠ 2 ∧ 1 ≠ 0)) | 
| 20 |  | prneimg 4854 | . . . 4
⊢ (((0
∈ ℤ ∧ 1 ∈ ℤ) ∧ (2 ∈ ℤ ∧ 0 ∈
ℤ)) → (((0 ≠ 2 ∧ 0 ≠ 0) ∨ (1 ≠ 2 ∧ 1 ≠ 0))
→ {0, 1} ≠ {2, 0})) | 
| 21 | 16, 19, 20 | mp2 9 | . . 3
⊢ {0, 1}
≠ {2, 0} | 
| 22 |  | 3nn 12345 | . . . . . 6
⊢ 3 ∈
ℕ | 
| 23 | 1, 22 | pm3.2i 470 | . . . . 5
⊢ (0 ∈
ℤ ∧ 3 ∈ ℕ) | 
| 24 | 3, 23 | pm3.2i 470 | . . . 4
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) ∧ (0 ∈ ℤ ∧ 3 ∈
ℕ)) | 
| 25 |  | 1re 11261 | . . . . . . 7
⊢ 1 ∈
ℝ | 
| 26 |  | 1lt3 12439 | . . . . . . 7
⊢ 1 <
3 | 
| 27 | 25, 26 | ltneii 11374 | . . . . . 6
⊢ 1 ≠
3 | 
| 28 | 7, 27 | pm3.2i 470 | . . . . 5
⊢ (1 ≠ 0
∧ 1 ≠ 3) | 
| 29 | 28 | olci 867 | . . . 4
⊢ ((0 ≠
0 ∧ 0 ≠ 3) ∨ (1 ≠ 0 ∧ 1 ≠ 3)) | 
| 30 |  | prneimg 4854 | . . . 4
⊢ (((0
∈ ℤ ∧ 1 ∈ ℤ) ∧ (0 ∈ ℤ ∧ 3 ∈
ℕ)) → (((0 ≠ 0 ∧ 0 ≠ 3) ∨ (1 ≠ 0 ∧ 1 ≠ 3))
→ {0, 1} ≠ {0, 3})) | 
| 31 | 24, 29, 30 | mp2 9 | . . 3
⊢ {0, 1}
≠ {0, 3} | 
| 32 | 14, 21, 31 | 3pm3.2i 1340 | . 2
⊢ ({0, 1}
≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) | 
| 33 | 5, 15 | pm3.2i 470 | . . . 4
⊢ ((1
∈ ℤ ∧ 2 ∈ ℤ) ∧ (2 ∈ ℤ ∧ 0 ∈
ℤ)) | 
| 34 | 18 | orci 866 | . . . 4
⊢ ((1 ≠
2 ∧ 1 ≠ 0) ∨ (2 ≠ 2 ∧ 2 ≠ 0)) | 
| 35 |  | prneimg 4854 | . . . 4
⊢ (((1
∈ ℤ ∧ 2 ∈ ℤ) ∧ (2 ∈ ℤ ∧ 0 ∈
ℤ)) → (((1 ≠ 2 ∧ 1 ≠ 0) ∨ (2 ≠ 2 ∧ 2 ≠ 0))
→ {1, 2} ≠ {2, 0})) | 
| 36 | 33, 34, 35 | mp2 9 | . . 3
⊢ {1, 2}
≠ {2, 0} | 
| 37 | 5, 23 | pm3.2i 470 | . . . 4
⊢ ((1
∈ ℤ ∧ 2 ∈ ℤ) ∧ (0 ∈ ℤ ∧ 3 ∈
ℕ)) | 
| 38 | 28 | orci 866 | . . . 4
⊢ ((1 ≠
0 ∧ 1 ≠ 3) ∨ (2 ≠ 0 ∧ 2 ≠ 3)) | 
| 39 |  | prneimg 4854 | . . . 4
⊢ (((1
∈ ℤ ∧ 2 ∈ ℤ) ∧ (0 ∈ ℤ ∧ 3 ∈
ℕ)) → (((1 ≠ 0 ∧ 1 ≠ 3) ∨ (2 ≠ 0 ∧ 2 ≠ 3))
→ {1, 2} ≠ {0, 3})) | 
| 40 | 37, 38, 39 | mp2 9 | . . 3
⊢ {1, 2}
≠ {0, 3} | 
| 41 | 15, 23 | pm3.2i 470 | . . . 4
⊢ ((2
∈ ℤ ∧ 0 ∈ ℤ) ∧ (0 ∈ ℤ ∧ 3 ∈
ℕ)) | 
| 42 |  | 2re 12340 | . . . . . . 7
⊢ 2 ∈
ℝ | 
| 43 |  | 2lt3 12438 | . . . . . . 7
⊢ 2 <
3 | 
| 44 | 42, 43 | ltneii 11374 | . . . . . 6
⊢ 2 ≠
3 | 
| 45 | 9, 44 | pm3.2i 470 | . . . . 5
⊢ (2 ≠ 0
∧ 2 ≠ 3) | 
| 46 | 45 | orci 866 | . . . 4
⊢ ((2 ≠
0 ∧ 2 ≠ 3) ∨ (0 ≠ 0 ∧ 0 ≠ 3)) | 
| 47 |  | prneimg 4854 | . . . 4
⊢ (((2
∈ ℤ ∧ 0 ∈ ℤ) ∧ (0 ∈ ℤ ∧ 3 ∈
ℕ)) → (((2 ≠ 0 ∧ 2 ≠ 3) ∨ (0 ≠ 0 ∧ 0 ≠ 3))
→ {2, 0} ≠ {0, 3})) | 
| 48 | 41, 46, 47 | mp2 9 | . . 3
⊢ {2, 0}
≠ {0, 3} | 
| 49 | 36, 40, 48 | 3pm3.2i 1340 | . 2
⊢ ({1, 2}
≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0, 3}) | 
| 50 | 32, 49 | pm3.2i 470 | 1
⊢ (({0, 1}
≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) ∧ ({1, 2}
≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0,
3})) |