Theorem zfstsnd ≪ | index | src | ≫ 

theorem zfstsnd (n: nat): $ zfst n -ZN zsnd n = n $;
StepHypRefExpression
1 eor 
(n = b0 (n // 2) -> zfst n -ZN zsnd n = n) -> (n = b1 (n // 2) -> zfst n -ZN zsnd n = n) -> n = b0 (n // 2) \/ n = b1 (n // 2) -> zfst n -ZN zsnd n = n
2 znsubpos 
zsnd n <= zfst n -> zfst n -ZN zsnd n = b0 (zfst n - zsnd n)
3 le01 
0 <= n // 2
4 zsndb0 
zsnd (b0 (n // 2)) = 0
5 zsndeq 
n = b0 (n // 2) -> zsnd n = zsnd (b0 (n // 2))
6 4, 5 syl6eq 
n = b0 (n // 2) -> zsnd n = 0
7 zfstb0 
zfst (b0 (n // 2)) = n // 2
8 zfsteq 
n = b0 (n // 2) -> zfst n = zfst (b0 (n // 2))
9 7, 8 syl6eq 
n = b0 (n // 2) -> zfst n = n // 2
10 6, 9 leeqd 
n = b0 (n // 2) -> (zsnd n <= zfst n <-> 0 <= n // 2)
11 3, 10 mpbiri 
n = b0 (n // 2) -> zsnd n <= zfst n
12 2, 11 syl 
n = b0 (n // 2) -> zfst n -ZN zsnd n = b0 (zfst n - zsnd n)
13 sub02 
n // 2 - 0 = n // 2
14 9, 6 subeqd 
n = b0 (n // 2) -> zfst n - zsnd n = n // 2 - 0
15 13, 14 syl6eq 
n = b0 (n // 2) -> zfst n - zsnd n = n // 2
16 15 b0eqd 
n = b0 (n // 2) -> b0 (zfst n - zsnd n) = b0 (n // 2)
17 id 
n = b0 (n // 2) -> n = b0 (n // 2)
18 16, 17 eqtr4d 
n = b0 (n // 2) -> b0 (zfst n - zsnd n) = n
19 12, 18 eqtrd 
n = b0 (n // 2) -> zfst n -ZN zsnd n = n
20 1, 19 ax_mp 
(n = b1 (n // 2) -> zfst n -ZN zsnd n = n) -> n = b0 (n // 2) \/ n = b1 (n // 2) -> zfst n -ZN zsnd n = n
21 znsubneg 
zfst n < zsnd n -> zfst n -ZN zsnd n = b1 (zsnd n - suc (zfst n))
22 lt01S 
0 < suc (n // 2)
23 zfstb1 
zfst (b1 (n // 2)) = 0
24 zfsteq 
n = b1 (n // 2) -> zfst n = zfst (b1 (n // 2))
25 23, 24 syl6eq 
n = b1 (n // 2) -> zfst n = 0
26 zsndb1 
zsnd (b1 (n // 2)) = suc (n // 2)
27 zsndeq 
n = b1 (n // 2) -> zsnd n = zsnd (b1 (n // 2))
28 26, 27 syl6eq 
n = b1 (n // 2) -> zsnd n = suc (n // 2)
29 25, 28 lteqd 
n = b1 (n // 2) -> (zfst n < zsnd n <-> 0 < suc (n // 2))
30 22, 29 mpbiri 
n = b1 (n // 2) -> zfst n < zsnd n
31 21, 30 syl 
n = b1 (n // 2) -> zfst n -ZN zsnd n = b1 (zsnd n - suc (zfst n))
32 eqtr 
suc (n // 2) - suc 0 = n // 2 - 0 -> n // 2 - 0 = n // 2 -> suc (n // 2) - suc 0 = n // 2
33 subSS 
suc (n // 2) - suc 0 = n // 2 - 0
34 32, 33 ax_mp 
n // 2 - 0 = n // 2 -> suc (n // 2) - suc 0 = n // 2
35 34, 13 ax_mp 
suc (n // 2) - suc 0 = n // 2
36 25 suceqd 
n = b1 (n // 2) -> suc (zfst n) = suc 0
37 28, 36 subeqd 
n = b1 (n // 2) -> zsnd n - suc (zfst n) = suc (n // 2) - suc 0
38 35, 37 syl6eq 
n = b1 (n // 2) -> zsnd n - suc (zfst n) = n // 2
39 38 b1eqd 
n = b1 (n // 2) -> b1 (zsnd n - suc (zfst n)) = b1 (n // 2)
40 id 
n = b1 (n // 2) -> n = b1 (n // 2)
41 39, 40 eqtr4d 
n = b1 (n // 2) -> b1 (zsnd n - suc (zfst n)) = n
42 31, 41 eqtrd 
n = b1 (n // 2) -> zfst n -ZN zsnd n = n
43 20, 42 ax_mp 
n = b0 (n // 2) \/ n = b1 (n // 2) -> zfst n -ZN zsnd n = n
44 b0orb1 
n = b0 (n // 2) \/ n = b1 (n // 2)
45 43, 44 ax_mp 
zfst n -ZN zsnd n = 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)