Metamath Proof Explorer


Theorem padicabv

Description: The p-adic absolute value (with arbitrary base) is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014)

Ref Expression
Hypotheses qrng.q 𝑄 = ( ℂflds ℚ )
qabsabv.a 𝐴 = ( AbsVal ‘ 𝑄 )
padic.f 𝐹 = ( 𝑥 ∈ ℚ ↦ if ( 𝑥 = 0 , 0 , ( 𝑁 ↑ ( 𝑃 pCnt 𝑥 ) ) ) )
Assertion padicabv ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ( 0 (,) 1 ) ) → 𝐹𝐴 )

Proof

Step Hyp Ref Expression
1 qrng.q 𝑄 = ( ℂflds ℚ )
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 ) ) → 𝐹𝐴 )