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	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	stle.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	stm1add3.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	stadd3i	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)+S\left(B\right)+S\left(C\right)=3\to S\left(A\right)=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		stle.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		stle.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		stm1add3.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4		stcl	$$⊢S\in \mathrm{States}\to \left(A\in {\mathbf{C}}_{\mathscr{H}}\to S\left(A\right)\in ℝ\right)$$
5	1 4	mpi	$$⊢S\in \mathrm{States}\to S\left(A\right)\in ℝ$$
6	5	recnd	$$⊢S\in \mathrm{States}\to S\left(A\right)\in ℂ$$
7		stcl	$$⊢S\in \mathrm{States}\to \left(B\in {\mathbf{C}}_{\mathscr{H}}\to S\left(B\right)\in ℝ\right)$$
8	2 7	mpi	$$⊢S\in \mathrm{States}\to S\left(B\right)\in ℝ$$
9	8	recnd	$$⊢S\in \mathrm{States}\to S\left(B\right)\in ℂ$$
10		stcl	$$⊢S\in \mathrm{States}\to \left(C\in {\mathbf{C}}_{\mathscr{H}}\to S\left(C\right)\in ℝ\right)$$
11	3 10	mpi	$$⊢S\in \mathrm{States}\to S\left(C\right)\in ℝ$$
12	11	recnd	$$⊢S\in \mathrm{States}\to S\left(C\right)\in ℂ$$
13	6 9 12	addassd	$$⊢S\in \mathrm{States}\to S\left(A\right)+S\left(B\right)+S\left(C\right)=S\left(A\right)+S\left(B\right)+S\left(C\right)$$
14	13	eqeq1d	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)+S\left(B\right)+S\left(C\right)=3\leftrightarrow S\left(A\right)+S\left(B\right)+S\left(C\right)=3\right)$$
15		eqcom	$$⊢S\left(A\right)+S\left(B\right)+S\left(C\right)=3\leftrightarrow 3=S\left(A\right)+S\left(B\right)+S\left(C\right)$$
16	8 11	readdcld	$$⊢S\in \mathrm{States}\to S\left(B\right)+S\left(C\right)\in ℝ$$
17	5 16	readdcld	$$⊢S\in \mathrm{States}\to S\left(A\right)+S\left(B\right)+S\left(C\right)\in ℝ$$
18		ltne	$$⊢\left(S\left(A\right)+S\left(B\right)+S\left(C\right)\in ℝ\wedge S\left(A\right)+S\left(B\right)+S\left(C\right)<3\right)\to 3\ne S\left(A\right)+S\left(B\right)+S\left(C\right)$$
19	18	ex	$$⊢S\left(A\right)+S\left(B\right)+S\left(C\right)\in ℝ\to \left(S\left(A\right)+S\left(B\right)+S\left(C\right)<3\to 3\ne S\left(A\right)+S\left(B\right)+S\left(C\right)\right)$$
20	17 19	syl	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)+S\left(B\right)+S\left(C\right)<3\to 3\ne S\left(A\right)+S\left(B\right)+S\left(C\right)\right)$$
21	20	necon2bd	$$⊢S\in \mathrm{States}\to \left(3=S\left(A\right)+S\left(B\right)+S\left(C\right)\to \neg S\left(A\right)+S\left(B\right)+S\left(C\right)<3\right)$$
22	15 21	biimtrid	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)+S\left(B\right)+S\left(C\right)=3\to \neg S\left(A\right)+S\left(B\right)+S\left(C\right)<3\right)$$
23		1re	$$⊢1\in ℝ$$
24	23 23	readdcli	$$⊢1+1\in ℝ$$
25	24	a1i	$$⊢S\in \mathrm{States}\to 1+1\in ℝ$$
26		1red	$$⊢S\in \mathrm{States}\to 1\in ℝ$$
27		stle1	$$⊢S\in \mathrm{States}\to \left(B\in {\mathbf{C}}_{\mathscr{H}}\to S\left(B\right)\le 1\right)$$
28	2 27	mpi	$$⊢S\in \mathrm{States}\to S\left(B\right)\le 1$$
29		stle1	$$⊢S\in \mathrm{States}\to \left(C\in {\mathbf{C}}_{\mathscr{H}}\to S\left(C\right)\le 1\right)$$
30	3 29	mpi	$$⊢S\in \mathrm{States}\to S\left(C\right)\le 1$$
31	8 11 26 26 28 30	le2addd	$$⊢S\in \mathrm{States}\to S\left(B\right)+S\left(C\right)\le 1+1$$
32	16 25 5 31	leadd2dd	$$⊢S\in \mathrm{States}\to S\left(A\right)+S\left(B\right)+S\left(C\right)\le S\left(A\right)+1+1$$
33	32	adantr	$$⊢\left(S\in \mathrm{States}\wedge S\left(A\right)<1\right)\to S\left(A\right)+S\left(B\right)+S\left(C\right)\le S\left(A\right)+1+1$$
34		ltadd1	$$⊢\left(S\left(A\right)\in ℝ\wedge 1\in ℝ\wedge 1+1\in ℝ\right)\to \left(S\left(A\right)<1\leftrightarrow S\left(A\right)+1+1<1+1+1\right)$$
35	34	biimpd	$$⊢\left(S\left(A\right)\in ℝ\wedge 1\in ℝ\wedge 1+1\in ℝ\right)\to \left(S\left(A\right)<1\to S\left(A\right)+1+1<1+1+1\right)$$
36	5 26 25 35	syl3anc	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)<1\to S\left(A\right)+1+1<1+1+1\right)$$
37	36	imp	$$⊢\left(S\in \mathrm{States}\wedge S\left(A\right)<1\right)\to S\left(A\right)+1+1<1+1+1$$
38		readdcl	$$⊢\left(S\left(A\right)\in ℝ\wedge 1+1\in ℝ\right)\to S\left(A\right)+1+1\in ℝ$$
39	5 24 38	sylancl	$$⊢S\in \mathrm{States}\to S\left(A\right)+1+1\in ℝ$$
40	23 24	readdcli	$$⊢1+1+1\in ℝ$$
41	40	a1i	$$⊢S\in \mathrm{States}\to 1+1+1\in ℝ$$
42		lelttr	$$⊢\left(S\left(A\right)+S\left(B\right)+S\left(C\right)\in ℝ\wedge S\left(A\right)+1+1\in ℝ\wedge 1+1+1\in ℝ\right)\to \left(\left(S\left(A\right)+S\left(B\right)+S\left(C\right)\le S\left(A\right)+1+1\wedge S\left(A\right)+1+1<1+1+1\right)\to S\left(A\right)+S\left(B\right)+S\left(C\right)<1+1+1\right)$$
43	17 39 41 42	syl3anc	$$⊢S\in \mathrm{States}\to \left(\left(S\left(A\right)+S\left(B\right)+S\left(C\right)\le S\left(A\right)+1+1\wedge S\left(A\right)+1+1<1+1+1\right)\to S\left(A\right)+S\left(B\right)+S\left(C\right)<1+1+1\right)$$
44	43	adantr	$$⊢\left(S\in \mathrm{States}\wedge S\left(A\right)<1\right)\to \left(\left(S\left(A\right)+S\left(B\right)+S\left(C\right)\le S\left(A\right)+1+1\wedge S\left(A\right)+1+1<1+1+1\right)\to S\left(A\right)+S\left(B\right)+S\left(C\right)<1+1+1\right)$$
45	33 37 44	mp2and	$$⊢\left(S\in \mathrm{States}\wedge S\left(A\right)<1\right)\to S\left(A\right)+S\left(B\right)+S\left(C\right)<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\in ℂ$$
50	49 49 49	addassi	$$⊢1+1+1=1+1+1$$
51	46 48 50	3eqtrri	$$⊢1+1+1=3$$
52	45 51	breqtrdi	$$⊢\left(S\in \mathrm{States}\wedge S\left(A\right)<1\right)\to S\left(A\right)+S\left(B\right)+S\left(C\right)<3$$
53	52	ex	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)<1\to S\left(A\right)+S\left(B\right)+S\left(C\right)<3\right)$$
54	53	con3d	$$⊢S\in \mathrm{States}\to \left(\neg S\left(A\right)+S\left(B\right)+S\left(C\right)<3\to \neg S\left(A\right)<1\right)$$
55		stle1	$$⊢S\in \mathrm{States}\to \left(A\in {\mathbf{C}}_{\mathscr{H}}\to S\left(A\right)\le 1\right)$$
56	1 55	mpi	$$⊢S\in \mathrm{States}\to S\left(A\right)\le 1$$
57		leloe	$$⊢\left(S\left(A\right)\in ℝ\wedge 1\in ℝ\right)\to \left(S\left(A\right)\le 1\leftrightarrow \left(S\left(A\right)<1\vee S\left(A\right)=1\right)\right)$$
58	5 23 57	sylancl	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)\le 1\leftrightarrow \left(S\left(A\right)<1\vee S\left(A\right)=1\right)\right)$$
59	56 58	mpbid	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)<1\vee S\left(A\right)=1\right)$$
60	59	ord	$$⊢S\in \mathrm{States}\to \left(\neg S\left(A\right)<1\to S\left(A\right)=1\right)$$
61	22 54 60	3syld	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)+S\left(B\right)+S\left(C\right)=3\to S\left(A\right)=1\right)$$
62	14 61	sylbid	$$⊢S\in \mathrm{States}\to \left(S\left(A\right)+S\left(B\right)+S\left(C\right)=3\to S\left(A\right)=1\right)$$