Theorem d2dvdS ≪ | index | src | ≫ 

theorem d2dvdS (n: nat): $ 2 || suc n <-> ~2 || n $;
StepHypRefExpression
1 d2dvd1 
~2 || 1
2 1 a1i 
2 || suc n -> ~2 || 1
3 dvdeq2 
n + 1 = suc n -> (2 || n + 1 <-> 2 || suc n)
4 add12 
n + 1 = suc n
5 3, 4 ax_mp 
2 || n + 1 <-> 2 || suc n
6 dvdadd1 
2 || n -> (2 || 1 <-> 2 || n + 1)
7 6 anwr 
2 || suc n /\ 2 || n -> (2 || 1 <-> 2 || n + 1)
8 5, 7 syl6bb 
2 || suc n /\ 2 || n -> (2 || 1 <-> 2 || suc n)
9 anl 
2 || suc n /\ 2 || n -> 2 || suc n
10 8, 9 mpbird 
2 || suc n /\ 2 || n -> 2 || 1
11 10 exp 
2 || suc n -> 2 || n -> 2 || 1
12 2, 11 mtd 
2 || suc n -> ~2 || n
13 eqidd 
_1 = n -> 2 = 2
14 id 
_1 = n -> _1 = n
15 13, 14 dvdeqd 
_1 = n -> (2 || _1 <-> 2 || n)
16 15 noteqd 
_1 = n -> (~2 || _1 <-> ~2 || n)
17 14 suceqd 
_1 = n -> suc _1 = suc n
18 13, 17 dvdeqd 
_1 = n -> (2 || suc _1 <-> 2 || suc n)
19 16, 18 imeqd 
_1 = n -> (~2 || _1 -> 2 || suc _1 <-> ~2 || n -> 2 || suc n)
20 eqidd 
_1 = 0 -> 2 = 2
21 id 
_1 = 0 -> _1 = 0
22 20, 21 dvdeqd 
_1 = 0 -> (2 || _1 <-> 2 || 0)
23 22 noteqd 
_1 = 0 -> (~2 || _1 <-> ~2 || 0)
24 21 suceqd 
_1 = 0 -> suc _1 = suc 0
25 20, 24 dvdeqd 
_1 = 0 -> (2 || suc _1 <-> 2 || suc 0)
26 23, 25 imeqd 
_1 = 0 -> (~2 || _1 -> 2 || suc _1 <-> ~2 || 0 -> 2 || suc 0)
27 eqidd 
_1 = a1 -> 2 = 2
28 id 
_1 = a1 -> _1 = a1
29 27, 28 dvdeqd 
_1 = a1 -> (2 || _1 <-> 2 || a1)
30 29 noteqd 
_1 = a1 -> (~2 || _1 <-> ~2 || a1)
31 28 suceqd 
_1 = a1 -> suc _1 = suc a1
32 27, 31 dvdeqd 
_1 = a1 -> (2 || suc _1 <-> 2 || suc a1)
33 30, 32 imeqd 
_1 = a1 -> (~2 || _1 -> 2 || suc _1 <-> ~2 || a1 -> 2 || suc a1)
34 eqidd 
_1 = suc a1 -> 2 = 2
35 id 
_1 = suc a1 -> _1 = suc a1
36 34, 35 dvdeqd 
_1 = suc a1 -> (2 || _1 <-> 2 || suc a1)
37 36 noteqd 
_1 = suc a1 -> (~2 || _1 <-> ~2 || suc a1)
38 35 suceqd 
_1 = suc a1 -> suc _1 = suc (suc a1)
39 34, 38 dvdeqd 
_1 = suc a1 -> (2 || suc _1 <-> 2 || suc (suc a1))
40 37, 39 imeqd 
_1 = suc a1 -> (~2 || _1 -> 2 || suc _1 <-> ~2 || suc a1 -> 2 || suc (suc a1))
41 orl 
2 || 0 -> 2 || 0 \/ 2 || suc 0
42 41 conv or 
2 || 0 -> ~2 || 0 -> 2 || suc 0
43 dvd02 
2 || 0
44 42, 43 ax_mp 
~2 || 0 -> 2 || suc 0
45 eor 
(2 || a1 -> ~2 || suc a1 -> 2 || suc (suc a1)) ->
  (2 || suc a1 -> ~2 || suc a1 -> 2 || suc (suc a1)) ->
  2 || a1 \/ 2 || suc a1 ->
  ~2 || suc a1 ->
  2 || suc (suc a1)
46 45 conv or 
(2 || a1 -> ~2 || suc a1 -> 2 || suc (suc a1)) ->
  (2 || suc a1 -> ~2 || suc a1 -> 2 || suc (suc a1)) ->
  (~2 || a1 -> 2 || suc a1) ->
  ~2 || suc a1 ->
  2 || suc (suc a1)
47 dvdeq2 
a1 + suc 1 = suc (suc a1) -> (2 || a1 + suc 1 <-> 2 || suc (suc a1))
48 eqtr 
a1 + suc 1 = suc (a1 + 1) -> suc (a1 + 1) = suc (suc a1) -> a1 + suc 1 = suc (suc a1)
49 addS 
a1 + suc 1 = suc (a1 + 1)
50 48, 49 ax_mp 
suc (a1 + 1) = suc (suc a1) -> a1 + suc 1 = suc (suc a1)
51 suceq 
a1 + 1 = suc a1 -> suc (a1 + 1) = suc (suc a1)
52 add12 
a1 + 1 = suc a1
53 51, 52 ax_mp 
suc (a1 + 1) = suc (suc a1)
54 50, 53 ax_mp 
a1 + suc 1 = suc (suc a1)
55 47, 54 ax_mp 
2 || a1 + suc 1 <-> 2 || suc (suc a1)
56 dvdid 
2 || 2
57 dvdadd1 
2 || a1 -> (2 || 2 <-> 2 || a1 + 2)
58 57 conv d2 
2 || a1 -> (2 || 2 <-> 2 || a1 + suc 1)
59 56, 58 mpbii 
2 || a1 -> 2 || a1 + suc 1
60 55, 59 sylib 
2 || a1 -> 2 || suc (suc a1)
61 60 orrd 
2 || a1 -> 2 || suc a1 \/ 2 || suc (suc a1)
62 61 conv or 
2 || a1 -> ~2 || suc a1 -> 2 || suc (suc a1)
63 46, 62 ax_mp 
(2 || suc a1 -> ~2 || suc a1 -> 2 || suc (suc a1)) -> (~2 || a1 -> 2 || suc a1) -> ~2 || suc a1 -> 2 || suc (suc a1)
64 orl 
2 || suc a1 -> 2 || suc a1 \/ 2 || suc (suc a1)
65 64 conv or 
2 || suc a1 -> ~2 || suc a1 -> 2 || suc (suc a1)
66 63, 65 ax_mp 
(~2 || a1 -> 2 || suc a1) -> ~2 || suc a1 -> 2 || suc (suc a1)
67 19, 26, 33, 40, 44, 66 ind 
~2 || n -> 2 || suc n
68 12, 67 ibii 
2 || suc n <-> ~2 || n

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, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)