Proof of Theorem stoweidlem22
Step | Hyp | Ref
| Expression |
1 | | stoweidlem22.8 |
. . . 4
|
2 | | stoweidlem22.9 |
. . . . 5
|
3 | 2 | nfel1 2779 |
. . . 4
|
4 | | stoweidlem22.10 |
. . . . 5
|
5 | 4 | nfel1 2779 |
. . . 4
|
6 | 1, 3, 5 | nf3an 1831 |
. . 3
|
7 | | simpr 477 |
. . . . . . 7
|
8 | | simpl1 1064 |
. . . . . . . . . 10
|
9 | | stoweidlem22.2 |
. . . . . . . . . . . 12
|
10 | | neg1rr 11125 |
. . . . . . . . . . . . 13
|
11 | | stoweidlem22.7 |
. . . . . . . . . . . . . 14
|
12 | 11 | stoweidlem4 40221 |
. . . . . . . . . . . . 13
|
13 | 10, 12 | mpan2 707 |
. . . . . . . . . . . 12
|
14 | 9, 13 | syl5eqel 2705 |
. . . . . . . . . . 11
|
15 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
16 | 15 | anbi2d 740 |
. . . . . . . . . . . . . 14
|
17 | | feq1 6026 |
. . . . . . . . . . . . . 14
|
18 | 16, 17 | imbi12d 334 |
. . . . . . . . . . . . 13
|
19 | | stoweidlem22.4 |
. . . . . . . . . . . . 13
|
20 | 18, 19 | vtoclg 3266 |
. . . . . . . . . . . 12
|
21 | 20 | anabsi7 860 |
. . . . . . . . . . 11
|
22 | 14, 21 | mpdan 702 |
. . . . . . . . . 10
|
23 | 8, 22 | syl 17 |
. . . . . . . . 9
|
24 | 23, 7 | ffvelrnd 6360 |
. . . . . . . 8
|
25 | | simpl3 1066 |
. . . . . . . . 9
|
26 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
27 | 26 | anbi2d 740 |
. . . . . . . . . . . . . 14
|
28 | | feq1 6026 |
. . . . . . . . . . . . . 14
|
29 | 27, 28 | imbi12d 334 |
. . . . . . . . . . . . 13
|
30 | 29, 19 | vtoclg 3266 |
. . . . . . . . . . . 12
|
31 | 30 | anabsi7 860 |
. . . . . . . . . . 11
|
32 | 31 | 3adant3 1081 |
. . . . . . . . . 10
|
33 | | simp3 1063 |
. . . . . . . . . 10
|
34 | 32, 33 | ffvelrnd 6360 |
. . . . . . . . 9
|
35 | 8, 25, 7, 34 | syl3anc 1326 |
. . . . . . . 8
|
36 | 24, 35 | remulcld 10070 |
. . . . . . 7
|
37 | | stoweidlem22.3 |
. . . . . . . 8
|
38 | 37 | fvmpt2 6291 |
. . . . . . 7
|
39 | 7, 36, 38 | syl2anc 693 |
. . . . . 6
|
40 | 9 | fvmpt2 6291 |
. . . . . . . . 9
|
41 | 10, 40 | mpan2 707 |
. . . . . . . 8
|
42 | 41 | adantl 482 |
. . . . . . 7
|
43 | 42 | oveq1d 6665 |
. . . . . 6
|
44 | 35 | recnd 10068 |
. . . . . . 7
|
45 | 44 | mulm1d 10482 |
. . . . . 6
|
46 | 39, 43, 45 | 3eqtrd 2660 |
. . . . 5
|
47 | 46 | oveq2d 6666 |
. . . 4
|
48 | | simpl2 1065 |
. . . . . . . 8
|
49 | | eleq1 2689 |
. . . . . . . . . . . 12
|
50 | 49 | anbi2d 740 |
. . . . . . . . . . 11
|
51 | | feq1 6026 |
. . . . . . . . . . 11
|
52 | 50, 51 | imbi12d 334 |
. . . . . . . . . 10
|
53 | 52, 19 | vtoclg 3266 |
. . . . . . . . 9
|
54 | 53 | anabsi7 860 |
. . . . . . . 8
|
55 | 8, 48, 54 | syl2anc 693 |
. . . . . . 7
|
56 | 55, 7 | ffvelrnd 6360 |
. . . . . 6
|
57 | 56 | recnd 10068 |
. . . . 5
|
58 | 57, 44 | negsubd 10398 |
. . . 4
|
59 | 47, 58 | eqtr2d 2657 |
. . 3
|
60 | 6, 59 | mpteq2da 4743 |
. 2
|
61 | 14 | 3ad2ant1 1082 |
. . . . 5
|
62 | | nfmpt1 4747 |
. . . . . . . 8
|
63 | 9, 62 | nfcxfr 2762 |
. . . . . . 7
|
64 | 63 | nfeq2 2780 |
. . . . . 6
|
65 | 4 | nfeq2 2780 |
. . . . . 6
|
66 | | stoweidlem22.6 |
. . . . . 6
|
67 | 64, 65, 66 | stoweidlem6 40223 |
. . . . 5
|
68 | 61, 67 | syld3an2 1373 |
. . . 4
|
69 | 37, 68 | syl5eqel 2705 |
. . 3
|
70 | | stoweidlem22.5 |
. . . 4
|
71 | | nfmpt1 4747 |
. . . . 5
|
72 | 37, 71 | nfcxfr 2762 |
. . . 4
|
73 | 70, 2, 72 | stoweidlem8 40225 |
. . 3
|
74 | 69, 73 | syld3an3 1371 |
. 2
|
75 | 60, 74 | eqeltrd 2701 |
1
|