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

Metamath Proof Explorer

Theorem isppw

Description: Two ways to say that A is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion isppw ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 }
2 1 vmaval ⊢ ( 𝐴 ∈ ℕ → ( Λ ‘ 𝐴 ) = if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) )
3 2 neeq1d ⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
4 reuen1 ⊢ ( ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝐴 ↔ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o )
5 hash1 ⊢ ( ♯ ‘ 1o ) = 1
6 5 eqeq2i ⊢ ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = ( ♯ ‘ 1o ) ↔ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 )
7 prmdvdsfi ⊢ ( 𝐴 ∈ ℕ → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ Fin )
8 1onn ⊢ 1o ∈ ω
9 nnfi ⊢ ( 1o ∈ ω → 1o ∈ Fin )
10 8 9 ax-mp ⊢ 1o ∈ Fin
11 hashen ⊢ ( ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ Fin ∧ 1o ∈ Fin ) → ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = ( ♯ ‘ 1o ) ↔ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) )
12 7 10 11 sylancl ⊢ ( 𝐴 ∈ ℕ → ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = ( ♯ ‘ 1o ) ↔ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) )
13 6 12 bitr3id ⊢ ( 𝐴 ∈ ℕ → ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 ↔ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) )
14 13 biimpar ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 )
15 14 iftrued ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) = ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) )
16 en1b ⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ↔ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } = { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } )
17 16 bilani ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } = { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } )
18 ssrab2 ⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ⊆ ℙ
19 17 18 eqsstrrdi ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } ⊆ ℙ )
20 7 uniexd ⊢ ( 𝐴 ∈ ℕ → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ V )
21 20 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ V )
22 snssg ⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ V → ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ ↔ { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } ⊆ ℙ ) )
23 21 22 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ ↔ { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } ⊆ ℙ ) )
24 19 23 mpbird ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ )
25 prmuz2 ⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) )
26 24 25 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) )
27 eluzelre ⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℝ )
28 26 27 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℝ )
29 eluz2gt1 ⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) → 1 < ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } )
30 26 29 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → 1 < ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } )
31 28 30 rplogcld ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℝ+ )
32 31 rpne0d ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ≠ 0 )
33 15 32 eqnetrd ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 )
34 33 ex ⊢ ( 𝐴 ∈ ℕ → ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
35 iffalse ⊢ ( ¬ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) = 0 )
36 35 necon1ai ⊢ ( if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 )
37 36 13 imbitrid ⊢ ( 𝐴 ∈ ℕ → ( if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) )
38 34 37 impbid ⊢ ( 𝐴 ∈ ℕ → ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ↔ if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
39 4 38 bitrid ⊢ ( 𝐴 ∈ ℕ → ( ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝐴 ↔ if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
40 3 39 bitr4d ⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝐴 ) )