Metamath Proof Explorer


Theorem staddi

Description: If the sum of 2 states is 2, then each state is 1. (Contributed by NM, 12-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypotheses stle.1 A C
stle.2 B C
Assertion staddi S States S A + S B = 2 S A = 1

Proof

Step Hyp Ref Expression
1 stle.1 A C
2 stle.2 B C
3 stcl S States A C S A
4 1 3 mpi S States S A
5 stcl S States B C S B
6 2 5 mpi S States S B
7 4 6 readdcld S States S A + S B
8 ltne S A + S B S A + S B < 2 2 S A + S B
9 8 necomd S A + S B S A + S B < 2 S A + S B 2
10 7 9 sylan S States S A + S B < 2 S A + S B 2
11 10 ex S States S A + S B < 2 S A + S B 2
12 11 necon2bd S States S A + S B = 2 ¬ S A + S B < 2
13 1re 1
14 13 a1i S States 1
15 stle1 S States B C S B 1
16 2 15 mpi S States S B 1
17 6 14 4 16 leadd2dd S States S A + S B S A + 1
18 17 adantr S States S A < 1 S A + S B S A + 1
19 ltadd1 S A 1 1 S A < 1 S A + 1 < 1 + 1
20 19 biimpd S A 1 1 S A < 1 S A + 1 < 1 + 1
21 4 14 14 20 syl3anc S States S A < 1 S A + 1 < 1 + 1
22 21 imp S States S A < 1 S A + 1 < 1 + 1
23 readdcl S A 1 S A + 1
24 4 13 23 sylancl S States S A + 1
25 13 13 readdcli 1 + 1
26 25 a1i S States 1 + 1
27 lelttr S A + S B S A + 1 1 + 1 S A + S B S A + 1 S A + 1 < 1 + 1 S A + S B < 1 + 1
28 7 24 26 27 syl3anc S States S A + S B S A + 1 S A + 1 < 1 + 1 S A + S B < 1 + 1
29 28 adantr S States S A < 1 S A + S B S A + 1 S A + 1 < 1 + 1 S A + S B < 1 + 1
30 18 22 29 mp2and S States S A < 1 S A + S B < 1 + 1
31 df-2 2 = 1 + 1
32 30 31 breqtrrdi S States S A < 1 S A + S B < 2
33 32 ex S States S A < 1 S A + S B < 2
34 33 con3d S States ¬ S A + S B < 2 ¬ S A < 1
35 stle1 S States A C S A 1
36 1 35 mpi S States S A 1
37 leloe S A 1 S A 1 S A < 1 S A = 1
38 4 13 37 sylancl S States S A 1 S A < 1 S A = 1
39 36 38 mpbid S States S A < 1 S A = 1
40 39 ord S States ¬ S A < 1 S A = 1
41 12 34 40 3syld S States S A + S B = 2 S A = 1