Metamath Proof Explorer

Theorem n0subs

Description: Subtraction of non-negative surreal integers. (Contributed by Scott Fenton, 26-May-2025)

Ref Expression
Assertion n0subs ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 ≤s 𝑁 ↔ ( 𝑁 -s 𝑀 ) ∈ ℕ0s ) )

Proof

Step Hyp Ref Expression
1 breq2 ⊢ ( 𝑥 = 0s → ( 𝑧 ≤s 𝑥 ↔ 𝑧 ≤s 0s ) )
2 oveq1 ⊢ ( 𝑥 = 0s → ( 𝑥 -s 𝑧 ) = ( 0s -s 𝑧 ) )
3 2 eleq1d ⊢ ( 𝑥 = 0s → ( ( 𝑥 -s 𝑧 ) ∈ ℕ0s ↔ ( 0s -s 𝑧 ) ∈ ℕ0s ) )
4 1 3 imbi12d ⊢ ( 𝑥 = 0s → ( ( 𝑧 ≤s 𝑥 → ( 𝑥 -s 𝑧 ) ∈ ℕ0s ) ↔ ( 𝑧 ≤s 0s → ( 0s -s 𝑧 ) ∈ ℕ0s ) ) )
5 4 ralbidv ⊢ ( 𝑥 = 0s → ( ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s 𝑥 → ( 𝑥 -s 𝑧 ) ∈ ℕ0s ) ↔ ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s 0s → ( 0s -s 𝑧 ) ∈ ℕ0s ) ) )
6 breq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑧 ≤s 𝑥 ↔ 𝑧 ≤s 𝑦 ) )
7 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 -s 𝑧 ) = ( 𝑦 -s 𝑧 ) )
8 7 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 -s 𝑧 ) ∈ ℕ0s ↔ ( 𝑦 -s 𝑧 ) ∈ ℕ0s ) )
9 6 8 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑧 ≤s 𝑥 → ( 𝑥 -s 𝑧 ) ∈ ℕ0s ) ↔ ( 𝑧 ≤s 𝑦 → ( 𝑦 -s 𝑧 ) ∈ ℕ0s ) ) )
10 9 ralbidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s 𝑥 → ( 𝑥 -s 𝑧 ) ∈ ℕ0s ) ↔ ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s 𝑦 → ( 𝑦 -s 𝑧 ) ∈ ℕ0s ) ) )
11 breq2 ⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 𝑧 ≤s 𝑥 ↔ 𝑧 ≤s ( 𝑦 +s 1s ) ) )
12 oveq1 ⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 𝑥 -s 𝑧 ) = ( ( 𝑦 +s 1s ) -s 𝑧 ) )
13 12 eleq1d ⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( ( 𝑥 -s 𝑧 ) ∈ ℕ0s ↔ ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ) )
14 11 13 imbi12d ⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( ( 𝑧 ≤s 𝑥 → ( 𝑥 -s 𝑧 ) ∈ ℕ0s ) ↔ ( 𝑧 ≤s ( 𝑦 +s 1s ) → ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ) ) )
15 14 ralbidv ⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s 𝑥 → ( 𝑥 -s 𝑧 ) ∈ ℕ0s ) ↔ ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s ( 𝑦 +s 1s ) → ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ) ) )
16 breq2 ⊢ ( 𝑥 = 𝑁 → ( 𝑧 ≤s 𝑥 ↔ 𝑧 ≤s 𝑁 ) )
17 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 -s 𝑧 ) = ( 𝑁 -s 𝑧 ) )
18 17 eleq1d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 -s 𝑧 ) ∈ ℕ0s ↔ ( 𝑁 -s 𝑧 ) ∈ ℕ0s ) )
19 16 18 imbi12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑧 ≤s 𝑥 → ( 𝑥 -s 𝑧 ) ∈ ℕ0s ) ↔ ( 𝑧 ≤s 𝑁 → ( 𝑁 -s 𝑧 ) ∈ ℕ0s ) ) )
20 19 ralbidv ⊢ ( 𝑥 = 𝑁 → ( ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s 𝑥 → ( 𝑥 -s 𝑧 ) ∈ ℕ0s ) ↔ ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s 𝑁 → ( 𝑁 -s 𝑧 ) ∈ ℕ0s ) ) )
21 n0sge0 ⊢ ( 𝑧 ∈ ℕ0s → 0s ≤s 𝑧 )
22 21 biantrud ⊢ ( 𝑧 ∈ ℕ0s → ( 𝑧 ≤s 0s ↔ ( 𝑧 ≤s 0s ∧ 0s ≤s 𝑧 ) ) )
23 n0sno ⊢ ( 𝑧 ∈ ℕ0s → 𝑧 ∈ No )
24 0sno ⊢ 0s ∈ No
25 sletri3 ⊢ ( ( 𝑧 ∈ No ∧ 0s ∈ No ) → ( 𝑧 = 0s ↔ ( 𝑧 ≤s 0s ∧ 0s ≤s 𝑧 ) ) )
26 23 24 25 sylancl ⊢ ( 𝑧 ∈ ℕ0s → ( 𝑧 = 0s ↔ ( 𝑧 ≤s 0s ∧ 0s ≤s 𝑧 ) ) )
27 22 26 bitr4d ⊢ ( 𝑧 ∈ ℕ0s → ( 𝑧 ≤s 0s ↔ 𝑧 = 0s ) )
28 oveq2 ⊢ ( 𝑧 = 0s → ( 0s -s 𝑧 ) = ( 0s -s 0s ) )
29 subsid ⊢ ( 0s ∈ No → ( 0s -s 0s ) = 0s )
30 24 29 ax-mp ⊢ ( 0s -s 0s ) = 0s
31 0n0s ⊢ 0s ∈ ℕ0s
32 30 31 eqeltri ⊢ ( 0s -s 0s ) ∈ ℕ0s
33 28 32 eqeltrdi ⊢ ( 𝑧 = 0s → ( 0s -s 𝑧 ) ∈ ℕ0s )
34 27 33 biimtrdi ⊢ ( 𝑧 ∈ ℕ0s → ( 𝑧 ≤s 0s → ( 0s -s 𝑧 ) ∈ ℕ0s ) )
35 34 rgen ⊢ ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s 0s → ( 0s -s 𝑧 ) ∈ ℕ0s )
36 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ≤s 𝑦 ↔ 𝑥 ≤s 𝑦 ) )
37 oveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑦 -s 𝑧 ) = ( 𝑦 -s 𝑥 ) )
38 37 eleq1d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 -s 𝑧 ) ∈ ℕ0s ↔ ( 𝑦 -s 𝑥 ) ∈ ℕ0s ) )
39 36 38 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ≤s 𝑦 → ( 𝑦 -s 𝑧 ) ∈ ℕ0s ) ↔ ( 𝑥 ≤s 𝑦 → ( 𝑦 -s 𝑥 ) ∈ ℕ0s ) ) )
40 39 cbvralvw ⊢ ( ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s 𝑦 → ( 𝑦 -s 𝑧 ) ∈ ℕ0s ) ↔ ∀ 𝑥 ∈ ℕ0s ( 𝑥 ≤s 𝑦 → ( 𝑦 -s 𝑥 ) ∈ ℕ0s ) )
41 n0sno ⊢ ( 𝑦 ∈ ℕ0s → 𝑦 ∈ No )
42 peano2no ⊢ ( 𝑦 ∈ No → ( 𝑦 +s 1s ) ∈ No )
43 subsid1 ⊢ ( ( 𝑦 +s 1s ) ∈ No → ( ( 𝑦 +s 1s ) -s 0s ) = ( 𝑦 +s 1s ) )
44 41 42 43 3syl ⊢ ( 𝑦 ∈ ℕ0s → ( ( 𝑦 +s 1s ) -s 0s ) = ( 𝑦 +s 1s ) )
45 peano2n0s ⊢ ( 𝑦 ∈ ℕ0s → ( 𝑦 +s 1s ) ∈ ℕ0s )
46 44 45 eqeltrd ⊢ ( 𝑦 ∈ ℕ0s → ( ( 𝑦 +s 1s ) -s 0s ) ∈ ℕ0s )
47 oveq2 ⊢ ( 𝑧 = 0s → ( ( 𝑦 +s 1s ) -s 𝑧 ) = ( ( 𝑦 +s 1s ) -s 0s ) )
48 47 eleq1d ⊢ ( 𝑧 = 0s → ( ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ↔ ( ( 𝑦 +s 1s ) -s 0s ) ∈ ℕ0s ) )
49 46 48 syl5ibrcom ⊢ ( 𝑦 ∈ ℕ0s → ( 𝑧 = 0s → ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ) )
50 49 2a1dd ⊢ ( 𝑦 ∈ ℕ0s → ( 𝑧 = 0s → ( ∀ 𝑥 ∈ ℕ0s ( 𝑥 ≤s 𝑦 → ( 𝑦 -s 𝑥 ) ∈ ℕ0s ) → ( 𝑧 ≤s ( 𝑦 +s 1s ) → ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ) ) ) )
51 50 adantr ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → ( 𝑧 = 0s → ( ∀ 𝑥 ∈ ℕ0s ( 𝑥 ≤s 𝑦 → ( 𝑦 -s 𝑥 ) ∈ ℕ0s ) → ( 𝑧 ≤s ( 𝑦 +s 1s ) → ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ) ) ) )
52 breq1 ⊢ ( 𝑥 = ( 𝑧 -s 1s ) → ( 𝑥 ≤s 𝑦 ↔ ( 𝑧 -s 1s ) ≤s 𝑦 ) )
53 oveq2 ⊢ ( 𝑥 = ( 𝑧 -s 1s ) → ( 𝑦 -s 𝑥 ) = ( 𝑦 -s ( 𝑧 -s 1s ) ) )
54 53 eleq1d ⊢ ( 𝑥 = ( 𝑧 -s 1s ) → ( ( 𝑦 -s 𝑥 ) ∈ ℕ0s ↔ ( 𝑦 -s ( 𝑧 -s 1s ) ) ∈ ℕ0s ) )
55 52 54 imbi12d ⊢ ( 𝑥 = ( 𝑧 -s 1s ) → ( ( 𝑥 ≤s 𝑦 → ( 𝑦 -s 𝑥 ) ∈ ℕ0s ) ↔ ( ( 𝑧 -s 1s ) ≤s 𝑦 → ( 𝑦 -s ( 𝑧 -s 1s ) ) ∈ ℕ0s ) ) )
56 55 rspcv ⊢ ( ( 𝑧 -s 1s ) ∈ ℕ0s → ( ∀ 𝑥 ∈ ℕ0s ( 𝑥 ≤s 𝑦 → ( 𝑦 -s 𝑥 ) ∈ ℕ0s ) → ( ( 𝑧 -s 1s ) ≤s 𝑦 → ( 𝑦 -s ( 𝑧 -s 1s ) ) ∈ ℕ0s ) ) )
57 23 adantl ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → 𝑧 ∈ No )
58 1sno ⊢ 1s ∈ No
59 58 a1i ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → 1s ∈ No )
60 41 adantr ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → 𝑦 ∈ No )
61 57 59 60 slesubaddd ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → ( ( 𝑧 -s 1s ) ≤s 𝑦 ↔ 𝑧 ≤s ( 𝑦 +s 1s ) ) )
62 60 57 59 subsubs2d ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → ( 𝑦 -s ( 𝑧 -s 1s ) ) = ( 𝑦 +s ( 1s -s 𝑧 ) ) )
63 60 59 57 addsubsassd ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → ( ( 𝑦 +s 1s ) -s 𝑧 ) = ( 𝑦 +s ( 1s -s 𝑧 ) ) )
64 62 63 eqtr4d ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → ( 𝑦 -s ( 𝑧 -s 1s ) ) = ( ( 𝑦 +s 1s ) -s 𝑧 ) )
65 64 eleq1d ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → ( ( 𝑦 -s ( 𝑧 -s 1s ) ) ∈ ℕ0s ↔ ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ) )
66 61 65 imbi12d ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → ( ( ( 𝑧 -s 1s ) ≤s 𝑦 → ( 𝑦 -s ( 𝑧 -s 1s ) ) ∈ ℕ0s ) ↔ ( 𝑧 ≤s ( 𝑦 +s 1s ) → ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ) ) )
67 66 biimpd ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → ( ( ( 𝑧 -s 1s ) ≤s 𝑦 → ( 𝑦 -s ( 𝑧 -s 1s ) ) ∈ ℕ0s ) → ( 𝑧 ≤s ( 𝑦 +s 1s ) → ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ) ) )
68 56 67 syl9r ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → ( ( 𝑧 -s 1s ) ∈ ℕ0s → ( ∀ 𝑥 ∈ ℕ0s ( 𝑥 ≤s 𝑦 → ( 𝑦 -s 𝑥 ) ∈ ℕ0s ) → ( 𝑧 ≤s ( 𝑦 +s 1s ) → ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ) ) ) )
69 n0s0m1 ⊢ ( 𝑧 ∈ ℕ0s → ( 𝑧 = 0s ∨ ( 𝑧 -s 1s ) ∈ ℕ0s ) )
70 69 adantl ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → ( 𝑧 = 0s ∨ ( 𝑧 -s 1s ) ∈ ℕ0s ) )
71 51 68 70 mpjaod ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝑧 ∈ ℕ0s ) → ( ∀ 𝑥 ∈ ℕ0s ( 𝑥 ≤s 𝑦 → ( 𝑦 -s 𝑥 ) ∈ ℕ0s ) → ( 𝑧 ≤s ( 𝑦 +s 1s ) → ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ) ) )
72 71 ralrimdva ⊢ ( 𝑦 ∈ ℕ0s → ( ∀ 𝑥 ∈ ℕ0s ( 𝑥 ≤s 𝑦 → ( 𝑦 -s 𝑥 ) ∈ ℕ0s ) → ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s ( 𝑦 +s 1s ) → ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ) ) )
73 40 72 biimtrid ⊢ ( 𝑦 ∈ ℕ0s → ( ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s 𝑦 → ( 𝑦 -s 𝑧 ) ∈ ℕ0s ) → ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s ( 𝑦 +s 1s ) → ( ( 𝑦 +s 1s ) -s 𝑧 ) ∈ ℕ0s ) ) )
74 5 10 15 20 35 73 n0sind ⊢ ( 𝑁 ∈ ℕ0s → ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s 𝑁 → ( 𝑁 -s 𝑧 ) ∈ ℕ0s ) )
75 breq1 ⊢ ( 𝑧 = 𝑀 → ( 𝑧 ≤s 𝑁 ↔ 𝑀 ≤s 𝑁 ) )
76 oveq2 ⊢ ( 𝑧 = 𝑀 → ( 𝑁 -s 𝑧 ) = ( 𝑁 -s 𝑀 ) )
77 76 eleq1d ⊢ ( 𝑧 = 𝑀 → ( ( 𝑁 -s 𝑧 ) ∈ ℕ0s ↔ ( 𝑁 -s 𝑀 ) ∈ ℕ0s ) )
78 75 77 imbi12d ⊢ ( 𝑧 = 𝑀 → ( ( 𝑧 ≤s 𝑁 → ( 𝑁 -s 𝑧 ) ∈ ℕ0s ) ↔ ( 𝑀 ≤s 𝑁 → ( 𝑁 -s 𝑀 ) ∈ ℕ0s ) ) )
79 78 rspcva ⊢ ( ( 𝑀 ∈ ℕ0s ∧ ∀ 𝑧 ∈ ℕ0s ( 𝑧 ≤s 𝑁 → ( 𝑁 -s 𝑧 ) ∈ ℕ0s ) ) → ( 𝑀 ≤s 𝑁 → ( 𝑁 -s 𝑀 ) ∈ ℕ0s ) )
80 74 79 sylan2 ⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 ≤s 𝑁 → ( 𝑁 -s 𝑀 ) ∈ ℕ0s ) )
81 n0sge0 ⊢ ( ( 𝑁 -s 𝑀 ) ∈ ℕ0s → 0s ≤s ( 𝑁 -s 𝑀 ) )
82 n0sno ⊢ ( 𝑁 ∈ ℕ0s → 𝑁 ∈ No )
83 82 adantl ⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 𝑁 ∈ No )
84 n0sno ⊢ ( 𝑀 ∈ ℕ0s → 𝑀 ∈ No )
85 84 adantr ⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 𝑀 ∈ No )
86 83 85 subsge0d ⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 0s ≤s ( 𝑁 -s 𝑀 ) ↔ 𝑀 ≤s 𝑁 ) )
87 81 86 imbitrid ⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( ( 𝑁 -s 𝑀 ) ∈ ℕ0s → 𝑀 ≤s 𝑁 ) )
88 80 87 impbid ⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 ≤s 𝑁 ↔ ( 𝑁 -s 𝑀 ) ∈ ℕ0s ) )