Theorem neltlt ≪ | index | src | ≫ 

theorem neltlt (a b: nat): $ a != b <-> a < b \/ b < a $;
StepHypRefExpression
1 ltorle 
a < b \/ b <= a
2 necom 
a != b -> b != a
3 ltlene 
b < a <-> b <= a /\ b != a
4 3 bi2i 
b <= a /\ b != a -> b < a
5 4 exp 
b <= a -> b != a -> b < a
6 5 com12 
b != a -> b <= a -> b < a
7 2, 6 rsyl 
a != b -> b <= a -> b < a
8 7 imim2d 
a != b -> (~a < b -> b <= a) -> ~a < b -> b < a
9 8 conv or 
a != b -> a < b \/ b <= a -> a < b \/ b < a
10 1, 9 mpi 
a != b -> a < b \/ b < a
11 eor 
(a < b -> a != b) -> (b < a -> a != b) -> a < b \/ b < a -> a != b
12 ltne 
a < b -> a != b
13 11, 12 ax_mp 
(b < a -> a != b) -> a < b \/ b < a -> a != b
14 ltner 
b < a -> a != b
15 13, 14 ax_mp 
a < b \/ b < a -> a != b
16 10, 15 ibii 
a != b <-> a < b \/ b < a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_peano (peano1, peano2, peano5, addeq, add0, addS)