| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elzs 28370 | . 2
⊢ (𝐴 ∈ ℤs
↔ ∃𝑛 ∈
ℕs ∃𝑚 ∈ ℕs 𝐴 = (𝑛 -s 𝑚)) | 
| 2 |  | nnsno 28329 | . . . . . . 7
⊢ (𝑛 ∈ ℕs
→ 𝑛 ∈  No ) | 
| 3 |  | nnsno 28329 | . . . . . . 7
⊢ (𝑚 ∈ ℕs
→ 𝑚 ∈  No ) | 
| 4 |  | subscl 28092 | . . . . . . 7
⊢ ((𝑛 ∈ 
No  ∧ 𝑚 ∈
 No ) → (𝑛 -s 𝑚) ∈  No
) | 
| 5 | 2, 3, 4 | syl2an 596 | . . . . . 6
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → (𝑛 -s 𝑚) ∈  No
) | 
| 6 |  | sletric 27809 | . . . . . . . 8
⊢ ((𝑚 ∈ 
No  ∧ 𝑛 ∈
 No ) → (𝑚 ≤s 𝑛 ∨ 𝑛 ≤s 𝑚)) | 
| 7 | 3, 2, 6 | syl2anr 597 | . . . . . . 7
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → (𝑚 ≤s 𝑛 ∨ 𝑛 ≤s 𝑚)) | 
| 8 |  | nnn0s 28332 | . . . . . . . . 9
⊢ (𝑚 ∈ ℕs
→ 𝑚 ∈
ℕ0s) | 
| 9 |  | nnn0s 28332 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕs
→ 𝑛 ∈
ℕ0s) | 
| 10 |  | n0subs 28360 | . . . . . . . . 9
⊢ ((𝑚 ∈ ℕ0s
∧ 𝑛 ∈
ℕ0s) → (𝑚 ≤s 𝑛 ↔ (𝑛 -s 𝑚) ∈
ℕ0s)) | 
| 11 | 8, 9, 10 | syl2anr 597 | . . . . . . . 8
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → (𝑚 ≤s 𝑛 ↔ (𝑛 -s 𝑚) ∈
ℕ0s)) | 
| 12 |  | n0subs 28360 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ0s
∧ 𝑚 ∈
ℕ0s) → (𝑛 ≤s 𝑚 ↔ (𝑚 -s 𝑛) ∈
ℕ0s)) | 
| 13 | 9, 8, 12 | syl2an 596 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → (𝑛 ≤s 𝑚 ↔ (𝑚 -s 𝑛) ∈
ℕ0s)) | 
| 14 | 2 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → 𝑛 ∈  No
) | 
| 15 | 3 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → 𝑚 ∈  No
) | 
| 16 | 14, 15 | negsubsdi2d 28110 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → ( -us ‘(𝑛 -s 𝑚)) = (𝑚 -s 𝑛)) | 
| 17 | 16 | eleq1d 2826 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → (( -us ‘(𝑛 -s 𝑚)) ∈ ℕ0s ↔ (𝑚 -s 𝑛) ∈
ℕ0s)) | 
| 18 | 13, 17 | bitr4d 282 | . . . . . . . 8
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → (𝑛 ≤s 𝑚 ↔ ( -us ‘(𝑛 -s 𝑚)) ∈
ℕ0s)) | 
| 19 | 11, 18 | orbi12d 919 | . . . . . . 7
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → ((𝑚 ≤s 𝑛 ∨ 𝑛 ≤s 𝑚) ↔ ((𝑛 -s 𝑚) ∈ ℕ0s ∨ (
-us ‘(𝑛
-s 𝑚)) ∈
ℕ0s))) | 
| 20 | 7, 19 | mpbid 232 | . . . . . 6
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → ((𝑛 -s 𝑚) ∈ ℕ0s ∨ (
-us ‘(𝑛
-s 𝑚)) ∈
ℕ0s)) | 
| 21 | 5, 20 | jca 511 | . . . . 5
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → ((𝑛 -s 𝑚) ∈  No 
∧ ((𝑛 -s
𝑚) ∈
ℕ0s ∨ ( -us ‘(𝑛 -s 𝑚)) ∈
ℕ0s))) | 
| 22 |  | eleq1 2829 | . . . . . 6
⊢ (𝐴 = (𝑛 -s 𝑚) → (𝐴 ∈  No 
↔ (𝑛 -s
𝑚) ∈  No )) | 
| 23 |  | eleq1 2829 | . . . . . . 7
⊢ (𝐴 = (𝑛 -s 𝑚) → (𝐴 ∈ ℕ0s ↔ (𝑛 -s 𝑚) ∈
ℕ0s)) | 
| 24 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝐴 = (𝑛 -s 𝑚) → ( -us ‘𝐴) = ( -us
‘(𝑛 -s
𝑚))) | 
| 25 | 24 | eleq1d 2826 | . . . . . . 7
⊢ (𝐴 = (𝑛 -s 𝑚) → (( -us ‘𝐴) ∈ ℕ0s
↔ ( -us ‘(𝑛 -s 𝑚)) ∈
ℕ0s)) | 
| 26 | 23, 25 | orbi12d 919 | . . . . . 6
⊢ (𝐴 = (𝑛 -s 𝑚) → ((𝐴 ∈ ℕ0s ∨ (
-us ‘𝐴)
∈ ℕ0s) ↔ ((𝑛 -s 𝑚) ∈ ℕ0s ∨ (
-us ‘(𝑛
-s 𝑚)) ∈
ℕ0s))) | 
| 27 | 22, 26 | anbi12d 632 | . . . . 5
⊢ (𝐴 = (𝑛 -s 𝑚) → ((𝐴 ∈  No 
∧ (𝐴 ∈
ℕ0s ∨ ( -us ‘𝐴) ∈ ℕ0s)) ↔
((𝑛 -s 𝑚) ∈ 
No  ∧ ((𝑛
-s 𝑚) ∈
ℕ0s ∨ ( -us ‘(𝑛 -s 𝑚)) ∈
ℕ0s)))) | 
| 28 | 21, 27 | syl5ibrcom 247 | . . . 4
⊢ ((𝑛 ∈ ℕs
∧ 𝑚 ∈
ℕs) → (𝐴 = (𝑛 -s 𝑚) → (𝐴 ∈  No 
∧ (𝐴 ∈
ℕ0s ∨ ( -us ‘𝐴) ∈
ℕ0s)))) | 
| 29 | 28 | rexlimivv 3201 | . . 3
⊢
(∃𝑛 ∈
ℕs ∃𝑚 ∈ ℕs 𝐴 = (𝑛 -s 𝑚) → (𝐴 ∈  No 
∧ (𝐴 ∈
ℕ0s ∨ ( -us ‘𝐴) ∈
ℕ0s))) | 
| 30 |  | n0p1nns 28361 | . . . . . 6
⊢ (𝐴 ∈ ℕ0s
→ (𝐴 +s
1s ) ∈ ℕs) | 
| 31 |  | 1nns 28352 | . . . . . . 7
⊢ 
1s ∈ ℕs | 
| 32 | 31 | a1i 11 | . . . . . 6
⊢ (𝐴 ∈ ℕ0s
→ 1s ∈ ℕs) | 
| 33 |  | n0sno 28328 | . . . . . . . 8
⊢ (𝐴 ∈ ℕ0s
→ 𝐴 ∈  No ) | 
| 34 |  | 1sno 27872 | . . . . . . . 8
⊢ 
1s ∈  No | 
| 35 |  | pncans 28102 | . . . . . . . 8
⊢ ((𝐴 ∈ 
No  ∧ 1s ∈  No ) →
((𝐴 +s
1s ) -s 1s ) = 𝐴) | 
| 36 | 33, 34, 35 | sylancl 586 | . . . . . . 7
⊢ (𝐴 ∈ ℕ0s
→ ((𝐴 +s
1s ) -s 1s ) = 𝐴) | 
| 37 | 36 | eqcomd 2743 | . . . . . 6
⊢ (𝐴 ∈ ℕ0s
→ 𝐴 = ((𝐴 +s 1s )
-s 1s )) | 
| 38 |  | rspceov 7480 | . . . . . 6
⊢ (((𝐴 +s 1s )
∈ ℕs ∧ 1s ∈ ℕs ∧
𝐴 = ((𝐴 +s 1s ) -s
1s )) → ∃𝑛 ∈ ℕs ∃𝑚 ∈ ℕs
𝐴 = (𝑛 -s 𝑚)) | 
| 39 | 30, 32, 37, 38 | syl3anc 1373 | . . . . 5
⊢ (𝐴 ∈ ℕ0s
→ ∃𝑛 ∈
ℕs ∃𝑚 ∈ ℕs 𝐴 = (𝑛 -s 𝑚)) | 
| 40 | 39 | adantl 481 | . . . 4
⊢ ((𝐴 ∈ 
No  ∧ 𝐴 ∈
ℕ0s) → ∃𝑛 ∈ ℕs ∃𝑚 ∈ ℕs
𝐴 = (𝑛 -s 𝑚)) | 
| 41 | 31 | a1i 11 | . . . . 5
⊢ ((𝐴 ∈ 
No  ∧ ( -us ‘𝐴) ∈ ℕ0s) →
1s ∈ ℕs) | 
| 42 | 34 | a1i 11 | . . . . . . . . 9
⊢ (𝐴 ∈ 
No  → 1s ∈  No
) | 
| 43 |  | id 22 | . . . . . . . . 9
⊢ (𝐴 ∈ 
No  → 𝐴 ∈
 No ) | 
