Metamath Proof Explorer

Theorem dec2nprm

Description: Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Hypotheses dec5nprm.1 ⊢ 𝐴 ∈ ℕ
dec2nprm.2 ⊢ 𝐵 ∈ ℕ0
dec2nprm.3 ⊢ ( 𝐵 · 2 ) = 𝐶
Assertion dec2nprm ¬ 𝐴 𝐶 ∈ ℙ

Proof

Step Hyp Ref Expression
1 dec5nprm.1 ⊢ 𝐴 ∈ ℕ
2 dec2nprm.2 ⊢ 𝐵 ∈ ℕ0
3 dec2nprm.3 ⊢ ( 𝐵 · 2 ) = 𝐶
4 5nn ⊢ 5 ∈ ℕ
5 4 1 nnmulcli ⊢ ( 5 · 𝐴 ) ∈ ℕ
6 nnnn0addcl ⊢ ( ( ( 5 · 𝐴 ) ∈ ℕ ∧ 𝐵 ∈ ℕ0 ) → ( ( 5 · 𝐴 ) + 𝐵 ) ∈ ℕ )
7 5 2 6 mp2an ⊢ ( ( 5 · 𝐴 ) + 𝐵 ) ∈ ℕ
8 2nn ⊢ 2 ∈ ℕ
9 1nn0 ⊢ 1 ∈ ℕ0
10 1lt5 ⊢ 1 < 5
11 4 1 2 9 10 numlti ⊢ 1 < ( ( 5 · 𝐴 ) + 𝐵 )
12 1lt2 ⊢ 1 < 2
13 4 nncni ⊢ 5 ∈ ℂ
14 1 nncni ⊢ 𝐴 ∈ ℂ
15 2cn ⊢ 2 ∈ ℂ
16 13 14 15 mul32i ⊢ ( ( 5 · 𝐴 ) · 2 ) = ( ( 5 · 2 ) · 𝐴 )
17 5t2e10 ⊢ ( 5 · 2 ) = 1 0
18 17 oveq1i ⊢ ( ( 5 · 2 ) · 𝐴 ) = ( 1 0 · 𝐴 )
19 16 18 eqtri ⊢ ( ( 5 · 𝐴 ) · 2 ) = ( 1 0 · 𝐴 )
20 19 3 oveq12i ⊢ ( ( ( 5 · 𝐴 ) · 2 ) + ( 𝐵 · 2 ) ) = ( ( 1 0 · 𝐴 ) + 𝐶 )
21 5 nncni ⊢ ( 5 · 𝐴 ) ∈ ℂ
22 2 nn0cni ⊢ 𝐵 ∈ ℂ
23 21 22 15 adddiri ⊢ ( ( ( 5 · 𝐴 ) + 𝐵 ) · 2 ) = ( ( ( 5 · 𝐴 ) · 2 ) + ( 𝐵 · 2 ) )
24 dfdec10 ⊢ 𝐴 𝐶 = ( ( 1 0 · 𝐴 ) + 𝐶 )
25 20 23 24 3eqtr4i ⊢ ( ( ( 5 · 𝐴 ) + 𝐵 ) · 2 ) = 𝐴 𝐶
26 7 8 11 12 25 nprmi ⊢ ¬ 𝐴 𝐶 ∈ ℙ