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

Metamath Proof Explorer

Theorem zrtdvds

Description: A positive integer root divides its integer. (Contributed by Steven Nguyen, 6-Apr-2023)

Ref Expression
Assertion zrtdvds 
|- ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. NN ) -> ( A ^c ( 1 / N ) ) || A )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( ( A ^c ( 1 / N ) ) e. NN -> ( A ^c ( 1 / N ) ) e. ZZ )
2 1 3ad2ant3 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. NN ) -> ( A ^c ( 1 / N ) ) e. ZZ )
3 simp2 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. NN ) -> N e. NN )
4 iddvdsexp 
 |-  ( ( ( A ^c ( 1 / N ) ) e. ZZ /\ N e. NN ) -> ( A ^c ( 1 / N ) ) || ( ( A ^c ( 1 / N ) ) ^ N ) )
5 2 3 4 syl2anc 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. NN ) -> ( A ^c ( 1 / N ) ) || ( ( A ^c ( 1 / N ) ) ^ N ) )
6 zcn 
 |-  ( A e. ZZ -> A e. CC )
7 6 3ad2ant1 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. NN ) -> A e. CC )
8 cxproot 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( A ^c ( 1 / N ) ) ^ N ) = A )
9 7 3 8 syl2anc 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. NN ) -> ( ( A ^c ( 1 / N ) ) ^ N ) = A )
10 5 9 breqtrd 
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A ^c ( 1 / N ) ) e. NN ) -> ( A ^c ( 1 / N ) ) || A )