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 simpr ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o )
17 en1b ⊢ ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ↔ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } = { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } )
18 16 17 sylib ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } = { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } )
19 ssrab2 ⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ⊆ ℙ
20 18 19 eqsstrrdi ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } ⊆ ℙ )
21 7 uniexd ⊢ ( 𝐴 ∈ ℕ → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ V )
22 21 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ V )
23 snssg ⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ V → ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ ↔ { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } ⊆ ℙ ) )
24 22 23 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ ↔ { ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } } ⊆ ℙ ) )
25 20 24 mpbird ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ )
26 prmuz2 ⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℙ → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) )
27 25 26 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) )
28 eluzelre ⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℝ )
29 27 28 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ℝ )
30 eluz2gt1 ⊢ ( ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ∈ ( ℤ≥ ‘ 2 ) → 1 < ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } )
31 27 30 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → 1 < ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } )
32 29 31 rplogcld ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ∈ ℝ+ )
33 32 rpne0d ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) ≠ 0 )
34 15 33 eqnetrd ⊢ ( ( 𝐴 ∈ ℕ ∧ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 )
35 34 ex ⊢ ( 𝐴 ∈ ℕ → ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
36 iffalse ⊢ ( ¬ ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 → if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) = 0 )
37 36 necon1ai ⊢ ( if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 → ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 )
38 37 13 imbitrid ⊢ ( 𝐴 ∈ ℕ → ( if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ) )
39 35 38 impbid ⊢ ( 𝐴 ∈ ℕ → ( { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ≈ 1o ↔ if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
40 4 39 bitrid ⊢ ( 𝐴 ∈ ℕ → ( ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝐴 ↔ if ( ( ♯ ‘ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) = 1 , ( log ‘ ∪ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } ) , 0 ) ≠ 0 ) )
41 3 40 bitr4d ⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ ∃! 𝑝 ∈ ℙ 𝑝 ∥ 𝐴 ) )