| Step |
Hyp |
Ref |
Expression |
| 1 |
|
qrng.q |
⊢ 𝑄 = ( ℂfld ↾s ℚ ) |
| 2 |
|
qabsabv.a |
⊢ 𝐴 = ( AbsVal ‘ 𝑄 ) |
| 3 |
|
padic.f |
⊢ 𝐹 = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑥 ) ) ) ) |
| 4 |
2
|
a1i |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → 𝐴 = ( AbsVal ‘ 𝑄 ) ) |
| 5 |
1
|
qrngbas |
⊢ ℚ = ( Base ‘ 𝑄 ) |
| 6 |
5
|
a1i |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → ℚ = ( Base ‘ 𝑄 ) ) |
| 7 |
|
qex |
⊢ ℚ ∈ V |
| 8 |
|
cnfldadd |
⊢ + = ( +g ‘ ℂfld ) |
| 9 |
1 8
|
ressplusg |
⊢ ( ℚ ∈ V → + = ( +g ‘ 𝑄 ) ) |
| 10 |
7 9
|
mp1i |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → + = ( +g ‘ 𝑄 ) ) |
| 11 |
|
cnfldmul |
⊢ · = ( .r ‘ ℂfld ) |
| 12 |
1 11
|
ressmulr |
⊢ ( ℚ ∈ V → · = ( .r ‘ 𝑄 ) ) |
| 13 |
7 12
|
mp1i |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → · = ( .r ‘ 𝑄 ) ) |
| 14 |
1
|
qrng0 |
⊢ 0 = ( 0g ‘ 𝑄 ) |
| 15 |
14
|
a1i |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → 0 = ( 0g ‘ 𝑄 ) ) |
| 16 |
1
|
qdrng |
⊢ 𝑄 ∈ DivRing |
| 17 |
|
drngring |
⊢ ( 𝑄 ∈ DivRing → 𝑄 ∈ Ring ) |
| 18 |
16 17
|
mp1i |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → 𝑄 ∈ Ring ) |
| 19 |
|
0red |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑥 ∈ ℚ ) ∧ 𝑥 = 0 ) → 0 ∈ ℝ ) |
| 20 |
|
ioossre |
⊢ ( 0 (,) 1 ) ⊆ ℝ |
| 21 |
|
simpr |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → 𝑁 ∈ ( 0 (,) 1 ) ) |
| 22 |
20 21
|
sselid |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → 𝑁 ∈ ℝ ) |
| 23 |
22
|
ad2antrr |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑥 ∈ ℚ ) ∧ ¬ 𝑥 = 0 ) → 𝑁 ∈ ℝ ) |
| 24 |
|
eliooord |
⊢ ( 𝑁 ∈ ( 0 (,) 1 ) → ( 0 < 𝑁 ∧ 𝑁 < 1 ) ) |
| 25 |
24
|
adantl |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → ( 0 < 𝑁 ∧ 𝑁 < 1 ) ) |
| 26 |
25
|
simpld |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → 0 < 𝑁 ) |
| 27 |
22 26
|
elrpd |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → 𝑁 ∈ ℝ+ ) |
| 28 |
27
|
rpne0d |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → 𝑁 ≠ 0 ) |
| 29 |
28
|
ad2antrr |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑥 ∈ ℚ ) ∧ ¬ 𝑥 = 0 ) → 𝑁 ≠ 0 ) |
| 30 |
|
df-ne |
⊢ ( 𝑥 ≠ 0 ↔ ¬ 𝑥 = 0 ) |
| 31 |
|
pcqcl |
⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑥 ∈ ℚ ∧ 𝑥 ≠ 0 ) ) → ( 𝑃 pCnt 𝑥 ) ∈ ℤ ) |
| 32 |
31
|
adantlr |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑥 ∈ ℚ ∧ 𝑥 ≠ 0 ) ) → ( 𝑃 pCnt 𝑥 ) ∈ ℤ ) |
| 33 |
32
|
anassrs |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑥 ∈ ℚ ) ∧ 𝑥 ≠ 0 ) → ( 𝑃 pCnt 𝑥 ) ∈ ℤ ) |
| 34 |
30 33
|
sylan2br |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑥 ∈ ℚ ) ∧ ¬ 𝑥 = 0 ) → ( 𝑃 pCnt 𝑥 ) ∈ ℤ ) |
| 35 |
23 29 34
|
reexpclzd |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑥 ∈ ℚ ) ∧ ¬ 𝑥 = 0 ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑥 ) ) ∈ ℝ ) |
| 36 |
19 35
|
ifclda |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑥 ∈ ℚ ) → if ( 𝑥 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑥 ) ) ) ∈ ℝ ) |
| 37 |
36 3
|
fmptd |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → 𝐹 : ℚ ⟶ ℝ ) |
| 38 |
|
0z |
⊢ 0 ∈ ℤ |
| 39 |
|
zq |
⊢ ( 0 ∈ ℤ → 0 ∈ ℚ ) |
| 40 |
38 39
|
ax-mp |
⊢ 0 ∈ ℚ |
| 41 |
|
iftrue |
⊢ ( 𝑥 = 0 → if ( 𝑥 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑥 ) ) ) = 0 ) |
| 42 |
|
c0ex |
⊢ 0 ∈ V |
| 43 |
41 3 42
|
fvmpt |
⊢ ( 0 ∈ ℚ → ( 𝐹 ‘ 0 ) = 0 ) |
| 44 |
40 43
|
mp1i |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → ( 𝐹 ‘ 0 ) = 0 ) |
| 45 |
22
|
3ad2ant1 |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) → 𝑁 ∈ ℝ ) |
| 46 |
|
pcqcl |
⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℤ ) |
| 47 |
46
|
adantlr |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℤ ) |
| 48 |
47
|
3impb |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) → ( 𝑃 pCnt 𝑦 ) ∈ ℤ ) |
| 49 |
26
|
3ad2ant1 |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) → 0 < 𝑁 ) |
| 50 |
|
expgt0 |
⊢ ( ( 𝑁 ∈ ℝ ∧ ( 𝑃 pCnt 𝑦 ) ∈ ℤ ∧ 0 < 𝑁 ) → 0 < ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) |
| 51 |
45 48 49 50
|
syl3anc |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) → 0 < ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) |
| 52 |
|
eqeq1 |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 0 ↔ 𝑦 = 0 ) ) |
| 53 |
|
oveq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝑃 pCnt 𝑥 ) = ( 𝑃 pCnt 𝑦 ) ) |
| 54 |
53
|
oveq2d |
⊢ ( 𝑥 = 𝑦 → ( 𝑁 ↑ ( 𝑃 pCnt 𝑥 ) ) = ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) |
| 55 |
52 54
|
ifbieq2d |
⊢ ( 𝑥 = 𝑦 → if ( 𝑥 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑥 ) ) ) = if ( 𝑦 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) |
| 56 |
|
ovex |
⊢ ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ∈ V |
| 57 |
42 56
|
ifex |
⊢ if ( 𝑦 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ∈ V |
| 58 |
55 3 57
|
fvmpt |
⊢ ( 𝑦 ∈ ℚ → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) |
| 59 |
58
|
3ad2ant2 |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) |
| 60 |
|
simp3 |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) → 𝑦 ≠ 0 ) |
| 61 |
60
|
neneqd |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) → ¬ 𝑦 = 0 ) |
| 62 |
61
|
iffalsed |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) → if ( 𝑦 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) = ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) |
| 63 |
59 62
|
eqtrd |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) |
| 64 |
51 63
|
breqtrrd |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) → 0 < ( 𝐹 ‘ 𝑦 ) ) |
| 65 |
|
pcqmul |
⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) = ( ( 𝑃 pCnt 𝑦 ) + ( 𝑃 pCnt 𝑧 ) ) ) |
| 66 |
65
|
3adant1r |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) = ( ( 𝑃 pCnt 𝑦 ) + ( 𝑃 pCnt 𝑧 ) ) ) |
| 67 |
66
|
oveq2d |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) ) = ( 𝑁 ↑ ( ( 𝑃 pCnt 𝑦 ) + ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 68 |
22
|
recnd |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → 𝑁 ∈ ℂ ) |
| 69 |
68
|
3ad2ant1 |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → 𝑁 ∈ ℂ ) |
| 70 |
28
|
3ad2ant1 |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → 𝑁 ≠ 0 ) |
| 71 |
47
|
3adant3 |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℤ ) |
| 72 |
|
simp1l |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → 𝑃 ∈ ℙ ) |
| 73 |
|
simp3l |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → 𝑧 ∈ ℚ ) |
| 74 |
|
simp3r |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → 𝑧 ≠ 0 ) |
| 75 |
|
pcqcl |
⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑃 pCnt 𝑧 ) ∈ ℤ ) |
| 76 |
72 73 74 75
|
syl12anc |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑃 pCnt 𝑧 ) ∈ ℤ ) |
| 77 |
|
expaddz |
⊢ ( ( ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) ∧ ( ( 𝑃 pCnt 𝑦 ) ∈ ℤ ∧ ( 𝑃 pCnt 𝑧 ) ∈ ℤ ) ) → ( 𝑁 ↑ ( ( 𝑃 pCnt 𝑦 ) + ( 𝑃 pCnt 𝑧 ) ) ) = ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) · ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 78 |
69 70 71 76 77
|
syl22anc |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑁 ↑ ( ( 𝑃 pCnt 𝑦 ) + ( 𝑃 pCnt 𝑧 ) ) ) = ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) · ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 79 |
67 78
|
eqtrd |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) ) = ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) · ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 80 |
|
simp2l |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → 𝑦 ∈ ℚ ) |
| 81 |
|
qmulcl |
⊢ ( ( 𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ ) → ( 𝑦 · 𝑧 ) ∈ ℚ ) |
| 82 |
80 73 81
|
syl2anc |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 · 𝑧 ) ∈ ℚ ) |
| 83 |
|
eqeq1 |
⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( 𝑥 = 0 ↔ ( 𝑦 · 𝑧 ) = 0 ) ) |
| 84 |
|
oveq2 |
⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( 𝑃 pCnt 𝑥 ) = ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) ) |
| 85 |
84
|
oveq2d |
⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑥 ) ) = ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) ) ) |
| 86 |
83 85
|
ifbieq2d |
⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → if ( 𝑥 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑥 ) ) ) = if ( ( 𝑦 · 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) ) ) ) |
| 87 |
|
ovex |
⊢ ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) ) ∈ V |
| 88 |
42 87
|
ifex |
⊢ if ( ( 𝑦 · 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) ) ) ∈ V |
| 89 |
86 3 88
|
fvmpt |
⊢ ( ( 𝑦 · 𝑧 ) ∈ ℚ → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = if ( ( 𝑦 · 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) ) ) ) |
| 90 |
82 89
|
syl |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = if ( ( 𝑦 · 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) ) ) ) |
| 91 |
|
qcn |
⊢ ( 𝑦 ∈ ℚ → 𝑦 ∈ ℂ ) |
| 92 |
80 91
|
syl |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → 𝑦 ∈ ℂ ) |
| 93 |
|
qcn |
⊢ ( 𝑧 ∈ ℚ → 𝑧 ∈ ℂ ) |
| 94 |
73 93
|
syl |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → 𝑧 ∈ ℂ ) |
| 95 |
|
simp2r |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → 𝑦 ≠ 0 ) |
| 96 |
92 94 95 74
|
mulne0d |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 · 𝑧 ) ≠ 0 ) |
| 97 |
96
|
neneqd |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ¬ ( 𝑦 · 𝑧 ) = 0 ) |
| 98 |
97
|
iffalsed |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → if ( ( 𝑦 · 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) ) ) = ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) ) ) |
| 99 |
90 98
|
eqtrd |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 · 𝑧 ) ) ) ) |
| 100 |
63
|
3expb |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) |
| 101 |
100
|
3adant3 |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) |
| 102 |
|
eqeq1 |
⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 0 ↔ 𝑧 = 0 ) ) |
| 103 |
|
oveq2 |
⊢ ( 𝑥 = 𝑧 → ( 𝑃 pCnt 𝑥 ) = ( 𝑃 pCnt 𝑧 ) ) |
| 104 |
103
|
oveq2d |
⊢ ( 𝑥 = 𝑧 → ( 𝑁 ↑ ( 𝑃 pCnt 𝑥 ) ) = ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) |
| 105 |
102 104
|
ifbieq2d |
⊢ ( 𝑥 = 𝑧 → if ( 𝑥 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑥 ) ) ) = if ( 𝑧 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 106 |
|
ovex |
⊢ ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ∈ V |
| 107 |
42 106
|
ifex |
⊢ if ( 𝑧 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ∈ V |
| 108 |
105 3 107
|
fvmpt |
⊢ ( 𝑧 ∈ ℚ → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 109 |
73 108
|
syl |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 110 |
74
|
neneqd |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ¬ 𝑧 = 0 ) |
| 111 |
110
|
iffalsed |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → if ( 𝑧 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) = ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) |
| 112 |
109 111
|
eqtrd |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) |
| 113 |
101 112
|
oveq12d |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) · ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 114 |
79 99 113
|
3eqtr4d |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) ) |
| 115 |
|
iftrue |
⊢ ( ( 𝑦 + 𝑧 ) = 0 → if ( ( 𝑦 + 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) = 0 ) |
| 116 |
115
|
breq1d |
⊢ ( ( 𝑦 + 𝑧 ) = 0 → ( if ( ( 𝑦 + 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ↔ 0 ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) ) |
| 117 |
|
ifnefalse |
⊢ ( ( 𝑦 + 𝑧 ) ≠ 0 → if ( ( 𝑦 + 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) = ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) |
| 118 |
117
|
adantl |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → if ( ( 𝑦 + 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) = ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) |
| 119 |
71
|
adantr |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑃 pCnt 𝑦 ) ∈ ℤ ) |
| 120 |
119
|
zred |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑃 pCnt 𝑦 ) ∈ ℝ ) |
| 121 |
76
|
adantr |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑃 pCnt 𝑧 ) ∈ ℤ ) |
| 122 |
121
|
zred |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑃 pCnt 𝑧 ) ∈ ℝ ) |
| 123 |
22
|
3ad2ant1 |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → 𝑁 ∈ ℝ ) |
| 124 |
123
|
ad2antrr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → 𝑁 ∈ ℝ ) |
| 125 |
70
|
ad2antrr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → 𝑁 ≠ 0 ) |
| 126 |
72
|
adantr |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → 𝑃 ∈ ℙ ) |
| 127 |
|
qaddcl |
⊢ ( ( 𝑦 ∈ ℚ ∧ 𝑧 ∈ ℚ ) → ( 𝑦 + 𝑧 ) ∈ ℚ ) |
| 128 |
80 73 127
|
syl2anc |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 + 𝑧 ) ∈ ℚ ) |
| 129 |
128
|
adantr |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑦 + 𝑧 ) ∈ ℚ ) |
| 130 |
|
simpr |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑦 + 𝑧 ) ≠ 0 ) |
| 131 |
|
pcqcl |
⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝑦 + 𝑧 ) ∈ ℚ ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ) → ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ∈ ℤ ) |
| 132 |
126 129 130 131
|
syl12anc |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ∈ ℤ ) |
| 133 |
132
|
adantr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ∈ ℤ ) |
| 134 |
124 125 133
|
reexpclzd |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ∈ ℝ ) |
| 135 |
119
|
adantr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → ( 𝑃 pCnt 𝑦 ) ∈ ℤ ) |
| 136 |
124 125 135
|
reexpclzd |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ∈ ℝ ) |
| 137 |
|
simpl1 |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ) |
| 138 |
137 22
|
syl |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → 𝑁 ∈ ℝ ) |
| 139 |
137 28
|
syl |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → 𝑁 ≠ 0 ) |
| 140 |
138 139 119
|
reexpclzd |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ∈ ℝ ) |
| 141 |
138 139 121
|
reexpclzd |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ∈ ℝ ) |
| 142 |
140 141
|
readdcld |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ∈ ℝ ) |
| 143 |
142
|
adantr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ∈ ℝ ) |
| 144 |
126
|
adantr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → 𝑃 ∈ ℙ ) |
| 145 |
80
|
ad2antrr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → 𝑦 ∈ ℚ ) |
| 146 |
73
|
ad2antrr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → 𝑧 ∈ ℚ ) |
| 147 |
|
simpr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) |
| 148 |
144 145 146 147
|
pcadd |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) |
| 149 |
137 27
|
syl |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → 𝑁 ∈ ℝ+ ) |
| 150 |
25
|
simprd |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → 𝑁 < 1 ) |
| 151 |
137 150
|
syl |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → 𝑁 < 1 ) |
| 152 |
149 119 132 151
|
ltexp2rd |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) < ( 𝑃 pCnt 𝑦 ) ↔ ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) < ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) ) |
| 153 |
152
|
notbid |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( ¬ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) < ( 𝑃 pCnt 𝑦 ) ↔ ¬ ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) < ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) ) |
| 154 |
132
|
zred |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ∈ ℝ ) |
| 155 |
120 154
|
lenltd |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ↔ ¬ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) < ( 𝑃 pCnt 𝑦 ) ) ) |
| 156 |
138 139 132
|
reexpclzd |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ∈ ℝ ) |
| 157 |
156 140
|
lenltd |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ≤ ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ↔ ¬ ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) < ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) ) |
| 158 |
153 155 157
|
3bitr4d |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ↔ ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ≤ ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) ) |
| 159 |
158
|
biimpa |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) → ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ≤ ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) |
| 160 |
148 159
|
syldan |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ≤ ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) |
| 161 |
27
|
3ad2ant1 |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → 𝑁 ∈ ℝ+ ) |
| 162 |
161 76
|
rpexpcld |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ∈ ℝ+ ) |
| 163 |
162
|
adantr |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ∈ ℝ+ ) |
| 164 |
163
|
rpge0d |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → 0 ≤ ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) |
| 165 |
140 141
|
addge01d |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 0 ≤ ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ↔ ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) ) |
| 166 |
164 165
|
mpbid |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 167 |
166
|
adantr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 168 |
134 136 143 160 167
|
letrd |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑦 ) ≤ ( 𝑃 pCnt 𝑧 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 169 |
156
|
adantr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ∈ ℝ ) |
| 170 |
141
|
adantr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ∈ ℝ ) |
| 171 |
142
|
adantr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) → ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ∈ ℝ ) |
| 172 |
126
|
adantr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) → 𝑃 ∈ ℙ ) |
| 173 |
73
|
ad2antrr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) → 𝑧 ∈ ℚ ) |
| 174 |
80
|
ad2antrr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) → 𝑦 ∈ ℚ ) |
| 175 |
|
simpr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) → ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) |
| 176 |
172 173 174 175
|
pcadd |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) → ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt ( 𝑧 + 𝑦 ) ) ) |
| 177 |
92 94
|
addcomd |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 + 𝑧 ) = ( 𝑧 + 𝑦 ) ) |
| 178 |
177
|
oveq2d |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) = ( 𝑃 pCnt ( 𝑧 + 𝑦 ) ) ) |
| 179 |
178
|
ad2antrr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) → ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) = ( 𝑃 pCnt ( 𝑧 + 𝑦 ) ) ) |
| 180 |
176 179
|
breqtrrd |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) → ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) |
| 181 |
149 121 132 151
|
ltexp2rd |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) < ( 𝑃 pCnt 𝑧 ) ↔ ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) < ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) ) |
| 182 |
181
|
notbid |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( ¬ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) < ( 𝑃 pCnt 𝑧 ) ↔ ¬ ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) < ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) ) |
| 183 |
122 154
|
lenltd |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ↔ ¬ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) < ( 𝑃 pCnt 𝑧 ) ) ) |
| 184 |
156 141
|
lenltd |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ≤ ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ↔ ¬ ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) < ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) ) |
| 185 |
182 183 184
|
3bitr4d |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ↔ ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ≤ ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 186 |
185
|
biimpa |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) → ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ≤ ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) |
| 187 |
180 186
|
syldan |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ≤ ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) |
| 188 |
161 71
|
rpexpcld |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ∈ ℝ+ ) |
| 189 |
188
|
adantr |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ∈ ℝ+ ) |
| 190 |
189
|
rpge0d |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → 0 ≤ ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ) |
| 191 |
141 140
|
addge02d |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 0 ≤ ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) ↔ ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) ) |
| 192 |
190 191
|
mpbid |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 193 |
192
|
adantr |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 194 |
169 170 171 187 193
|
letrd |
⊢ ( ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) ∧ ( 𝑃 pCnt 𝑧 ) ≤ ( 𝑃 pCnt 𝑦 ) ) → ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 195 |
120 122 168 194
|
lecasei |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 196 |
118 195
|
eqbrtrd |
⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) ∧ ( 𝑦 + 𝑧 ) ≠ 0 ) → if ( ( 𝑦 + 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 197 |
188 162
|
rpaddcld |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ∈ ℝ+ ) |
| 198 |
197
|
rpge0d |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → 0 ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 199 |
116 196 198
|
pm2.61ne |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → if ( ( 𝑦 + 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) ≤ ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 200 |
|
eqeq1 |
⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → ( 𝑥 = 0 ↔ ( 𝑦 + 𝑧 ) = 0 ) ) |
| 201 |
|
oveq2 |
⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → ( 𝑃 pCnt 𝑥 ) = ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) |
| 202 |
201
|
oveq2d |
⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → ( 𝑁 ↑ ( 𝑃 pCnt 𝑥 ) ) = ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) |
| 203 |
200 202
|
ifbieq2d |
⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → if ( 𝑥 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑥 ) ) ) = if ( ( 𝑦 + 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) ) |
| 204 |
|
ovex |
⊢ ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ∈ V |
| 205 |
42 204
|
ifex |
⊢ if ( ( 𝑦 + 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) ∈ V |
| 206 |
203 3 205
|
fvmpt |
⊢ ( ( 𝑦 + 𝑧 ) ∈ ℚ → ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) = if ( ( 𝑦 + 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) ) |
| 207 |
128 206
|
syl |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) = if ( ( 𝑦 + 𝑧 ) = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt ( 𝑦 + 𝑧 ) ) ) ) ) |
| 208 |
101 112
|
oveq12d |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝑁 ↑ ( 𝑃 pCnt 𝑦 ) ) + ( 𝑁 ↑ ( 𝑃 pCnt 𝑧 ) ) ) ) |
| 209 |
199 207 208
|
3brtr4d |
⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) ∧ ( 𝑦 ∈ ℚ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ ℚ ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) ≤ ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) ) |
| 210 |
4 6 10 13 15 18 37 44 64 114 209
|
isabvd |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → 𝐹 ∈ 𝐴 ) |