Theorem natinj | index | src |

theorem natinj (p q: wff): $ p <-> q <-> nat p = nat q $;
StepHypRefExpression
1 bitr4
(p <-> q <-> nat p <= nat q /\ nat q <= nat p) -> (nat p = nat q <-> nat p <= nat q /\ nat q <= nat p) -> (p <-> q <-> nat p = nat q)
2 aneq
(p -> q <-> nat p <= nat q) -> (q -> p <-> nat q <= nat p) -> ((p -> q) /\ (q -> p) <-> nat p <= nat q /\ nat q <= nat p)
3 2 conv iff
(p -> q <-> nat p <= nat q) -> (q -> p <-> nat q <= nat p) -> (p <-> q <-> nat p <= nat q /\ nat q <= nat p)
4 natle
p -> q <-> nat p <= nat q
5 3, 4 ax_mp
(q -> p <-> nat q <= nat p) -> (p <-> q <-> nat p <= nat q /\ nat q <= nat p)
6 natle
q -> p <-> nat q <= nat p
7 5, 6 ax_mp
p <-> q <-> nat p <= nat q /\ nat q <= nat p
8 1, 7 ax_mp
(nat p = nat q <-> nat p <= nat q /\ nat q <= nat p) -> (p <-> q <-> nat p = nat q)
9 eqlele
nat p = nat q <-> nat p <= nat q /\ nat q <= nat p
10 8, 9 ax_mp
p <-> q <-> nat p = nat q

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_set (elab, ax_8), axs_the (theid), axs_peano (peano1, peano2, peano5, addeq, add0, addS)