Metamath Proof Explorer

Theorem recut

Description: The cut involved in defining surreal reals is a genuine cut. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Assertion recut ⊢ A ∈ No → x | ∃ n ∈ ℕ s x = A - s 1 s / su n ≪ s x | ∃ n ∈ ℕ s x = A + s 1 s / su n

Proof

Step Hyp Ref Expression
1 nnsex ⊢ ℕ s ∈ V
2 1 abrexex ⊢ x | ∃ n ∈ ℕ s x = A - s 1 s / su n ∈ V
3 2 a1i ⊢ A ∈ No → x | ∃ n ∈ ℕ s x = A - s 1 s / su n ∈ V
4 1 abrexex ⊢ x | ∃ n ∈ ℕ s x = A + s 1 s / su n ∈ V
5 4 a1i ⊢ A ∈ No → x | ∃ n ∈ ℕ s x = A + s 1 s / su n ∈ V
6 1sno ⊢ 1 s ∈ No
7 6 a1i ⊢ n ∈ ℕ s → 1 s ∈ No
8 nnsno ⊢ n ∈ ℕ s → n ∈ No
9 nnne0s ⊢ n ∈ ℕ s → n ≠ 0 s
10 7 8 9 divscld ⊢ n ∈ ℕ s → 1 s / su n ∈ No
11 subscl ⊢ A ∈ No ∧ 1 s / su n ∈ No → A - s 1 s / su n ∈ No
12 10 11 sylan2 ⊢ A ∈ No ∧ n ∈ ℕ s → A - s 1 s / su n ∈ No
13 eleq1 ⊢ x = A - s 1 s / su n → x ∈ No ↔ A - s 1 s / su n ∈ No
14 12 13 syl5ibrcom ⊢ A ∈ No ∧ n ∈ ℕ s → x = A - s 1 s / su n → x ∈ No
15 14 rexlimdva ⊢ A ∈ No → ∃ n ∈ ℕ s x = A - s 1 s / su n → x ∈ No
16 15 abssdv ⊢ A ∈ No → x | ∃ n ∈ ℕ s x = A - s 1 s / su n ⊆ No
17 addscl ⊢ A ∈ No ∧ 1 s / su n ∈ No → A + s 1 s / su n ∈ No
18 10 17 sylan2 ⊢ A ∈ No ∧ n ∈ ℕ s → A + s 1 s / su n ∈ No
19 eleq1 ⊢ x = A + s 1 s / su n → x ∈ No ↔ A + s 1 s / su n ∈ No
20 18 19 syl5ibrcom ⊢ A ∈ No ∧ n ∈ ℕ s → x = A + s 1 s / su n → x ∈ No
21 20 rexlimdva ⊢ A ∈ No → ∃ n ∈ ℕ s x = A + s 1 s / su n → x ∈ No
22 21 abssdv ⊢ A ∈ No → x | ∃ n ∈ ℕ s x = A + s 1 s / su n ⊆ No
23 vex ⊢ y ∈ V
24 eqeq1 ⊢ x = y → x = A - s 1 s / su n ↔ y = A - s 1 s / su n
25 24 rexbidv ⊢ x = y → ∃ n ∈ ℕ s x = A - s 1 s / su n ↔ ∃ n ∈ ℕ s y = A - s 1 s / su n
26 23 25 elab ⊢ y ∈ x | ∃ n ∈ ℕ s x = A - s 1 s / su n ↔ ∃ n ∈ ℕ s y = A - s 1 s / su n
27 vex ⊢ z ∈ V
28 eqeq1 ⊢ x = z → x = A + s 1 s / su n ↔ z = A + s 1 s / su n
29 28 rexbidv ⊢ x = z → ∃ n ∈ ℕ s x = A + s 1 s / su n ↔ ∃ n ∈ ℕ s z = A + s 1 s / su n
30 oveq2 ⊢ n = m → 1 s / su n = 1 s / su m
31 30 oveq2d ⊢ n = m → A + s 1 s / su n = A + s 1 s / su m
32 31 eqeq2d ⊢ n = m → z = A + s 1 s / su n ↔ z = A + s 1 s / su m
33 32 cbvrexvw ⊢ ∃ n ∈ ℕ s z = A + s 1 s / su n ↔ ∃ m ∈ ℕ s z = A + s 1 s / su m
34 29 33 bitrdi ⊢ x = z → ∃ n ∈ ℕ s x = A + s 1 s / su n ↔ ∃ m ∈ ℕ s z = A + s 1 s / su m
35 27 34 elab ⊢ z ∈ x | ∃ n ∈ ℕ s x = A + s 1 s / su n ↔ ∃ m ∈ ℕ s z = A + s 1 s / su m
36 26 35 anbi12i ⊢ y ∈ x | ∃ n ∈ ℕ s x = A - s 1 s / su n ∧ z ∈ x | ∃ n ∈ ℕ s x = A + s 1 s / su n ↔ ∃ n ∈ ℕ s y = A - s 1 s / su n ∧ ∃ m ∈ ℕ s z = A + s 1 s / su m
37 reeanv ⊢ ∃ n ∈ ℕ s ∃ m ∈ ℕ s y = A - s 1 s / su n ∧ z = A + s 1 s / su m ↔ ∃ n ∈ ℕ s y = A - s 1 s / su n ∧ ∃ m ∈ ℕ s z = A + s 1 s / su m
38 36 37 bitr4i ⊢ y ∈ x | ∃ n ∈ ℕ s x = A - s 1 s / su n ∧ z ∈ x | ∃ n ∈ ℕ s x = A + s 1 s / su n ↔ ∃ n ∈ ℕ s ∃ m ∈ ℕ s y = A - s 1 s / su n ∧ z = A + s 1 s / su m
39 simpl ⊢ A ∈ No ∧ n ∈ ℕ s → A ∈ No
40 10 adantl ⊢ A ∈ No ∧ n ∈ ℕ s → 1 s / su n ∈ No
41 39 40 subsvald ⊢ A ∈ No ∧ n ∈ ℕ s → A - s 1 s / su n = A + s + s ⁡ 1 s / su n
42 41 adantrr ⊢ A ∈ No ∧ n ∈ ℕ s ∧ m ∈ ℕ s → A - s 1 s / su n = A + s + s ⁡ 1 s / su n
43 10 negscld ⊢ n ∈ ℕ s → + s ⁡ 1 s / su n ∈ No
44 43 adantr ⊢ n ∈ ℕ s ∧ m ∈ ℕ s → + s ⁡ 1 s / su n ∈ No
45 0sno ⊢ 0 s ∈ No
46 45 a1i ⊢ n ∈ ℕ s ∧ m ∈ ℕ s → 0 s ∈ No
47 6 a1i ⊢ m ∈ ℕ s → 1 s ∈ No
48 nnsno ⊢ m ∈ ℕ s → m ∈ No
49 nnne0s ⊢ m ∈ ℕ s → m ≠ 0 s
50 47 48 49 divscld ⊢ m ∈ ℕ s → 1 s / su m ∈ No
51 50 adantl ⊢ n ∈ ℕ s ∧ m ∈ ℕ s → 1 s / su m ∈ No
52 id ⊢ n ∈ ℕ s → n ∈ ℕ s
53 52 nnsrecgt0d ⊢ n ∈ ℕ s → 0 s < s 1 s / su n
54 45 a1i ⊢ n ∈ ℕ s → 0 s ∈ No
55 54 10 sltnegd ⊢ n ∈ ℕ s → 0 s < s 1 s / su n ↔ + s ⁡ 1 s / su n < s + s ⁡ 0 s
56 53 55 mpbid ⊢ n ∈ ℕ s → + s ⁡ 1 s / su n < s + s ⁡ 0 s
57 negs0s ⊢ + s ⁡ 0 s = 0 s
58 56 57 breqtrdi ⊢ n ∈ ℕ s → + s ⁡ 1 s / su n < s 0 s
59 58 adantr ⊢ n ∈ ℕ s ∧ m ∈ ℕ s → + s ⁡ 1 s / su n < s 0 s
60 id ⊢ m ∈ ℕ s → m ∈ ℕ s
61 60 nnsrecgt0d ⊢ m ∈ ℕ s → 0 s < s 1 s / su m
62 61 adantl ⊢ n ∈ ℕ s ∧ m ∈ ℕ s → 0 s < s 1 s / su m
63 44 46 51 59 62 slttrd ⊢ n ∈ ℕ s ∧ m ∈ ℕ s → + s ⁡ 1 s / su n < s 1 s / su m
64 63 adantl ⊢ A ∈ No ∧ n ∈ ℕ s ∧ m ∈ ℕ s → + s ⁡ 1 s / su n < s 1 s / su m
65 44 adantl ⊢ A ∈ No ∧ n ∈ ℕ s ∧ m ∈ ℕ s → + s ⁡ 1 s / su n ∈ No
66 50 ad2antll ⊢ A ∈ No ∧ n ∈ ℕ s ∧ m ∈ ℕ s → 1 s / su m ∈ No
67 simpl ⊢ A ∈ No ∧ n ∈ ℕ s ∧ m ∈ ℕ s → A ∈ No
68 65 66 67 sltadd2d ⊢ A ∈ No ∧ n ∈ ℕ s ∧ m ∈ ℕ s → + s ⁡ 1 s / su n < s 1 s / su m ↔ A + s + s ⁡ 1 s / su n < s A + s 1 s / su m
69 64 68 mpbid ⊢ A ∈ No ∧ n ∈ ℕ s ∧ m ∈ ℕ s → A + s + s ⁡ 1 s / su n < s A + s 1 s / su m
70 42 69 eqbrtrd ⊢ A ∈ No ∧ n ∈ ℕ s ∧ m ∈ ℕ s → A - s 1 s / su n < s A + s 1 s / su m
71 breq12 ⊢ y = A - s 1 s / su n ∧ z = A + s 1 s / su m → y < s z ↔ A - s 1 s / su n < s A + s 1 s / su m
72 70 71 syl5ibrcom ⊢ A ∈ No ∧ n ∈ ℕ s ∧ m ∈ ℕ s → y = A - s 1 s / su n ∧ z = A + s 1 s / su m → y < s z
73 72 rexlimdvva ⊢ A ∈ No → ∃ n ∈ ℕ s ∃ m ∈ ℕ s y = A - s 1 s / su n ∧ z = A + s 1 s / su m → y < s z
74 38 73 biimtrid ⊢ A ∈ No → y ∈ x | ∃ n ∈ ℕ s x = A - s 1 s / su n ∧ z ∈ x | ∃ n ∈ ℕ s x = A + s 1 s / su n → y < s z
75 74 3impib ⊢ A ∈ No ∧ y ∈ x | ∃ n ∈ ℕ s x = A - s 1 s / su n ∧ z ∈ x | ∃ n ∈ ℕ s x = A + s 1 s / su n → y < s z
76 3 5 16 22 75 ssltd ⊢ A ∈ No → x | ∃ n ∈ ℕ s x = A - s 1 s / su n ≪ s x | ∃ n ∈ ℕ s x = A + s 1 s / su n