Theorem stadd3 10170

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 5289	. . . 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 10138	. . . . . 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 5327	. . . 4 |- (S e. States -> (S` A) e. CC)
6		stle.2	. . . . . 6 |- B e. CH
7		stclt 10138	. . . . . 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 5327	. . . 4 |- (S e. States -> (S` B) e. CC)
10		stm1add3.3	. . . . . 6 |- C e. CH
11		stclt 10138	. . . . . 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 5327	. . . 4 |- (S e. States -> (S` C) e. CC)
14	1, 5, 9, 13	syl3anc 860	. . 3 |- (S e. States -> (((S` A) + (S` B)) + (S` C)) = ((S` A) + ((S` B) + (S` C))))
15	14	eqeq1d 1486	. 2 |- (S e. States -> ((((S` A) + (S` B)) + (S` C)) = 3 <-> ((S` A) + ((S` B) + (S` C))) = 3))
16		3re 5983	. . . . . 6 |- 3 e. RR
17		axaddrcl 5284	. . . . . . . 8 |- (((S` A) e. RR /\ ((S` B) + (S` C)) e. RR) -> ((S` A) + ((S` B) + (S` C))) e. RR)
18		axaddrcl 5284	. . . . . . . . 9 |- (((S` B) e. RR /\ (S` C) e. RR) -> ((S` B) + (S` C)) e. RR)
19	18, 8, 12	sylanc 473	. . . . . . . 8 |- (S e. States -> ((S` B) + (S` C)) e. RR)
20	17, 4, 19	sylanc 473	. . . . . . 7 |- (S e. States -> ((S` A) + ((S` B) + (S` C))) e. RR)
21		ltnet 5528	. . . . . . . 8 |- ((((S` A) + ((S` B) + (S` C))) e. RR /\ 3 e. RR /\ ((S` A) + ((S` B) + (S` C))) < 3) -> 3 =/= ((S` A) + ((S` B) + (S` C))))
22	21	3exp 834	. . . . . . 7 |- (((S` A) + ((S` B) + (S` C))) e. RR -> (3 e. RR -> (((S` A) + ((S` B) + (S` C))) < 3 -> 3 =/= ((S` A) + ((S` B) + (S` C))))))
23	20, 22	syl 10	. . . . . 6 |- (S e. States -> (3 e. RR -> (((S` A) + ((S` B) + (S` C))) < 3 -> 3 =/= ((S` A) + ((S` B) + (S` C))))))
24	16, 23	mpi 44	. . . . 5 |- (S e. States -> (((S` A) + ((S` B) + (S` C))) < 3 -> 3 =/= ((S` A) + ((S` B) + (S` C)))))
25	24	necon2bd 1618	. . . 4 |- (S e. States -> (3 = ((S` A) + ((S` B) + (S` C))) -> -. ((S` A) + ((S` B) + (S` C))) < 3))
26		eqcom 1480	. . . 4 |- (((S` A) + ((S` B) + (S` C))) = 3 <-> 3 = ((S` A) + ((S` B) + (S` C))))
27	25, 26	syl5ib 206	. . 3 |- (S e. States -> (((S` A) + ((S` B) + (S` C))) = 3 -> -. ((S` A) + ((S` B) + (S` C))) < 3))
28		1re 5447	. . . . . . . . . . . . 13 |- 1 e. RR
29	8, 28	jctir 293	. . . . . . . . . . . 12 |- (S e. States -> ((S` B) e. RR /\ 1 e. RR))
30		axaddrcl 5284	. . . . . . . . . . . 12 |- (((S` B) e. RR /\ 1 e. RR) -> ((S` B) + 1) e. RR)
31	29, 30	syl 10	. . . . . . . . . . 11 |- (S e. States -> ((S` B) + 1) e. RR)
32	28, 28	readdcl 5346	. . . . . . . . . . . 12 |- (1 + 1) e. RR
33	32	a1i 8	. . . . . . . . . . 11 |- (S e. States -> (1 + 1) e. RR)
34		stle1t 10147	. . . . . . . . . . . . 13 |- (S e. States -> (C e. CH -> (S` C) <_ 1))
35	10, 34	mpi 44	. . . . . . . . . . . 12 |- (S e. States -> (S` C) <_ 1)
36		leadd2t 5638	. . . . . . . . . . . . 13 |- (((S` C) e. RR /\ 1 e. RR /\ (S` B) e. RR) -> ((S` C) <_ 1 <-> ((S` B) + (S` C)) <_ ((S` B) + 1)))
37	28	a1i 8	. . . . . . . . . . . . 13 |- (S e. States -> 1 e. RR)
38	36, 12, 37, 8	syl3anc 860	. . . . . . . . . . . 12 |- (S e. States -> ((S` C) <_ 1 <-> ((S` B) + (S` C)) <_ ((S` B) + 1)))
39	35, 38	mpbid 195	. . . . . . . . . . 11 |- (S e. States -> ((S` B) + (S` C)) <_ ((S` B) + 1))
40		stle1t 10147	. . . . . . . . . . . . 13 |- (S e. States -> (B e. CH -> (S` B) <_ 1))
41	6, 40	mpi 44	. . . . . . . . . . . 12 |- (S e. States -> (S` B) <_ 1)
42		leadd1t 5637	. . . . . . . . . . . . 13 |- (((S` B) e. RR /\ 1 e. RR /\ 1 e. RR) -> ((S` B) <_ 1 <-> ((S` B) + 1) <_ (1 + 1)))
43	42, 8, 37, 37	syl3anc 860	. . . . . . . . . . . 12 |- (S e. States -> ((S` B) <_ 1 <-> ((S` B) + 1) <_ (1 + 1)))
44	41, 43	mpbid 195	. . . . . . . . . . 11 |- (S e. States -> ((S` B) + 1) <_ (1 + 1))
45	19, 31, 33, 39, 44	letrd 5538	. . . . . . . . . 10 |- (S e. States -> ((S` B) + (S` C)) <_ (1 + 1))
46		leadd2t 5638	. . . . . . . . . . 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))))
47	46, 19, 33, 4	syl3anc 860	. . . . . . . . . 10 |- (S e. States -> (((S` B) + (S` C)) <_ (1 + 1) <-> ((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1))))
48	45, 47	mpbid 195	. . . . . . . . 9 |- (S e. States -> ((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1)))
49	48	adantr 391	. . . . . . . 8 |- ((S e. States /\ (S` A) < 1) -> ((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1)))
50		ltadd1t 5635	. . . . . . . . . . 11 |- (((S` A) e. RR /\ 1 e. RR /\ (1 + 1) e. RR) -> ((S` A) < 1 <-> ((S` A) + (1 + 1)) < (1 + (1 + 1))))
51	50	biimpd 153	. . . . . . . . . 10 |- (((S` A) e. RR /\ 1 e. RR /\ (1 + 1) e. RR) -> ((S` A) < 1 -> ((S` A) + (1 + 1)) < (1 + (1 + 1))))
52	51, 4, 37, 33	syl3anc 860	. . . . . . . . 9 |- (S e. States -> ((S` A) < 1 -> ((S` A) + (1 + 1)) < (1 + (1 + 1))))
53	52	imp 350	. . . . . . . 8 |- ((S e. States /\ (S` A) < 1) -> ((S` A) + (1 + 1)) < (1 + (1 + 1)))
54		lelttrt 5535	. . . . . . . . . 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))))
55	4, 32	jctir 293	. . . . . . . . . . 11 |- (S e. States -> ((S` A) e. RR /\ (1 + 1) e. RR))
56		axaddrcl 5284	. . . . . . . . . . 11 |- (