| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | halfcut.5 | . . . . . 6
⊢ 𝐶 = ({𝐴} |s {𝐵}) | 
| 2 |  | halfcut.1 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈  No
) | 
| 3 |  | halfcut.2 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈  No
) | 
| 4 |  | halfcut.3 | . . . . . . . 8
⊢ (𝜑 → 𝐴 <s 𝐵) | 
| 5 | 2, 3, 4 | ssltsn 27837 | . . . . . . 7
⊢ (𝜑 → {𝐴} <<s {𝐵}) | 
| 6 | 5 | scutcld 27848 | . . . . . 6
⊢ (𝜑 → ({𝐴} |s {𝐵}) ∈  No
) | 
| 7 | 1, 6 | eqeltrid 2845 | . . . . 5
⊢ (𝜑 → 𝐶 ∈  No
) | 
| 8 |  | no2times 28401 | . . . . 5
⊢ (𝐶 ∈ 
No  → (2s ·s 𝐶) = (𝐶 +s 𝐶)) | 
| 9 | 7, 8 | syl 17 | . . . 4
⊢ (𝜑 → (2s
·s 𝐶) =
(𝐶 +s 𝐶)) | 
| 10 | 1 | a1i 11 | . . . . 5
⊢ (𝜑 → 𝐶 = ({𝐴} |s {𝐵})) | 
| 11 | 5, 5, 10, 10 | addsunif 28035 | . . . 4
⊢ (𝜑 → (𝐶 +s 𝐶) = (({𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝑦 +s 𝐶)} ∪ {𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝐶 +s 𝑦)}) |s ({𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝑦 +s 𝐶)} ∪ {𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝐶 +s 𝑦)}))) | 
| 12 |  | oveq1 7438 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝐴 → (𝑦 +s 𝐶) = (𝐴 +s 𝐶)) | 
| 13 | 12 | eqeq2d 2748 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → (𝑥 = (𝑦 +s 𝐶) ↔ 𝑥 = (𝐴 +s 𝐶))) | 
| 14 | 13 | rexsng 4676 | . . . . . . . . . . 11
⊢ (𝐴 ∈ 
No  → (∃𝑦
∈ {𝐴}𝑥 = (𝑦 +s 𝐶) ↔ 𝑥 = (𝐴 +s 𝐶))) | 
| 15 | 2, 14 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (∃𝑦 ∈ {𝐴}𝑥 = (𝑦 +s 𝐶) ↔ 𝑥 = (𝐴 +s 𝐶))) | 
| 16 | 15 | abbidv 2808 | . . . . . . . . 9
⊢ (𝜑 → {𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝑦 +s 𝐶)} = {𝑥 ∣ 𝑥 = (𝐴 +s 𝐶)}) | 
| 17 |  | df-sn 4627 | . . . . . . . . 9
⊢ {(𝐴 +s 𝐶)} = {𝑥 ∣ 𝑥 = (𝐴 +s 𝐶)} | 
| 18 | 16, 17 | eqtr4di 2795 | . . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝑦 +s 𝐶)} = {(𝐴 +s 𝐶)}) | 
| 19 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝐴 → (𝐶 +s 𝑦) = (𝐶 +s 𝐴)) | 
| 20 | 19 | eqeq2d 2748 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝐴 → (𝑥 = (𝐶 +s 𝑦) ↔ 𝑥 = (𝐶 +s 𝐴))) | 
| 21 | 20 | rexsng 4676 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ 
No  → (∃𝑦
∈ {𝐴}𝑥 = (𝐶 +s 𝑦) ↔ 𝑥 = (𝐶 +s 𝐴))) | 
| 22 | 2, 21 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (∃𝑦 ∈ {𝐴}𝑥 = (𝐶 +s 𝑦) ↔ 𝑥 = (𝐶 +s 𝐴))) | 
| 23 | 7, 2 | addscomd 28000 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 +s 𝐴) = (𝐴 +s 𝐶)) | 
| 24 | 23 | eqeq2d 2748 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑥 = (𝐶 +s 𝐴) ↔ 𝑥 = (𝐴 +s 𝐶))) | 
| 25 | 22, 24 | bitrd 279 | . . . . . . . . . 10
⊢ (𝜑 → (∃𝑦 ∈ {𝐴}𝑥 = (𝐶 +s 𝑦) ↔ 𝑥 = (𝐴 +s 𝐶))) | 
| 26 | 25 | abbidv 2808 | . . . . . . . . 9
⊢ (𝜑 → {𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝐶 +s 𝑦)} = {𝑥 ∣ 𝑥 = (𝐴 +s 𝐶)}) | 
| 27 | 26, 17 | eqtr4di 2795 | . . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝐶 +s 𝑦)} = {(𝐴 +s 𝐶)}) | 
| 28 | 18, 27 | uneq12d 4169 | . . . . . . 7
⊢ (𝜑 → ({𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝑦 +s 𝐶)} ∪ {𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝐶 +s 𝑦)}) = ({(𝐴 +s 𝐶)} ∪ {(𝐴 +s 𝐶)})) | 
| 29 |  | unidm 4157 | . . . . . . 7
⊢ ({(𝐴 +s 𝐶)} ∪ {(𝐴 +s 𝐶)}) = {(𝐴 +s 𝐶)} | 
| 30 | 28, 29 | eqtrdi 2793 | . . . . . 6
⊢ (𝜑 → ({𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝑦 +s 𝐶)} ∪ {𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝐶 +s 𝑦)}) = {(𝐴 +s 𝐶)}) | 
| 31 |  | oveq1 7438 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → (𝑦 +s 𝐶) = (𝐵 +s 𝐶)) | 
| 32 | 31 | eqeq2d 2748 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝐵 → (𝑥 = (𝑦 +s 𝐶) ↔ 𝑥 = (𝐵 +s 𝐶))) | 
| 33 | 32 | rexsng 4676 | . . . . . . . . . . 11
⊢ (𝐵 ∈ 
No  → (∃𝑦
∈ {𝐵}𝑥 = (𝑦 +s 𝐶) ↔ 𝑥 = (𝐵 +s 𝐶))) | 
| 34 | 3, 33 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (∃𝑦 ∈ {𝐵}𝑥 = (𝑦 +s 𝐶) ↔ 𝑥 = (𝐵 +s 𝐶))) | 
| 35 | 34 | abbidv 2808 | . . . . . . . . 9
⊢ (𝜑 → {𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝑦 +s 𝐶)} = {𝑥 ∣ 𝑥 = (𝐵 +s 𝐶)}) | 
| 36 |  | df-sn 4627 | . . . . . . . . 9
⊢ {(𝐵 +s 𝐶)} = {𝑥 ∣ 𝑥 = (𝐵 +s 𝐶)} | 
| 37 | 35, 36 | eqtr4di 2795 | . . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝑦 +s 𝐶)} = {(𝐵 +s 𝐶)}) | 
| 38 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝐵 → (𝐶 +s 𝑦) = (𝐶 +s 𝐵)) | 
| 39 | 38 | eqeq2d 2748 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → (𝑥 = (𝐶 +s 𝑦) ↔ 𝑥 = (𝐶 +s 𝐵))) | 
| 40 | 39 | rexsng 4676 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ 
No  → (∃𝑦
∈ {𝐵}𝑥 = (𝐶 +s 𝑦) ↔ 𝑥 = (𝐶 +s 𝐵))) | 
| 41 | 3, 40 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (∃𝑦 ∈ {𝐵}𝑥 = (𝐶 +s 𝑦) ↔ 𝑥 = (𝐶 +s 𝐵))) | 
| 42 | 7, 3 | addscomd 28000 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 +s 𝐵) = (𝐵 +s 𝐶)) | 
| 43 | 42 | eqeq2d 2748 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑥 = (𝐶 +s 𝐵) ↔ 𝑥 = (𝐵 +s 𝐶))) | 
| 44 | 41, 43 | bitrd 279 | . . . . . . . . . 10
⊢ (𝜑 → (∃𝑦 ∈ {𝐵}𝑥 = (𝐶 +s 𝑦) ↔ 𝑥 = (𝐵 +s 𝐶))) | 
| 45 | 44 | abbidv 2808 | . . . . . . . . 9
⊢ (𝜑 → {𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝐶 +s 𝑦)} = {𝑥 ∣ 𝑥 = (𝐵 +s 𝐶)}) | 
| 46 | 45, 36 | eqtr4di 2795 | . . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝐶 +s 𝑦)} = {(𝐵 +s 𝐶)}) | 
| 47 | 37, 46 | uneq12d 4169 | . . . . . . 7
⊢ (𝜑 → ({𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝑦 +s 𝐶)} ∪ {𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝐶 +s 𝑦)}) = ({(𝐵 +s 𝐶)} ∪ {(𝐵 +s 𝐶)})) | 
| 48 |  | unidm 4157 | . . . . . . 7
⊢ ({(𝐵 +s 𝐶)} ∪ {(𝐵 +s 𝐶)}) = {(𝐵 +s 𝐶)} | 
| 49 | 47, 48 | eqtrdi 2793 | . . . . . 6
⊢ (𝜑 → ({𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝑦 +s 𝐶)} ∪ {𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝐶 +s 𝑦)}) = {(𝐵 +s 𝐶)}) | 
| 50 | 30, 49 | oveq12d 7449 | . . . . 5
⊢ (𝜑 → (({𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝑦 +s 𝐶)} ∪ {𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝐶 +s 𝑦)}) |s ({𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝑦 +s 𝐶)} ∪ {𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝐶 +s 𝑦)})) = ({(𝐴 +s 𝐶)} |s {(𝐵 +s 𝐶)})) | 
| 51 |  | 2sno 28403 | . . . . . . . . 9
⊢
2s ∈  No | 
| 52 | 51 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 2s ∈  No ) | 
| 53 | 52, 2 | mulscld 28161 | . . . . . . 7
⊢ (𝜑 → (2s
·s 𝐴)
∈  No ) | 
| 54 | 52, 3 | mulscld 28161 | . . . . . . 7
⊢ (𝜑 → (2s
·s 𝐵)
∈  No ) | 
| 55 |  | 2nns 28402 | . . . . . . . . . 10
⊢
2s ∈ ℕs | 
| 56 |  | nnsgt0 28342 | . . . . . . . . . 10
⊢
(2s ∈ ℕs → 0s <s
2s) | 
| 57 | 55, 56 | mp1i 13 | . . . . . . . . 9
⊢ (𝜑 → 0s <s
2s) | 
| 58 | 2, 3, 52, 57 | sltmul2d 28198 | . . . . . . . 8
⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (2s ·s
𝐴) <s (2s
·s 𝐵))) | 
| 59 | 4, 58 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → (2s
·s 𝐴)
<s (2s ·s 𝐵)) | 
| 60 | 53, 54, 59 | ssltsn 27837 | . . . . . 6
⊢ (𝜑 → {(2s
·s 𝐴)}
<<s {(2s ·s 𝐵)}) | 
| 61 | 2, 7 | addscld 28013 | . . . . . . . 8
⊢ (𝜑 → (𝐴 +s 𝐶) ∈  No
) | 
| 62 |  | no2times 28401 | . . . . . . . . . 10
⊢ (𝐴 ∈ 
No  → (2s ·s 𝐴) = (𝐴 +s 𝐴)) | 
| 63 | 2, 62 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (2s
·s 𝐴) =
(𝐴 +s 𝐴)) | 
| 64 |  | slerflex 27808 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 
No  → 𝐴 ≤s
𝐴) | 
| 65 | 2, 64 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ≤s 𝐴) | 
| 66 |  | breq2 5147 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐴 → (𝐴 ≤s 𝑥 ↔ 𝐴 ≤s 𝐴)) | 
| 67 | 66 | rexsng 4676 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 
No  → (∃𝑥
∈ {𝐴}𝐴 ≤s 𝑥 ↔ 𝐴 ≤s 𝐴)) | 
| 68 | 2, 67 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (∃𝑥 ∈ {𝐴}𝐴 ≤s 𝑥 ↔ 𝐴 ≤s 𝐴)) | 
| 69 | 65, 68 | mpbird 257 | . . . . . . . . . . . 12
⊢ (𝜑 → ∃𝑥 ∈ {𝐴}𝐴 ≤s 𝑥) | 
| 70 | 69 | orcd 874 | . . . . . . . . . . 11
⊢ (𝜑 → (∃𝑥 ∈ {𝐴}𝐴 ≤s 𝑥 ∨ ∃𝑦 ∈ ( R ‘𝐴)𝑦 ≤s 𝐶)) | 
| 71 |  | lltropt 27911 | . . . . . . . . . . . . 13
⊢ ( L
‘𝐴) <<s ( R
‘𝐴) | 
| 72 | 71 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → ( L ‘𝐴) <<s ( R ‘𝐴)) | 
| 73 |  | lrcut 27941 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 
No  → (( L ‘𝐴) |s ( R ‘𝐴)) = 𝐴) | 
| 74 | 2, 73 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (( L ‘𝐴) |s ( R ‘𝐴)) = 𝐴) | 
| 75 | 74 | eqcomd 2743 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 = (( L ‘𝐴) |s ( R ‘𝐴))) | 
| 76 |  | sltrec 27865 | . . . . . . . . . . . 12
⊢ (((( L
‘𝐴) <<s ( R
‘𝐴) ∧ {𝐴} <<s {𝐵}) ∧ (𝐴 = (( L ‘𝐴) |s ( R ‘𝐴)) ∧ 𝐶 = ({𝐴} |s {𝐵}))) → (𝐴 <s 𝐶 ↔ (∃𝑥 ∈ {𝐴}𝐴 ≤s 𝑥 ∨ ∃𝑦 ∈ ( R ‘𝐴)𝑦 ≤s 𝐶))) | 
| 77 | 72, 5, 75, 10, 76 | syl22anc 839 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 <s 𝐶 ↔ (∃𝑥 ∈ {𝐴}𝐴 ≤s 𝑥 ∨ ∃𝑦 ∈ ( R ‘𝐴)𝑦 ≤s 𝐶))) | 
| 78 | 70, 77 | mpbird 257 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 <s 𝐶) | 
| 79 | 2, 7, 2 | sltadd2d 28030 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 <s 𝐶 ↔ (𝐴 +s 𝐴) <s (𝐴 +s 𝐶))) | 
| 80 | 78, 79 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 +s 𝐴) <s (𝐴 +s 𝐶)) | 
| 81 | 63, 80 | eqbrtrd 5165 | . . . . . . . 8
⊢ (𝜑 → (2s
·s 𝐴)
<s (𝐴 +s
𝐶)) | 
| 82 | 53, 61, 81 | sltled 27814 | . . . . . . 7
⊢ (𝜑 → (2s
·s 𝐴)
≤s (𝐴 +s
𝐶)) | 
| 83 |  | ovex 7464 | . . . . . . . . . 10
⊢ (𝐴 +s 𝐶) ∈ V | 
| 84 |  | breq2 5147 | . . . . . . . . . 10
⊢ (𝑦 = (𝐴 +s 𝐶) → (𝑥 ≤s 𝑦 ↔ 𝑥 ≤s (𝐴 +s 𝐶))) | 
| 85 | 83, 84 | rexsn 4682 | . . . . . . . . 9
⊢
(∃𝑦 ∈
{(𝐴 +s 𝐶)}𝑥 ≤s 𝑦 ↔ 𝑥 ≤s (𝐴 +s 𝐶)) | 
| 86 | 85 | ralbii 3093 | . . . . . . . 8
⊢
(∀𝑥 ∈
{(2s ·s 𝐴)}∃𝑦 ∈ {(𝐴 +s 𝐶)}𝑥 ≤s 𝑦 ↔ ∀𝑥 ∈ {(2s ·s
𝐴)}𝑥 ≤s (𝐴 +s 𝐶)) | 
| 87 |  | ovex 7464 | . . . . . . . . 9
⊢
(2s ·s 𝐴) ∈ V | 
| 88 |  | breq1 5146 | . . . . . . . . 9
⊢ (𝑥 = (2s
·s 𝐴)
→ (𝑥 ≤s (𝐴 +s 𝐶) ↔ (2s ·s
𝐴) ≤s (𝐴 +s 𝐶))) | 
| 89 | 87, 88 | ralsn 4681 | . . . . . . . 8
⊢
(∀𝑥 ∈
{(2s ·s 𝐴)}𝑥 ≤s (𝐴 +s 𝐶) ↔ (2s ·s
𝐴) ≤s (𝐴 +s 𝐶)) | 
| 90 | 86, 89 | bitri 275 | . . . . . . 7
⊢
(∀𝑥 ∈
{(2s ·s 𝐴)}∃𝑦 ∈ {(𝐴 +s 𝐶)}𝑥 ≤s 𝑦 ↔ (2s ·s
𝐴) ≤s (𝐴 +s 𝐶)) | 
| 91 | 82, 90 | sylibr 234 | . . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ {(2s ·s
𝐴)}∃𝑦 ∈ {(𝐴 +s 𝐶)}𝑥 ≤s 𝑦) | 
| 92 | 3, 7 | addscld 28013 | . . . . . . . 8
⊢ (𝜑 → (𝐵 +s 𝐶) ∈  No
) | 
| 93 |  | slerflex 27808 | . . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 
No  → 𝐵 ≤s
𝐵) | 
| 94 | 3, 93 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ≤s 𝐵) | 
| 95 |  | breq1 5146 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝐵 → (𝑦 ≤s 𝐵 ↔ 𝐵 ≤s 𝐵)) | 
| 96 | 95 | rexsng 4676 | . . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 
No  → (∃𝑦
∈ {𝐵}𝑦 ≤s 𝐵 ↔ 𝐵 ≤s 𝐵)) | 
| 97 | 3, 96 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (∃𝑦 ∈ {𝐵}𝑦 ≤s 𝐵 ↔ 𝐵 ≤s 𝐵)) | 
| 98 | 94, 97 | mpbird 257 | . . . . . . . . . . . 12
⊢ (𝜑 → ∃𝑦 ∈ {𝐵}𝑦 ≤s 𝐵) | 
| 99 | 98 | olcd 875 | . . . . . . . . . . 11
⊢ (𝜑 → (∃𝑥 ∈ ( L ‘𝐵)𝐶 ≤s 𝑥 ∨ ∃𝑦 ∈ {𝐵}𝑦 ≤s 𝐵)) | 
| 100 |  | lltropt 27911 | . . . . . . . . . . . . 13
⊢ ( L
‘𝐵) <<s ( R
‘𝐵) | 
| 101 | 100 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → ( L ‘𝐵) <<s ( R ‘𝐵)) | 
| 102 |  | lrcut 27941 | . . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 
No  → (( L ‘𝐵) |s ( R ‘𝐵)) = 𝐵) | 
| 103 | 3, 102 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (( L ‘𝐵) |s ( R ‘𝐵)) = 𝐵) | 
| 104 | 103 | eqcomd 2743 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 = (( L ‘𝐵) |s ( R ‘𝐵))) | 
| 105 |  | sltrec 27865 | . . . . . . . . . . . 12
⊢ ((({𝐴} <<s {𝐵} ∧ ( L ‘𝐵) <<s ( R ‘𝐵)) ∧ (𝐶 = ({𝐴} |s {𝐵}) ∧ 𝐵 = (( L ‘𝐵) |s ( R ‘𝐵)))) → (𝐶 <s 𝐵 ↔ (∃𝑥 ∈ ( L ‘𝐵)𝐶 ≤s 𝑥 ∨ ∃𝑦 ∈ {𝐵}𝑦 ≤s 𝐵))) | 
| 106 | 5, 101, 10, 104, 105 | syl22anc 839 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐶 <s 𝐵 ↔ (∃𝑥 ∈ ( L ‘𝐵)𝐶 ≤s 𝑥 ∨ ∃𝑦 ∈ {𝐵}𝑦 ≤s 𝐵))) | 
| 107 | 99, 106 | mpbird 257 | . . . . . . . . . 10
⊢ (𝜑 → 𝐶 <s 𝐵) | 
| 108 | 7, 3, 3 | sltadd2d 28030 | . . . . . . . . . 10
⊢ (𝜑 → (𝐶 <s 𝐵 ↔ (𝐵 +s 𝐶) <s (𝐵 +s 𝐵))) | 
| 109 | 107, 108 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 +s 𝐶) <s (𝐵 +s 𝐵)) | 
| 110 |  | no2times 28401 | . . . . . . . . . 10
⊢ (𝐵 ∈ 
No  → (2s ·s 𝐵) = (𝐵 +s 𝐵)) | 
| 111 | 3, 110 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (2s
·s 𝐵) =
(𝐵 +s 𝐵)) | 
| 112 | 109, 111 | breqtrrd 5171 | . . . . . . . 8
⊢ (𝜑 → (𝐵 +s 𝐶) <s (2s ·s
𝐵)) | 
| 113 | 92, 54, 112 | sltled 27814 | . . . . . . 7
⊢ (𝜑 → (𝐵 +s 𝐶) ≤s (2s ·s
𝐵)) | 
| 114 |  | ovex 7464 | . . . . . . . . . 10
⊢ (𝐵 +s 𝐶) ∈ V | 
| 115 |  | breq1 5146 | . . . . . . . . . 10
⊢ (𝑦 = (𝐵 +s 𝐶) → (𝑦 ≤s 𝑥 ↔ (𝐵 +s 𝐶) ≤s 𝑥)) | 
| 116 | 114, 115 | rexsn 4682 | . . . . . . . . 9
⊢
(∃𝑦 ∈
{(𝐵 +s 𝐶)}𝑦 ≤s 𝑥 ↔ (𝐵 +s 𝐶) ≤s 𝑥) | 
| 117 | 116 | ralbii 3093 | . . . . . . . 8
⊢
(∀𝑥 ∈
{(2s ·s 𝐵)}∃𝑦 ∈ {(𝐵 +s 𝐶)}𝑦 ≤s 𝑥 ↔ ∀𝑥 ∈ {(2s ·s
𝐵)} (𝐵 +s 𝐶) ≤s 𝑥) | 
| 118 |  | ovex 7464 | . . . . . . . . 9
⊢
(2s ·s 𝐵) ∈ V | 
| 119 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑥 = (2s
·s 𝐵)
→ ((𝐵 +s
𝐶) ≤s 𝑥 ↔ (𝐵 +s 𝐶) ≤s (2s ·s
𝐵))) | 
| 120 | 118, 119 | ralsn 4681 | . . . . . . . 8
⊢
(∀𝑥 ∈
{(2s ·s 𝐵)} (𝐵 +s 𝐶) ≤s 𝑥 ↔ (𝐵 +s 𝐶) ≤s (2s ·s
𝐵)) | 
| 121 | 117, 120 | bitri 275 | . . . . . . 7
⊢
(∀𝑥 ∈
{(2s ·s 𝐵)}∃𝑦 ∈ {(𝐵 +s 𝐶)}𝑦 ≤s 𝑥 ↔ (𝐵 +s 𝐶) ≤s (2s ·s
𝐵)) | 
| 122 | 113, 121 | sylibr 234 | . . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ {(2s ·s
𝐵)}∃𝑦 ∈ {(𝐵 +s 𝐶)}𝑦 ≤s 𝑥) | 
| 123 | 2, 3 | addscld 28013 | . . . . . . . 8
⊢ (𝜑 → (𝐴 +s 𝐵) ∈  No
) | 
| 124 | 7, 3, 2 | sltadd2d 28030 | . . . . . . . . 9
⊢ (𝜑 → (𝐶 <s 𝐵 ↔ (𝐴 +s 𝐶) <s (𝐴 +s 𝐵))) | 
| 125 | 107, 124 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → (𝐴 +s 𝐶) <s (𝐴 +s 𝐵)) | 
| 126 | 61, 123, 125 | ssltsn 27837 | . . . . . . 7
⊢ (𝜑 → {(𝐴 +s 𝐶)} <<s {(𝐴 +s 𝐵)}) | 
| 127 |  | halfcut.4 | . . . . . . . 8
⊢ (𝜑 → ({(2s
·s 𝐴)} |s
{(2s ·s 𝐵)}) = (𝐴 +s 𝐵)) | 
| 128 | 127 | sneqd 4638 | . . . . . . 7
⊢ (𝜑 → {({(2s
·s 𝐴)} |s
{(2s ·s 𝐵)})} = {(𝐴 +s 𝐵)}) | 
| 129 | 126, 128 | breqtrrd 5171 | . . . . . 6
⊢ (𝜑 → {(𝐴 +s 𝐶)} <<s {({(2s
·s 𝐴)} |s
{(2s ·s 𝐵)})}) | 
| 130 | 2, 3 | addscomd 28000 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 +s 𝐵) = (𝐵 +s 𝐴)) | 
| 131 | 2, 7, 3 | sltadd2d 28030 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 <s 𝐶 ↔ (𝐵 +s 𝐴) <s (𝐵 +s 𝐶))) | 
| 132 | 78, 131 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 +s 𝐴) <s (𝐵 +s 𝐶)) | 
| 133 | 130, 132 | eqbrtrd 5165 | . . . . . . . 8
⊢ (𝜑 → (𝐴 +s 𝐵) <s (𝐵 +s 𝐶)) | 
| 134 | 123, 92, 133 | ssltsn 27837 | . . . . . . 7
⊢ (𝜑 → {(𝐴 +s 𝐵)} <<s {(𝐵 +s 𝐶)}) | 
| 135 | 128, 134 | eqbrtrd 5165 | . . . . . 6
⊢ (𝜑 → {({(2s
·s 𝐴)} |s
{(2s ·s 𝐵)})} <<s {(𝐵 +s 𝐶)}) | 
| 136 | 60, 91, 122, 129, 135 | cofcut1d 27955 | . . . . 5
⊢ (𝜑 → ({(2s
·s 𝐴)} |s
{(2s ·s 𝐵)}) = ({(𝐴 +s 𝐶)} |s {(𝐵 +s 𝐶)})) | 
| 137 | 50, 136, 127 | 3eqtr2d 2783 | . . . 4
⊢ (𝜑 → (({𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝑦 +s 𝐶)} ∪ {𝑥 ∣ ∃𝑦 ∈ {𝐴}𝑥 = (𝐶 +s 𝑦)}) |s ({𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝑦 +s 𝐶)} ∪ {𝑥 ∣ ∃𝑦 ∈ {𝐵}𝑥 = (𝐶 +s 𝑦)})) = (𝐴 +s 𝐵)) | 
| 138 | 9, 11, 137 | 3eqtrd 2781 | . . 3
⊢ (𝜑 → (2s
·s 𝐶) =
(𝐴 +s 𝐵)) | 
| 139 |  | 2ne0s 28404 | . . . . 5
⊢
2s ≠ 0s | 
| 140 | 139 | a1i 11 | . . . 4
⊢ (𝜑 → 2s ≠
0s ) | 
| 141 | 123, 7, 52, 140 | divsmuld 28246 | . . 3
⊢ (𝜑 → (((𝐴 +s 𝐵) /su 2s) = 𝐶 ↔ (2s
·s 𝐶) =
(𝐴 +s 𝐵))) | 
| 142 | 138, 141 | mpbird 257 | . 2
⊢ (𝜑 → ((𝐴 +s 𝐵) /su 2s) = 𝐶) | 
| 143 | 142 | eqcomd 2743 | 1
⊢ (𝜑 → 𝐶 = ((𝐴 +s 𝐵) /su
2s)) |