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	$⊢ A \in C_{ℋ}$
	stle.2	$⊢ B \in C_{ℋ}$
Assertion	staddi	$⊢ S \in States \to (S (A) + S (B) = 2 \to S (A) = 1)$

Proof

Step	Hyp	Ref	Expression
1		stle.1	$⊢ A \in C_{ℋ}$
2		stle.2	$⊢ B \in C_{ℋ}$
3		stcl	$⊢ S \in States \to (A \in C_{ℋ} \to S (A) \in ℝ)$
4	1 3	mpi	$⊢ S \in States \to S (A) \in ℝ$
5		stcl	$⊢ S \in States \to (B \in C_{ℋ} \to S (B) \in ℝ)$
6	2 5	mpi	$⊢ S \in States \to S (B) \in ℝ$
7	4 6	readdcld	$⊢ S \in States \to S (A) + S (B) \in ℝ$
8		ltne	$⊢ (S (A) + S (B) \in ℝ \land S (A) + S (B) < 2) \to 2 \neq S (A) + S (B)$
9	8	necomd	$⊢ (S (A) + S (B) \in ℝ \land S (A) + S (B) < 2) \to S (A) + S (B) \neq 2$
10	7 9	sylan	$⊢ (S \in States \land S (A) + S (B) < 2) \to S (A) + S (B) \neq 2$
11	10	ex	$⊢ S \in States \to (S (A) + S (B) < 2 \to S (A) + S (B) \neq 2)$
12	11	necon2bd	$⊢ S \in States \to (S (A) + S (B) = 2 \to \neg S (A) + S (B) < 2)$
13		1re	$⊢ 1 \in ℝ$
14	13	a1i	$⊢ S \in States \to 1 \in ℝ$
15		stle1	$⊢ S \in States \to (B \in C_{ℋ} \to S (B) \leq 1)$
16	2 15	mpi	$⊢ S \in States \to S (B) \leq 1$
17	6 14 4 16	leadd2dd	$⊢ S \in States \to S (A) + S (B) \leq S (A) + 1$
18	17	adantr	$⊢ (S \in States \land S (A) < 1) \to S (A) + S (B) \leq S (A) + 1$
19		ltadd1	$⊢ (S (A) \in ℝ \land 1 \in ℝ \land 1 \in ℝ) \to (S (A) < 1 \leftrightarrow S (A) + 1 < 1 + 1)$
20	19	biimpd	$⊢ (S (A) \in ℝ \land 1 \in ℝ \land 1 \in ℝ) \to (S (A) < 1 \to S (A) + 1 < 1 + 1)$
21	4 14 14 20	syl3anc	$⊢ S \in States \to (S (A) < 1 \to S (A) + 1 < 1 + 1)$
22	21	imp	$⊢ (S \in States \land S (A) < 1) \to S (A) + 1 < 1 + 1$
23		readdcl	$⊢ (S (A) \in ℝ \land 1 \in ℝ) \to S (A) + 1 \in ℝ$
24	4 13 23	sylancl	$⊢ S \in States \to S (A) + 1 \in ℝ$
25	13 13	readdcli	$⊢ 1 + 1 \in ℝ$
26	25	a1i	$⊢ S \in States \to 1 + 1 \in ℝ$
27		lelttr	$⊢ (S (A) + S (B) \in ℝ \land S (A) + 1 \in ℝ \land 1 + 1 \in ℝ) \to ((S (A) + S (B) \leq S (A) + 1 \land S (A) + 1 < 1 + 1) \to S (A) + S (B) < 1 + 1)$
28	7 24 26 27	syl3anc	$⊢ S \in States \to ((S (A) + S (B) \leq S (A) + 1 \land S (A) + 1 < 1 + 1) \to S (A) + S (B) < 1 + 1)$
29	28	adantr	$⊢ (S \in States \land S (A) < 1) \to ((S (A) + S (B) \leq S (A) + 1 \land S (A) + 1 < 1 + 1) \to S (A) + S (B) < 1 + 1)$
30	18 22 29	mp2and	$⊢ (S \in States \land S (A) < 1) \to S (A) + S (B) < 1 + 1$
31		df-2	$⊢ 2 = 1 + 1$
32	30 31	breqtrrdi	$⊢ (S \in States \land S (A) < 1) \to S (A) + S (B) < 2$
33	32	ex	$⊢ S \in States \to (S (A) < 1 \to S (A) + S (B) < 2)$
34	33	con3d	$⊢ S \in States \to (\neg S (A) + S (B) < 2 \to \neg S (A) < 1)$
35		stle1	$⊢ S \in States \to (A \in C_{ℋ} \to S (A) \leq 1)$
36	1 35	mpi	$⊢ S \in States \to S (A) \leq 1$
37		leloe	$⊢ (S (A) \in ℝ \land 1 \in ℝ) \to (S (A) \leq 1 \leftrightarrow (S (A) < 1 \lor S (A) = 1))$
38	4 13 37	sylancl	$⊢ S \in States \to (S (A) \leq 1 \leftrightarrow (S (A) < 1 \lor S (A) = 1))$
39	36 38	mpbid	$⊢ S \in States \to (S (A) < 1 \lor S (A) = 1)$
40	39	ord	$⊢ S \in States \to (\neg S (A) < 1 \to S (A) = 1)$
41	12 34 40	3syld	$⊢ S \in States \to (S (A) + S (B) = 2 \to S (A) = 1)$

Metamath Proof Explorer

Theorem staddi

Proof