Metamath Proof Explorer

Theorem stadd3i

Description: If the sum of 3 states is 3, then each state is 1. (Contributed by NM, 13-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypotheses stle.1 ⊢ 𝐴 ∈ Cℋ
stle.2 ⊢ 𝐵 ∈ Cℋ
stm1add3.3 ⊢ 𝐶 ∈ Cℋ
Assertion stadd3i ( 𝑆 ∈ States → ( ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) + ( 𝑆 ‘ 𝐶 ) ) = 3 → ( 𝑆 ‘ 𝐴 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 stle.1 ⊢ 𝐴 ∈ Cℋ
2 stle.2 ⊢ 𝐵 ∈ Cℋ
3 stm1add3.3 ⊢ 𝐶 ∈ Cℋ
4 stcl ⊢ ( 𝑆 ∈ States → ( 𝐴 ∈ Cℋ → ( 𝑆 ‘ 𝐴 ) ∈ ℝ ) )
5 1 4 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐴 ) ∈ ℝ )
6 5 recnd ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐴 ) ∈ ℂ )
7 stcl ⊢ ( 𝑆 ∈ States → ( 𝐵 ∈ Cℋ → ( 𝑆 ‘ 𝐵 ) ∈ ℝ ) )
8 2 7 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐵 ) ∈ ℝ )
9 8 recnd ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐵 ) ∈ ℂ )
10 stcl ⊢ ( 𝑆 ∈ States → ( 𝐶 ∈ Cℋ → ( 𝑆 ‘ 𝐶 ) ∈ ℝ ) )
11 3 10 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐶 ) ∈ ℝ )
12 11 recnd ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐶 ) ∈ ℂ )
13 6 9 12 addassd ⊢ ( 𝑆 ∈ States → ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) + ( 𝑆 ‘ 𝐶 ) ) = ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) )
14 13 eqeq1d ⊢ ( 𝑆 ∈ States → ( ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) + ( 𝑆 ‘ 𝐶 ) ) = 3 ↔ ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) = 3 ) )
15 eqcom ⊢ ( ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) = 3 ↔ 3 = ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) )
16 8 11 readdcld ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ∈ ℝ )
17 5 16 readdcld ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) ∈ ℝ )
18 ltne ⊢ ( ( ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) ∈ ℝ ∧ ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) < 3 ) → 3 ≠ ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) )
19 18 ex ⊢ ( ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) ∈ ℝ → ( ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) < 3 → 3 ≠ ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) ) )
20 17 19 syl ⊢ ( 𝑆 ∈ States → ( ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) < 3 → 3 ≠ ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) ) )
21 20 necon2bd ⊢ ( 𝑆 ∈ States → ( 3 = ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) → ¬ ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) < 3 ) )
22 15 21 biimtrid ⊢ ( 𝑆 ∈ States → ( ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) = 3 → ¬ ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) < 3 ) )
23 1re ⊢ 1 ∈ ℝ
24 23 23 readdcli ⊢ ( 1 + 1 ) ∈ ℝ
25 24 a1i ⊢ ( 𝑆 ∈ States → ( 1 + 1 ) ∈ ℝ )
26 1red ⊢ ( 𝑆 ∈ States → 1 ∈ ℝ )
27 stle1 ⊢ ( 𝑆 ∈ States → ( 𝐵 ∈ Cℋ → ( 𝑆 ‘ 𝐵 ) ≤ 1 ) )
28 2 27 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐵 ) ≤ 1 )
29 stle1 ⊢ ( 𝑆 ∈ States → ( 𝐶 ∈ Cℋ → ( 𝑆 ‘ 𝐶 ) ≤ 1 ) )
30 3 29 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐶 ) ≤ 1 )
31 8 11 26 26 28 30 le2addd ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ≤ ( 1 + 1 ) )
32 16 25 5 31 leadd2dd ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) ≤ ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) )
33 32 adantr ⊢ ( ( 𝑆 ∈ States ∧ ( 𝑆 ‘ 𝐴 ) < 1 ) → ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) ≤ ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) )
34 ltadd1 ⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 1 + 1 ) ∈ ℝ ) → ( ( 𝑆 ‘ 𝐴 ) < 1 ↔ ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) < ( 1 + ( 1 + 1 ) ) ) )
35 34 biimpd ⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 1 + 1 ) ∈ ℝ ) → ( ( 𝑆 ‘ 𝐴 ) < 1 → ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) < ( 1 + ( 1 + 1 ) ) ) )
36 5 26 25 35 syl3anc ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) < 1 → ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) < ( 1 + ( 1 + 1 ) ) ) )
37 36 imp ⊢ ( ( 𝑆 ∈ States ∧ ( 𝑆 ‘ 𝐴 ) < 1 ) → ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) < ( 1 + ( 1 + 1 ) ) )
38 readdcl ⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℝ ∧ ( 1 + 1 ) ∈ ℝ ) → ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) ∈ ℝ )
39 5 24 38 sylancl ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) ∈ ℝ )
40 23 24 readdcli ⊢ ( 1 + ( 1 + 1 ) ) ∈ ℝ
41 40 a1i ⊢ ( 𝑆 ∈ States → ( 1 + ( 1 + 1 ) ) ∈ ℝ )
42 lelttr ⊢ ( ( ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) ∈ ℝ ∧ ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) ∈ ℝ ∧ ( 1 + ( 1 + 1 ) ) ∈ ℝ ) → ( ( ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) ≤ ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) < ( 1 + ( 1 + 1 ) ) ) → ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) < ( 1 + ( 1 + 1 ) ) ) )
43 17 39 41 42 syl3anc ⊢ ( 𝑆 ∈ States → ( ( ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) ≤ ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) < ( 1 + ( 1 + 1 ) ) ) → ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) < ( 1 + ( 1 + 1 ) ) ) )
44 43 adantr ⊢ ( ( 𝑆 ∈ States ∧ ( 𝑆 ‘ 𝐴 ) < 1 ) → ( ( ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) ≤ ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) ∧ ( ( 𝑆 ‘ 𝐴 ) + ( 1 + 1 ) ) < ( 1 + ( 1 + 1 ) ) ) → ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) < ( 1 + ( 1 + 1 ) ) ) )
45 33 37 44 mp2and ⊢ ( ( 𝑆 ∈ States ∧ ( 𝑆 ‘ 𝐴 ) < 1 ) → ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) < ( 1 + ( 1 + 1 ) ) )
46 df-3 ⊢ 3 = ( 2 + 1 )
47 df-2 ⊢ 2 = ( 1 + 1 )
48 47 oveq1i ⊢ ( 2 + 1 ) = ( ( 1 + 1 ) + 1 )
49 ax-1cn ⊢ 1 ∈ ℂ
50 49 49 49 addassi ⊢ ( ( 1 + 1 ) + 1 ) = ( 1 + ( 1 + 1 ) )
51 46 48 50 3eqtrri ⊢ ( 1 + ( 1 + 1 ) ) = 3
52 45 51 breqtrdi ⊢ ( ( 𝑆 ∈ States ∧ ( 𝑆 ‘ 𝐴 ) < 1 ) → ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) < 3 )
53 52 ex ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) < 1 → ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) < 3 ) )
54 53 con3d ⊢ ( 𝑆 ∈ States → ( ¬ ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) < 3 → ¬ ( 𝑆 ‘ 𝐴 ) < 1 ) )
55 stle1 ⊢ ( 𝑆 ∈ States → ( 𝐴 ∈ Cℋ → ( 𝑆 ‘ 𝐴 ) ≤ 1 ) )
56 1 55 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐴 ) ≤ 1 )
57 leloe ⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝑆 ‘ 𝐴 ) ≤ 1 ↔ ( ( 𝑆 ‘ 𝐴 ) < 1 ∨ ( 𝑆 ‘ 𝐴 ) = 1 ) ) )
58 5 23 57 sylancl ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) ≤ 1 ↔ ( ( 𝑆 ‘ 𝐴 ) < 1 ∨ ( 𝑆 ‘ 𝐴 ) = 1 ) ) )
59 56 58 mpbid ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) < 1 ∨ ( 𝑆 ‘ 𝐴 ) = 1 ) )
60 59 ord ⊢ ( 𝑆 ∈ States → ( ¬ ( 𝑆 ‘ 𝐴 ) < 1 → ( 𝑆 ‘ 𝐴 ) = 1 ) )
61 22 54 60 3syld ⊢ ( 𝑆 ∈ States → ( ( ( 𝑆 ‘ 𝐴 ) + ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ 𝐶 ) ) ) = 3 → ( 𝑆 ‘ 𝐴 ) = 1 ) )
62 14 61 sylbid ⊢ ( 𝑆 ∈ States → ( ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) + ( 𝑆 ‘ 𝐶 ) ) = 3 → ( 𝑆 ‘ 𝐴 ) = 1 ) )