Metamath Proof Explorer


Theorem strlem5

Description: Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypotheses strlem3.1 S = x C norm proj x u 2
strlem3.2 φ u A B norm u = 1
strlem3.3 A C
strlem3.4 B C
Assertion strlem5 φ S B < 1

Proof

Step Hyp Ref Expression
1 strlem3.1 S = x C norm proj x u 2
2 strlem3.2 φ u A B norm u = 1
3 strlem3.3 A C
4 strlem3.4 B C
5 1 strlem2 B C S B = norm proj B u 2
6 4 5 ax-mp S B = norm proj B u 2
7 eldif u A B u A ¬ u B
8 3 cheli u A u
9 pjnel B C u ¬ u B norm proj B u < norm u
10 4 9 mpan u ¬ u B norm proj B u < norm u
11 10 biimpa u ¬ u B norm proj B u < norm u
12 8 11 sylan u A ¬ u B norm proj B u < norm u
13 7 12 sylbi u A B norm proj B u < norm u
14 breq2 norm u = 1 norm proj B u < norm u norm proj B u < 1
15 13 14 syl5ib norm u = 1 u A B norm proj B u < 1
16 15 impcom u A B norm u = 1 norm proj B u < 1
17 eldifi u A B u A
18 4 pjhcli u proj B u
19 normcl proj B u norm proj B u
20 18 19 syl u norm proj B u
21 normge0 proj B u 0 norm proj B u
22 18 21 syl u 0 norm proj B u
23 1re 1
24 0le1 0 1
25 lt2sq norm proj B u 0 norm proj B u 1 0 1 norm proj B u < 1 norm proj B u 2 < 1 2
26 23 24 25 mpanr12 norm proj B u 0 norm proj B u norm proj B u < 1 norm proj B u 2 < 1 2
27 20 22 26 syl2anc u norm proj B u < 1 norm proj B u 2 < 1 2
28 17 8 27 3syl u A B norm proj B u < 1 norm proj B u 2 < 1 2
29 28 adantr u A B norm u = 1 norm proj B u < 1 norm proj B u 2 < 1 2
30 16 29 mpbid u A B norm u = 1 norm proj B u 2 < 1 2
31 6 30 eqbrtrid u A B norm u = 1 S B < 1 2
32 sq1 1 2 = 1
33 31 32 breqtrdi u A B norm u = 1 S B < 1
34 2 33 sylbi φ S B < 1