This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pnfinf

Description: Plus infinity is an infinite for the completed real line, as any real number is infinitesimal compared to it. (Contributed by Thierry Arnoux, 1-Feb-2018)

Ref Expression
Assertion pnfinf 
|- ( A e. RR+ -> A ( <<< ` RR*s ) +oo )

Proof

Step Hyp Ref Expression
1 rpgt0 
 |-  ( A e. RR+ -> 0 < A )
2 nnz 
 |-  ( n e. NN -> n e. ZZ )
3 2 adantl 
 |-  ( ( A e. RR+ /\ n e. NN ) -> n e. ZZ )
4 rpxr 
 |-  ( A e. RR+ -> A e. RR* )
5 4 adantr 
 |-  ( ( A e. RR+ /\ n e. NN ) -> A e. RR* )
6 xrsmulgzz 
 |-  ( ( n e. ZZ /\ A e. RR* ) -> ( n ( .g ` RR*s ) A ) = ( n *e A ) )
7 3 5 6 syl2anc 
 |-  ( ( A e. RR+ /\ n e. NN ) -> ( n ( .g ` RR*s ) A ) = ( n *e A ) )
8 3 zred 
 |-  ( ( A e. RR+ /\ n e. NN ) -> n e. RR )
9 rpre 
 |-  ( A e. RR+ -> A e. RR )
10 9 adantr 
 |-  ( ( A e. RR+ /\ n e. NN ) -> A e. RR )
11 rexmul 
 |-  ( ( n e. RR /\ A e. RR ) -> ( n *e A ) = ( n x. A ) )
12 remulcl 
 |-  ( ( n e. RR /\ A e. RR ) -> ( n x. A ) e. RR )
13 11 12 eqeltrd 
 |-  ( ( n e. RR /\ A e. RR ) -> ( n *e A ) e. RR )
14 8 10 13 syl2anc 
 |-  ( ( A e. RR+ /\ n e. NN ) -> ( n *e A ) e. RR )
15 7 14 eqeltrd 
 |-  ( ( A e. RR+ /\ n e. NN ) -> ( n ( .g ` RR*s ) A ) e. RR )
16 ltpnf 
 |-  ( ( n ( .g ` RR*s ) A ) e. RR -> ( n ( .g ` RR*s ) A ) < +oo )
17 15 16 syl 
 |-  ( ( A e. RR+ /\ n e. NN ) -> ( n ( .g ` RR*s ) A ) < +oo )
18 17 ralrimiva 
 |-  ( A e. RR+ -> A. n e. NN ( n ( .g ` RR*s ) A ) < +oo )
19 xrsex 
 |-  RR*s e. _V
20 pnfxr 
 |-  +oo e. RR*
21 xrsbas 
 |-  RR* = ( Base ` RR*s )
22 xrs0 
 |-  0 = ( 0g ` RR*s )
23 eqid 
 |-  ( .g ` RR*s ) = ( .g ` RR*s )
24 xrslt 
 |-  < = ( lt ` RR*s )
25 21 22 23 24 isinftm 
 |-  ( ( RR*s e. _V /\ A e. RR* /\ +oo e. RR* ) -> ( A ( <<< ` RR*s ) +oo <-> ( 0 < A /\ A. n e. NN ( n ( .g ` RR*s ) A ) < +oo ) ) )
26 19 20 25 mp3an13 
 |-  ( A e. RR* -> ( A ( <<< ` RR*s ) +oo <-> ( 0 < A /\ A. n e. NN ( n ( .g ` RR*s ) A ) < +oo ) ) )
27 4 26 syl 
 |-  ( A e. RR+ -> ( A ( <<< ` RR*s ) +oo <-> ( 0 < A /\ A. n e. NN ( n ( .g ` RR*s ) A ) < +oo ) ) )
28 1 18 27 mpbir2and 
 |-  ( A e. RR+ -> A ( <<< ` RR*s ) +oo )