Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  carsgclctunlem2 Structured version   Visualization version   GIF version

Theorem carsgclctunlem2 33307
Description: Lemma for carsgclctun 33309. (Contributed by Thierry Arnoux, 25-May-2020.)
Hypotheses
Ref Expression
carsgval.1 (𝜑𝑂𝑉)
carsgval.2 (𝜑𝑀:𝒫 𝑂⟶(0[,]+∞))
carsgsiga.1 (𝜑 → (𝑀‘∅) = 0)
carsgsiga.2 ((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
carsgsiga.3 ((𝜑𝑥𝑦𝑦 ∈ 𝒫 𝑂) → (𝑀𝑥) ≤ (𝑀𝑦))
carsgclctunlem2.1 (𝜑Disj 𝑘 ∈ ℕ 𝐴)
carsgclctunlem2.2 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ (toCaraSiga‘𝑀))
carsgclctunlem2.3 (𝜑𝐸 ∈ 𝒫 𝑂)
carsgclctunlem2.4 (𝜑 → (𝑀𝐸) ≠ +∞)
Assertion
Ref Expression
carsgclctunlem2 (𝜑 → ((𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) ≤ (𝑀𝐸))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐸,𝑦   𝑥,𝑀,𝑦   𝑥,𝑂,𝑦   𝜑,𝑥,𝑦,𝑘   𝑘,𝐸   𝑘,𝑀   𝑘,𝑂   𝜑,𝑘
Allowed substitution hints:   𝐴(𝑘)   𝑉(𝑥,𝑦,𝑘)

Proof of Theorem carsgclctunlem2
Dummy variables 𝑒 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iunin2 5074 . . . . 5 𝑘 ∈ ℕ (𝐸𝐴) = (𝐸 𝑘 ∈ ℕ 𝐴)
21fveq2i 6892 . . . 4 (𝑀 𝑘 ∈ ℕ (𝐸𝐴)) = (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))
3 iccssxr 13404 . . . . 5 (0[,]+∞) ⊆ ℝ*
4 carsgval.2 . . . . . 6 (𝜑𝑀:𝒫 𝑂⟶(0[,]+∞))
5 nnex 12215 . . . . . . . 8 ℕ ∈ V
65a1i 11 . . . . . . 7 (𝜑 → ℕ ∈ V)
7 carsgclctunlem2.3 . . . . . . . . 9 (𝜑𝐸 ∈ 𝒫 𝑂)
87adantr 482 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 𝐸 ∈ 𝒫 𝑂)
98elpwincl1 31751 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝐸𝐴) ∈ 𝒫 𝑂)
106, 9elpwiuncl 31753 . . . . . 6 (𝜑 𝑘 ∈ ℕ (𝐸𝐴) ∈ 𝒫 𝑂)
114, 10ffvelcdmd 7085 . . . . 5 (𝜑 → (𝑀 𝑘 ∈ ℕ (𝐸𝐴)) ∈ (0[,]+∞))
123, 11sselid 3980 . . . 4 (𝜑 → (𝑀 𝑘 ∈ ℕ (𝐸𝐴)) ∈ ℝ*)
132, 12eqeltrrid 2839 . . 3 (𝜑 → (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ∈ ℝ*)
144, 7ffvelcdmd 7085 . . . . 5 (𝜑 → (𝑀𝐸) ∈ (0[,]+∞))
153, 14sselid 3980 . . . 4 (𝜑 → (𝑀𝐸) ∈ ℝ*)
167elpwdifcl 31752 . . . . . . 7 (𝜑 → (𝐸 𝑘 ∈ ℕ 𝐴) ∈ 𝒫 𝑂)
174, 16ffvelcdmd 7085 . . . . . 6 (𝜑 → (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ∈ (0[,]+∞))
183, 17sselid 3980 . . . . 5 (𝜑 → (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ∈ ℝ*)
1918xnegcld 13276 . . . 4 (𝜑 → -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ∈ ℝ*)
2015, 19xaddcld 13277 . . 3 (𝜑 → ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) ∈ ℝ*)
214adantr 482 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
2221, 9ffvelcdmd 7085 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑀‘(𝐸𝐴)) ∈ (0[,]+∞))
2322ralrimiva 3147 . . . . . . 7 (𝜑 → ∀𝑘 ∈ ℕ (𝑀‘(𝐸𝐴)) ∈ (0[,]+∞))
24 nfcv 2904 . . . . . . . 8 𝑘
2524esumcl 33017 . . . . . . 7 ((ℕ ∈ V ∧ ∀𝑘 ∈ ℕ (𝑀‘(𝐸𝐴)) ∈ (0[,]+∞)) → Σ*𝑘 ∈ ℕ(𝑀‘(𝐸𝐴)) ∈ (0[,]+∞))
266, 23, 25syl2anc 585 . . . . . 6 (𝜑 → Σ*𝑘 ∈ ℕ(𝑀‘(𝐸𝐴)) ∈ (0[,]+∞))
273, 26sselid 3980 . . . . 5 (𝜑 → Σ*𝑘 ∈ ℕ(𝑀‘(𝐸𝐴)) ∈ ℝ*)
289ralrimiva 3147 . . . . . . . . 9 (𝜑 → ∀𝑘 ∈ ℕ (𝐸𝐴) ∈ 𝒫 𝑂)
29 dfiun3g 5962 . . . . . . . . 9 (∀𝑘 ∈ ℕ (𝐸𝐴) ∈ 𝒫 𝑂 𝑘 ∈ ℕ (𝐸𝐴) = ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)))
3028, 29syl 17 . . . . . . . 8 (𝜑 𝑘 ∈ ℕ (𝐸𝐴) = ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)))
3130fveq2d 6893 . . . . . . 7 (𝜑 → (𝑀 𝑘 ∈ ℕ (𝐸𝐴)) = (𝑀 ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))))
32 nnct 13943 . . . . . . . . . 10 ℕ ≼ ω
33 mptct 10530 . . . . . . . . . 10 (ℕ ≼ ω → (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ≼ ω)
34 rnct 10517 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ (𝐸𝐴)) ≼ ω → ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ≼ ω)
3532, 33, 34mp2b 10 . . . . . . . . 9 ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ≼ ω
3635a1i 11 . . . . . . . 8 (𝜑 → ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ≼ ω)
37 eqid 2733 . . . . . . . . . 10 (𝑘 ∈ ℕ ↦ (𝐸𝐴)) = (𝑘 ∈ ℕ ↦ (𝐸𝐴))
3837rnmptss 7119 . . . . . . . . 9 (∀𝑘 ∈ ℕ (𝐸𝐴) ∈ 𝒫 𝑂 → ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ⊆ 𝒫 𝑂)
3928, 38syl 17 . . . . . . . 8 (𝜑 → ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ⊆ 𝒫 𝑂)
40 mptexg 7220 . . . . . . . . . 10 (ℕ ∈ V → (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ∈ V)
41 rnexg 7892 . . . . . . . . . 10 ((𝑘 ∈ ℕ ↦ (𝐸𝐴)) ∈ V → ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ∈ V)
425, 40, 41mp2b 10 . . . . . . . . 9 ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ∈ V
43 breq1 5151 . . . . . . . . . . . 12 (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) → (𝑥 ≼ ω ↔ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ≼ ω))
44 sseq1 4007 . . . . . . . . . . . 12 (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) → (𝑥 ⊆ 𝒫 𝑂 ↔ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ⊆ 𝒫 𝑂))
4543, 443anbi23d 1440 . . . . . . . . . . 11 (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) → ((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) ↔ (𝜑 ∧ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ≼ ω ∧ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ⊆ 𝒫 𝑂)))
46 unieq 4919 . . . . . . . . . . . . 13 (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) → 𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)))
4746fveq2d 6893 . . . . . . . . . . . 12 (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) → (𝑀 𝑥) = (𝑀 ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))))
48 esumeq1 33021 . . . . . . . . . . . 12 (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) → Σ*𝑦𝑥(𝑀𝑦) = Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))(𝑀𝑦))
4947, 48breq12d 5161 . . . . . . . . . . 11 (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) → ((𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦) ↔ (𝑀 ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))) ≤ Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))(𝑀𝑦)))
5045, 49imbi12d 345 . . . . . . . . . 10 (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) → (((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦)) ↔ ((𝜑 ∧ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ≼ ω ∧ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ⊆ 𝒫 𝑂) → (𝑀 ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))) ≤ Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))(𝑀𝑦))))
51 carsgsiga.2 . . . . . . . . . 10 ((𝜑𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
5250, 51vtoclg 3557 . . . . . . . . 9 (ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ∈ V → ((𝜑 ∧ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ≼ ω ∧ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ⊆ 𝒫 𝑂) → (𝑀 ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))) ≤ Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))(𝑀𝑦)))
5342, 52ax-mp 5 . . . . . . . 8 ((𝜑 ∧ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ≼ ω ∧ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴)) ⊆ 𝒫 𝑂) → (𝑀 ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))) ≤ Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))(𝑀𝑦))
5436, 39, 53mpd3an23 1464 . . . . . . 7 (𝜑 → (𝑀 ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))) ≤ Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))(𝑀𝑦))
5531, 54eqbrtrd 5170 . . . . . 6 (𝜑 → (𝑀 𝑘 ∈ ℕ (𝐸𝐴)) ≤ Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))(𝑀𝑦))
56 fveq2 6889 . . . . . . 7 (𝑦 = (𝐸𝐴) → (𝑀𝑦) = (𝑀‘(𝐸𝐴)))
57 simpr 486 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝐸𝐴) = ∅) → (𝐸𝐴) = ∅)
5857fveq2d 6893 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ (𝐸𝐴) = ∅) → (𝑀‘(𝐸𝐴)) = (𝑀‘∅))
59 carsgsiga.1 . . . . . . . . 9 (𝜑 → (𝑀‘∅) = 0)
6059ad2antrr 725 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ (𝐸𝐴) = ∅) → (𝑀‘∅) = 0)
6158, 60eqtrd 2773 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ (𝐸𝐴) = ∅) → (𝑀‘(𝐸𝐴)) = 0)
62 carsgclctunlem2.1 . . . . . . . . 9 (𝜑Disj 𝑘 ∈ ℕ 𝐴)
63 disjin 31805 . . . . . . . . 9 (Disj 𝑘 ∈ ℕ 𝐴Disj 𝑘 ∈ ℕ (𝐴𝐸))
6462, 63syl 17 . . . . . . . 8 (𝜑Disj 𝑘 ∈ ℕ (𝐴𝐸))
65 incom 4201 . . . . . . . . . 10 (𝐴𝐸) = (𝐸𝐴)
6665rgenw 3066 . . . . . . . . 9 𝑘 ∈ ℕ (𝐴𝐸) = (𝐸𝐴)
67 disjeq2 5117 . . . . . . . . 9 (∀𝑘 ∈ ℕ (𝐴𝐸) = (𝐸𝐴) → (Disj 𝑘 ∈ ℕ (𝐴𝐸) ↔ Disj 𝑘 ∈ ℕ (𝐸𝐴)))
6866, 67ax-mp 5 . . . . . . . 8 (Disj 𝑘 ∈ ℕ (𝐴𝐸) ↔ Disj 𝑘 ∈ ℕ (𝐸𝐴))
6964, 68sylib 217 . . . . . . 7 (𝜑Disj 𝑘 ∈ ℕ (𝐸𝐴))
7056, 6, 22, 9, 61, 69esumrnmpt2 33055 . . . . . 6 (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸𝐴))(𝑀𝑦) = Σ*𝑘 ∈ ℕ(𝑀‘(𝐸𝐴)))
7155, 70breqtrd 5174 . . . . 5 (𝜑 → (𝑀 𝑘 ∈ ℕ (𝐸𝐴)) ≤ Σ*𝑘 ∈ ℕ(𝑀‘(𝐸𝐴)))
72 carsgval.1 . . . . . . . 8 (𝜑𝑂𝑉)
73 difssd 4132 . . . . . . . 8 (𝜑 → (𝐸 𝑘 ∈ ℕ 𝐴) ⊆ 𝐸)
74 carsgsiga.3 . . . . . . . 8 ((𝜑𝑥𝑦𝑦 ∈ 𝒫 𝑂) → (𝑀𝑥) ≤ (𝑀𝑦))
7572, 4, 73, 7, 74carsgmon 33302 . . . . . . 7 (𝜑 → (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ≤ (𝑀𝐸))
7614, 17, 75xrge0subcld 31964 . . . . . 6 (𝜑 → ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) ∈ (0[,]+∞))
774adantr 482 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
787adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 𝐸 ∈ 𝒫 𝑂)
7978elpwincl1 31751 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝐸 𝑘 ∈ (1...𝑛)𝐴) ∈ 𝒫 𝑂)
8077, 79ffvelcdmd 7085 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ (0[,]+∞))
813, 80sselid 3980 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ*)
82 xrge0neqmnf 13426 . . . . . . . . . . 11 ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ (0[,]+∞) → (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞)
8380, 82syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞)
8478elpwdifcl 31752 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝐸 𝑘 ∈ (1...𝑛)𝐴) ∈ 𝒫 𝑂)
8577, 84ffvelcdmd 7085 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ (0[,]+∞))
863, 85sselid 3980 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ*)
87 xrge0neqmnf 13426 . . . . . . . . . . 11 ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ (0[,]+∞) → (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞)
8885, 87syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞)
8986xnegcld 13276 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ*)
90 xnegneg 13190 . . . . . . . . . . . . . . . . 17 ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* → -𝑒-𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)))
9186, 90syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → -𝑒-𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)))
9291adantr 482 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -∞) → -𝑒-𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)))
93 xnegeq 13183 . . . . . . . . . . . . . . . . 17 (-𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -∞ → -𝑒-𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -𝑒-∞)
9493adantl 483 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -∞) → -𝑒-𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -𝑒-∞)
95 xnegmnf 13186 . . . . . . . . . . . . . . . 16 -𝑒-∞ = +∞
9694, 95eqtrdi 2789 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -∞) → -𝑒-𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = +∞)
9792, 96eqtr3d 2775 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -∞) → (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = +∞)
9897oveq2d 7422 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -∞) → ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) = ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 +∞))
99 simpll 766 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑)
100 fz1ssnn 13529 . . . . . . . . . . . . . . . . . . . . . . 23 (1...𝑛) ⊆ ℕ
101100a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑛 ∈ ℕ) → (1...𝑛) ⊆ ℕ)
102101sselda 3982 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ)
103 carsgclctunlem2.2 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ ℕ) → 𝐴 ∈ (toCaraSiga‘𝑀))
10499, 102, 103syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (toCaraSiga‘𝑀))
105104ralrimiva 3147 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ∀𝑘 ∈ (1...𝑛)𝐴 ∈ (toCaraSiga‘𝑀))
106 dfiun3g 5962 . . . . . . . . . . . . . . . . . . 19 (∀𝑘 ∈ (1...𝑛)𝐴 ∈ (toCaraSiga‘𝑀) → 𝑘 ∈ (1...𝑛)𝐴 = ran (𝑘 ∈ (1...𝑛) ↦ 𝐴))
107105, 106syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → 𝑘 ∈ (1...𝑛)𝐴 = ran (𝑘 ∈ (1...𝑛) ↦ 𝐴))
10872adantr 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → 𝑂𝑉)
10959adantr 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → (𝑀‘∅) = 0)
110513adant1r 1178 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀 𝑥) ≤ Σ*𝑦𝑥(𝑀𝑦))
111 fzfi 13934 . . . . . . . . . . . . . . . . . . . . 21 (1...𝑛) ∈ Fin
112 mptfi 9348 . . . . . . . . . . . . . . . . . . . . 21 ((1...𝑛) ∈ Fin → (𝑘 ∈ (1...𝑛) ↦ 𝐴) ∈ Fin)
113 rnfi 9332 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ (1...𝑛) ↦ 𝐴) ∈ Fin → ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ∈ Fin)
114111, 112, 113mp2b 10 . . . . . . . . . . . . . . . . . . . 20 ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ∈ Fin
115114a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ∈ Fin)
116 eqid 2733 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ (1...𝑛) ↦ 𝐴) = (𝑘 ∈ (1...𝑛) ↦ 𝐴)
117116rnmptss 7119 . . . . . . . . . . . . . . . . . . . 20 (∀𝑘 ∈ (1...𝑛)𝐴 ∈ (toCaraSiga‘𝑀) → ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ (toCaraSiga‘𝑀))
118105, 117syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛 ∈ ℕ) → ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ (toCaraSiga‘𝑀))
119108, 77, 109, 110, 115, 118fiunelcarsg 33304 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ∈ (toCaraSiga‘𝑀))
120107, 119eqeltrd 2834 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → 𝑘 ∈ (1...𝑛)𝐴 ∈ (toCaraSiga‘𝑀))
121108, 77elcarsg 33293 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → ( 𝑘 ∈ (1...𝑛)𝐴 ∈ (toCaraSiga‘𝑀) ↔ ( 𝑘 ∈ (1...𝑛)𝐴𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴))) = (𝑀𝑒))))
122120, 121mpbid 231 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → ( 𝑘 ∈ (1...𝑛)𝐴𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴))) = (𝑀𝑒)))
123122simprd 497 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴))) = (𝑀𝑒))
124 ineq1 4205 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝐸 → (𝑒 𝑘 ∈ (1...𝑛)𝐴) = (𝐸 𝑘 ∈ (1...𝑛)𝐴))
125124fveq2d 6893 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝐸 → (𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴)) = (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)))
126 difeq1 4115 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝐸 → (𝑒 𝑘 ∈ (1...𝑛)𝐴) = (𝐸 𝑘 ∈ (1...𝑛)𝐴))
127126fveq2d 6893 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝐸 → (𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴)) = (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)))
128125, 127oveq12d 7424 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝐸 → ((𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴))) = ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))))
129 fveq2 6889 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝐸 → (𝑀𝑒) = (𝑀𝐸))
130128, 129eqeq12d 2749 . . . . . . . . . . . . . . . 16 (𝑒 = 𝐸 → (((𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴))) = (𝑀𝑒) ↔ ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) = (𝑀𝐸)))
131130rspcv 3609 . . . . . . . . . . . . . . 15 (𝐸 ∈ 𝒫 𝑂 → (∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝑒 𝑘 ∈ (1...𝑛)𝐴))) = (𝑀𝑒) → ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) = (𝑀𝐸)))
13278, 123, 131sylc 65 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) = (𝑀𝐸))
133132adantr 482 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -∞) → ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) = (𝑀𝐸))
134 xaddpnf1 13202 . . . . . . . . . . . . . . 15 (((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* ∧ (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞) → ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 +∞) = +∞)
13581, 83, 134syl2anc 585 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 +∞) = +∞)
136135adantr 482 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -∞) → ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 +∞) = +∞)
13798, 133, 1363eqtr3d 2781 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -∞) → (𝑀𝐸) = +∞)
138 carsgclctunlem2.4 . . . . . . . . . . . . . 14 (𝜑 → (𝑀𝐸) ≠ +∞)
139138ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -∞) → (𝑀𝐸) ≠ +∞)
140139neneqd 2946 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -∞) → ¬ (𝑀𝐸) = +∞)
141137, 140pm2.65da 816 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ¬ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = -∞)
142141neqned 2948 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞)
143 xaddass 13225 . . . . . . . . . 10 ((((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* ∧ (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞) ∧ ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* ∧ (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞) ∧ (-𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* ∧ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞)) → (((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) = ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)))))
14481, 83, 86, 88, 89, 142, 143syl222anc 1387 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) = ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)))))
145 xnegid 13214 . . . . . . . . . . 11 ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* → ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) = 0)
14686, 145syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) = 0)
147146oveq2d 7422 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)))) = ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 0))
148 xaddrid 13217 . . . . . . . . . 10 ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* → ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 0) = (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)))
14981, 148syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 0) = (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)))
150144, 147, 1493eqtrd 2777 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) = (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)))
151132oveq1d 7421 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (((𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) = ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))))
152107ineq2d 4212 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐸 𝑘 ∈ (1...𝑛)𝐴) = (𝐸 ran (𝑘 ∈ (1...𝑛) ↦ 𝐴)))
153152fveq2d 6893 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = (𝑀‘(𝐸 ran (𝑘 ∈ (1...𝑛) ↦ 𝐴))))
154 mptss 6041 . . . . . . . . . . . . 13 ((1...𝑛) ⊆ ℕ → (𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ (𝑘 ∈ ℕ ↦ 𝐴))
155 rnss 5937 . . . . . . . . . . . . 13 ((𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ (𝑘 ∈ ℕ ↦ 𝐴) → ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ ran (𝑘 ∈ ℕ ↦ 𝐴))
156100, 154, 155mp2b 10 . . . . . . . . . . . 12 ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ ran (𝑘 ∈ ℕ ↦ 𝐴)
157156a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ ran (𝑘 ∈ ℕ ↦ 𝐴))
158 disjrnmpt 31804 . . . . . . . . . . . . 13 (Disj 𝑘 ∈ ℕ 𝐴Disj 𝑦 ∈ ran (𝑘 ∈ ℕ ↦ 𝐴)𝑦)
15962, 158syl 17 . . . . . . . . . . . 12 (𝜑Disj 𝑦 ∈ ran (𝑘 ∈ ℕ ↦ 𝐴)𝑦)
160159adantr 482 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → Disj 𝑦 ∈ ran (𝑘 ∈ ℕ ↦ 𝐴)𝑦)
161 disjss1 5119 . . . . . . . . . . 11 (ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ ran (𝑘 ∈ ℕ ↦ 𝐴) → (Disj 𝑦 ∈ ran (𝑘 ∈ ℕ ↦ 𝐴)𝑦Disj 𝑦 ∈ ran (𝑘 ∈ (1...𝑛) ↦ 𝐴)𝑦))
162157, 160, 161sylc 65 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → Disj 𝑦 ∈ ran (𝑘 ∈ (1...𝑛) ↦ 𝐴)𝑦)
163108, 77, 109, 110, 115, 118, 162, 78carsgclctunlem1 33305 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑀‘(𝐸 ran (𝑘 ∈ (1...𝑛) ↦ 𝐴))) = Σ*𝑦 ∈ ran (𝑘 ∈ (1...𝑛) ↦ 𝐴)(𝑀‘(𝐸𝑦)))
164 ineq2 4206 . . . . . . . . . . 11 (𝑦 = 𝐴 → (𝐸𝑦) = (𝐸𝐴))
165164fveq2d 6893 . . . . . . . . . 10 (𝑦 = 𝐴 → (𝑀‘(𝐸𝑦)) = (𝑀‘(𝐸𝐴)))
166111elexi 3494 . . . . . . . . . . 11 (1...𝑛) ∈ V
167166a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1...𝑛) ∈ V)
16899, 102, 22syl2anc 585 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑀‘(𝐸𝐴)) ∈ (0[,]+∞))
169 inss2 4229 . . . . . . . . . . . . . . 15 (𝐸𝐴) ⊆ 𝐴
170 sseq2 4008 . . . . . . . . . . . . . . 15 (𝐴 = ∅ → ((𝐸𝐴) ⊆ 𝐴 ↔ (𝐸𝐴) ⊆ ∅))
171169, 170mpbii 232 . . . . . . . . . . . . . 14 (𝐴 = ∅ → (𝐸𝐴) ⊆ ∅)
172 ss0 4398 . . . . . . . . . . . . . 14 ((𝐸𝐴) ⊆ ∅ → (𝐸𝐴) = ∅)
173171, 172syl 17 . . . . . . . . . . . . 13 (𝐴 = ∅ → (𝐸𝐴) = ∅)
174173adantl 483 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ 𝐴 = ∅) → (𝐸𝐴) = ∅)
175174fveq2d 6893 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ 𝐴 = ∅) → (𝑀‘(𝐸𝐴)) = (𝑀‘∅))
176109ad2antrr 725 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ 𝐴 = ∅) → (𝑀‘∅) = 0)
177175, 176eqtrd 2773 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ 𝐴 = ∅) → (𝑀‘(𝐸𝐴)) = 0)
17862adantr 482 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → Disj 𝑘 ∈ ℕ 𝐴)
179 disjss1 5119 . . . . . . . . . . 11 ((1...𝑛) ⊆ ℕ → (Disj 𝑘 ∈ ℕ 𝐴Disj 𝑘 ∈ (1...𝑛)𝐴))
180101, 178, 179sylc 65 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → Disj 𝑘 ∈ (1...𝑛)𝐴)
181165, 167, 168, 104, 177, 180esumrnmpt2 33055 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → Σ*𝑦 ∈ ran (𝑘 ∈ (1...𝑛) ↦ 𝐴)(𝑀‘(𝐸𝑦)) = Σ*𝑘 ∈ (1...𝑛)(𝑀‘(𝐸𝐴)))
182153, 163, 1813eqtrd 2777 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) = Σ*𝑘 ∈ (1...𝑛)(𝑀‘(𝐸𝐴)))
183150, 151, 1823eqtr3rd 2782 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑛)(𝑀‘(𝐸𝐴)) = ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))))
18417adantr 482 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ∈ (0[,]+∞))
1853, 184sselid 3980 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ∈ ℝ*)
186185xnegcld 13276 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ∈ ℝ*)
18715adantr 482 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝑀𝐸) ∈ ℝ*)
188 iunss1 5011 . . . . . . . . . . . 12 ((1...𝑛) ⊆ ℕ → 𝑘 ∈ (1...𝑛)𝐴 𝑘 ∈ ℕ 𝐴)
189100, 188mp1i 13 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑘 ∈ (1...𝑛)𝐴 𝑘 ∈ ℕ 𝐴)
190189sscond 4141 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐸 𝑘 ∈ ℕ 𝐴) ⊆ (𝐸 𝑘 ∈ (1...𝑛)𝐴))
191743adant1r 1178 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑥𝑦𝑦 ∈ 𝒫 𝑂) → (𝑀𝑥) ≤ (𝑀𝑦))
192108, 77, 190, 84, 191carsgmon 33302 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ≤ (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)))
193 xleneg 13194 . . . . . . . . . 10 (((𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ∈ ℝ* ∧ (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ*) → ((𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ≤ (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ↔ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ≤ -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))))
194193biimpa 478 . . . . . . . . 9 ((((𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ∈ ℝ* ∧ (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ*) ∧ (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ≤ (𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) → -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ≤ -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)))
195185, 86, 192, 194syl21anc 837 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ≤ -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)))
196 xleadd2a 13230 . . . . . . . 8 (((-𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* ∧ -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ∈ ℝ* ∧ (𝑀𝐸) ∈ ℝ*) ∧ -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴)) ≤ -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) → ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) ≤ ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))))
19789, 186, 187, 195, 196syl31anc 1374 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ (1...𝑛)𝐴))) ≤ ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))))
198183, 197eqbrtrd 5170 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → Σ*𝑘 ∈ (1...𝑛)(𝑀‘(𝐸𝐴)) ≤ ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))))
19976, 22, 198esumgect 33077 . . . . 5 (𝜑 → Σ*𝑘 ∈ ℕ(𝑀‘(𝐸𝐴)) ≤ ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))))
20012, 27, 20, 71, 199xrletrd 13138 . . . 4 (𝜑 → (𝑀 𝑘 ∈ ℕ (𝐸𝐴)) ≤ ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))))
2012, 200eqbrtrrid 5184 . . 3 (𝜑 → (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ≤ ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))))
202 xleadd1a 13229 . . 3 ((((𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ∈ ℝ* ∧ ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) ∈ ℝ* ∧ (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ∈ ℝ*) ∧ (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ≤ ((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)))) → ((𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) ≤ (((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) +𝑒 (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))))
20313, 20, 18, 201, 202syl31anc 1374 . 2 (𝜑 → ((𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) ≤ (((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) +𝑒 (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))))
204 xrge0npcan 32183 . . 3 (((𝑀𝐸) ∈ (0[,]+∞) ∧ (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ∈ (0[,]+∞) ∧ (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) ≤ (𝑀𝐸)) → (((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) +𝑒 (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) = (𝑀𝐸))
20514, 17, 75, 204syl3anc 1372 . 2 (𝜑 → (((𝑀𝐸) +𝑒 -𝑒(𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) +𝑒 (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) = (𝑀𝐸))
206203, 205breqtrd 5174 1 (𝜑 → ((𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴)) +𝑒 (𝑀‘(𝐸 𝑘 ∈ ℕ 𝐴))) ≤ (𝑀𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  wne 2941  wral 3062  Vcvv 3475  cdif 3945  cin 3947  wss 3948  c0 4322  𝒫 cpw 4602   cuni 4908   ciun 4997  Disj wdisj 5113   class class class wbr 5148  cmpt 5231  ran crn 5677  wf 6537  cfv 6541  (class class class)co 7406  ωcom 7852  cdom 8934  Fincfn 8936  0cc0 11107  1c1 11108  +∞cpnf 11242  -∞cmnf 11243  *cxr 11244  cle 11246  cn 12209  -𝑒cxne 13086   +𝑒 cxad 13087  [,]cicc 13324  ...cfz 13481  Σ*cesum 33014  toCaraSigaccarsg 33289
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633  ax-ac2 10455  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185  ax-addf 11186  ax-mulf 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-disj 5114  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-of 7667  df-om 7853  df-1st 7972  df-2nd 7973  df-supp 8144  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-2o 8464  df-er 8700  df-map 8819  df-pm 8820  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-dju 9893  df-card 9931  df-acn 9934  df-ac 10108  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-fac 14231  df-bc 14260  df-hash 14288  df-shft 15011  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-limsup 15412  df-clim 15429  df-rlim 15430  df-sum 15630  df-ef 16008  df-sin 16010  df-cos 16011  df-pi 16013  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-ress 17171  df-plusg 17207  df-mulr 17208  df-starv 17209  df-sca 17210  df-vsca 17211  df-ip 17212  df-tset 17213  df-ple 17214  df-ds 17216  df-unif 17217  df-hom 17218  df-cco 17219  df-rest 17365  df-topn 17366  df-0g 17384  df-gsum 17385  df-topgen 17386  df-pt 17387  df-prds 17390  df-ordt 17444  df-xrs 17445  df-qtop 17450  df-imas 17451  df-xps 17453  df-mre 17527  df-mrc 17528  df-acs 17530  df-ps 18516  df-tsr 18517  df-plusf 18557  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-mhm 18668  df-submnd 18669  df-grp 18819  df-minusg 18820  df-sbg 18821  df-mulg 18946  df-subg 18998  df-cntz 19176  df-cmn 19645  df-abl 19646  df-mgp 19983  df-ur 20000  df-ring 20052  df-cring 20053  df-subrg 20354  df-abv 20418  df-lmod 20466  df-scaf 20467  df-sra 20778  df-rgmod 20779  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-fbas 20934  df-fg 20935  df-cnfld 20938  df-top 22388  df-topon 22405  df-topsp 22427  df-bases 22441  df-cld 22515  df-ntr 22516  df-cls 22517  df-nei 22594  df-lp 22632  df-perf 22633  df-cn 22723  df-cnp 22724  df-haus 22811  df-tx 23058  df-hmeo 23251  df-fil 23342  df-fm 23434  df-flim 23435  df-flf 23436  df-tmd 23568  df-tgp 23569  df-tsms 23623  df-trg 23656  df-xms 23818  df-ms 23819  df-tms 23820  df-nm 24083  df-ngp 24084  df-nrg 24086  df-nlm 24087  df-ii 24385  df-cncf 24386  df-limc 25375  df-dv 25376  df-log 26057  df-esum 33015  df-carsg 33290
This theorem is referenced by:  carsgclctunlem3  33308
  Copyright terms: Public domain W3C validator