| 44 | 42, 43 | subsvald 28091 | . . . . . . . 8
⊢ (𝐴 ∈ 
No  → ( 1s -s 𝐴) = ( 1s +s (
-us ‘𝐴))) | 
| 45 |  | negscl 28068 | . . . . . . . . 9
⊢ (𝐴 ∈ 
No  → ( -us ‘𝐴) ∈  No
) | 
| 46 | 42, 45 | addscomd 28000 | . . . . . . . 8
⊢ (𝐴 ∈ 
No  → ( 1s +s ( -us ‘𝐴)) = (( -us
‘𝐴) +s
1s )) | 
| 47 | 44, 46 | eqtrd 2777 | . . . . . . 7
⊢ (𝐴 ∈ 
No  → ( 1s -s 𝐴) = (( -us ‘𝐴) +s 1s
)) | 
| 48 | 47 | adantr 480 | . . . . . 6
⊢ ((𝐴 ∈ 
No  ∧ ( -us ‘𝐴) ∈ ℕ0s) → (
1s -s 𝐴) = (( -us ‘𝐴) +s 1s
)) | 
| 49 |  | n0p1nns 28361 | . . . . . . 7
⊢ ((
-us ‘𝐴)
∈ ℕ0s → (( -us ‘𝐴) +s 1s ) ∈
ℕs) | 
| 50 | 49 | adantl 481 | . . . . . 6
⊢ ((𝐴 ∈ 
No  ∧ ( -us ‘𝐴) ∈ ℕ0s) → ((
-us ‘𝐴)
+s 1s ) ∈ ℕs) | 
| 51 | 48, 50 | eqeltrd 2841 | . . . . 5
⊢ ((𝐴 ∈ 
No  ∧ ( -us ‘𝐴) ∈ ℕ0s) → (
1s -s 𝐴) ∈
ℕs) | 
| 52 | 42, 43 | nncansd 28126 | . . . . . . 7
⊢ (𝐴 ∈ 
No  → ( 1s -s ( 1s -s
𝐴)) = 𝐴) | 
| 53 | 52 | eqcomd 2743 | . . . . . 6
⊢ (𝐴 ∈ 
No  → 𝐴 = (
1s -s ( 1s -s 𝐴))) | 
| 54 | 53 | adantr 480 | . . . . 5
⊢ ((𝐴 ∈ 
No  ∧ ( -us ‘𝐴) ∈ ℕ0s) → 𝐴 = ( 1s -s
( 1s -s 𝐴))) | 
| 55 |  | rspceov 7480 | . . . . 5
⊢ ((
1s ∈ ℕs ∧ ( 1s -s
𝐴) ∈
ℕs ∧ 𝐴
= ( 1s -s ( 1s -s 𝐴))) → ∃𝑛 ∈ ℕs ∃𝑚 ∈ ℕs
𝐴 = (𝑛 -s 𝑚)) | 
| 56 | 41, 51, 54, 55 | syl3anc 1373 | . . . 4
⊢ ((𝐴 ∈ 
No  ∧ ( -us ‘𝐴) ∈ ℕ0s) →
∃𝑛 ∈
ℕs ∃𝑚 ∈ ℕs 𝐴 = (𝑛 -s 𝑚)) | 
| 57 | 40, 56 | jaodan 960 | . . 3
⊢ ((𝐴 ∈ 
No  ∧ (𝐴 ∈
ℕ0s ∨ ( -us ‘𝐴) ∈ ℕ0s)) →
∃𝑛 ∈
ℕs ∃𝑚 ∈ ℕs 𝐴 = (𝑛 -s 𝑚)) | 
| 58 | 29, 57 | impbii 209 | . 2
⊢
(∃𝑛 ∈
ℕs ∃𝑚 ∈ ℕs 𝐴 = (𝑛 -s 𝑚) ↔ (𝐴 ∈  No 
∧ (𝐴 ∈
ℕ0s ∨ ( -us ‘𝐴) ∈
ℕ0s))) | 
| 59 | 1, 58 | bitri 275 | 1
⊢ (𝐴 ∈ ℤs
↔ (𝐴 ∈  No  ∧ (𝐴 ∈ ℕ0s ∨ (
-us ‘𝐴)
∈ ℕ0s))) |