HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem stadd3 10085
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
StepHypRef Expression
1 axaddass 5249 . . . 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 10053 . . . . . 6 |- (S e. States -> (A e. CH -> (S` A) e. RR))
42, 3mpi 44 . . . . 5 |- (S e. States -> (S` A) e. RR)
54recnd 5287 . . . 4 |- (S e. States -> (S` A) e. CC)
6 stle.2 . . . . . 6 |- B e. CH
7 stclt 10053 . . . . . 6 |- (S e. States -> (B e. CH -> (S` B) e. RR))
86, 7mpi 44 . . . . 5 |- (S e. States -> (S` B) e. RR)
98recnd 5287 . . . 4 |- (S e. States -> (S` B) e. CC)
10 stm1add3.3 . . . . . 6 |- C e. CH
11 stclt 10053 . . . . . 6 |- (S e. States -> (C e. CH -> (S` C) e. RR))
1210, 11mpi 44 . . . . 5 |- (S e. States -> (S` C) e. RR)
1312recnd 5287 . . . 4 |- (S e. States -> (S` C) e. CC)
141, 5, 9, 13syl3anc 856 . . 3 |- (S e. States -> (((S` A) + (S` B)) + (S` C)) = ((S` A) + ((S` B) + (S` C))))
1514eqeq1d 1475 . 2 |- (S e. States -> ((((S` A) + (S` B)) + (S` C)) = 3 <-> ((S` A) + ((S` B) + (S` C))) = 3))
16 axaddrcl 5244 . . . . . . 7 |- (((S` A) e. RR /\ ((S` B) + (S` C)) e. RR) -> ((S` A) + ((S` B) + (S` C))) e. RR)
17 axaddrcl 5244 . . . . . . . 8 |- (((S` B) e. RR /\ (S` C) e. RR) -> ((S` B) + (S` C)) e. RR)
1817, 8, 12sylanc 471 . . . . . . 7 |- (S e. States -> ((S` B) + (S` C)) e. RR)
1916, 4, 18sylanc 471 . . . . . 6 |- (S e. States -> ((S` A) + ((S` B) + (S` C))) e. RR)
20 3re 5928 . . . . . 6 |- 3 e. RR
2119, 20jctir 293 . . . . 5 |- (S e. States -> (((S` A) + ((S` B) + (S` C))) e. RR /\ 3 e. RR))
22 ltnetOLD 5489 . . . . 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))
2321, 22syl 10 . . . 4 |- (S e. States -> (((S` A) + ((S` B) + (S` C))) < 3 -> -. ((S` A) + ((S` B) + (S` C))) = 3))
2423con2d 91 . . 3 |- (S e. States -> (((S` A) + ((S` B) + (S` C))) = 3 -> -. ((S` A) + ((S` B) + (S` C))) < 3))
25 1re 5407 . . . . . . . . . . . . 13 |- 1 e. RR
268, 25jctir 293 . . . . . . . . . . . 12 |- (S e. States -> ((S` B) e. RR /\ 1 e. RR))
27 axaddrcl 5244 . . . . . . . . . . . 12 |- (((S` B) e. RR /\ 1 e. RR) -> ((S` B) + 1) e. RR)
2826, 27syl 10 . . . . . . . . . . 11 |- (S e. States -> ((S` B) + 1) e. RR)
2925, 25readdcl 5306 . . . . . . . . . . . 12 |- (1 + 1) e. RR
3029a1i 8 . . . . . . . . . . 11 |- (S e. States -> (1 + 1) e. RR)
31 stle1t 10062 . . . . . . . . . . . . 13 |- (S e. States -> (C e. CH -> (S` C) <_ 1))
3210, 31mpi 44 . . . . . . . . . . . 12 |- (S e. States -> (S` C) <_ 1)
33 leadd2t 5600 . . . . . . . . . . . . 13 |- (((S` C) e. RR /\ 1 e. RR /\ (S` B) e. RR) -> ((S` C) <_ 1 <-> ((S` B) + (S` C)) <_ ((S` B) + 1)))
3425a1i 8 . . . . . . . . . . . . 13 |- (S e. States -> 1 e. RR)
3533, 12, 34, 8syl3anc 856 . . . . . . . . . . . 12 |- (S e. States -> ((S` C) <_ 1 <-> ((S` B) + (S` C)) <_ ((S` B) + 1)))
3632, 35mpbid 195 . . . . . . . . . . 11 |- (S e. States -> ((S` B) + (S` C)) <_ ((S` B) + 1))
37 stle1t 10062 . . . . . . . . . . . . 13 |- (S e. States -> (B e. CH -> (S` B) <_ 1))
386, 37mpi 44 . . . . . . . . . . . 12 |- (S e. States -> (S` B) <_ 1)
39 leadd1t 5599 . . . . . . . . . . . . 13 |- (((S` B) e. RR /\ 1 e. RR /\ 1 e. RR) -> ((S` B) <_ 1 <-> ((S` B) + 1) <_ (1 + 1)))
4039, 8, 34, 34syl3anc 856 . . . . . . . . . . . 12 |- (S e. States -> ((S` B) <_ 1 <-> ((S` B) + 1) <_ (1 + 1)))
4138, 40mpbid 195 . . . . . . . . . . 11 |- (S e. States -> ((S` B) + 1) <_ (1 + 1))
4218, 28, 30, 36, 41letrd 5499 . . . . . . . . . 10 |- (S e. States -> ((S` B) + (S` C)) <_ (1 + 1))
43 leadd2t 5600 . . . . . . . . . . 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))))
4443, 18, 30, 4syl3anc 856 . . . . . . . . . 10 |- (S e. States -> (((S` B) + (S` C)) <_ (1 + 1) <-> ((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1))))
4542, 44mpbid 195 . . . . . . . . 9 |- (S e. States -> ((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1)))
4645adantr 389 . . . . . . . 8 |- ((S e. States /\ (S` A) < 1) -> ((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1)))
47 ltadd1t 5597 . . . . . . . . . . 11 |- (((S` A) e. RR /\ 1 e. RR /\ (1 + 1) e. RR) -> ((S` A) < 1 <-> ((S` A) + (1 + 1)) < (1 + (1 + 1))))
4847biimpd 153 . . . . . . . . . 10 |- (((S` A) e. RR /\ 1 e. RR /\ (1 + 1) e. RR) -> ((S` A) < 1 -> ((S` A) + (1 + 1)) < (1 + (1 + 1))))
4948, 4, 34, 30syl3anc 856 . . . . . . . . 9 |- (S e. States -> ((S` A) < 1 -> ((S` A) + (1 + 1)) < (1 + (1 + 1))))
5049imp 350 . . . . . . . 8 |- ((S e. States /\ (S` A) < 1) -> ((S` A) + (1 + 1)) < (1 + (1 + 1)))
51 lelttrt 5496 . . . . . . . . . 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))))
524, 29jctir 293 . . . . . . . . . . 11 |- (S e. States -> ((S` A) e. RR /\ (1 + 1) e. RR))
53 axaddrcl 5244 . . . . . . . . . . 11 |- (((S` A) e. RR /\ (1 + 1) e. RR) -> ((S` A) + (1 + 1)) e. RR)
5452, 53syl 10 . . . . . . . . . 10 |- (S e. States -> ((S` A) + (1 + 1)) e. RR)
5525, 29readdcl 5306 . . . . . . . . . . 11 |- (1 + (1 + 1)) e. RR
5655a1i 8 . . . . . . . . . 10 |- (S e. States -> (1 + (1 + 1)) e. RR)
5751, 19, 54, 56syl3anc 856 . . . . . . . . 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))))
5857adantr 389 . . . . . . . 8 |- ((S e. States /\ (S` A) < 1)