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 id 
_1 = n -> _1 = n
14 13 dvdeq2d 
_1 = n -> (2 || _1 <-> 2 || n)
15 14 noteqd 
_1 = n -> (~2 || _1 <-> ~2 || n)
16 13 suceqd 
_1 = n -> suc _1 = suc n
17 16 dvdeq2d 
_1 = n -> (2 || suc _1 <-> 2 || suc n)
18 15, 17 imeqd 
_1 = n -> (~2 || _1 -> 2 || suc _1 <-> ~2 || n -> 2 || suc n)
19 id 
_1 = 0 -> _1 = 0
20 19 dvdeq2d 
_1 = 0 -> (2 || _1 <-> 2 || 0)
21 20 noteqd 
_1 = 0 -> (~2 || _1 <-> ~2 || 0)
22 19 suceqd 
_1 = 0 -> suc _1 = suc 0
23 22 dvdeq2d 
_1 = 0 -> (2 || suc _1 <-> 2 || suc 0)
24 21, 23 imeqd 
_1 = 0 -> (~2 || _1 -> 2 || suc _1 <-> ~2 || 0 -> 2 || suc 0)
25 id 
_1 = a1 -> _1 = a1
26 25 dvdeq2d 
_1 = a1 -> (2 || _1 <-> 2 || a1)
27 26 noteqd 
_1 = a1 -> (~2 || _1 <-> ~2 || a1)
28 25 suceqd 
_1 = a1 -> suc _1 = suc a1
29 28 dvdeq2d 
_1 = a1 -> (2 || suc _1 <-> 2 || suc a1)
30 27, 29 imeqd 
_1 = a1 -> (~2 || _1 -> 2 || suc _1 <-> ~2 || a1 -> 2 || suc a1)
31 id 
_1 = suc a1 -> _1 = suc a1
32 31 dvdeq2d 
_1 = suc a1 -> (2 || _1 <-> 2 || suc a1)
33 32 noteqd 
_1 = suc a1 -> (~2 || _1 <-> ~2 || suc a1)
34 31 suceqd 
_1 = suc a1 -> suc _1 = suc (suc a1)
35 34 dvdeq2d 
_1 = suc a1 -> (2 || suc _1 <-> 2 || suc (suc a1))
36 33, 35 imeqd 
_1 = suc a1 -> (~2 || _1 -> 2 || suc _1 <-> ~2 || suc a1 -> 2 || suc (suc a1))
37 orl 
2 || 0 -> 2 || 0 \/ 2 || suc 0
38 37 conv or 
2 || 0 -> ~2 || 0 -> 2 || suc 0
39 dvd02 
2 || 0
40 38, 39 ax_mp 
~2 || 0 -> 2 || suc 0
41 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)
42 41 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)
43 dvdeq2 
a1 + suc 1 = suc (suc a1) -> (2 || a1 + suc 1 <-> 2 || suc (suc a1))
44 eqtr 
a1 + suc 1 = suc (a1 + 1) -> suc (a1 + 1) = suc (suc a1) -> a1 + suc 1 = suc (suc a1)
45 addS 
a1 + suc 1 = suc (a1 + 1)
46 44, 45 ax_mp 
suc (a1 + 1) = suc (suc a1) -> a1 + suc 1 = suc (suc a1)
47 suceq 
a1 + 1 = suc a1 -> suc (a1 + 1) = suc (suc a1)
48 add12 
a1 + 1 = suc a1
49 47, 48 ax_mp 
suc (a1 + 1) = suc (suc a1)
50 46, 49 ax_mp 
a1 + suc 1 = suc (suc a1)
51 43, 50 ax_mp 
2 || a1 + suc 1 <-> 2 || suc (suc a1)
52 dvdid 
2 || 2
53 dvdadd1 
2 || a1 -> (2 || 2 <-> 2 || a1 + 2)
54 53 conv d2 
2 || a1 -> (2 || 2 <-> 2 || a1 + suc 1)
55 52, 54 mpbii 
2 || a1 -> 2 || a1 + suc 1
56 51, 55 sylib 
2 || a1 -> 2 || suc (suc a1)
57 56 orrd 
2 || a1 -> 2 || suc a1 \/ 2 || suc (suc a1)
58 57 conv or 
2 || a1 -> ~2 || suc a1 -> 2 || suc (suc a1)
59 42, 58 ax_mp 
(2 || suc a1 -> ~2 || suc a1 -> 2 || suc (suc a1)) -> (~2 || a1 -> 2 || suc a1) -> ~2 || suc a1 -> 2 || suc (suc a1)
60 orl 
2 || suc a1 -> 2 || suc a1 \/ 2 || suc (suc a1)
61 60 conv or 
2 || suc a1 -> ~2 || suc a1 -> 2 || suc (suc a1)
62 59, 61 ax_mp 
(~2 || a1 -> 2 || suc a1) -> ~2 || suc a1 -> 2 || suc (suc a1)
63 18, 24, 30, 36, 40, 62 ind 
~2 || n -> 2 || suc n
64 12, 63 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)