![]() |
Mathbox for Glauco Siliprandi |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > sge0repnf | Structured version Visualization version GIF version |
Description: The of nonnegative extended reals is a real number if and only if it is not +∞. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Ref | Expression |
---|---|
sge0repnf.x | ⊢ (𝜑 → 𝑋 ∈ 𝑉) |
sge0repnf.f | ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) |
Ref | Expression |
---|---|
sge0repnf | ⊢ (𝜑 → ((Σ^‘𝐹) ∈ ℝ ↔ ¬ (Σ^‘𝐹) = +∞)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | renepnf 10482 | . . . 4 ⊢ ((Σ^‘𝐹) ∈ ℝ → (Σ^‘𝐹) ≠ +∞) | |
2 | 1 | neneqd 2966 | . . 3 ⊢ ((Σ^‘𝐹) ∈ ℝ → ¬ (Σ^‘𝐹) = +∞) |
3 | 2 | a1i 11 | . 2 ⊢ (𝜑 → ((Σ^‘𝐹) ∈ ℝ → ¬ (Σ^‘𝐹) = +∞)) |
4 | rge0ssre 12654 | . . . 4 ⊢ (0[,)+∞) ⊆ ℝ | |
5 | 0xr 10481 | . . . . . 6 ⊢ 0 ∈ ℝ* | |
6 | 5 | a1i 11 | . . . . 5 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) = +∞) → 0 ∈ ℝ*) |
7 | pnfxr 10488 | . . . . . 6 ⊢ +∞ ∈ ℝ* | |
8 | 7 | a1i 11 | . . . . 5 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) = +∞) → +∞ ∈ ℝ*) |
9 | sge0repnf.x | . . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝑉) | |
10 | sge0repnf.f | . . . . . . 7 ⊢ (𝜑 → 𝐹:𝑋⟶(0[,]+∞)) | |
11 | 9, 10 | sge0xrcl 42098 | . . . . . 6 ⊢ (𝜑 → (Σ^‘𝐹) ∈ ℝ*) |
12 | 11 | adantr 473 | . . . . 5 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) = +∞) → (Σ^‘𝐹) ∈ ℝ*) |
13 | 9, 10 | sge0ge0 42097 | . . . . . 6 ⊢ (𝜑 → 0 ≤ (Σ^‘𝐹)) |
14 | 13 | adantr 473 | . . . . 5 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) = +∞) → 0 ≤ (Σ^‘𝐹)) |
15 | simpr 477 | . . . . . . 7 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) = +∞) → ¬ (Σ^‘𝐹) = +∞) | |
16 | nltpnft 12368 | . . . . . . . . 9 ⊢ ((Σ^‘𝐹) ∈ ℝ* → ((Σ^‘𝐹) = +∞ ↔ ¬ (Σ^‘𝐹) < +∞)) | |
17 | 11, 16 | syl 17 | . . . . . . . 8 ⊢ (𝜑 → ((Σ^‘𝐹) = +∞ ↔ ¬ (Σ^‘𝐹) < +∞)) |
18 | 17 | adantr 473 | . . . . . . 7 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) = +∞) → ((Σ^‘𝐹) = +∞ ↔ ¬ (Σ^‘𝐹) < +∞)) |
19 | 15, 18 | mtbid 316 | . . . . . 6 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) = +∞) → ¬ ¬ (Σ^‘𝐹) < +∞) |
20 | 19 | notnotrd 131 | . . . . 5 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) = +∞) → (Σ^‘𝐹) < +∞) |
21 | 6, 8, 12, 14, 20 | elicod 12597 | . . . 4 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) = +∞) → (Σ^‘𝐹) ∈ (0[,)+∞)) |
22 | 4, 21 | sseldi 3850 | . . 3 ⊢ ((𝜑 ∧ ¬ (Σ^‘𝐹) = +∞) → (Σ^‘𝐹) ∈ ℝ) |
23 | 22 | ex 405 | . 2 ⊢ (𝜑 → (¬ (Σ^‘𝐹) = +∞ → (Σ^‘𝐹) ∈ ℝ)) |
24 | 3, 23 | impbid 204 | 1 ⊢ (𝜑 → ((Σ^‘𝐹) ∈ ℝ ↔ ¬ (Σ^‘𝐹) = +∞)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 ∈ wcel 2050 class class class wbr 4923 ⟶wf 6178 ‘cfv 6182 (class class class)co 6970 ℝcr 10328 0cc0 10329 +∞cpnf 10465 ℝ*cxr 10467 < clt 10468 ≤ cle 10469 [,)cico 12550 [,]cicc 12551 Σ^csumge0 42075 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-inf2 8892 ax-cnex 10385 ax-resscn 10386 ax-1cn 10387 ax-icn 10388 ax-addcl 10389 ax-addrcl 10390 ax-mulcl 10391 ax-mulrcl 10392 ax-mulcom 10393 ax-addass 10394 ax-mulass 10395 ax-distr 10396 ax-i2m1 10397 ax-1ne0 10398 ax-1rid 10399 ax-rnegex 10400 ax-rrecex 10401 ax-cnre 10402 ax-pre-lttri 10403 ax-pre-lttrn 10404 ax-pre-ltadd 10405 ax-pre-mulgt0 10406 ax-pre-sup 10407 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rmo 3090 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-pss 3839 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-int 4744 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5306 df-eprel 5311 df-po 5320 df-so 5321 df-fr 5360 df-se 5361 df-we 5362 df-xp 5407 df-rel 5408 df-cnv 5409 df-co 5410 df-dm 5411 df-rn 5412 df-res 5413 df-ima 5414 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-isom 6191 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-om 7391 df-1st 7495 df-2nd 7496 df-wrecs 7744 df-recs 7806 df-rdg 7844 df-1o 7899 df-oadd 7903 df-er 8083 df-en 8301 df-dom 8302 df-sdom 8303 df-fin 8304 df-sup 8695 df-oi 8763 df-card 9156 df-pnf 10470 df-mnf 10471 df-xr 10472 df-ltxr 10473 df-le 10474 df-sub 10666 df-neg 10667 df-div 11093 df-nn 11434 df-2 11497 df-3 11498 df-n0 11702 df-z 11788 df-uz 12053 df-rp 12199 df-ico 12554 df-icc 12555 df-fz 12703 df-fzo 12844 df-seq 13179 df-exp 13239 df-hash 13500 df-cj 14313 df-re 14314 df-im 14315 df-sqrt 14449 df-abs 14450 df-clim 14700 df-sum 14898 df-sumge0 42076 |
This theorem is referenced by: sge0rern 42101 sge0supre 42102 sge0less 42105 sge0le 42120 sge0split 42122 sge0iunmpt 42131 sge0rpcpnf 42134 sge0xadd 42148 sge0repnfmpt 42152 sge0gtfsumgt 42156 omeiunltfirp 42232 hoidmv1lelem1 42304 hoidmv1lelem2 42305 hoidmv1lelem3 42306 hoidmv1le 42307 hoidmvlelem3 42310 hoidmvlelem5 42312 |
Copyright terms: Public domain | W3C validator |