Proof of Theorem staddi
| Step | Hyp | Ref
| Expression |
| 1 | | stle.1 |
. . . . . . 7
⊢ 𝐴 ∈
Cℋ |
| 2 | | stcl 32235 |
. . . . . . 7
⊢ (𝑆 ∈ States → (𝐴 ∈
Cℋ → (𝑆‘𝐴) ∈ ℝ)) |
| 3 | 1, 2 | mpi 20 |
. . . . . 6
⊢ (𝑆 ∈ States → (𝑆‘𝐴) ∈ ℝ) |
| 4 | | stle.2 |
. . . . . . 7
⊢ 𝐵 ∈
Cℋ |
| 5 | | stcl 32235 |
. . . . . . 7
⊢ (𝑆 ∈ States → (𝐵 ∈
Cℋ → (𝑆‘𝐵) ∈ ℝ)) |
| 6 | 4, 5 | mpi 20 |
. . . . . 6
⊢ (𝑆 ∈ States → (𝑆‘𝐵) ∈ ℝ) |
| 7 | 3, 6 | readdcld 11290 |
. . . . 5
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) + (𝑆‘𝐵)) ∈ ℝ) |
| 8 | | ltne 11358 |
. . . . . 6
⊢ ((((𝑆‘𝐴) + (𝑆‘𝐵)) ∈ ℝ ∧ ((𝑆‘𝐴) + (𝑆‘𝐵)) < 2) → 2 ≠ ((𝑆‘𝐴) + (𝑆‘𝐵))) |
| 9 | 8 | necomd 2996 |
. . . . 5
⊢ ((((𝑆‘𝐴) + (𝑆‘𝐵)) ∈ ℝ ∧ ((𝑆‘𝐴) + (𝑆‘𝐵)) < 2) → ((𝑆‘𝐴) + (𝑆‘𝐵)) ≠ 2) |
| 10 | 7, 9 | sylan 580 |
. . . 4
⊢ ((𝑆 ∈ States ∧ ((𝑆‘𝐴) + (𝑆‘𝐵)) < 2) → ((𝑆‘𝐴) + (𝑆‘𝐵)) ≠ 2) |
| 11 | 10 | ex 412 |
. . 3
⊢ (𝑆 ∈ States → (((𝑆‘𝐴) + (𝑆‘𝐵)) < 2 → ((𝑆‘𝐴) + (𝑆‘𝐵)) ≠ 2)) |
| 12 | 11 | necon2bd 2956 |
. 2
⊢ (𝑆 ∈ States → (((𝑆‘𝐴) + (𝑆‘𝐵)) = 2 → ¬ ((𝑆‘𝐴) + (𝑆‘𝐵)) < 2)) |
| 13 | | 1re 11261 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
| 14 | 13 | a1i 11 |
. . . . . . . 8
⊢ (𝑆 ∈ States → 1 ∈
ℝ) |
| 15 | | stle1 32244 |
. . . . . . . . 9
⊢ (𝑆 ∈ States → (𝐵 ∈
Cℋ → (𝑆‘𝐵) ≤ 1)) |
| 16 | 4, 15 | mpi 20 |
. . . . . . . 8
⊢ (𝑆 ∈ States → (𝑆‘𝐵) ≤ 1) |
| 17 | 6, 14, 3, 16 | leadd2dd 11878 |
. . . . . . 7
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) + (𝑆‘𝐵)) ≤ ((𝑆‘𝐴) + 1)) |
| 18 | 17 | adantr 480 |
. . . . . 6
⊢ ((𝑆 ∈ States ∧ (𝑆‘𝐴) < 1) → ((𝑆‘𝐴) + (𝑆‘𝐵)) ≤ ((𝑆‘𝐴) + 1)) |
| 19 | | ltadd1 11730 |
. . . . . . . . 9
⊢ (((𝑆‘𝐴) ∈ ℝ ∧ 1 ∈ ℝ
∧ 1 ∈ ℝ) → ((𝑆‘𝐴) < 1 ↔ ((𝑆‘𝐴) + 1) < (1 + 1))) |
| 20 | 19 | biimpd 229 |
. . . . . . . 8
⊢ (((𝑆‘𝐴) ∈ ℝ ∧ 1 ∈ ℝ
∧ 1 ∈ ℝ) → ((𝑆‘𝐴) < 1 → ((𝑆‘𝐴) + 1) < (1 + 1))) |
| 21 | 3, 14, 14, 20 | syl3anc 1373 |
. . . . . . 7
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) < 1 → ((𝑆‘𝐴) + 1) < (1 + 1))) |
| 22 | 21 | imp 406 |
. . . . . 6
⊢ ((𝑆 ∈ States ∧ (𝑆‘𝐴) < 1) → ((𝑆‘𝐴) + 1) < (1 + 1)) |
| 23 | | readdcl 11238 |
. . . . . . . . 9
⊢ (((𝑆‘𝐴) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((𝑆‘𝐴) + 1) ∈
ℝ) |
| 24 | 3, 13, 23 | sylancl 586 |
. . . . . . . 8
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) + 1) ∈ ℝ) |
| 25 | 13, 13 | readdcli 11276 |
. . . . . . . . 9
⊢ (1 + 1)
∈ ℝ |
| 26 | 25 | a1i 11 |
. . . . . . . 8
⊢ (𝑆 ∈ States → (1 + 1)
∈ ℝ) |
| 27 | | lelttr 11351 |
. . . . . . . 8
⊢ ((((𝑆‘𝐴) + (𝑆‘𝐵)) ∈ ℝ ∧ ((𝑆‘𝐴) + 1) ∈ ℝ ∧ (1 + 1) ∈
ℝ) → ((((𝑆‘𝐴) + (𝑆‘𝐵)) ≤ ((𝑆‘𝐴) + 1) ∧ ((𝑆‘𝐴) + 1) < (1 + 1)) → ((𝑆‘𝐴) + (𝑆‘𝐵)) < (1 + 1))) |
| 28 | 7, 24, 26, 27 | syl3anc 1373 |
. . . . . . 7
⊢ (𝑆 ∈ States → ((((𝑆‘𝐴) + (𝑆‘𝐵)) ≤ ((𝑆‘𝐴) + 1) ∧ ((𝑆‘𝐴) + 1) < (1 + 1)) → ((𝑆‘𝐴) + (𝑆‘𝐵)) < (1 + 1))) |
| 29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝑆 ∈ States ∧ (𝑆‘𝐴) < 1) → ((((𝑆‘𝐴) + (𝑆‘𝐵)) ≤ ((𝑆‘𝐴) + 1) ∧ ((𝑆‘𝐴) + 1) < (1 + 1)) → ((𝑆‘𝐴) + (𝑆‘𝐵)) < (1 + 1))) |
| 30 | 18, 22, 29 | mp2and 699 |
. . . . 5
⊢ ((𝑆 ∈ States ∧ (𝑆‘𝐴) < 1) → ((𝑆‘𝐴) + (𝑆‘𝐵)) < (1 + 1)) |
| 31 | | df-2 12329 |
. . . . 5
⊢ 2 = (1 +
1) |
| 32 | 30, 31 | breqtrrdi 5185 |
. . . 4
⊢ ((𝑆 ∈ States ∧ (𝑆‘𝐴) < 1) → ((𝑆‘𝐴) + (𝑆‘𝐵)) < 2) |
| 33 | 32 | ex 412 |
. . 3
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) < 1 → ((𝑆‘𝐴) + (𝑆‘𝐵)) < 2)) |
| 34 | 33 | con3d 152 |
. 2
⊢ (𝑆 ∈ States → (¬
((𝑆‘𝐴) + (𝑆‘𝐵)) < 2 → ¬ (𝑆‘𝐴) < 1)) |
| 35 | | stle1 32244 |
. . . . 5
⊢ (𝑆 ∈ States → (𝐴 ∈
Cℋ → (𝑆‘𝐴) ≤ 1)) |
| 36 | 1, 35 | mpi 20 |
. . . 4
⊢ (𝑆 ∈ States → (𝑆‘𝐴) ≤ 1) |
| 37 | | leloe 11347 |
. . . . 5
⊢ (((𝑆‘𝐴) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((𝑆‘𝐴) ≤ 1 ↔ ((𝑆‘𝐴) < 1 ∨ (𝑆‘𝐴) = 1))) |
| 38 | 3, 13, 37 | sylancl 586 |
. . . 4
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) ≤ 1 ↔ ((𝑆‘𝐴) < 1 ∨ (𝑆‘𝐴) = 1))) |
| 39 | 36, 38 | mpbid 232 |
. . 3
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) < 1 ∨ (𝑆‘𝐴) = 1)) |
| 40 | 39 | ord 865 |
. 2
⊢ (𝑆 ∈ States → (¬
(𝑆‘𝐴) < 1 → (𝑆‘𝐴) = 1)) |
| 41 | 12, 34, 40 | 3syld 60 |
1
⊢ (𝑆 ∈ States → (((𝑆‘𝐴) + (𝑆‘𝐵)) = 2 → (𝑆‘𝐴) = 1)) |