Metamath Proof Explorer

Theorem staddi

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

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

Proof

Step Hyp Ref Expression
1 stle.1 ⊢ 𝐴 ∈ Cℋ
2 stle.2 ⊢ 𝐵 ∈ Cℋ
3 stcl ⊢ ( 𝑆 ∈ States → ( 𝐴 ∈ Cℋ → ( 𝑆 ‘ 𝐴 ) ∈ ℝ ) )
4 1 3 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐴 ) ∈ ℝ )
5 stcl ⊢ ( 𝑆 ∈ States → ( 𝐵 ∈ Cℋ → ( 𝑆 ‘ 𝐵 ) ∈ ℝ ) )
6 2 5 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐵 ) ∈ ℝ )
7 4 6 readdcld ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) ∈ ℝ )
8 ltne ⊢ ( ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) ∈ ℝ ∧ ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) < 2 ) → 2 ≠ ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) )
9 8 necomd ⊢ ( ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) ∈ ℝ ∧ ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) < 2 ) → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) ≠ 2 )
10 7 9 sylan ⊢ ( ( 𝑆 ∈ States ∧ ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) < 2 ) → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) ≠ 2 )
11 10 ex ⊢ ( 𝑆 ∈ States → ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) < 2 → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) ≠ 2 ) )
12 11 necon2bd ⊢ ( 𝑆 ∈ States → ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) = 2 → ¬ ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) < 2 ) )
13 1re ⊢ 1 ∈ ℝ
14 13 a1i ⊢ ( 𝑆 ∈ States → 1 ∈ ℝ )
15 stle1 ⊢ ( 𝑆 ∈ States → ( 𝐵 ∈ Cℋ → ( 𝑆 ‘ 𝐵 ) ≤ 1 ) )
16 2 15 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐵 ) ≤ 1 )
17 6 14 4 16 leadd2dd ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) ≤ ( ( 𝑆 ‘ 𝐴 ) + 1 ) )
18 17 adantr ⊢ ( ( 𝑆 ∈ States ∧ ( 𝑆 ‘ 𝐴 ) < 1 ) → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) ≤ ( ( 𝑆 ‘ 𝐴 ) + 1 ) )
19 ltadd1 ⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝑆 ‘ 𝐴 ) < 1 ↔ ( ( 𝑆 ‘ 𝐴 ) + 1 ) < ( 1 + 1 ) ) )
20 19 biimpd ⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝑆 ‘ 𝐴 ) < 1 → ( ( 𝑆 ‘ 𝐴 ) + 1 ) < ( 1 + 1 ) ) )
21 4 14 14 20 syl3anc ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) < 1 → ( ( 𝑆 ‘ 𝐴 ) + 1 ) < ( 1 + 1 ) ) )
22 21 imp ⊢ ( ( 𝑆 ∈ States ∧ ( 𝑆 ‘ 𝐴 ) < 1 ) → ( ( 𝑆 ‘ 𝐴 ) + 1 ) < ( 1 + 1 ) )
23 readdcl ⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝑆 ‘ 𝐴 ) + 1 ) ∈ ℝ )
24 4 13 23 sylancl ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) + 1 ) ∈ ℝ )
25 13 13 readdcli ⊢ ( 1 + 1 ) ∈ ℝ
26 25 a1i ⊢ ( 𝑆 ∈ States → ( 1 + 1 ) ∈ ℝ )
27 lelttr ⊢ ( ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) ∈ ℝ ∧ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ∈ ℝ ∧ ( 1 + 1 ) ∈ ℝ ) → ( ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) ≤ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ∧ ( ( 𝑆 ‘ 𝐴 ) + 1 ) < ( 1 + 1 ) ) → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) < ( 1 + 1 ) ) )
28 7 24 26 27 syl3anc ⊢ ( 𝑆 ∈ States → ( ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) ≤ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ∧ ( ( 𝑆 ‘ 𝐴 ) + 1 ) < ( 1 + 1 ) ) → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) < ( 1 + 1 ) ) )
29 28 adantr ⊢ ( ( 𝑆 ∈ States ∧ ( 𝑆 ‘ 𝐴 ) < 1 ) → ( ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) ≤ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ∧ ( ( 𝑆 ‘ 𝐴 ) + 1 ) < ( 1 + 1 ) ) → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) < ( 1 + 1 ) ) )
30 18 22 29 mp2and ⊢ ( ( 𝑆 ∈ States ∧ ( 𝑆 ‘ 𝐴 ) < 1 ) → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) < ( 1 + 1 ) )
31 df-2 ⊢ 2 = ( 1 + 1 )
32 30 31 breqtrrdi ⊢ ( ( 𝑆 ∈ States ∧ ( 𝑆 ‘ 𝐴 ) < 1 ) → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) < 2 )
33 32 ex ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) < 1 → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) < 2 ) )
34 33 con3d ⊢ ( 𝑆 ∈ States → ( ¬ ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) < 2 → ¬ ( 𝑆 ‘ 𝐴 ) < 1 ) )
35 stle1 ⊢ ( 𝑆 ∈ States → ( 𝐴 ∈ Cℋ → ( 𝑆 ‘ 𝐴 ) ≤ 1 ) )
36 1 35 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐴 ) ≤ 1 )
37 leloe ⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝑆 ‘ 𝐴 ) ≤ 1 ↔ ( ( 𝑆 ‘ 𝐴 ) < 1 ∨ ( 𝑆 ‘ 𝐴 ) = 1 ) ) )
38 4 13 37 sylancl ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) ≤ 1 ↔ ( ( 𝑆 ‘ 𝐴 ) < 1 ∨ ( 𝑆 ‘ 𝐴 ) = 1 ) ) )
39 36 38 mpbid ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) < 1 ∨ ( 𝑆 ‘ 𝐴 ) = 1 ) )
40 39 ord ⊢ ( 𝑆 ∈ States → ( ¬ ( 𝑆 ‘ 𝐴 ) < 1 → ( 𝑆 ‘ 𝐴 ) = 1 ) )
41 12 34 40 3syld ⊢ ( 𝑆 ∈ States → ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) = 2 → ( 𝑆 ‘ 𝐴 ) = 1 ) )