Metamath Proof Explorer


Theorem axcontlem8

Description: Lemma for axcont . A point in D is between two others if its function value falls in the middle. (Contributed by Scott Fenton, 18-Jun-2013)

Ref Expression
Hypotheses axcontlem8.1 D = p 𝔼 N | U Btwn Z p p Btwn Z U
axcontlem8.2 F = x t | x D t 0 +∞ i 1 N x i = 1 t Z i + t U i
Assertion axcontlem8 N Z 𝔼 N U 𝔼 N Z U P D Q D R D F P F Q F Q F R Q Btwn P R

Proof

Step Hyp Ref Expression
1 axcontlem8.1 D = p 𝔼 N | U Btwn Z p p Btwn Z U
2 axcontlem8.2 F = x t | x D t 0 +∞ i 1 N x i = 1 t Z i + t U i
3 1 2 axcontlem6 N Z 𝔼 N U 𝔼 N Z U P D F P 0 +∞ i 1 N P i = 1 F P Z i + F P U i
4 3 ex N Z 𝔼 N U 𝔼 N Z U P D F P 0 +∞ i 1 N P i = 1 F P Z i + F P U i
5 1 2 axcontlem6 N Z 𝔼 N U 𝔼 N Z U Q D F Q 0 +∞ i 1 N Q i = 1 F Q Z i + F Q U i
6 5 ex N Z 𝔼 N U 𝔼 N Z U Q D F Q 0 +∞ i 1 N Q i = 1 F Q Z i + F Q U i
7 1 2 axcontlem6 N Z 𝔼 N U 𝔼 N Z U R D F R 0 +∞ i 1 N R i = 1 F R Z i + F R U i
8 7 ex N Z 𝔼 N U 𝔼 N Z U R D F R 0 +∞ i 1 N R i = 1 F R Z i + F R U i
9 4 6 8 3anim123d N Z 𝔼 N U 𝔼 N Z U P D Q D R D F P 0 +∞ i 1 N P i = 1 F P Z i + F P U i F Q 0 +∞ i 1 N Q i = 1 F Q Z i + F Q U i F R 0 +∞ i 1 N R i = 1 F R Z i + F R U i
10 9 imp N Z 𝔼 N U 𝔼 N Z U P D Q D R D F P 0 +∞ i 1 N P i = 1 F P Z i + F P U i F Q 0 +∞ i 1 N Q i = 1 F Q Z i + F Q U i F R 0 +∞ i 1 N R i = 1 F R Z i + F R U i
11 10 adantr N Z 𝔼 N U 𝔼 N Z U P D Q D R D F P F Q F Q F R F P 0 +∞ i 1 N P i = 1 F P Z i + F P U i F Q 0 +∞ i 1 N Q i = 1 F Q Z i + F Q U i F R 0 +∞ i 1 N R i = 1 F R Z i + F R U i
12 3an6 F P 0 +∞ i 1 N P i = 1 F P Z i + F P U i F Q 0 +∞ i 1 N Q i = 1 F Q Z i + F Q U i F R 0 +∞ i 1 N R i = 1 F R Z i + F R U i F P 0 +∞ F Q 0 +∞ F R 0 +∞ i 1 N P i = 1 F P Z i + F P U i i 1 N Q i = 1 F Q Z i + F Q U i i 1 N R i = 1 F R Z i + F R U i
13 0elunit 0 0 1
14 simplr1 N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F P 0 +∞
15 14 ad2antlr F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F P 0 +∞
16 elrege0 F P 0 +∞ F P 0 F P
17 16 simplbi F P 0 +∞ F P
18 15 17 syl F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F P
19 18 recnd F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F P
20 simprrl F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F P F Q
21 20 adantr F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F P F Q
22 simprrr F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F Q F R
23 simpl F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F P = F R
24 22 23 breqtrrd F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F Q F P
25 24 adantr F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F Q F P
26 simplr2 N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F Q 0 +∞
27 26 ad2antlr F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F Q 0 +∞
28 elrege0 F Q 0 +∞ F Q 0 F Q
29 28 simplbi F Q 0 +∞ F Q
30 27 29 syl F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F Q
31 18 30 letri3d F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F P = F Q F P F Q F Q F P
32 21 25 31 mpbir2and F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F P = F Q
33 simpll F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F P = F R
34 simpll2 N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ Z 𝔼 N
35 34 adantr N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R Z 𝔼 N
36 35 ad2antlr F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N Z 𝔼 N
37 fveecn Z 𝔼 N i 1 N Z i
38 36 37 sylancom F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N Z i
39 simpll3 N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ U 𝔼 N
40 39 adantr N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R U 𝔼 N
41 40 ad2antlr F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N U 𝔼 N
42 fveecn U 𝔼 N i 1 N U i
43 41 42 sylancom F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N U i
44 ax-1cn 1
45 simpl F P Z i U i F P
46 subcl 1 F P 1 F P
47 44 45 46 sylancr F P Z i U i 1 F P
48 simprl F P Z i U i Z i
49 47 48 mulcld F P Z i U i 1 F P Z i
50 mulcl F P U i F P U i
51 50 adantrl F P Z i U i F P U i
52 49 51 addcld F P Z i U i 1 F P Z i + F P U i
53 52 mulid2d F P Z i U i 1 1 F P Z i + F P U i = 1 F P Z i + F P U i
54 52 mul02d F P Z i U i 0 1 F P Z i + F P U i = 0
55 53 54 oveq12d F P Z i U i 1 1 F P Z i + F P U i + 0 1 F P Z i + F P U i = 1 F P Z i + F P U i + 0
56 52 addid1d F P Z i U i 1 F P Z i + F P U i + 0 = 1 F P Z i + F P U i
57 55 56 eqtr2d F P Z i U i 1 F P Z i + F P U i = 1 1 F P Z i + F P U i + 0 1 F P Z i + F P U i
58 57 3adant2 F P F P = F Q F P = F R Z i U i 1 F P Z i + F P U i = 1 1 F P Z i + F P U i + 0 1 F P Z i + F P U i
59 oveq2 F P = F Q 1 F P = 1 F Q
60 59 oveq1d F P = F Q 1 F P Z i = 1 F Q Z i
61 oveq1 F P = F Q F P U i = F Q U i
62 60 61 oveq12d F P = F Q 1 F P Z i + F P U i = 1 F Q Z i + F Q U i
63 oveq2 F P = F R 1 F P = 1 F R
64 63 oveq1d F P = F R 1 F P Z i = 1 F R Z i
65 oveq1 F P = F R F P U i = F R U i
66 64 65 oveq12d F P = F R 1 F P Z i + F P U i = 1 F R Z i + F R U i
67 66 oveq2d F P = F R 0 1 F P Z i + F P U i = 0 1 F R Z i + F R U i
68 67 oveq2d F P = F R 1 1 F P Z i + F P U i + 0 1 F P Z i + F P U i = 1 1 F P Z i + F P U i + 0 1 F R Z i + F R U i
69 62 68 eqeqan12d F P = F Q F P = F R 1 F P Z i + F P U i = 1 1 F P Z i + F P U i + 0 1 F P Z i + F P U i 1 F Q Z i + F Q U i = 1 1 F P Z i + F P U i + 0 1 F R Z i + F R U i
70 69 3ad2ant2 F P F P = F Q F P = F R Z i U i 1 F P Z i + F P U i = 1 1 F P Z i + F P U i + 0 1 F P Z i + F P U i 1 F Q Z i + F Q U i = 1 1 F P Z i + F P U i + 0 1 F R Z i + F R U i
71 58 70 mpbid F P F P = F Q F P = F R Z i U i 1 F Q Z i + F Q U i = 1 1 F P Z i + F P U i + 0 1 F R Z i + F R U i
72 19 32 33 38 43 71 syl122anc F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N 1 F Q Z i + F Q U i = 1 1 F P Z i + F P U i + 0 1 F R Z i + F R U i
73 72 ralrimiva F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N 1 F Q Z i + F Q U i = 1 1 F P Z i + F P U i + 0 1 F R Z i + F R U i
74 oveq2 t = 0 1 t = 1 0
75 1m0e1 1 0 = 1
76 74 75 syl6eq t = 0 1 t = 1
77 76 oveq1d t = 0 1 t 1 F P Z i + F P U i = 1 1 F P Z i + F P U i
78 oveq1 t = 0 t 1 F R Z i + F R U i = 0 1 F R Z i + F R U i
79 77 78 oveq12d t = 0 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i = 1 1 F P Z i + F P U i + 0 1 F R Z i + F R U i
80 79 eqeq2d t = 0 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i 1 F Q Z i + F Q U i = 1 1 F P Z i + F P U i + 0 1 F R Z i + F R U i
81 80 ralbidv t = 0 i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i i 1 N 1 F Q Z i + F Q U i = 1 1 F P Z i + F P U i + 0 1 F R Z i + F R U i
82 81 rspcev 0 0 1 i 1 N 1 F Q Z i + F Q U i = 1 1 F P Z i + F P U i + 0 1 F R Z i + F R U i t 0 1 i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
83 13 73 82 sylancr F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R t 0 1 i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
84 83 ex F P = F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R t 0 1 i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
85 26 adantl F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F Q 0 +∞
86 85 29 syl F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F Q
87 simplr3 N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F R 0 +∞
88 87 adantl F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F R 0 +∞
89 elrege0 F R 0 +∞ F R 0 F R
90 89 simplbi F R 0 +∞ F R
91 88 90 syl F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F R
92 14 adantl F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F P 0 +∞
93 92 17 syl F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F P
94 simprrr F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F Q F R
95 86 91 93 94 lesub1dd F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F Q F P F R F P
96 86 93 resubcld F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F Q F P
97 simprrl F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F P F Q
98 86 93 subge0d F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R 0 F Q F P F P F Q
99 97 98 mpbird F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R 0 F Q F P
100 91 93 resubcld F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F R F P
101 93 86 91 97 94 letrd F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F P F R
102 simpl F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F P F R
103 102 necomd F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F R F P
104 93 91 101 103 leneltd F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F P < F R
105 93 91 posdifd F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F P < F R 0 < F R F P
106 104 105 mpbid F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R 0 < F R F P
107 divelunit F Q F P 0 F Q F P F R F P 0 < F R F P F Q F P F R F P 0 1 F Q F P F R F P
108 96 99 100 106 107 syl22anc F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F Q F P F R F P 0 1 F Q F P F R F P
109 95 108 mpbird F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R F Q F P F R F P 0 1
110 14 ad2antlr F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F P 0 +∞
111 17 recnd F P 0 +∞ F P
112 110 111 syl F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F P
113 simpll F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F P F R
114 26 ad2antlr F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F Q 0 +∞
115 29 recnd F Q 0 +∞ F Q
116 114 115 syl F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F Q
117 87 ad2antlr F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F R 0 +∞
118 90 recnd F R 0 +∞ F R
119 117 118 syl F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N F R
120 34 ad2antrl F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R Z 𝔼 N
121 120 37 sylan F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N Z i
122 39 ad2antrl F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R U 𝔼 N
123 122 42 sylan F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N U i
124 simp2r F P F P F R F Q F R Z i U i F R
125 simp2l F P F P F R F Q F R Z i U i F Q
126 124 125 subcld F P F P F R F Q F R Z i U i F R F Q
127 simp1l F P F P F R F Q F R Z i U i F P
128 44 127 46 sylancr F P F P F R F Q F R Z i U i 1 F P
129 126 128 mulcld F P F P F R F Q F R Z i U i F R F Q 1 F P
130 125 127 subcld F P F P F R F Q F R Z i U i F Q F P
131 subcl 1 F R 1 F R
132 44 124 131 sylancr F P F P F R F Q F R Z i U i 1 F R
133 130 132 mulcld F P F P F R F Q F R Z i U i F Q F P 1 F R
134 124 127 subcld F P F P F R F Q F R Z i U i F R F P
135 simp1r F P F P F R F Q F R Z i U i F P F R
136 135 necomd F P F P F R F Q F R Z i U i F R F P
137 124 127 136 subne0d F P F P F R F Q F R Z i U i F R F P 0
138 129 133 134 137 divdird F P F P F R F Q F R Z i U i F R F Q 1 F P + F Q F P 1 F R F R F P = F R F Q 1 F P F R F P + F Q F P 1 F R F R F P
139 134 mulid1d F P F P F R F Q F R Z i U i F R F P 1 = F R F P
140 134 125 mulcomd F P F P F R F Q F R Z i U i F R F P F Q = F Q F R F P
141 125 124 127 subdid F P F P F R F Q F R Z i U i F Q F R F P = F Q F R F Q F P
142 140 141 eqtrd F P F P F R F Q F R Z i U i F R F P F Q = F Q F R F Q F P
143 139 142 oveq12d F P F P F R F Q F R Z i U i F R F P 1 F R F P F Q = F R - F P - F Q F R F Q F P
144 subdi F R F P 1 F Q F R F P 1 F Q = F R F P 1 F R F P F Q
145 44 144 mp3an2 F R F P F Q F R F P 1 F Q = F R F P 1 F R F P F Q
146 134 125 145 syl2anc F P F P F R F Q F R Z i U i F R F P 1 F Q = F R F P 1 F R F P F Q
147 subdi F R F Q 1 F P F R F Q 1 F P = F R F Q 1 F R F Q F P
148 44 147 mp3an2 F R F Q F P F R F Q 1 F P = F R F Q 1 F R F Q F P
149 126 127 148 syl2anc F P F P F R F Q F R Z i U i F R F Q 1 F P = F R F Q 1 F R F Q F P
150 126 mulid1d F P F P F R F Q F R Z i U i F R F Q 1 = F R F Q
151 124 125 127 subdird F P F P F R F Q F R Z i U i F R F Q F P = F R F P F Q F P
152 124 127 mulcomd F P F P F R F Q F R Z i U i F R F P = F P F R
153 152 oveq1d F P F P F R F Q F R Z i U i F R F P F Q F P = F P F R F Q F P
154 151 153 eqtrd F P F P F R F Q F R Z i U i F R F Q F P = F P F R F Q F P
155 150 154 oveq12d F P F P F R F Q F R Z i U i F R F Q 1 F R F Q F P = F R - F Q - F P F R F Q F P
156 149 155 eqtrd F P F P F R F Q F R Z i U i F R F Q 1 F P = F R - F Q - F P F R F Q F P
157 subdi F Q F P 1 F R F Q F P 1 F R = F Q F P 1 F Q F P F R
158 44 157 mp3an2 F Q F P F R F Q F P 1 F R = F Q F P 1 F Q F P F R
159 130 124 158 syl2anc F P F P F R F Q F R Z i U i F Q F P 1 F R = F Q F P 1 F Q F P F R
160 130 mulid1d F P F P F R F Q F R Z i U i F Q F P 1 = F Q F P
161 125 127 124 subdird F P F P F R F Q F R Z i U i F Q F P F R = F Q F R F P F R
162 160 161 oveq12d F P F P F R F Q F R Z i U i F Q F P 1 F Q F P F R = F Q - F P - F Q F R F P F R
163 159 162 eqtrd F P F P F R F Q F R Z i U i F Q F P 1 F R = F Q - F P - F Q F R F P F R
164 156 163 oveq12d F P F P F R F Q F R Z i U i F R F Q 1 F P + F Q F P 1 F R = F R - F Q - F P F R F Q F P + F Q F P - F Q F R F P F R
165 127 124 mulcld F P F P F R F Q F R Z i U i F P F R
166 125 127 mulcld F P F P F R F Q F R Z i U i F Q F P
167 165 166 subcld F P F P F R F Q F R Z i U i F P F R F Q F P
168 mulcl F Q F R F Q F R
169 168 3ad2ant2 F P F P F R F Q F R Z i U i F Q F R
170 169 165 subcld F P F P F R F Q F R Z i U i F Q F R F P F R
171 126 130 167 170 addsub4d F P F P F R F Q F R Z i U i F R F Q + F Q F P - F P F R F Q F P + F Q F R - F P F R = F R - F Q - F P F R F Q F P + F Q F P - F Q F R F P F R
172 124 125 127 npncand F P F P F R F Q F R Z i U i F R F Q + F Q - F P = F R F P
173 165 166 169 npncan3d F P F P F R F Q F R Z i U i F P F R F Q F P + F Q F R - F P F R = F Q F R F Q F P
174 172 173 oveq12d F P F P F R F Q F R Z i U i F R F Q + F Q F P - F P F R F Q F P + F Q F R - F P F R = F R - F P - F Q F R F Q F P
175 164 171 174 3eqtr2d F P F P F R F Q F R Z i U i F R F Q 1 F P + F Q F P 1 F R = F R - F P - F Q F R F Q F P
176 143 146 175 3eqtr4d F P F P F R F Q F R Z i U i F R F P 1 F Q = F R F Q 1 F P + F Q F P 1 F R
177 129 133 addcld F P F P F R F Q F R Z i U i F R F Q 1 F P + F Q F P 1 F R
178 subcl 1 F Q 1 F Q
179 44 125 178 sylancr F P F P F R F Q F R Z i U i 1 F Q
180 177 134 179 137 divmuld F P F P F R F Q F R Z i U i F R F Q 1 F P + F Q F P 1 F R F R F P = 1 F Q F R F P 1 F Q = F R F Q 1 F P + F Q F P 1 F R
181 176 180 mpbird F P F P F R F Q F R Z i U i F R F Q 1 F P + F Q F P 1 F R F R F P = 1 F Q
182 126 128 134 137 div23d F P F P F R F Q F R Z i U i F R F Q 1 F P F R F P = F R F Q F R F P 1 F P
183 134 130 134 137 divsubdird F P F P F R F Q F R Z i U i F R - F P - F Q F P F R F P = F R F P F R F P F Q F P F R F P
184 124 125 127 nnncan2d F P F P F R F Q F R Z i U i F R - F P - F Q F P = F R F Q
185 184 oveq1d F P F P F R F Q F R Z i U i F R - F P - F Q F P F R F P = F R F Q F R F P
186 134 137 dividd F P F P F R F Q F R Z i U i F R F P F R F P = 1
187 186 oveq1d F P F P F R F Q F R Z i U i F R F P F R F P F Q F P F R F P = 1 F Q F P F R F P
188 183 185 187 3eqtr3d F P F P F R F Q F R Z i U i F R F Q F R F P = 1 F Q F P F R F P
189 188 oveq1d F P F P F R F Q F R Z i U i F R F Q F R F P 1 F P = 1 F Q F P F R F P 1 F P
190 182 189 eqtrd F P F P F R F Q F R Z i U i F R F Q 1 F P F R F P = 1 F Q F P F R F P 1 F P
191 130 132 134 137 div23d F P F P F R F Q F R Z i U i F Q F P 1 F R F R F P = F Q F P F R F P 1 F R
192 190 191 oveq12d F P F P F R F Q F R Z i U i F R F Q 1 F P F R F P + F Q F P 1 F R F R F P = 1 F Q F P F R F P 1 F P + F Q F P F R F P 1 F R
193 138 181 192 3eqtr3d F P F P F R F Q F R Z i U i 1 F Q = 1 F Q F P F R F P 1 F P + F Q F P F R F P 1 F R
194 193 oveq1d F P F P F R F Q F R Z i U i 1 F Q Z i = 1 F Q F P F R F P 1 F P + F Q F P F R F P 1 F R Z i
195 126 127 mulcld F P F P F R F Q F R Z i U i F R F Q F P
196 130 124 mulcld F P F P F R F Q F R Z i U i F Q F P F R
197 195 196 134 137 divdird F P F P F R F Q F R Z i U i F R F Q F P + F Q F P F R F R F P = F R F Q F P F R F P + F Q F P F R F R F P
198 154 161 oveq12d F P F P F R F Q F R Z i U i F R F Q F P + F Q F P F R = F P F R F Q F P + F Q F R - F P F R
199 173 198 142 3eqtr4rd F P F P F R F Q F R Z i U i F R F P F Q = F R F Q F P + F Q F P F R
200 195 196 addcld F P F P F R F Q F R Z i U i F R F Q F P + F Q F P F R
201 200 134 125 137 divmuld F P F P F R F Q F R Z i U i F R F Q F P + F Q F P F R F R F P = F Q F R F P F Q = F R F Q F P + F Q F P F R
202 199 201 mpbird F P F P F R F Q F R Z i U i F R F Q F P + F Q F P F R F R F P = F Q
203 126 127 134 137 div23d F P F P F R F Q F R Z i U i F R F Q F P F R F P = F R F Q F R F P F P
204 188 oveq1d F P F P F R F Q F R Z i U i F R F Q F R F P F P = 1 F Q F P F R F P F P
205 203 204 eqtrd F P F P F R F Q F R Z i U i F R F Q F P F R F P = 1 F Q F P F R F P F P
206 130 124 134 137 div23d F P F P F R F Q F R Z i U i F Q F P F R F R F P = F Q F P F R F P F R
207 205 206 oveq12d F P F P F R F Q F R Z i U i F R F Q F P F R F P + F Q F P F R F R F P = 1 F Q F P F R F P F P + F Q F P F R F P F R
208 197 202 207 3eqtr3d F P F P F R F Q F R Z i U i F Q = 1 F Q F P F R F P F P + F Q F P F R F P F R
209 208 oveq1d F P F P F R F Q F R Z i U i F Q U i = 1 F Q F P F R F P F P + F Q F P F R F P F R U i
210 194 209 oveq12d F P F P F R F Q F R Z i U i 1 F Q Z i + F Q U i = 1 F Q F P F R F P 1 F P + F Q F P F R F P 1 F R Z i + 1 F Q F P F R F P F P + F Q F P F R F P F R U i
211 130 134 137 divcld F P F P F R F Q F R Z i U i F Q F P F R F P
212 subcl 1 F Q F P F R F P 1 F Q F P F R F P
213 44 211 212 sylancr F P F P F R F Q F R Z i U i 1 F Q F P F R F P
214 simp3l F P F P F R F Q F R Z i U i Z i
215 128 214 mulcld F P F P F R F Q F R Z i U i 1 F P Z i
216 213 215 mulcld F P F P F R F Q F R Z i U i 1 F Q F P F R F P 1 F P Z i
217 132 214 mulcld F P F P F R F Q F R Z i U i 1 F R Z i
218 211 217 mulcld F P F P F R F Q F R Z i U i F Q F P F R F P 1 F R Z i
219 simp3r F P F P F R F Q F R Z i U i U i
220 127 219 mulcld F P F P F R F Q F R Z i U i F P U i
221 213 220 mulcld F P F P F R F Q F R Z i U i 1 F Q F P F R F P F P U i
222 124 219 mulcld F P F P F R F Q F R Z i U i F R U i
223 211 222 mulcld F P F P F R F Q F R Z i U i F Q F P F R F P F R U i
224 216 218 221 223 add4d F P F P F R F Q F R Z i U i 1 F Q F P F R F P 1 F P Z i + F Q F P F R F P 1 F R Z i + 1 F Q F P F R F P F P U i + F Q F P F R F P F R U i = 1 F Q F P F R F P 1 F P Z i + 1 F Q F P F R F P F P U i + F Q F P F R F P 1 F R Z i + F Q F P F R F P F R U i
225 213 128 mulcld F P F P F R F Q F R Z i U i 1 F Q F P F R F P 1 F P
226 211 132 mulcld F P F P F R F Q F R Z i U i F Q F P F R F P 1 F R
227 213 128 214 mulassd F P F P F R F Q F R Z i U i 1 F Q F P F R F P 1 F P Z i = 1 F Q F P F R F P 1 F P Z i
228 211 132 214 mulassd F P F P F R F Q F R Z i U i F Q F P F R F P 1 F R Z i = F Q F P F R F P 1 F R Z i
229 227 228 oveq12d F P F P F R F Q F R Z i U i 1 F Q F P F R F P 1 F P Z i + F Q F P F R F P 1 F R Z i = 1 F Q F P F R F P 1 F P Z i + F Q F P F R F P 1 F R Z i
230 225 214 226 229 joinlmuladdmuld F P F P F R F Q F R Z i U i 1 F Q F P F R F P 1 F P + F Q F P F R F P 1 F R Z i = 1 F Q F P F R F P 1 F P Z i + F Q F P F R F P 1 F R Z i
231 213 127 mulcld F P F P F R F Q F R Z i U i 1 F Q F P F R F P F P
232 211 124 mulcld F P F P F R F Q F R Z i U i F Q F P F R F P F R
233 213 127 219 mulassd F P F P F R F Q F R Z i U i 1 F Q F P F R F P F P U i = 1 F Q F P F R F P F P U i
234 211 124 219 mulassd F P F P F R F Q F R Z i U i F Q F P F R F P F R U i = F Q F P F R F P F R U i
235 233 234 oveq12d F P F P F R F Q F R Z i U i 1 F Q F P F R F P F P U i + F Q F P F R F P F R U i = 1 F Q F P F R F P F P U i + F Q F P F R F P F R U i
236 231 219 232 235 joinlmuladdmuld F P F P F R F Q F R Z i U i 1 F Q F P F R F P F P + F Q F P F R F P F R U i = 1 F Q F P F R F P F P U i + F Q F P F R F P F R U i
237 230 236 oveq12d F P F P F R F Q F R Z i U i 1 F Q F P F R F P 1 F P + F Q F P F R F P 1 F R Z i + 1 F Q F P F R F P F P + F Q F P F R F P F R U i = 1 F Q F P F R F P 1 F P Z i + F Q F P F R F P 1 F R Z i + 1 F Q F P F R F P F P U i + F Q F P F R F P F R U i
238 213 215 220 adddid F P F P F R F Q F R Z i U i 1 F Q F P F R F P 1 F P Z i + F P U i = 1 F Q F P F R F P 1 F P Z i + 1 F Q F P F R F P F P U i
239 211 217 222 adddid F P F P F R F Q F R Z i U i F Q F P F R F P 1 F R Z i + F R U i = F Q F P F R F P 1 F R Z i + F Q F P F R F P F R U i
240 238 239 oveq12d F P F P F R F Q F R Z i U i 1 F Q F P F R F P 1 F P Z i + F P U i + F Q F P F R F P 1 F R Z i + F R U i = 1 F Q F P F R F P 1 F P Z i + 1 F Q F P F R F P F P U i + F Q F P F R F P 1 F R Z i + F Q F P F R F P F R U i
241 224 237 240 3eqtr4rd F P F P F R F Q F R Z i U i 1 F Q F P F R F P 1 F P Z i + F P U i + F Q F P F R F P 1 F R Z i + F R U i = 1 F Q F P F R F P 1 F P + F Q F P F R F P 1 F R Z i + 1 F Q F P F R F P F P + F Q F P F R F P F R U i
242 210 241 eqtr4d F P F P F R F Q F R Z i U i 1 F Q Z i + F Q U i = 1 F Q F P F R F P 1 F P Z i + F P U i + F Q F P F R F P 1 F R Z i + F R U i
243 112 113 116 119 121 123 242 syl222anc F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N 1 F Q Z i + F Q U i = 1 F Q F P F R F P 1 F P Z i + F P U i + F Q F P F R F P 1 F R Z i + F R U i
244 243 ralrimiva F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N 1 F Q Z i + F Q U i = 1 F Q F P F R F P 1 F P Z i + F P U i + F Q F P F R F P 1 F R Z i + F R U i
245 oveq2 t = F Q F P F R F P 1 t = 1 F Q F P F R F P
246 245 oveq1d t = F Q F P F R F P 1 t 1 F P Z i + F P U i = 1 F Q F P F R F P 1 F P Z i + F P U i
247 oveq1 t = F Q F P F R F P t 1 F R Z i + F R U i = F Q F P F R F P 1 F R Z i + F R U i
248 246 247 oveq12d t = F Q F P F R F P 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i = 1 F Q F P F R F P 1 F P Z i + F P U i + F Q F P F R F P 1 F R Z i + F R U i
249 248 eqeq2d t = F Q F P F R F P 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i 1 F Q Z i + F Q U i = 1 F Q F P F R F P 1 F P Z i + F P U i + F Q F P F R F P 1 F R Z i + F R U i
250 249 ralbidv t = F Q F P F R F P i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i i 1 N 1 F Q Z i + F Q U i = 1 F Q F P F R F P 1 F P Z i + F P U i + F Q F P F R F P 1 F R Z i + F R U i
251 250 rspcev F Q F P F R F P 0 1 i 1 N 1 F Q Z i + F Q U i = 1 F Q F P F R F P 1 F P Z i + F P U i + F Q F P F R F P 1 F R Z i + F R U i t 0 1 i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
252 109 244 251 syl2anc F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R t 0 1 i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
253 252 ex F P F R N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R t 0 1 i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
254 84 253 pm2.61ine N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R t 0 1 i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
255 r19.26-3 i 1 N P i = 1 F P Z i + F P U i Q i = 1 F Q Z i + F Q U i R i = 1 F R Z i + F R U i i 1 N P i = 1 F P Z i + F P U i i 1 N Q i = 1 F Q Z i + F Q U i i 1 N R i = 1 F R Z i + F R U i
256 simp2 P i = 1 F P Z i + F P U i Q i = 1 F Q Z i + F Q U i R i = 1 F R Z i + F R U i Q i = 1 F Q Z i + F Q U i
257 oveq2 P i = 1 F P Z i + F P U i 1 t P i = 1 t 1 F P Z i + F P U i
258 oveq2 R i = 1 F R Z i + F R U i t R i = t 1 F R Z i + F R U i
259 257 258 oveqan12d P i = 1 F P Z i + F P U i R i = 1 F R Z i + F R U i 1 t P i + t R i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
260 259 3adant2 P i = 1 F P Z i + F P U i Q i = 1 F Q Z i + F Q U i R i = 1 F R Z i + F R U i 1 t P i + t R i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
261 256 260 eqeq12d P i = 1 F P Z i + F P U i Q i = 1 F Q Z i + F Q U i R i = 1 F R Z i + F R U i Q i = 1 t P i + t R i 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
262 261 ralimi i 1 N P i = 1 F P Z i + F P U i Q i = 1 F Q Z i + F Q U i R i = 1 F R Z i + F R U i i 1 N Q i = 1 t P i + t R i 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
263 ralbi i 1 N Q i = 1 t P i + t R i 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i i 1 N Q i = 1 t P i + t R i i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
264 262 263 syl i 1 N P i = 1 F P Z i + F P U i Q i = 1 F Q Z i + F Q U i R i = 1 F R Z i + F R U i i 1 N Q i = 1 t P i + t R i i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
265 264 rexbidv i 1 N P i = 1 F P Z i + F P U i Q i = 1 F Q Z i + F Q U i R i = 1 F R Z i + F R U i t 0 1 i 1 N Q i = 1 t P i + t R i t 0 1 i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i
266 265 biimprcd t 0 1 i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i i 1 N P i = 1 F P Z i + F P U i Q i = 1 F Q Z i + F Q U i R i = 1 F R Z i + F R U i t 0 1 i 1 N Q i = 1 t P i + t R i
267 255 266 syl5bir t 0 1 i 1 N 1 F Q Z i + F Q U i = 1 t 1 F P Z i + F P U i + t 1 F R Z i + F R U i i 1 N P i = 1 F P Z i + F P U i i 1 N Q i = 1 F Q Z i + F Q U i i 1 N R i = 1 F R Z i + F R U i t 0 1 i 1 N Q i = 1 t P i + t R i
268 254 267 syl N Z 𝔼 N U 𝔼 N Z U F P 0 +∞ F Q 0 +∞ F R 0 +∞ F P F Q F Q F R i 1 N P i = 1 F P Z i + F P U i i 1 N Q i = 1 F Q Z i + F Q U i i 1 N R i = 1 F R Z i + F R U i t 0 1 i 1 N Q i = 1 t P i + t R i
269 268 an32s N Z 𝔼 N U 𝔼 N Z U F P F Q F Q F R F P 0 +∞ F Q 0 +∞ F R 0 +∞ i 1 N P i = 1 F P Z i + F P U i i 1 N Q i = 1 F Q Z i + F Q U i i 1 N R i = 1 F R Z i + F R U i t 0 1 i 1 N Q i = 1 t P i + t R i
270 269 expimpd N Z 𝔼 N U 𝔼 N Z U F P F Q F Q F R F P 0 +∞ F Q 0 +∞ F R 0 +∞ i 1 N P i = 1 F P Z i + F P U i i 1 N Q i = 1 F Q Z i + F Q U i i 1 N R i = 1 F R Z i + F R U i t 0 1 i 1 N Q i = 1 t P i + t R i
271 270 adantlr N Z 𝔼 N U 𝔼 N Z U P D Q D R D F P F Q F Q F R F P 0 +∞ F Q 0 +∞ F R 0 +∞ i 1 N P i = 1 F P Z i + F P U i i 1 N Q i = 1 F Q Z i + F Q U i i 1 N R i = 1 F R Z i + F R U i t 0 1 i 1 N Q i = 1 t P i + t R i
272 12 271 syl5bi