Proof of Theorem stadd3i
Step | Hyp | Ref
| Expression |
1 | | stle.1 |
. . . . . 6
⊢ 𝐴 ∈
Cℋ |
2 | | stcl 29920 |
. . . . . 6
⊢ (𝑆 ∈ States → (𝐴 ∈
Cℋ → (𝑆‘𝐴) ∈ ℝ)) |
3 | 1, 2 | mpi 20 |
. . . . 5
⊢ (𝑆 ∈ States → (𝑆‘𝐴) ∈ ℝ) |
4 | 3 | recnd 10657 |
. . . 4
⊢ (𝑆 ∈ States → (𝑆‘𝐴) ∈ ℂ) |
5 | | stle.2 |
. . . . . 6
⊢ 𝐵 ∈
Cℋ |
6 | | stcl 29920 |
. . . . . 6
⊢ (𝑆 ∈ States → (𝐵 ∈
Cℋ → (𝑆‘𝐵) ∈ ℝ)) |
7 | 5, 6 | mpi 20 |
. . . . 5
⊢ (𝑆 ∈ States → (𝑆‘𝐵) ∈ ℝ) |
8 | 7 | recnd 10657 |
. . . 4
⊢ (𝑆 ∈ States → (𝑆‘𝐵) ∈ ℂ) |
9 | | stm1add3.3 |
. . . . . 6
⊢ 𝐶 ∈
Cℋ |
10 | | stcl 29920 |
. . . . . 6
⊢ (𝑆 ∈ States → (𝐶 ∈
Cℋ → (𝑆‘𝐶) ∈ ℝ)) |
11 | 9, 10 | mpi 20 |
. . . . 5
⊢ (𝑆 ∈ States → (𝑆‘𝐶) ∈ ℝ) |
12 | 11 | recnd 10657 |
. . . 4
⊢ (𝑆 ∈ States → (𝑆‘𝐶) ∈ ℂ) |
13 | 4, 8, 12 | addassd 10651 |
. . 3
⊢ (𝑆 ∈ States → (((𝑆‘𝐴) + (𝑆‘𝐵)) + (𝑆‘𝐶)) = ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶)))) |
14 | 13 | eqeq1d 2820 |
. 2
⊢ (𝑆 ∈ States → ((((𝑆‘𝐴) + (𝑆‘𝐵)) + (𝑆‘𝐶)) = 3 ↔ ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) = 3)) |
15 | | eqcom 2825 |
. . . 4
⊢ (((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) = 3 ↔ 3 = ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶)))) |
16 | 7, 11 | readdcld 10658 |
. . . . . . 7
⊢ (𝑆 ∈ States → ((𝑆‘𝐵) + (𝑆‘𝐶)) ∈ ℝ) |
17 | 3, 16 | readdcld 10658 |
. . . . . 6
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) ∈ ℝ) |
18 | | ltne 10725 |
. . . . . . 7
⊢ ((((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) ∈ ℝ ∧ ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) < 3) → 3 ≠ ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶)))) |
19 | 18 | ex 413 |
. . . . . 6
⊢ (((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) ∈ ℝ → (((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) < 3 → 3 ≠ ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))))) |
20 | 17, 19 | syl 17 |
. . . . 5
⊢ (𝑆 ∈ States → (((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) < 3 → 3 ≠ ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))))) |
21 | 20 | necon2bd 3029 |
. . . 4
⊢ (𝑆 ∈ States → (3 =
((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) → ¬ ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) < 3)) |
22 | 15, 21 | syl5bi 243 |
. . 3
⊢ (𝑆 ∈ States → (((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) = 3 → ¬ ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) < 3)) |
23 | | 1re 10629 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
24 | 23, 23 | readdcli 10644 |
. . . . . . . . . 10
⊢ (1 + 1)
∈ ℝ |
25 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝑆 ∈ States → (1 + 1)
∈ ℝ) |
26 | | 1red 10630 |
. . . . . . . . . 10
⊢ (𝑆 ∈ States → 1 ∈
ℝ) |
27 | | stle1 29929 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ States → (𝐵 ∈
Cℋ → (𝑆‘𝐵) ≤ 1)) |
28 | 5, 27 | mpi 20 |
. . . . . . . . . 10
⊢ (𝑆 ∈ States → (𝑆‘𝐵) ≤ 1) |
29 | | stle1 29929 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ States → (𝐶 ∈
Cℋ → (𝑆‘𝐶) ≤ 1)) |
30 | 9, 29 | mpi 20 |
. . . . . . . . . 10
⊢ (𝑆 ∈ States → (𝑆‘𝐶) ≤ 1) |
31 | 7, 11, 26, 26, 28, 30 | le2addd 11247 |
. . . . . . . . 9
⊢ (𝑆 ∈ States → ((𝑆‘𝐵) + (𝑆‘𝐶)) ≤ (1 + 1)) |
32 | 16, 25, 3, 31 | leadd2dd 11243 |
. . . . . . . 8
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) ≤ ((𝑆‘𝐴) + (1 + 1))) |
33 | 32 | adantr 481 |
. . . . . . 7
⊢ ((𝑆 ∈ States ∧ (𝑆‘𝐴) < 1) → ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) ≤ ((𝑆‘𝐴) + (1 + 1))) |
34 | | ltadd1 11095 |
. . . . . . . . . 10
⊢ (((𝑆‘𝐴) ∈ ℝ ∧ 1 ∈ ℝ
∧ (1 + 1) ∈ ℝ) → ((𝑆‘𝐴) < 1 ↔ ((𝑆‘𝐴) + (1 + 1)) < (1 + (1 +
1)))) |
35 | 34 | biimpd 230 |
. . . . . . . . 9
⊢ (((𝑆‘𝐴) ∈ ℝ ∧ 1 ∈ ℝ
∧ (1 + 1) ∈ ℝ) → ((𝑆‘𝐴) < 1 → ((𝑆‘𝐴) + (1 + 1)) < (1 + (1 +
1)))) |
36 | 3, 26, 25, 35 | syl3anc 1363 |
. . . . . . . 8
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) < 1 → ((𝑆‘𝐴) + (1 + 1)) < (1 + (1 +
1)))) |
37 | 36 | imp 407 |
. . . . . . 7
⊢ ((𝑆 ∈ States ∧ (𝑆‘𝐴) < 1) → ((𝑆‘𝐴) + (1 + 1)) < (1 + (1 +
1))) |
38 | | readdcl 10608 |
. . . . . . . . . 10
⊢ (((𝑆‘𝐴) ∈ ℝ ∧ (1 + 1) ∈
ℝ) → ((𝑆‘𝐴) + (1 + 1)) ∈
ℝ) |
39 | 3, 24, 38 | sylancl 586 |
. . . . . . . . 9
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) + (1 + 1)) ∈
ℝ) |
40 | 23, 24 | readdcli 10644 |
. . . . . . . . . 10
⊢ (1 + (1 +
1)) ∈ ℝ |
41 | 40 | a1i 11 |
. . . . . . . . 9
⊢ (𝑆 ∈ States → (1 + (1 +
1)) ∈ ℝ) |
42 | | lelttr 10719 |
. . . . . . . . 9
⊢ ((((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) ∈ ℝ ∧ ((𝑆‘𝐴) + (1 + 1)) ∈ ℝ ∧ (1 + (1 +
1)) ∈ ℝ) → ((((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) ≤ ((𝑆‘𝐴) + (1 + 1)) ∧ ((𝑆‘𝐴) + (1 + 1)) < (1 + (1 + 1))) →
((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) < (1 + (1 + 1)))) |
43 | 17, 39, 41, 42 | syl3anc 1363 |
. . . . . . . 8
⊢ (𝑆 ∈ States → ((((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) ≤ ((𝑆‘𝐴) + (1 + 1)) ∧ ((𝑆‘𝐴) + (1 + 1)) < (1 + (1 + 1))) →
((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) < (1 + (1 + 1)))) |
44 | 43 | adantr 481 |
. . . . . . 7
⊢ ((𝑆 ∈ States ∧ (𝑆‘𝐴) < 1) → ((((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) ≤ ((𝑆‘𝐴) + (1 + 1)) ∧ ((𝑆‘𝐴) + (1 + 1)) < (1 + (1 + 1))) →
((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) < (1 + (1 + 1)))) |
45 | 33, 37, 44 | mp2and 695 |
. . . . . 6
⊢ ((𝑆 ∈ States ∧ (𝑆‘𝐴) < 1) → ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) < (1 + (1 + 1))) |
46 | | df-3 11689 |
. . . . . . 7
⊢ 3 = (2 +
1) |
47 | | df-2 11688 |
. . . . . . . 8
⊢ 2 = (1 +
1) |
48 | 47 | oveq1i 7155 |
. . . . . . 7
⊢ (2 + 1) =
((1 + 1) + 1) |
49 | | ax-1cn 10583 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
50 | 49, 49, 49 | addassi 10639 |
. . . . . . 7
⊢ ((1 + 1)
+ 1) = (1 + (1 + 1)) |
51 | 46, 48, 50 | 3eqtrri 2846 |
. . . . . 6
⊢ (1 + (1 +
1)) = 3 |
52 | 45, 51 | breqtrdi 5098 |
. . . . 5
⊢ ((𝑆 ∈ States ∧ (𝑆‘𝐴) < 1) → ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) < 3) |
53 | 52 | ex 413 |
. . . 4
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) < 1 → ((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) < 3)) |
54 | 53 | con3d 155 |
. . 3
⊢ (𝑆 ∈ States → (¬
((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) < 3 → ¬ (𝑆‘𝐴) < 1)) |
55 | | stle1 29929 |
. . . . . 6
⊢ (𝑆 ∈ States → (𝐴 ∈
Cℋ → (𝑆‘𝐴) ≤ 1)) |
56 | 1, 55 | mpi 20 |
. . . . 5
⊢ (𝑆 ∈ States → (𝑆‘𝐴) ≤ 1) |
57 | | leloe 10715 |
. . . . . 6
⊢ (((𝑆‘𝐴) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((𝑆‘𝐴) ≤ 1 ↔ ((𝑆‘𝐴) < 1 ∨ (𝑆‘𝐴) = 1))) |
58 | 3, 23, 57 | sylancl 586 |
. . . . 5
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) ≤ 1 ↔ ((𝑆‘𝐴) < 1 ∨ (𝑆‘𝐴) = 1))) |
59 | 56, 58 | mpbid 233 |
. . . 4
⊢ (𝑆 ∈ States → ((𝑆‘𝐴) < 1 ∨ (𝑆‘𝐴) = 1)) |
60 | 59 | ord 858 |
. . 3
⊢ (𝑆 ∈ States → (¬
(𝑆‘𝐴) < 1 → (𝑆‘𝐴) = 1)) |
61 | 22, 54, 60 | 3syld 60 |
. 2
⊢ (𝑆 ∈ States → (((𝑆‘𝐴) + ((𝑆‘𝐵) + (𝑆‘𝐶))) = 3 → (𝑆‘𝐴) = 1)) |
62 | 14, 61 | sylbid 241 |
1
⊢ (𝑆 ∈ States → ((((𝑆‘𝐴) + (𝑆‘𝐵)) + (𝑆‘𝐶)) = 3 → (𝑆‘𝐴) = 1)) |