Theorem stadd3 10113

Description: If the sum of 3 states is 3, then each state is 1.

Hypotheses

Ref	Expression
stle.1	|- A e. CH
stle.2	|- B e. CH
stm1add3.3	|- C e. CH

Assertion

Ref	Expression
stadd3	|- (S e. States -> ((((S` A) + (S` B)) + (S` C)) = 3 -> (S` A) = 1))

Proof of Theorem stadd3

Step	Hyp	Ref	Expression
1		axaddass 5257	. . . 4 |- (((S` A) e. CC /\ (S` B) e. CC /\ (S` C) e. CC) -> (((S` A) + (S` B)) + (S` C)) = ((S` A) + ((S` B) + (S` C))))
2		stle.1	. . . . . 6 |- A e. CH
3		stclt 10081	. . . . . 6 |- (S e. States -> (A e. CH -> (S` A) e. RR))
4	2, 3	mpi 44	. . . . 5 |- (S e. States -> (S` A) e. RR)
5	4	recnd 5295	. . . 4 |- (S e. States -> (S` A) e. CC)
6		stle.2	. . . . . 6 |- B e. CH
7		stclt 10081	. . . . . 6 |- (S e. States -> (B e. CH -> (S` B) e. RR))
8	6, 7	mpi 44	. . . . 5 |- (S e. States -> (S` B) e. RR)
9	8	recnd 5295	. . . 4 |- (S e. States -> (S` B) e. CC)
10		stm1add3.3	. . . . . 6 |- C e. CH
11		stclt 10081	. . . . . 6 |- (S e. States -> (C e. CH -> (S` C) e. RR))
12	10, 11	mpi 44	. . . . 5 |- (S e. States -> (S` C) e. RR)
13	12	recnd 5295	. . . 4 |- (S e. States -> (S` C) e. CC)
14	1, 5, 9, 13	syl3anc 857	. . 3 |- (S e. States -> (((S` A) + (S` B)) + (S` C)) = ((S` A) + ((S` B) + (S` C))))
15	14	eqeq1d 1480	. 2 |- (S e. States -> ((((S` A) + (S` B)) + (S` C)) = 3 <-> ((S` A) + ((S` B) + (S` C))) = 3))
16		axaddrcl 5252	. . . . . . 7 |- (((S` A) e. RR /\ ((S` B) + (S` C)) e. RR) -> ((S` A) + ((S` B) + (S` C))) e. RR)
17		axaddrcl 5252	. . . . . . . 8 |- (((S` B) e. RR /\ (S` C) e. RR) -> ((S` B) + (S` C)) e. RR)
18	17, 8, 12	sylanc 471	. . . . . . 7 |- (S e. States -> ((S` B) + (S` C)) e. RR)
19	16, 4, 18	sylanc 471	. . . . . 6 |- (S e. States -> ((S` A) + ((S` B) + (S` C))) e. RR)
20		3re 5936	. . . . . 6 |- 3 e. RR
21	19, 20	jctir 293	. . . . 5 |- (S e. States -> (((S` A) + ((S` B) + (S` C))) e. RR /\ 3 e. RR))
22		ltnetOLD 5497	. . . . 5 |- ((((S` A) + ((S` B) + (S` C))) e. RR /\ 3 e. RR) -> (((S` A) + ((S` B) + (S` C))) < 3 -> -. ((S` A) + ((S` B) + (S` C))) = 3))
23	21, 22	syl 10	. . . 4 |- (S e. States -> (((S` A) + ((S` B) + (S` C))) < 3 -> -. ((S` A) + ((S` B) + (S` C))) = 3))
24	23	con2d 91	. . 3 |- (S e. States -> (((S` A) + ((S` B) + (S` C))) = 3 -> -. ((S` A) + ((S` B) + (S` C))) < 3))
25		1re 5415	. . . . . . . . . . . . 13 |- 1 e. RR
26	8, 25	jctir 293	. . . . . . . . . . . 12 |- (S e. States -> ((S` B) e. RR /\ 1 e. RR))
27		axaddrcl 5252	. . . . . . . . . . . 12 |- (((S` B) e. RR /\ 1 e. RR) -> ((S` B) + 1) e. RR)
28	26, 27	syl 10	. . . . . . . . . . 11 |- (S e. States -> ((S` B) + 1) e. RR)
29	25, 25	readdcl 5314	. . . . . . . . . . . 12 |- (1 + 1) e. RR
30	29	a1i 8	. . . . . . . . . . 11 |- (S e. States -> (1 + 1) e. RR)
31		stle1t 10090	. . . . . . . . . . . . 13 |- (S e. States -> (C e. CH -> (S` C) <_ 1))
32	10, 31	mpi 44	. . . . . . . . . . . 12 |- (S e. States -> (S` C) <_ 1)
33		leadd2t 5608	. . . . . . . . . . . . 13 |- (((S` C) e. RR /\ 1 e. RR /\ (S` B) e. RR) -> ((S` C) <_ 1 <-> ((S` B) + (S` C)) <_ ((S` B) + 1)))
34	25	a1i 8	. . . . . . . . . . . . 13 |- (S e. States -> 1 e. RR)
35	33, 12, 34, 8	syl3anc 857	. . . . . . . . . . . 12 |- (S e. States -> ((S` C) <_ 1 <-> ((S` B) + (S` C)) <_ ((S` B) + 1)))
36	32, 35	mpbid 195	. . . . . . . . . . 11 |- (S e. States -> ((S` B) + (S` C)) <_ ((S` B) + 1))
37		stle1t 10090	. . . . . . . . . . . . 13 |- (S e. States -> (B e. CH -> (S` B) <_ 1))
38	6, 37	mpi 44	. . . . . . . . . . . 12 |- (S e. States -> (S` B) <_ 1)
39		leadd1t 5607	. . . . . . . . . . . . 13 |- (((S` B) e. RR /\ 1 e. RR /\ 1 e. RR) -> ((S` B) <_ 1 <-> ((S` B) + 1) <_ (1 + 1)))
40	39, 8, 34, 34	syl3anc 857	. . . . . . . . . . . 12 |- (S e. States -> ((S` B) <_ 1 <-> ((S` B) + 1) <_ (1 + 1)))
41	38, 40	mpbid 195	. . . . . . . . . . 11 |- (S e. States -> ((S` B) + 1) <_ (1 + 1))
42	18, 28, 30, 36, 41	letrd 5507	. . . . . . . . . 10 |- (S e. States -> ((S` B) + (S` C)) <_ (1 + 1))
43		leadd2t 5608	. . . . . . . . . . 11 |- ((((S` B) + (S` C)) e. RR /\ (1 + 1) e. RR /\ (S` A) e. RR) -> (((S` B) + (S` C)) <_ (1 + 1) <-> ((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1))))
44	43, 18, 30, 4	syl3anc 857	. . . . . . . . . 10 |- (S e. States -> (((S` B) + (S` C)) <_ (1 + 1) <-> ((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1))))
45	42, 44	mpbid 195	. . . . . . . . 9 |- (S e. States -> ((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1)))
46	45	adantr 389	. . . . . . . 8 |- ((S e. States /\ (S` A) < 1) -> ((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1)))
47		ltadd1t 5605	. . . . . . . . . . 11 |- (((S` A) e. RR /\ 1 e. RR /\ (1 + 1) e. RR) -> ((S` A) < 1 <-> ((S` A) + (1 + 1)) < (1 + (1 + 1))))
48	47	biimpd 153	. . . . . . . . . 10 |- (((S` A) e. RR /\ 1 e. RR /\ (1 + 1) e. RR) -> ((S` A) < 1 -> ((S` A) + (1 + 1)) < (1 + (1 + 1))))
49	48, 4, 34, 30	syl3anc 857	. . . . . . . . 9 |- (S e. States -> ((S` A) < 1 -> ((S` A) + (1 + 1)) < (1 + (1 + 1))))
50	49	imp 350	. . . . . . . 8 |- ((S e. States /\ (S` A) < 1) -> ((S` A) + (1 + 1)) < (1 + (1 + 1)))
51		lelttrt 5504	. . . . . . . . . 10 |- ((((S` A) + ((S` B) + (S` C))) e. RR /\ ((S` A) + (1 + 1)) e. RR /\ (1 + (1 + 1)) e. RR) -> ((((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1)) /\ ((S` A) + (1 + 1)) < (1 + (1 + 1))) -> ((S` A) + ((S` B) + (S` C))) < (1 + (1 + 1))))
52	4, 29	jctir 293	. . . . . . . . . . 11 |- (S e. States -> ((S` A) e. RR /\ (1 + 1) e. RR))
53		axaddrcl 5252	. . . . . . . . . . 11 |- (((S` A) e. RR /\ (1 + 1) e. RR) -> ((S` A) + (1 + 1)) e. RR)
54	52, 53	syl 10	. . . . . . . . . 10 |- (S e. States -> ((S` A) + (1 + 1)) e. RR)
55	25, 29	readdcl 5314	. . . . . . . . . . 11 |- (1 + (1 + 1)) e. RR
56	55	a1i 8	. . . . . . . . . 10 |- (S e. States -> (1 + (1 + 1)) e. RR)
57	51, 19, 54, 56	syl3anc 857	. . . . . . . . 9 |- (S e. States -> ((((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1)) /\ ((S` A) + (1 + 1)) < (1 + (1 + 1))) -> ((S` A) + ((S` B) + (S` C))) < (1 + (1 + 1))))
58	57	adantr 389	. . . . . . . 8 |- ((S e. States /\ (S` A) < 1)