HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem stadd3 5689
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 4072 . . . 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 5672 . . . . . 6 |- (S e. States -> (A e. CH -> (S` A) e. RR))
42, 3mpi 44 . . . . 5 |- (S e. States -> (S` A) e. RR)
54recnd 4099 . . . 4 |- (S e. States -> (S` A) e. CC)
6 stle.2 . . . . . 6 |- B e. CH
7 stclt 5672 . . . . . 6 |- (S e. States -> (B e. CH -> (S` B) e. RR))
86, 7mpi 44 . . . . 5 |- (S e. States -> (S` B) e. RR)
98recnd 4099 . . . 4 |- (S e. States -> (S` B) e. CC)
10 stm1add3.3 . . . . . 6 |- C e. CH
11 stclt 5672 . . . . . 6 |- (S e. States -> (C e. CH -> (S` C) e. RR))
1210, 11mpi 44 . . . . 5 |- (S e. States -> (S` C) e. RR)
1312recnd 4099 . . . 4 |- (S e. States -> (S` C) e. CC)
141, 5, 9, 13syl3anc 629 . . 3 |- (S e. States -> (((S` A) + (S` B)) + (S` C)) = ((S` A) + ((S` B) + (S` C))))
1514cleq1d 1109 . 2 |- (S e. States -> ((((S` A) + (S` B)) + (S` C)) = 3 <-> ((S` A) + ((S` B) + (S` C))) = 3))
16 axaddrcl 4067 . . . . . . 7 |- (((S` A) e. RR /\ ((S` B) + (S` C)) e. RR) -> ((S` A) + ((S` B) + (S` C))) e. RR)
17 axaddrcl 4067 . . . . . . . 8 |- (((S` B) e. RR /\ (S` C) e. RR) -> ((S` B) + (S` C)) e. RR)
1817, 8, 12sylanc 361 . . . . . . 7 |- (S e. States -> ((S` B) + (S` C)) e. RR)
1916, 4, 18sylanc 361 . . . . . 6 |- (S e. States -> ((S` A) + ((S` B) + (S` C))) e. RR)
20 3re 4472 . . . . . 6 |- 3 e. RR
2119, 20jctir 241 . . . . 5 |- (S e. States -> (((S` A) + ((S` B) + (S` C))) e. RR /\ 3 e. RR))
22 ltnet 4282 . . . . 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 12 . . . 4 |- (S e. States -> (((S` A) + ((S` B) + (S` C))) < 3 -> -. ((S` A) + ((S` B) + (S` C))) = 3))
2423con2d 83 . . 3 |- (S e. States -> (((S` A) + ((S` B) + (S` C))) = 3 -> -. ((S` A) + ((S` B) + (S` C))) < 3))
25 letrt 4291 . . . . . . . . . . 11 |- ((((S` B) + (S` C)) e. RR /\ ((S` B) + 1) e. RR /\ (1 + 1) e. RR) -> ((((S` B) + (S` C)) <_ ((S` B) + 1) /\ ((S` B) + 1) <_ (1 + 1)) -> ((S` B) + (S` C)) <_ (1 + 1)))
26 ax1re 4064 . . . . . . . . . . . . . 14 |- 1 e. RR
278, 26jctir 241 . . . . . . . . . . . . 13 |- (S e. States -> ((S` B) e. RR /\ 1 e. RR))
28 axaddrcl 4067 . . . . . . . . . . . . 13 |- (((S` B) e. RR /\ 1 e. RR) -> ((S` B) + 1) e. RR)
2927, 28syl 12 . . . . . . . . . . . 12 |- (S e. States -> ((S` B) + 1) e. RR)
3026, 26readdcl 4118 . . . . . . . . . . . . 13 |- (1 + 1) e. RR
3130a1i 7 . . . . . . . . . . . 12 |- (S e. States -> (1 + 1) e. RR)
3218, 29, 313jca 604 . . . . . . . . . . 11 |- (S e. States -> (((S` B) + (S` C)) e. RR /\ ((S` B) + 1) e. RR /\ (1 + 1) e. RR))
33 stle1t 5674 . . . . . . . . . . . . . 14 |- (S e. States -> (C e. CH -> (S` C) <_ 1))
3410, 33mpi 44 . . . . . . . . . . . . 13 |- (S e. States -> (S` C) <_ 1)
35 leadd2t 4351 . . . . . . . . . . . . . 14 |- (((S` C) e. RR /\ 1 e. RR /\ (S` B) e. RR) -> ((S` C) <_ 1 <-> ((S` B) + (S` C)) <_ ((S` B) + 1)))
3626a1i 7 . . . . . . . . . . . . . 14 |- (S e. States -> 1 e. RR)
3735, 12, 36, 8syl3anc 629 . . . . . . . . . . . . 13 |- (S e. States -> ((S` C) <_ 1 <-> ((S` B) + (S` C)) <_ ((S` B) + 1)))
3834, 37mpbid 170 . . . . . . . . . . . 12 |- (S e. States -> ((S` B) + (S` C)) <_ ((S` B) + 1))
39 stle1t 5674 . . . . . . . . . . . . . 14 |- (S e. States -> (B e. CH -> (S` B) <_ 1))
406, 39mpi 44 . . . . . . . . . . . . 13 |- (S e. States -> (S` B) <_ 1)
41 leadd1t 4350 . . . . . . . . . . . . . 14 |- (((S` B) e. RR /\ 1 e. RR /\ 1 e. RR) -> ((S` B) <_ 1 <-> ((S` B) + 1) <_ (1 + 1)))
4241, 8, 36, 36syl3anc 629 . . . . . . . . . . . . 13 |- (S e. States -> ((S` B) <_ 1 <-> ((S` B) + 1) <_ (1 + 1)))
4340, 42mpbid 170 . . . . . . . . . . . 12 |- (S e. States -> ((S` B) + 1) <_ (1 + 1))
4438, 43jca 236 . . . . . . . . . . 11 |- (S e. States -> (((S` B) + (S` C)) <_ ((S` B) + 1) /\ ((S` B) + 1) <_ (1 + 1)))
4525, 32, 44sylc 62 . . . . . . . . . 10 |- (S e. States -> ((S` B) + (S` C)) <_ (1 + 1))
46 leadd2t 4351 . . . . . . . . . . 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))))
4746, 18, 31, 4syl3anc 629 . . . . . . . . . 10 |- (S e. States -> (((S` B) + (S` C)) <_ (1 + 1) <-> ((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1))))
4845, 47mpbid 170 . . . . . . . . 9 |- (S e. States -> ((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1)))
4948adantr 306 . . . . . . . 8 |- ((S e. States /\ (S` A) < 1) -> ((S` A) + ((S` B) + (S` C))) <_ ((S` A) + (1 + 1)))
50 ltadd1t 4348 . . . . . . . . . . 11 |- (((S` A) e. RR /\ 1 e. RR /\ (1 + 1) e. RR) -> ((S` A) < 1 <-> ((S` A) + (1 + 1)) < (1 + (1 + 1))))
5150biimpd 135 . . . . . . . . . 10 |- (((S` A) e. RR /\ 1 e. RR /\ (1 + 1) e. RR) -> ((S` A) < 1 -> ((S` A) + (1 + 1)) < (1 + (1 + 1))))
5251, 4, 36, 31syl3anc 629 . . . . . . . . 9 |- (S e. States -> ((S` A) < 1 -> ((S` A) + (1 + 1)) < (1 + (1 + 1))))
5352imp 277 . . . . . . . 8 |- ((S e. States /\ (S` A) < 1) -> ((S` A) + (1 + 1)) < (1 + (1 + 1)))
54 lelttrt 4289 . . . . . . . . . 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))))
554, 30jctir 241 . . . . . . . . . . 11 |- (S e. States -> ((S` A) e. RR /\ (1 + 1) e. RR))
56 axaddrcl 4067 . . . . . . . . . . 11 |- (((S` A) e. RR /\ (1 + 1) e. RR) -> ((S` A) + (1 + 1)) e. RR)
5755, 56syl 12 . . . . . . . . . 10 |- (S e. States -> ((S` A) + (1 + 1)) e. RR)
5826, 30readdcl 4118 . . . . . . . . . . 11 |- (1 + (1 + 1)) e. RR
5958a1i 7 . . . . . . . . . 10 |- (S